[Eva] Multidim domain: ignores assignments of size zero (empty structs or unions).

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

tests/value/oracle_multidim/empty_union.res.oracle

-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