module Eva_annotations:sig
..end
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 |
(* | 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 |
(* | 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 |
| |
Predicate of |
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.
type
allocation_kind =
| |
By_stack |
| |
Fresh |
| |
Fresh_weak |
| |
Imprecise |
typearray_segmentation =
Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
typedomain_scope =
string * Cil_types.varinfo list
val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
val get_allocation : Cil_types.stmt -> allocation_kind
val add_slevel_annot : emitter:Emitter.t ->
Cil_types.stmt -> slevel_annotation -> unit
val add_unroll_annot : emitter:Emitter.t ->
Cil_types.stmt -> unroll_annotation -> unit
val add_flow_annot : emitter:Emitter.t ->
Cil_types.stmt -> flow_annotation -> unit
val add_subdivision_annot : emitter:Emitter.t -> Cil_types.stmt -> int -> unit
val add_array_segmentation : emitter:Emitter.t ->
Cil_types.stmt -> array_segmentation -> unit
val add_domain_scope : emitter:Emitter.t ->
Cil_types.stmt -> domain_scope -> unit