sig
type slevel_annotation =
SlevelMerge
| SlevelDefault
| SlevelLocal of int
| SlevelFull
type unroll_annotation = UnrollAmount of Cil_types.term | UnrollFull
type split_kind = Static | Dynamic
type split_term =
Expression of Cil_types.exp
| Predicate of Cil_types.predicate
type flow_annotation =
FlowSplit of Eva_annotations.split_term * Eva_annotations.split_kind
| FlowMerge of Eva_annotations.split_term
type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
type array_segmentation =
Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
type domain_scope = string * Cil_types.varinfo list
val get_slevel_annot :
Cil_types.stmt -> Eva_annotations.slevel_annotation option
val get_unroll_annot :
Cil_types.stmt -> Eva_annotations.unroll_annotation list
val get_flow_annot : Cil_types.stmt -> Eva_annotations.flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
val get_allocation : Cil_types.stmt -> Eva_annotations.allocation_kind
val add_slevel_annot :
emitter:Emitter.t ->
Cil_types.stmt -> Eva_annotations.slevel_annotation -> unit
val add_unroll_annot :
emitter:Emitter.t ->
Cil_types.stmt -> Eva_annotations.unroll_annotation -> unit
val add_flow_annot :
emitter:Emitter.t ->
Cil_types.stmt -> Eva_annotations.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 -> Eva_annotations.array_segmentation -> unit
val add_domain_scope :
emitter:Emitter.t ->
Cil_types.stmt -> Eva_annotations.domain_scope -> unit
val read_array_segmentation :
Cil_types.acsl_extension -> Eva_annotations.array_segmentation
val read_domain_scope :
Cil_types.acsl_extension -> Eva_annotations.domain_scope
end