diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 378c06407ac8824f2683a91c507acd6eb9a59ded..bd42be08f83a7ba1e603712d610a01bfe4865297 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -92,6 +92,15 @@ module type S = sig
floating-point values. *)
val assume_not_nan: assume_finite:bool -> fkind -> t -> t truth
+ (** Assumes that the abstract value only represents well-formed pointer values:
+ pointers either to an element of an array object or one past the last
+ element of an array object. (A pointer to an object that is not an element
+ of an array is viewed as a pointer to the first element of an array of
+ length one with the type of the object as its element type.)
+ The NULL pointer is always a valid pointer value. Function pointers are
+ also considered as valid pointer values for now. *)
+ val assume_pointer: t -> t truth
+
(* [assume_comparable cmp v1 v2] assumes that the integer or pointer values
[v1] and [v2] are comparable for [cmp]. Integers are always comparable.
If one value is a pointer, then both values should be pointers, and:
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index ad45ab9ddb82a3401e4b49807eb891aefcc2e9c9..6822e5f5a5c0218144b3776f9d489431f8c63b9e 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -220,6 +220,35 @@ let assume_not_nan ~assume_finite fkind v =
let res = Bottom.non_bottom (backward_propagate kind res) in
`Unknown (V.inject_float res)
+let nearly_valid_bits = function
+ | Base.Empty
+ | Base.Invalid -> Integer.zero, Integer.zero
+ | Base.Known (min, max) | Base.Unknown (min, _, max) -> min, Integer.succ max
+ | Base.Variable variable -> Integer.zero, Integer.succ variable.Base.max_alloc
+
+let nearly_valid_offset base =
+ let min, max = nearly_valid_bits base in
+ let to_byte bound = Some (Integer.e_div bound (Bit_utils.sizeofchar ())) in
+ Ival.inject_range (to_byte min) (to_byte max)
+
+let assume_pointer loc =
+ let aux base ival (acc_v, acc_ok) =
+ let validity = Base.validity base in
+ let nearly_valid_ival = nearly_valid_offset validity in
+ let new_ival = Ival.narrow ival nearly_valid_ival in
+ let ival, ok =
+ if Base.is_null base && Ival.contains_zero ival
+ then Ival.(join zero new_ival), acc_ok && Ival.is_zero ival
+ else new_ival, acc_ok && Ival.equal ival new_ival
+ in
+ Locations.Location_Bytes.add base ival acc_v, ok
+ in
+ try
+ let loc, ok = Cvalue.V.(fold_topset_ok aux loc (bottom, true)) in
+ if Cvalue.V.is_bottom loc then `False
+ else if ok then `True else `Unknown loc
+ with Abstract_interp.Error_Top -> `Unknown loc
+
(* --------------------------------------------------------------------------
Integer overflow
-------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/values/cvalue_forward.mli b/src/plugins/value/values/cvalue_forward.mli
index 77b587c28e4ab060e78f25b509f4c9147cd5ed78..07fb2ef75915314f21d06964eaecb79275586f9a 100644
--- a/src/plugins/value/values/cvalue_forward.mli
+++ b/src/plugins/value/values/cvalue_forward.mli
@@ -31,6 +31,7 @@ val are_comparable: Abstract_interp.Comp.t -> V.t -> V.t -> bool
val assume_non_zero: V.t -> V.t truth
val assume_bounded: bound_kind -> bound -> V.t -> V.t truth
val assume_not_nan: assume_finite:bool -> fkind -> V.t -> V.t truth
+val assume_pointer: V.t -> V.t truth
val assume_comparable: pointer_comparison -> V.t -> V.t -> (V.t * V.t) truth
val forward_binop_int: typ: typ -> V.t -> binop -> V.t -> V.t
diff --git a/src/plugins/value/values/main_values.ml b/src/plugins/value/values/main_values.ml
index ebd8d3b0989f20f0823c5a3f7d1d39ba2ee204b3..9218b0a03a3487a1a5db9ebe2458e0f0685c7c63 100644
--- a/src/plugins/value/values/main_values.ml
+++ b/src/plugins/value/values/main_values.ml
@@ -46,6 +46,7 @@ module CVal = struct
let assume_non_zero = Cvalue_forward.assume_non_zero
let assume_bounded = Cvalue_forward.assume_bounded
let assume_not_nan = Cvalue_forward.assume_not_nan
+ let assume_pointer = Cvalue_forward.assume_pointer
let assume_comparable = Cvalue_forward.assume_comparable
let constant exp = function
@@ -165,6 +166,7 @@ module Interval = struct
let assume_non_zero v = `Unknown v
let assume_bounded _ _ v = `Unknown v
let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
let constant _ _ = top
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index da6a115444b5f7ae2e53d052a4e279a68ec1898d..443a2dd4434c76dadcaf3a6cf0f9b5131db5be81 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -312,6 +312,7 @@ let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
let assume_non_zero v = `Unknown v
let assume_bounded _kind _bound v = `Unknown v
let assume_not_nan ~assume_finite:_ _fkind v = `Unknown v
+let assume_pointer v = `Unknown v
let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
let rewrap_integer _ _ = top
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index 672025219b711c59baca3137ee4f3f38190af6f1..d6d7995ae35610386a32b37fe3a7bf6b3c5c6740 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -423,6 +423,7 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
let assume_non_zero v = `Unknown v
let assume_bounded _ _ v = `Unknown v
let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
let constant e _c =
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 58f961a324df016d91c2ad5360353f5fdcba03d3..74c45a2c26862947e8909f5d0997dbf695722b5a 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -120,6 +120,7 @@ let assume_non_zero v =
let assume_bounded _ _ v = `Unknown v
let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
(** {2 Forward transfer functions} *)
diff --git a/src/plugins/value/values/value_product.ml b/src/plugins/value/values/value_product.ml
index 5b612953614ba7ba8dfd9fbbeefe6462af8b8de3..99d6ff34751be79fb0497c2969ab6b8a4ecf1963 100644
--- a/src/plugins/value/values/value_product.ml
+++ b/src/plugins/value/values/value_product.ml
@@ -81,6 +81,11 @@ module Make
and right_truth = Right.assume_not_nan ~assume_finite fkind right in
narrow_truth (left, left_truth) (right, right_truth)
+ let assume_pointer (left, right) =
+ let left_truth = Left.assume_pointer left
+ and right_truth = Right.assume_pointer right in
+ narrow_truth (left, left_truth) (right, right_truth)
+
let assume_comparable op (l1, r1) (l2, r2) =
let left_truth = Left.assume_comparable op l1 l2
and right_truth = Right.assume_comparable op r1 r2 in