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.Eva_annotations.split_term *
Eva.Eva_annotations.split_kind
| FlowMerge of Eva.Eva_annotations.split_term
val add_slevel_annot :
emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> Eva.Eva_annotations.slevel_annotation -> unit
val add_unroll_annot :
emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> Eva.Eva_annotations.unroll_annotation -> unit
val add_flow_annot :
emitter:Emitter.t ->
loc:Cil_types.location ->
Cil_types.stmt -> Eva.Eva_annotations.flow_annotation -> unit
val add_subdivision_annot :
emitter:Emitter.t ->
loc:Cil_types.location -> Cil_types.stmt -> int -> unit
end