Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_annotations

Register special annotations to locally guide the Eva analysis:

  • slevel annotations: "slevel default", "slevel merge" and "slevel i"
  • loop unroll annotations: "loop unroll term"
  • value partitioning annotations: "split term" and "merge term"
  • subdivision annotations: "subdivide i"
type slevel_annotation =
  1. | SlevelMerge
    (*

    Join all states separated by slevel.

    *)
  2. | SlevelDefault
    (*

    Use the limit defined by -eva-slevel.

    *)
  3. | SlevelLocal of int
    (*

    Use the given limit instead of -eva-slevel.

    *)
  4. | SlevelFull
    (*

    Remove the limit of number of separated states.

    *)

Annotations tweaking the behavior of the -eva-slevel parameter.

type unroll_annotation =
  1. | UnrollAmount of Frama_c_kernel.Cil_types.term
    (*

    Unroll the n first iterations.

    *)
  2. | UnrollFull
    (*

    Unroll amount defined by -eva-default-loop-unroll.

    *)
  3. | UnrollAuto of int
    (*

    Use the automatic loop unrolling with the given limit, as if -eva-auto-loop-unroll N was locally set.

    *)

Loop unroll annotations.

type split_kind =
  1. | Static
  2. | Dynamic
type split_term =
  1. | Expression of Frama_c_kernel.Cil_types.exp
  2. | Predicate of Frama_c_kernel.Cil_types.predicate

Splits can be performed according to a C expression or an ACSL predicate.

type flow_annotation =
  1. | FlowSplit of split_term * split_kind
    (*

    Split states according to a term.

    *)
  2. | FlowMerge of split_term
    (*

    Merge states separated by a previous split.

    *)

Split/merge annotations for value partitioning.

type allocation_kind =
  1. | By_stack
  2. | Fresh
  3. | Fresh_weak
  4. | Imprecise
type domain_scope = string * Frama_c_kernel.Cil_types.varinfo list
val get_slevel_annot : Frama_c_kernel.Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Frama_c_kernel.Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Frama_c_kernel.Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Frama_c_kernel.Cil_types.stmt -> int list
val add_slevel_annot : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> slevel_annotation -> unit
val add_unroll_annot : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> unroll_annotation -> unit
val add_subdivision_annot : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> int -> unit
val add_array_segmentation : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> array_segmentation -> unit
val add_domain_scope : emitter:Frama_c_kernel.Emitter.t -> Frama_c_kernel.Cil_types.stmt -> domain_scope -> unit