Merge branch 'fix/eva/equality-domain' into 'master'

[Eva] Uses enumerate_valid_bits instead of enumerate_bits.

See merge request frama-c/frama-c!2084

src/plugins/value/domains/equality/equality_domain.ml

@@ -406,7 +406,9 @@ module Make
     let assign _stmt left_value right_expr value valuation state =
       let open Locations in
       let left_loc = Precise_locs.imprecise_location left_value.lloc in
-      let direct_left_zone = Locations.enumerate_bits left_loc in
+      let direct_left_zone =
+        Locations.enumerate_valid_bits ~for_writing:true left_loc
+      in
       let state = kill Hcexprs.Modified direct_left_zone state in
       let right_expr = Cil.constFold true right_expr in
       try
@@ -513,7 +515,7 @@ module Make
 
   let logic_assign _assigns location ~pre:_ state =
     let loc = Precise_locs.imprecise_location location in
-    let zone = Locations.enumerate_bits loc in
+    let zone = Locations.enumerate_valid_bits ~for_writing:true loc in
     kill Hcexprs.Modified zone state
 
   let evaluate_predicate _ _ _ = Alarmset.Unknown

src/plugins/value/utils/value_util.ml

@@ -269,8 +269,9 @@ let rec zone_of_expr find_loc expr =
 (* dereference of an lvalue: first, its address must be computed,
    then its contents themselves are read *)
 and zone_of_lval find_loc lval =
-  let loc = find_loc lval in
-  let zone = Locations.enumerate_bits (Precise_locs.imprecise_location loc) in
+  let ploc = find_loc lval in
+  let loc = Precise_locs.imprecise_location ploc in
+  let zone = Locations.enumerate_valid_bits ~for_writing:false loc in
   Locations.Zone.join zone
     (indirect_zone_of_lval find_loc lval)
 

tests/builtins/diff_equalities

@@ -315,14 +315,10 @@ diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_equalities
 <   more than 200(300) elements to enumerate. Approximating.
 < [kernel] tests/builtins/imprecise.c:114: 
 <   more than 200(300) elements to enumerate. Approximating.
-diff tests/builtins/oracle/linked_list.0.res.oracle tests/builtins/oracle_equalities/linked_list.0.res.oracle
-421a422,423
-> [kernel] tests/builtins/linked_list.c:19: 
->   more than 200(536870912) elements to enumerate. Approximating.
 diff tests/builtins/oracle/linked_list.1.res.oracle tests/builtins/oracle_equalities/linked_list.1.res.oracle
 422a423,424
 > [kernel] tests/builtins/linked_list.c:19: 
->   more than 100(0x20000000) elements to enumerate. Approximating.
+>   more than 100(128) elements to enumerate. Approximating.
 470a473,474
 > [kernel] tests/builtins/linked_list.c:43: 
 >   more than 100(128) elements to enumerate. Approximating.

tests/value/diff_equalities

@@ -116,10 +116,6 @@ diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_equalities/alias.6
 <   x ∈ {0; 4; 33}
 ---
 >   x ∈ {33}
-diff tests/value/oracle/assigns.res.oracle tests/value/oracle_equalities/assigns.res.oracle
-143a144,145
->   more than 200(4294967296) elements to enumerate. Approximating.
-> [kernel] tests/value/assigns.i:104: 
 diff tests/value/oracle/backward_add_ptr.res.oracle tests/value/oracle_equalities/backward_add_ptr.res.oracle
 12c12
 <   Frama_C_show_each_only_a: {0; 1}, {{ &a }}, {0}
@@ -237,6 +233,11 @@ diff tests/value/oracle/backward_add_ptr.res.oracle tests/value/oracle_equalitie
 >     (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
 >   {{ garbled mix of &{b; c}
 >     (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
+diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_equalities/bitfield.res.oracle
+132a133,135
+> [eva] tests/value/bitfield.i:71: 
+>   Frama_C_show_each:
+>   {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
 diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_equalities/bitwise_pointer.res.oracle
 58c58
 <   x ∈ [0..9]