Module Eva.Eva_annotations

Register special annotations to locally guide the Eva analysis:

type slevel_annotation =
| SlevelMerge(*

Join all states separated by slevel.

*)
| SlevelDefault(*

Use the limit defined by -eva-slevel.

*)
| SlevelLocal of int(*

Use the given limit instead of -eva-slevel.

*)
| SlevelFull(*

Remove the limit of number of separated states.

*)

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

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

Unroll the n first iterations.

*)
| UnrollFull(*

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

*)

Loop unroll annotations.

type split_kind =
| Static
| Dynamic
type split_term =
| Expression of Frama_c_kernel.Cil_types.exp
| Predicate of Frama_c_kernel.Cil_types.predicate
type flow_annotation =
| FlowSplit of split_term * split_kind(*

Split states according to a term.

*)
| FlowMerge of split_term(*

Merge states separated by a previous split.

*)

Split/merge annotations for value partitioning.

type allocation_kind =
| By_stack
| Fresh
| Fresh_weak
| 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