Eva.Eva_annotations
Register special annotations to locally guide the Eva analysis:
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_term =
| Expression of Frama_c_kernel.Cil_types.exp
| Predicate of Frama_c_kernel.Cil_types.predicate
Splits can be performed according to a C expression or an ACSL 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 array_segmentation =
Frama_c_kernel.Cil_types.varinfo
* Frama_c_kernel.Cil_types.offset
* Frama_c_kernel.Cil_types.exp list
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 get_allocation : Frama_c_kernel.Cil_types.stmt -> allocation_kind
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_flow_annot :
emitter:Frama_c_kernel.Emitter.t ->
Frama_c_kernel.Cil_types.stmt ->
flow_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