diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 6cb042290b0944179c00f4989636aa6c80a2a469..17afc0cb0009c8dd7452ed1ee8f6940e60b21f00 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 e51dcf068bc415d4295ea78d753037d8585abdbb..d807740cf802b11d785e27cf7522d8cf673567f9 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 ecc6d928ac22807e6ba6d5430d6e41d8a68f47b8..a4f0a3e3065f582eab966749d0c87bcdb2265d98 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 9d9436836ec6a35e0df4dc837eae0c634d9def9f..7b86d44704aec8a4d451079e449bfd9320966bd0 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 47e6cda07df505a5319c1e6a660712eb26020172..145aeb752d3a920752391a5eaaa261f9a2e3e284 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 b26af8c3d53534959a87ff13679b46921c6bef2d..4560b0573061290b9ec67795f6988d164a980fc6 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 06b83c96a7ef143df4a3b8ca490632b2bcbb2f78..46154e7440ca51b5e742d0548aad9600d1ff5c1a 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 cc02d7626c304a49b207b43061c0a01f901e8e97..02f251803d78aa639a83968d99ce891aa2168226 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)