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 |
(* | 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 |
(* | Unroll the n first iterations. | *) |
| |
UnrollFull |
(* | Unroll amount defined by -eva-default-loop-unroll. | *) |
Loop unroll annotations.
type
flow_annotation =
| |
FlowSplit of |
(* | Split states according to a term. | *) |
| |
FlowMerge of |
(* | 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