Module Eva.Eva_annotations

module Eva_annotations: sig .. end

Register special annotations to locally guide the partitioning of states performed by an 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 paramter.

type unroll_annotation = 
| UnrollAmount of Cil_types.term (*

Unroll the n first iterations.

*)
| UnrollFull (*

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

*)

Loop unroll annotations.

type flow_annotation = 
| FlowSplit of Cil_types.term (*

Split states according to a term.

*)
| FlowMerge of Cil_types.term (*

Merge states separated by a previous split.

*)

Split/merge annotations for value partitioning.

val add_slevel_annot : emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> slevel_annotation -> unit
val add_unroll_annot : emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> unroll_annotation -> unit
val add_flow_annot : emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> flow_annotation -> unit
val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location -> Cil_types.stmt -> int -> unit