Merge branch 'fix/eva/logic-plevel' into 'master'

[Eva] Do not disable all logic reductions when plevel is set to 0.

See merge request frama-c/frama-c!3434

src/plugins/value/legacy/eval_op.ml

@@ -166,14 +166,20 @@ let apply_on_all_locs f loc state =
   match loc.Locations.size with
   | Int_Base.Top -> state
   | Int_Base.Value _ as size ->
-    try
-      let loc = Locations.valid_part Locations.Read loc in
-      let loc = loc.Locations.loc in
-      let plevel = Value_parameters.ArrayPrecisionLevel.get() in
-      ignore (Locations.Location_Bits.cardinal_less_than loc plevel);
-      Locations.Location_Bits.fold_enum
-        (fun l acc -> f (Locations.make_loc l size) acc) loc state
-    with Not_less_than | Abstract_interp.Error_Top -> state
+    let loc = Locations.valid_part Locations.Read loc in
+    let plevel = Value_parameters.ArrayPrecisionLevel.get () in
+    let ilevel = Int_set.get_small_cardinal () in
+    let limit = max plevel ilevel in
+    let apply_f base ival state =
+      f Locations.(make_loc (Location_Bits.inject base ival) size) state
+    in
+    let aux base ival state =
+      if Ival.cardinal_is_less_than ival limit
+      then Ival.fold_enum (fun i acc -> apply_f base i acc) ival state
+      else state
+    in
+    try Locations.Location_Bits.fold_i aux loc.loc state
+    with Abstract_interp.Error_Top -> state
 
 (* Display [o] as a single value, when this is more readable and more precise
    than the standard display. *)

tests/value/oracle/multidim.res.oracle

@@ -96,22 +96,6 @@
 [eva] tests/value/multidim.c:63: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/multidim.c:63: Warning: 
-  accessing out of bounds index.
-  assert 0 ≤ tmp;
-  (tmp from Frama_C_interval(0, 4 - 1))
-[eva:alarm] tests/value/multidim.c:63: Warning: 
-  accessing out of bounds index.
-  assert tmp < 4;
-  (tmp from Frama_C_interval(0, 4 - 1))
-[eva:alarm] tests/value/multidim.c:63: Warning: 
-  accessing out of bounds index.
-  assert 0 ≤ tmp_0;
-  (tmp_0 from Frama_C_interval(0, 4 - 1))
-[eva:alarm] tests/value/multidim.c:63: Warning: 
-  accessing out of bounds index.
-  assert tmp_0 < 4;
-  (tmp_0 from Frama_C_interval(0, 4 - 1))
 [eva] tests/value/multidim.c:65: 
   Frama_C_domain_show_each:
   t1 : # cvalue: [--..--]