diff --git a/src/plugins/eva/legacy/eval_op.ml b/src/plugins/eva/legacy/eval_op.ml index aa9227c45553d7d538902228d7a64968d56395e2..2aff52c9bf29e0e89220b727bcada149633d33eb 100644 --- a/src/plugins/eva/legacy/eval_op.ml +++ b/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 diff --git a/tests/value/oracle/reduce_by_valid.res.oracle b/tests/value/oracle/reduce_by_valid.res.oracle index 1779ee8c716488fdc0f783559066655c68cc23c9..a4bafca7fceaafd44e41fd0fcfcc599a2f6c42ec 100644 --- a/tests/value/oracle/reduce_by_valid.res.oracle +++ b/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] ∈ [--..--] diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle index 78f84b5adc28a23ea09391128d089ce0c39e5da7..022406b2a822fbd89d2cb53235062f9a3296e260 100644 --- a/tests/value/oracle/summary.4.res.oracle +++ b/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: