From 9d695290b7d3e19f089dfe129f8529e4b3cb0cc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Apr 2022 16:49:14 +0200
Subject: [PATCH] [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.
---
src/plugins/value/domains/multidim/multidim_domain.ml | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index 1f94290c18f..806c5a95ba9 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -689,12 +689,10 @@ struct
| `Value loc ->
let update value' =
let v = Value_or_Uninitialized.narrow value value' in
- (* The value can legitimately be bottom on escaping variables (not
- tracked by the multidim domain), or on empty structs or unions.
- In these cases, do not reduce the state to bottom. *)
- if Value_or_Uninitialized.is_bottom v
- && not record.value.escaping
- && not (Int_Base.is_zero (Bit_utils.sizeof_lval lv))
+ (* The value can legitimately be bottom on escaping variables,
+ which are not tracked by the multidim domain.
+ In this case, do not reduce the state to bottom. *)
+ if Value_or_Uninitialized.is_bottom v && not record.value.escaping
then `Bottom
else `Value v
in
--
GitLab