From db2c36f751ca79ba83491b8c23489c5c44d3736a 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:11:44 +0200
Subject: [PATCH] [Eva] Multidim domain: ignores assignments of size zero
 (empty structs or unions).

---
 .../value/domains/multidim/multidim_domain.ml | 11 ++--
 .../oracle_multidim/empty_union.res.oracle    | 65 -------------------
 2 files changed, 7 insertions(+), 69 deletions(-)
 delete mode 100644 tests/value/oracle_multidim/empty_union.res.oracle

diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index 65cff3ec0ea..1f94290c18f 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -726,10 +726,13 @@ struct
         | `Value src ->
           overwrite ~oracle state dst src
 
-  let assign _kinstr { lval=dst } src assigned_value valuation state =
-    let+ state = assume_valuation valuation state in
-    let oracle = valuation_to_oracle state valuation in
-    assign' ~oracle ~value:assigned_value dst (Some src) state
+  let assign _kinstr { lval=dst; ltyp } src assigned_value valuation state =
+    if Int_Base.is_zero (Bit_utils.sizeof ltyp)
+    then `Value state
+    else
+      let+ state = assume_valuation valuation state in
+      let oracle = valuation_to_oracle state valuation in
+      assign' ~oracle ~value:assigned_value dst (Some src) state
 
   let assume _stmt _expr _pos valuation state =
     assume_valuation valuation state
diff --git a/tests/value/oracle_multidim/empty_union.res.oracle b/tests/value/oracle_multidim/empty_union.res.oracle
deleted file mode 100644
index 23a5ad4e379..00000000000
--- a/tests/value/oracle_multidim/empty_union.res.oracle
+++ /dev/null
@@ -1,65 +0,0 @@
-37a38,41
-> [eva] empty_union.c:30: 
->   The evaluation of the expression s.b + 10
->   led to bottom without alarms:
->   at this point the product of states has no possible concretization.
-40,46d43
-< [eva] computing for function copy_empty <- main.
-<   Called from empty_union.c:81.
-< [eva:alarm] empty_union.c:37: Warning: 
-<   function copy_empty: postcondition got status unknown.
-< [eva] Recording results for copy_empty
-< [eva] Done for function copy_empty
-< [eva] empty_union.c:83: Frama_C_show_each_res: {74}
-50,51d46
-< [eva:final-states] Values at end of function copy_empty:
-<   
-53c48
-<   res{.a; .e{}; .b} ∈ {74}
----
->   NON TERMINATING FUNCTION
-55,64c50
-<   c1{.a; .e{}; .b} ∈ {77}
-<   c2{.a; .e{}; .b} ∈ {77}
-<   res{.a; .e{}; .b} ∈ {74}
-<   cb{.s{}; .i} ∈ {91}
-<   ce{.ch; .ss{}} ∈ {90}
-<   p ∈ {{ (union empty *)&cb }}
-<   pc ∈ {{ &empty_init_array[0] }}
-<   __retres ∈ {0}
-< [from] Computing for function copy_empty
-< [from] Done for function copy_empty
----
->   NON TERMINATING FUNCTION
-65a52
-> [from] Non-terminating function f (no dependencies)
-69a57
-> [from] Non-terminating function main (no dependencies)
-73,74d60
-< [from] Function copy_empty:
-<   NO EFFECTS
-76c62
-<   \result FROM s
----
->   NON TERMINATING - NO EFFECTS
-81c67
-<   \result FROM \nothing
----
->   NON TERMINATING - NO EFFECTS
-83,86d68
-< [inout] Out (internal) for function copy_empty:
-<     \nothing
-< [inout] Inputs for function copy_empty:
-<     \nothing
-90c72
-<     nondet
----
->     \nothing
-92c74
-<     c1; c2; res; cb; ce; p; pc; __retres
----
->     c1; c2; res
-94c76
-<     nondet
----
->     \nothing
-- 
GitLab