Module Eva.Eva_annotationsSource

Register special annotations to locally guide the Eva analysis:

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.

    *)

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
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