From 72781a6353a89c02518480a395a71fac8612d1fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 28 Feb 2020 16:11:58 +0100
Subject: [PATCH] [Eva] Base: fixes the possible offsets for the Null base
without memory access.
When -absolute-valid-range is enabled, the Null base has a Known validity,
but a pointer can always points to Null+{0}.
---
src/kernel_services/abstract_interp/base.ml | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index e0ff1e50268..226eefc98e5 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -306,7 +306,14 @@ let offset_for_validity ~bitfield access base =
let valid_offset ?(bitfield=true) access base =
if for_writing access && is_read_only base
then Ival.bottom
- else offset_for_validity ~bitfield access base
+ else
+ let offset = offset_for_validity ~bitfield access base in
+ (* When -absolute-valid-range is enabled, the Null base has a Known validity
+ that does not include 0. In this case, adds 0 as possible offset for a
+ pointer without memory access. *)
+ if access = No_access && is_null base
+ then Ival.(join zero offset)
+ else offset
let offset_is_in_validity access base ival =
let is_valid_for_bounds min_bound max_bound =
@@ -327,7 +334,8 @@ let offset_is_in_validity access base ival =
let is_valid_offset access base offset =
Ival.is_bottom offset
|| not (for_writing access && (is_read_only base))
- && offset_is_in_validity access base offset
+ && (offset_is_in_validity access base offset
+ || access = No_access && is_null base && Ival.(equal zero offset))
let is_function base =
match base with
--
GitLab