[Eva] Reduction by \valid and \valid_read always remove indeterminate values.

src/plugins/eva/legacy/eval_op.ml

@@ -128,22 +128,28 @@ let reduce_by_initialized_defined f loc state =
     state
 
 let reduce_by_valid_loc ~positive access loc typ state =
-  let value = Cvalue.Model.find state loc in
-  let loc_bits = Locations.loc_bytes_to_loc_bits value in
+  let value = Cvalue.Model.find_indeterminate state loc in
+  let loc_bytes = Cvalue.V_Or_Uninitialized.get_v value in
+  let loc_bits = Locations.loc_bytes_to_loc_bits loc_bytes in
   let size = Bit_utils.sizeof_pointed typ in
-  let value_as_loc = Locations.make_loc loc_bits size in
+  let location = Locations.make_loc loc_bits size in
+  let reduced_location =
+    if positive
+    then Locations.valid_part access location
+    else Locations.invalid_part location
+  in
+  let reduced_loc_bytes = Locations.loc_to_loc_without_size reduced_location in
   let reduced_value =
-    Locations.loc_to_loc_without_size
-      (if positive
-       then Locations.valid_part access value_as_loc
-       else Locations.invalid_part value_as_loc )
+    if positive
+    then Cvalue.V_Or_Uninitialized.initialized reduced_loc_bytes
+    else Cvalue.V_Or_Uninitialized.map (fun _ -> reduced_loc_bytes) value
   in
-  if V.equal value reduced_value
+  if Cvalue.V_Or_Uninitialized.equal value reduced_value
   then state
   else
-  if V.equal V.bottom reduced_value
+  if Cvalue.V_Or_Uninitialized.(equal bottom reduced_value)
   then Cvalue.Model.bottom
-  else Cvalue.Model.reduce_previous_binding state loc reduced_value
+  else Cvalue.Model.reduce_indeterminate_binding state loc reduced_value
 
 let make_loc_contiguous loc =
   try

tests/value/oracle/reduce_by_valid.res.oracle

@@ -230,7 +230,7 @@
 [eva:final-states] Values at end of function main5:
   q ∈ {{ &y }}
   p ∈ {0}
-  r ∈ {{ &y }} or UNINITIALIZED
+  r ∈ {{ &y }}
 [eva:final-states] Values at end of function main6:
   S_f1_0_S_vs[0] ∈ {1}
              [1] ∈ [--..--]

tests/value/oracle/summary.4.res.oracle

@@ -61,9 +61,6 @@
   locals {z} escaping the scope of a block of alarms through p
 [eva:alarm] summary.i:45: Warning: 
   assertion 'rte,mem_access' got status unknown.
-[eva:alarm] summary.i:45: Warning: 
-  accessing left-value that contains escaping addresses.
-  assert ¬\dangling(&p);
 [eva] Recording results for alarms
 [eva] Done for function alarms
 [eva] computing for function logic <- main.
@@ -111,7 +108,7 @@
     by the Eva analyzer:      0 errors    1 warning
     by the Frama-C kernel:    0 errors    3 warnings
   ----------------------------------------------------------------------------
-  18 alarms generated by the analysis:
+  17 alarms generated by the analysis:
        3 invalid memory accesses
        3 integer overflows
        2 accesses out of bounds index
@@ -119,7 +116,6 @@
        2 nan or infinite floating-point values
        2 illegal conversions from floating-point to integer
        1 division by zero
-       1 escaping address
        2 others
   ----------------------------------------------------------------------------
   Evaluation of the logical properties reached by the analysis: