From 61f61907ff14970073a05faf907921223f1f1a2d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Apr 2022 14:52:17 +0200
Subject: [PATCH] [from] Uses the new Eva API instead of Db.Value when
possible.
---
src/plugins/from/from_compute.ml | 6 +++---
src/plugins/from/from_register.ml | 10 ++++------
src/plugins/from/functionwise.ml | 2 +-
tests/builtins/oracle/memcpy.res.oracle | 1 -
tests/pdg/oracle/bts1194.res.oracle | 1 -
tests/pdg/oracle/top_pdg_input.res.oracle | 5 -----
tests/sparecode/oracle/bts334.2.res.oracle | 1 -
tests/value/oracle/loopfun.0.res.oracle | 4 ----
8 files changed, 8 insertions(+), 22 deletions(-)
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 6cb042290b0..17afc0cb000 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -551,13 +551,13 @@ struct
(* Filter out unreachable values. *)
let transfer_stmt s d =
- if Db.Value.is_reachable (To_Use.get_value_state s) &&
+ if Eva.Results.is_reachable s &&
not (Function_Froms.Memory.is_bottom d.deps_table)
then transfer_stmt s d
else []
let doEdge s succ d =
- if Db.Value.is_reachable (To_Use.get_value_state succ)
+ if Eva.Results.is_reachable succ
then
let dt = d.deps_table in
let opened = Kernel_function.blocks_opened_by_edge s succ in
@@ -647,7 +647,7 @@ struct
let _poped = Stack.pop call_stack in
let last_from =
try
- if Db.Value.is_reachable (To_Use.get_value_state ret_id)
+ if Eva.Results.is_reachable ret_id
then
externalize
ret_id
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index e51dcf068bc..d807740cf80 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -30,7 +30,7 @@ let display fmtopt =
Option.iter (fun fmt -> Format.fprintf fmt "@[<v>") fmtopt;
Callgraph.Uses.iter_in_rev_order
(fun kf ->
- if !Db.Value.is_called kf then
+ if Eva.Results.is_called kf then
let header fmt =
Format.fprintf fmt "Function %a:" Kernel_function.pretty kf
in
@@ -101,13 +101,11 @@ let print_calldeps () =
if !Db.Value.no_results (Kernel_function.get_definition caller)
then "<unknown>", funtype
else
- try
- let set = Db.Value.call_to_kernel_function s in
- let kf = Kernel_function.Hptset.choose set in
+ match Eva.Results.callee s with
+ | kf :: _ ->
Pretty_utils.to_string Kernel_function.pretty kf,
Kernel_function.get_type kf
- with
- | Not_found ->
+ | [] ->
From_parameters.fatal
~source:(fst (Cil_datatype.Stmt.loc s))
"Invalid call %a@." Printer.pp_stmt s
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index ecc6d928ac2..a4f0a3e3065 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -95,7 +95,7 @@ let force_compute_all () =
Eva.Analysis.compute ();
Callgraph.Uses.iter_in_rev_order
(fun kf ->
- if Kernel_function.is_definition kf && !Db.Value.is_called kf
+ if Kernel_function.is_definition kf && Eva.Results.is_called kf
then !Db.From.compute kf)
(* Db Registration for function-wise from *)
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 9d9436836ec..7b86d44704a 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -364,7 +364,6 @@
[eva] Done for function copy_0
[eva] Recording results for main_all
[from] Computing for function main_all
-[from] Non-terminating function main_all (no dependencies)
[from] Done for function main_all
[eva] done for function main_all
[scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 47e6cda07df..145aeb752d3 100644
--- a/tests/pdg/oracle/bts1194.res.oracle
+++ b/tests/pdg/oracle/bts1194.res.oracle
@@ -24,7 +24,6 @@
[eva] bts1194.c:20: function g: no state left, postcondition got status valid.
[eva] Recording results for g
[from] Computing for function g
-[from] Non-terminating function g (no dependencies)
[from] Done for function g
[eva] Done for function g
[eva] Recording results for h
diff --git a/tests/pdg/oracle/top_pdg_input.res.oracle b/tests/pdg/oracle/top_pdg_input.res.oracle
index b26af8c3d53..4560b057306 100644
--- a/tests/pdg/oracle/top_pdg_input.res.oracle
+++ b/tests/pdg/oracle/top_pdg_input.res.oracle
@@ -256,17 +256,12 @@ Cannot filter: dumping raw memory (including unchanged variables)
[from] Done for function fun_asm
[from] Computing for function main_asm
[from] Done for function main_asm
-[from] Computing for function no_results
-[from] Done for function no_results
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function fun_asm:
\result FROM i
[from] Function main_asm:
\result FROM \nothing
-[from] Function no_results:
- FROMTOP
- \result FROM ANYTHING(origin:Unknown)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function fun_asm:
__retres
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index 06b83c96a7e..46154e7440c 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -97,7 +97,6 @@
[eva] Done for function loop_body
[eva] Recording results for process
[from] Computing for function process
-[from] Non-terminating function process (no dependencies)
[from] Done for function process
[eva] Done for function process
[eva] Recording results for main_init
diff --git a/tests/value/oracle/loopfun.0.res.oracle b/tests/value/oracle/loopfun.0.res.oracle
index cc02d7626c3..02f251803d7 100644
--- a/tests/value/oracle/loopfun.0.res.oracle
+++ b/tests/value/oracle/loopfun.0.res.oracle
@@ -44,8 +44,6 @@
[eva] ====== VALUES COMPUTED ======
[from] Computing for function main
[from] Done for function main
-[from] Computing for function main2
-[from] Done for function main2
[from] Computing for function test
[from] Done for function test
[from] ====== DEPENDENCIES COMPUTED ======
@@ -53,8 +51,6 @@
[from] Function main:
FROMTOP
\result FROM ANYTHING(origin:Unknown)
-[from] Function main2:
- FROMTOP
[from] Function test:
FROMTOP
\result FROM ANYTHING(origin:Unknown)
--
GitLab