From 65e4bfd3aebf2c4a91432d5bf6111586c27fd8b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 8 Sep 2020 15:25:05 +0200
Subject: [PATCH] [Eva] Builtins string: misaligned pointers are considered
invalid.
But they are not reduced to properly aligned pointers for now.
---
src/plugins/value/domains/cvalue/builtins_string.ml | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index c5d67fdf4cb..b4ac0886249 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
--
GitLab