[LoopAnalysis] Use the new EVA API

src/plugins/loop_analysis/Makefile.in

@@ -33,6 +33,7 @@ PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
 PLUGIN_NAME:= LoopAnalysis
 PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register
 PLUGIN_CMI:= region_analysis_sig
+PLUGIN_DEPENDENCIES:= Eva
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
 PLUGIN_TESTS_DIRS:=loop_analysis
 

src/plugins/loop_analysis/loop_analysis.ml

@@ -340,37 +340,18 @@ module Store(* (B:sig *)
         Printer.pp_stmt stmt
 
   let value_min_max stmt vi =
-    if (Db.Value.is_computed ()) then
+    if (Eva.Analysis.is_computed ()) then
       begin
         Options.feedback ~dkey ~once:true
           "value analysis computed, trying results";
-        if Db.Value.is_reachable_stmt stmt then
-          let state = Db.Value.get_stmt_state stmt in
-          try
-            let loc = Locations.loc_of_varinfo vi in
-            let v = Db.Value.find state loc in
-            let ival = Cvalue.V.project_ival v in
-            let omin, omax = Ival.min_and_max ival in
-            omin, omax
-          with
-          | Not_found ->
-            Options.feedback ~dkey "value_min_max: not found: %a@.\
-                                    function: %a, stmt: %a"
-              Printer.pp_varinfo vi Kernel_function.pretty
-              (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt;
-            None, None
-          | Cvalue.V.Not_based_on_null ->
-            Options.feedback ~dkey "value_min_max: not based on null: %a@.\
-                                    function: %a, stmt: %a"
-              Printer.pp_varinfo vi Kernel_function.pretty
-              (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt;
-            None, None
-        else
-          begin
+        let value = Eva.Results.(before stmt |> eval_var vi |> as_ival) in
+        match value with
+        | Result.Ok ival -> Ival.min_and_max ival
+        | Error e ->
+          if e = Eva.Results.Bottom then
             Options.feedback ~dkey "skipping unreachable stmt (function: %a)"
               Kernel_function.pretty (Kernel_function.find_englobing_kf stmt);
-            None, None
-          end
+          None, None
       end
     else
       begin
@@ -490,7 +471,7 @@ module Store(* (B:sig *)
             with Not_found -> ()
           end
         | c ->
-          if (Db.Value.is_computed ()) then
+          if (Eva.Analysis.is_computed ()) then
             begin
               let min_max_int = value_min_max stmt in
               match c with

src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle

@@ -433,6 +433,10 @@
   with_value.i:26: 5
   with_value.i:30: 5
   with_value.i:34: 4
+  with_value.i:38: 2147483648
+  with_value.i:42: 2147483649
+  with_value.i:46: 2147483649
+  with_value.i:50: 2147483648
   with_value.i:54: 2147483646
   with_value.i:58: 2147483647
   with_value.i:62: 2147483647