From 9a2aada8b9b5f5b579387f37329d73e6a5986cea Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 20 Jan 2022 20:01:40 +0100
Subject: [PATCH] [Eva] Completely remove the loc parameter to
Eva_annotations.add_*
---
src/plugins/aorai/aorai_eva_analysis.enabled.ml | 3 +--
src/plugins/value/Eva.mli | 8 ++++----
src/plugins/value/utils/eva_annotations.ml | 8 ++++----
src/plugins/value/utils/eva_annotations.mli | 8 ++++----
4 files changed, 13 insertions(+), 14 deletions(-)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 86437066d6b..8b007c55b15 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -70,9 +70,8 @@ let add_slevel_annotation vi kind =
| Aorai_visitors.Aux_funcs.(Pre _ | Post _) ->
let kf = Globals.Functions.get vi in
let stmt = Kernel_function.find_first_stmt kf
- and loc = Kernel_function.get_location kf
and emitter = Aorai_option.emitter in
- Eva.Eva_annotations.(add_slevel_annot ~emitter ~loc stmt SlevelFull)
+ Eva.Eva_annotations.(add_slevel_annot ~emitter stmt SlevelFull)
| _ -> ()
let add_slevel_annotations () =
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 6887ef6e6a0..74ac173305e 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -104,13 +104,13 @@ module Eva_annotations: sig
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 ->
+ val add_slevel_annot : emitter:Emitter.t ->
Cil_types.stmt -> slevel_annotation -> unit
- val add_unroll_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
+ val add_unroll_annot : emitter:Emitter.t ->
Cil_types.stmt -> unroll_annotation -> unit
- val add_flow_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
+ val add_flow_annot : emitter:Emitter.t ->
Cil_types.stmt -> flow_annotation -> unit
- val add_subdivision_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
+ val add_subdivision_annot : emitter:Emitter.t ->
Cil_types.stmt -> int -> unit
end
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 1a6ea6ddc0b..c493b1149b5 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -102,8 +102,8 @@ struct
in
List.rev (Annotations.fold_code_annot filter_add stmt [])
- let add ~emitter ?loc stmt annot =
- let loc = Option.value ~default:(Cil_datatype.Stmt.loc stmt) loc in
+ let add ~emitter stmt annot =
+ let loc = Cil_datatype.Stmt.loc stmt 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
@@ -262,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 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 stmt (annot, None)
module Subdivision = Register (struct
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 77ddc30b1bc..df768e5a1fb 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/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 ->
Cil_types.stmt -> slevel_annotation -> unit
-val add_unroll_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
+val add_unroll_annot : emitter:Emitter.t ->
Cil_types.stmt -> unroll_annotation -> unit
-val add_flow_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
+val add_flow_annot : emitter:Emitter.t ->
Cil_types.stmt -> flow_annotation -> unit
-val add_subdivision_annot : emitter:Emitter.t -> ?loc:Cil_types.location ->
+val add_subdivision_annot : emitter:Emitter.t ->
Cil_types.stmt -> int -> unit
--
GitLab