diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml index f2db71da693e981cf70d699cb9c6c241c6188c50..69c822f12d8d82379993cecfb6ae7027c97daf6d 100644 --- a/src/plugins/value/domains/equality/equality_domain.ml +++ b/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 diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml index 0a9f4e8d73e9d4a104df8f3bb8b8a49d8c21ff08..509706949c4a74c3f2be0fe9d311dac6c298a855 100644 --- a/src/plugins/value/utils/value_util.ml +++ b/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) diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities index c967b2a64eeb9dc9de674551e093ecd6fc57f977..dc9d2d37177c919701635b8c46f9ebd3a3e9d1ab 100644 --- a/tests/builtins/diff_equalities +++ b/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. diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities index 7120cfb086274487c1455db9fce565050865a079..dff0951199db5e7fd420203047add34788d4aa4f 100644 --- a/tests/value/diff_equalities +++ b/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]