[Eva] Improve the annotation API

- loc is now optional and copied from statement if not given
- get_* functions are now exported

src/plugins/value/Eva.mli

@@ -99,13 +99,18 @@ module Eva_annotations: sig
     | FlowMerge of split_term
     (** Merge states separated by a previous split. *)
 
-  val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+  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 add_slevel_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
     Cil_types.stmt -> slevel_annotation -> unit
-  val add_unroll_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+  val add_unroll_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
     Cil_types.stmt -> unroll_annotation -> unit
-  val add_flow_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+  val add_flow_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
     Cil_types.stmt -> flow_annotation -> unit
-  val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+  val add_subdivision_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
     Cil_types.stmt -> int -> unit
 end
 

src/plugins/value/utils/eva_annotations.ml

@@ -102,7 +102,8 @@ struct
     in
     List.rev (Annotations.fold_code_annot filter_add stmt [])
 
-  let add ~emitter ~loc stmt annot =
+  let add ~emitter ?loc stmt annot =
+    let loc = Option.value ~default:(Cil_datatype.Stmt.loc stmt) loc in
     let param = M.export annot in
     let extension = Logic_const.new_acsl_extension name loc false param in
     let annot_node = Cil_types.AExtended ([], is_loop_annot, extension) in
@@ -261,14 +262,14 @@ let add_slevel_annot = Slevel.add
 
 let add_unroll_annot = Unroll.add
 
-let add_flow_annot ~emitter ~loc stmt flow_annotation =
+let add_flow_annot ~emitter ?loc stmt flow_annotation =
   let f, annot =
     match flow_annotation with
     | FlowSplit (annot, Static) -> Split.add, annot
     | FlowSplit (annot, Dynamic) -> DynamicSplit.add, annot
     | FlowMerge annot -> Merge.add, annot
   in
-  f ~emitter ~loc stmt (annot, None)
+  f ~emitter ?loc stmt (annot, None)
 
 
 module Subdivision = Register (struct

src/plugins/value/utils/eva_annotations.mli

@@ -56,11 +56,11 @@ 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 -> loc:Cil_types.location ->
+val add_slevel_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
   Cil_types.stmt -> slevel_annotation -> unit
-val add_unroll_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+val add_unroll_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
   Cil_types.stmt -> unroll_annotation -> unit
-val add_flow_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+val add_flow_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
   Cil_types.stmt -> flow_annotation -> unit
-val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+val add_subdivision_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
   Cil_types.stmt -> int -> unit