diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml index 641d132bb185712cbd6379e68600ac5a61906202..966726399171fb0f62b0454284db9e9fd23211eb 100644 --- a/src/plugins/value/legacy/eval_op.ml +++ b/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. *) diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle index 1cd669ba3b370838b808559dcd759396728d8b02..483f85fcb1f3e104afb64bd5889e563eb7caffdb 100644 --- a/tests/value/oracle/multidim.res.oracle +++ b/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: [--..--]