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