From 94f1dd548c7909bcee4eb8cc026f6a9f1854f33f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 13:29:58 +0200
Subject: [PATCH] [Eva] Uses the new kernel API to set the current location.
No need to reset the current location after the analysis of a function or
after calling a visitor, as the new API ensures that this is the case.
---
src/plugins/eva/domains/cvalue/cvalue_init.ml | 3 ++-
src/plugins/eva/engine/initialization.ml | 3 ++-
src/plugins/eva/engine/iterator.ml | 15 ++++++---------
src/plugins/eva/engine/transfer_stmt.ml | 9 ++-------
src/plugins/eva/gui/gui_eval.ml | 3 ++-
src/plugins/eva/legacy/eval_annots.ml | 16 ++++++----------
src/plugins/eva/utils/eva_utils.ml | 14 ++++----------
tests/value/oracle/noreturn.res.oracle | 2 +-
8 files changed, 25 insertions(+), 40 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index 084207175c4..d080059b3ae 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -111,7 +111,8 @@ let reject_empty_struct b offset typ =
(** [initialize_var_using_type varinfo state] uses the type of [varinfo]
to create an initial value in [state]. *)
let initialize_var_using_type varinfo state =
- Current_loc.set varinfo.vdecl;
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = varinfo.vdecl in
let rec add_offsetmap depth b name_desc name typ offset_orig typ_orig state =
let typ = Cil.unrollType typ in
let loc = lazy (loc_of_typoffset b typ_orig offset_orig) in
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index ab92b750abf..22bd7987f91 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -309,7 +309,8 @@ module Make
with Initialization_failed -> `Bottom
let initialize_global_variable ~lib_entry vi init state =
- Current_loc.set vi.vdecl;
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = vi.vdecl in
let state = Domain.enter_scope Abstract_domain.Global [vi] state in
let state = if vi.vsource then
let initialize =
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 6629af3bd03..c025cb72135 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -441,7 +441,8 @@ module Make_Dataflow
Async.yield ();
check_signals ();
current_ki := kinstr;
- Current_loc.set e.edge_loc;
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = e.edge_loc in
let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
if not (Partitioning.is_empty_flow flow) then
@@ -461,14 +462,10 @@ module Make_Dataflow
let update_vertex ?(widening : bool = false) (v : vertex)
(sources : ('branch * flow) list) : bool =
- begin match v.vertex_start_of with
- | Some stmt ->
- (* Set location *)
- current_ki := Kstmt stmt;
- let current_loc = Cil_datatype.Stmt.loc stmt in
- Current_loc.set current_loc
- | None -> ()
- end;
+ Option.iter (fun stmt -> current_ki := Kstmt stmt) v.vertex_start_of;
+ let location = Option.map Cil_datatype.Stmt.loc v.vertex_start_of in
+ let open Current_loc.Operators in
+ let<?> UpdatedCurrentLoc = location in
(* Get vertex store *)
let store = get_vertex_store v in
(* Join incoming states *)
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index bc4fc022505..2d8e5dc404a 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -305,11 +305,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Returns the result of a call. *)
let process_call stmt call recursion valuation state =
Eva_utils.push_call_stack call.kf stmt;
- let cleanup () =
- Eva_utils.pop_call_stack ();
- (* Changed by compute_call_ref, called from process_call *)
- Current_loc.set (Cil_datatype.Stmt.loc stmt);
- in
let process () =
let domain_valuation = Eval.to_domain_valuation valuation in
let res =
@@ -322,11 +317,11 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| `Bottom ->
{ states = []; cacheable = Cacheable; }
in
- cleanup ();
+ Eva_utils.pop_call_stack ();
res
in
Eva_utils.protect process
- ~cleanup:(fun () -> InOutCallback.clear (); cleanup ())
+ ~cleanup:(fun () -> InOutCallback.clear (); Eva_utils.pop_call_stack ())
(* ------------------- Retro propagation on formals ----------------------- *)
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 37ec8affc0c..6d1e506fff5 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -612,7 +612,8 @@ module Make (X: Analysis.S) = struct
In this case, nothing is displayed by the GUI. *)
| `Bottom -> [], [] (* Bottom case: nothing is displayed either. *)
| `Value before ->
- Current_loc.set (gui_loc_loc loc);
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = gui_loc_loc loc in
clear_caches ();
make_data_all_callstacks_from_states ev ~before ~after:states_after v
end
diff --git a/src/plugins/eva/legacy/eval_annots.ml b/src/plugins/eva/legacy/eval_annots.ml
index bb5de81d88d..8b6ae759c10 100644
--- a/src/plugins/eva/legacy/eval_annots.ml
+++ b/src/plugins/eva/legacy/eval_annots.ml
@@ -164,15 +164,10 @@ end
let contains_c_at ca =
let vis = new contains_c_at in
- let loc = Current_loc.get () in
- let r =
- try
- ignore (Visitor.visitFramacCodeAnnotation vis ca);
- false
- with Exit -> true
- in
- Current_loc.set loc;
- r
+ try
+ ignore (Visitor.visitFramacCodeAnnotation vis ca);
+ false
+ with Exit -> true
(* Re-evaluate all alarms, and see if we can put a 'green' or 'red' status,
which would be more precise than those we have emitted during the current
@@ -187,7 +182,8 @@ let mark_green_and_red () =
| AAssert (_, p) | AInvariant (_, true, p) ->
let p = p.tp_statement in
let loc = code_annotation_loc ca stmt in
- Current_loc.set loc;
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = loc in
let kf = Kernel_function.find_englobing_kf stmt in
let ip = Property.ip_of_code_annot_single kf stmt ca in
(* This status is exact: we are _not_ refining the statuses previously
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 456ad09c557..9c7f2b5d521 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -168,21 +168,15 @@ class postconditions_mention_result = object
| _ -> Cil.DoChildren
end
let postconditions_mention_result spec =
- (* We save the current location because the visitor modifies it. *)
- let loc = Current_loc.get () in
let vis = new postconditions_mention_result in
let aux_bhv bhv =
let aux (_, post) = ignore (Visitor.visitFramacIdPredicate vis post) in
List.iter aux bhv.b_post_cond
in
- let res =
- try
- List.iter aux_bhv spec.spec_behavior;
- false
- with Exit -> true
- in
- Current_loc.set loc;
- res
+ try
+ List.iter aux_bhv spec.spec_behavior;
+ false
+ with Exit -> true
let conv_comp op =
let module C = Abstract_interp.Comp in
diff --git a/tests/value/oracle/noreturn.res.oracle b/tests/value/oracle/noreturn.res.oracle
index 955ecabd508..304917afda2 100644
--- a/tests/value/oracle/noreturn.res.oracle
+++ b/tests/value/oracle/noreturn.res.oracle
@@ -37,7 +37,7 @@
[eva] computing for function should_never_end <- main.
Called from noreturn.i:32.
[eva] Recording results for should_never_end
-[eva] noreturn.i:13: Warning:
+[eva] noreturn.i:32: Warning:
function should_never_end may terminate but has the noreturn attribute
[eva] Done for function should_never_end
[eva] computing for function should_never_end <- main.
--
GitLab