Skip to content
Snippets Groups Projects
Commit 9d695290 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Multidim domain: removes an unnecessary condition.

Non-scalar lvalues are now completely ignored from the valuation, so no need
to check for empty structs or unions here.
parent db2c36f7
No related branches found
No related tags found
No related merge requests found
...@@ -689,12 +689,10 @@ struct ...@@ -689,12 +689,10 @@ struct
| `Value loc -> | `Value loc ->
let update value' = let update value' =
let v = Value_or_Uninitialized.narrow value value' in let v = Value_or_Uninitialized.narrow value value' in
(* The value can legitimately be bottom on escaping variables (not (* The value can legitimately be bottom on escaping variables,
tracked by the multidim domain), or on empty structs or unions. which are not tracked by the multidim domain.
In these cases, do not reduce the state to bottom. *) In this case, do not reduce the state to bottom. *)
if Value_or_Uninitialized.is_bottom v if Value_or_Uninitialized.is_bottom v && not record.value.escaping
&& not record.value.escaping
&& not (Int_Base.is_zero (Bit_utils.sizeof_lval lv))
then `Bottom then `Bottom
else `Value v else `Value v
in in
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment