[from] Uses the new Eva API instead of Db.Value when possible.

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

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

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 *)

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)

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

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

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

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)