diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml index c5d67fdf4cb17f38c4f6dee5dc7c2f78a86ae1e1..b4ac08862493c3272bd84e284c68b5995b20ba74 100644 --- a/src/plugins/value/domains/cvalue/builtins_string.ml +++ b/src/plugins/value/domains/cvalue/builtins_string.ml @@ -339,7 +339,12 @@ let reduce_by_validity ~size cvalue = let loc_bits = Locations.loc_bytes_to_loc_bits cvalue in let loc = Locations.make_loc loc_bits (Int_Base.inject size) in if Locations.(is_valid Read loc) - then loc.Locations.loc, true + then + let is_aligned _base ival = + Ival.is_zero (Ival.scale_rem ~pos:true size ival) + in + let valid = Locations.Location_Bits.for_all is_aligned loc_bits in + loc.Locations.loc, valid else let valid_loc = Locations.(valid_part Read ~bitfield:true loc) in valid_loc.Locations.loc, false