diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml index 7a58005d92be8f394687268b4a7f44a76084b3e7..84e733c6df405f9918dcb0daf26aab1ad41cd283 100644 --- a/src/plugins/eva/engine/evaluation.ml +++ b/src/plugins/eva/engine/evaluation.ml @@ -451,12 +451,18 @@ module Make | _ -> assert false let assume_pointer expr value = - if Kernel.InvalidPointer.get () - then - let truth = Value.assume_pointer value in - let alarm () = Alarms.Invalid_pointer expr in - interpret_truth ~alarm value truth - else return value + let value, alarms = + if Kernel.InvalidPointer.get () + then + let truth = Value.assume_pointer value in + let alarm () = Alarms.Invalid_pointer expr in + interpret_truth ~alarm value truth + else return value + in + (* Rewrap absolute addresses of pointer values, seen as unsigned + integers, to ensure a consistent representation of pointers. *) + let range = Eval_typ.pointer_range () in + value >>-: Value.rewrap_integer range, alarms let handle_overflow ~may_overflow expr typ value = match Eval_typ.classify_as_scalar typ with diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml index 129d1db7b5643e23fd52bda72966245818eba026..96f0c767a464317fee680bdcb4a8a43ecc1fc5e8 100644 --- a/src/plugins/eva/utils/eval_typ.ml +++ b/src/plugins/eva/utils/eval_typ.ml @@ -211,16 +211,15 @@ type scalar_typ = | TSPtr of integer_range | TSFloat of fkind +let pointer_range () = + { i_bits = Cil.bitsSizeOfInt Cil.theMachine.Cil.upointKind; + i_signed = Cil.isSigned Cil.theMachine.Cil.upointKind } + let classify_as_scalar typ = match Cil.unrollType typ with | TInt (ik, attrs) | TEnum ({ekind=ik}, attrs) -> Some (TSInt (ik_attrs_range ik attrs)) - | TPtr _ -> - let range = - { i_bits = Cil.bitsSizeOfInt Cil.theMachine.Cil.upointKind; - i_signed = Cil.isSigned Cil.theMachine.Cil.upointKind } - in - Some (TSPtr range) + | TPtr _ -> Some (TSPtr (pointer_range ())) | TFloat (fk, _) -> Some (TSFloat fk) | _ -> None diff --git a/src/plugins/eva/utils/eval_typ.mli b/src/plugins/eva/utils/eval_typ.mli index f6ce26872bcabf8ed6897ac74cfef6202c434c14..18e94b718afae26e34319dc1f7c757d3d8f943e6 100644 --- a/src/plugins/eva/utils/eval_typ.mli +++ b/src/plugins/eva/utils/eval_typ.mli @@ -75,6 +75,9 @@ val ik_attrs_range: ikind -> attributes -> integer_range (** Range for an integer type with some attributes. The attribute {!Cil.bitfield_attribute_name} influences the width of the type. *) +val pointer_range: unit -> integer_range +(** Range for a pointer type. *) + val range_inclusion: integer_range -> integer_range -> bool (** Checks inclusion of two integer ranges. *) diff --git a/src/plugins/eva/values/abstract_value.ml b/src/plugins/eva/values/abstract_value.ml index e63cc2c575d9c80f65234f92f420cc9da1b3248e..353773dc05fd30888d102d17cd863907ef0b6384 100644 --- a/src/plugins/eva/values/abstract_value.ml +++ b/src/plugins/eva/values/abstract_value.ml @@ -133,7 +133,8 @@ module type S = sig val forward_binop : typ -> binop -> t -> t -> t or_bottom (** [rewrap_integer irange t] wraps around the abstract value [t] to fit the - integer range [irange], assuming 2's complement. *) + integer range [irange], assuming 2's complement. Also used on absolute + addresses for pointer values, seen as unsigned integers. *) val rewrap_integer: Eval_typ.integer_range -> t -> t (** Abstract evaluation of casts operators from [src_type] to [dst_type]. *) diff --git a/tests/value/oracle/absolute_pointer.1.res.oracle b/tests/value/oracle/absolute_pointer.1.res.oracle index 1a7896cbbe0d439eeb0da5169506f653cec2cdf4..0aca61ab004a4d4e16594efdc9213507d1037014 100644 --- a/tests/value/oracle/absolute_pointer.1.res.oracle +++ b/tests/value/oracle/absolute_pointer.1.res.oracle @@ -6,21 +6,16 @@ NULL[rbits 0 to 147573952589676412935] ∈ [--..--] R ∈ {0} nondet ∈ [--..--] -[eva:alarm] absolute_pointer.c:43: Warning: - out of bounds write. assert \valid(p - 100); -[kernel] absolute_pointer.c:43: Warning: - all target addresses were invalid. This path is assumed to be dead. +[eva] absolute_pointer.c:44: Frama_C_show_each: {4294967196} [eva] absolute_pointer.c:47: Frama_C_show_each: {4294967196} [eva] absolute_pointer.c:52: Frama_C_show_each: {4294967197} [eva] absolute_pointer.c:56: Frama_C_show_each: {4294967197} [eva] Recording results for negative_absolute_address [eva] Done for function negative_absolute_address -[eva] absolute_pointer.c:43: - assertion 'Eva,mem_access' got final status invalid. [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function negative_absolute_address: NULL[rbits 0 to 34359737567] ∈ [--..--] - [rbits 34359737568 to 34359737575] ∈ {1} + [rbits 34359737568 to 34359737575] ∈ {1; 25} [rbits 34359737576 to 34359737583] ∈ {2; 42} [rbits 34359737584 to 147573952589676412935] ∈ [--..--] uptr ∈ {0} diff --git a/tests/value/oracle_multidim/strings_logic.res.oracle b/tests/value/oracle_multidim/strings_logic.res.oracle index ed8b014f3c938746a7a7790d93d56af817eedd62..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 --- a/tests/value/oracle_multidim/strings_logic.res.oracle +++ b/tests/value/oracle_multidim/strings_logic.res.oracle @@ -1,8 +0,0 @@ -83c83 -< {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ; ---- -> {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ; -92c92 -< {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ; ---- -> {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;