From 48f0beafe945e70c035a739dbb879c282f78602f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 26 Mar 2020 19:24:13 +0100
Subject: [PATCH] [Kernel] Fixes alarm: uses TCastE instead of TLogic_coerce.
New smart constructor for TCastE in logic_const.
---
src/kernel_services/ast_data/alarms.ml | 3 +-
.../ast_queries/logic_const.ml | 3 +
.../ast_queries/logic_const.mli | 3 +
.../oracle/imprecise-malloc-free.res.oracle | 12 ++--
tests/builtins/oracle/imprecise.res.oracle | 8 +--
tests/builtins/oracle/memchr.res.oracle | 2 +-
tests/builtins/oracle/memcpy.res.oracle | 8 +--
tests/builtins/oracle/memset.res.oracle | 4 +-
tests/builtins/oracle/strchr.res.oracle | 4 +-
tests/builtins/oracle/strlen.res.oracle | 2 +-
tests/builtins/oracle/strnlen2.res.oracle | 2 +-
tests/builtins/oracle/wcslen.res.oracle | 8 +--
tests/float/oracle/builtins.res.oracle | 2 +-
tests/float/oracle/nonlin.0.res.oracle | 4 +-
tests/float/oracle/nonlin.1.res.oracle | 4 +-
tests/float/oracle/nonlin.2.res.oracle | 4 +-
tests/float/oracle/nonlin.3.res.oracle | 4 +-
tests/float/oracle/nonlin.4.res.oracle | 4 +-
tests/float/oracle/nonlin.5.res.oracle | 4 +-
tests/value/oracle/addition.res.oracle | 68 ++++++++++---------
.../value/oracle/align_char_array.res.oracle | 16 ++---
tests/value/oracle/arith_pointer.res.oracle | 4 +-
tests/value/oracle/array_ptr.res.oracle | 2 +-
tests/value/oracle/assigns.res.oracle | 8 +--
tests/value/oracle/bitfield.res.oracle | 12 ++--
tests/value/oracle/bitwise_pointer.res.oracle | 4 +-
tests/value/oracle/cmp_ptr.0.res.oracle | 2 +-
tests/value/oracle/cmp_ptr.1.res.oracle | 2 +-
tests/value/oracle/context_free.res.oracle | 2 +-
tests/value/oracle/conversion.res.oracle | 4 +-
tests/value/oracle/deps_addr.res.oracle | 2 +-
tests/value/oracle/deps_mixed.res.oracle | 2 +-
tests/value/oracle/div.0.res.oracle | 10 +--
tests/value/oracle/div.1.res.oracle | 10 +--
tests/value/oracle/eval_separated.res.oracle | 4 +-
tests/value/oracle/from_call.0.res.oracle | 4 +-
tests/value/oracle/from_call.1.res.oracle | 4 +-
tests/value/oracle/from_ptr.0.res.oracle | 4 +-
tests/value/oracle/from_ptr.1.res.oracle | 4 +-
tests/value/oracle/fun_ptr.1.res.oracle | 4 +-
.../oracle/imprecise_invalid_write.res.oracle | 2 +-
tests/value/oracle/initialized.res.oracle | 2 +-
tests/value/oracle/join_misaligned.res.oracle | 4 +-
tests/value/oracle/label.res.oracle | 2 +-
tests/value/oracle/leaf2.res.oracle | 2 +-
tests/value/oracle/mini_pointrer.res.oracle | 2 +-
tests/value/oracle/nonlin.res.oracle | 2 +-
.../value/oracle/not_ct_array_arg.res.oracle | 2 +-
tests/value/oracle/offset_top.res.oracle | 2 +-
tests/value/oracle/offsetmap.0.res.oracle | 2 +-
tests/value/oracle/offsetmap.1.res.oracle | 2 +-
tests/value/oracle/origin.0.res.oracle | 22 +++---
tests/value/oracle/origin.1.res.oracle | 2 +-
tests/value/oracle/period.res.oracle | 6 +-
.../oracle/pointer_comparison.0.res.oracle | 12 ++--
.../oracle/pointer_comparison.1.res.oracle | 12 ++--
.../value/oracle/pointer_int_cast.res.oracle | 2 +-
tests/value/oracle/shift.0.res.oracle | 2 +-
tests/value/oracle/shift.1.res.oracle | 2 +-
tests/value/oracle/sizeof.res.oracle | 4 +-
tests/value/oracle/struct3.res.oracle | 2 +-
tests/value/oracle/struct_array.res.oracle | 12 ++--
tests/value/oracle/struct_incl.res.oracle | 6 +-
tests/value/oracle/symbolic_locs.res.oracle | 2 +-
tests/value/oracle/volatile.res.oracle | 2 +-
65 files changed, 189 insertions(+), 180 deletions(-)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 445efc3204d..2faab4979f1 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -553,8 +553,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
let t = match kind with
| Pointer_downcast ->
let t = Logic_utils.expr_to_term ~cast:true e in
- let typ = Cil.theMachine.upointType in
- Logic_const.tlogic_coerce ~loc t (Ctype typ)
+ Logic_const.tcast ~loc t Cil.theMachine.upointType
| Signed_downcast | Unsigned_downcast ->
Logic_utils.expr_to_term ~cast:true e
| _ ->
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 8da10c3cf69..e9417dd0256 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -305,6 +305,9 @@ let tat ?(loc=Cil_datatype.Location.unknown) (t,label) =
let told ?(loc=Cil_datatype.Location.unknown) t = tat ~loc (t,old_label)
+let tcast ?(loc=Cil_datatype.Location.unknown) t ct =
+ term ~loc (TCastE (ct, t)) (Ctype ct)
+
let tlogic_coerce ?(loc=Cil_datatype.Location.unknown) t lt =
term ~loc (TLogic_coerce (lt, t)) lt
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index c3be4194f94..280661c522f 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -321,6 +321,9 @@ val tvar: ?loc:Location.t -> logic_var -> term
(** \result *)
val tresult: ?loc:Location.t -> typ -> term
+(** cast to the given C type *)
+val tcast: ?loc:Location.t -> term -> typ -> term
+
(** coercion to the given logic type *)
val tlogic_coerce: ?loc:Location.t -> term -> logic_type -> term
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index c748e18da98..4d7ac635f76 100644
--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -5,9 +5,9 @@
[eva:initial-state] Values of globals at initialization
i ∈ [--..--]
[eva:alarm] tests/builtins/imprecise-malloc-free.c:12: Warning:
- pointer downcast. assert (unsigned int)&size1 + i ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&size1 + i) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:13: Warning:
- pointer downcast. assert (unsigned int)&size2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&size2) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:13: Warning:
signed overflow. assert -2147483648 ≤ i + (int)((int)(&size2) >> 1);
[eva:alarm] tests/builtins/imprecise-malloc-free.c:13: Warning:
@@ -17,7 +17,7 @@
The imprecision originates from Arithmetic
{tests/builtins/imprecise-malloc-free.c:13}
[eva:alarm] tests/builtins/imprecise-malloc-free.c:14: Warning:
- pointer downcast. assert (unsigned int)&i ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&i) ≤ 2147483647;
[eva] tests/builtins/imprecise-malloc-free.c:14: Call to builtin malloc
[eva] tests/builtins/imprecise-malloc-free.c:14:
allocating variable __malloc_main_l14
@@ -37,15 +37,15 @@
[eva:alarm] tests/builtins/imprecise-malloc-free.c:21: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] tests/builtins/imprecise-malloc-free.c:21: Warning:
- pointer downcast. assert (unsigned int)p + 1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(p + 1) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:22: Warning:
out of bounds write. assert \valid(q);
[eva:alarm] tests/builtins/imprecise-malloc-free.c:22: Warning:
- pointer downcast. assert (unsigned int)q + 2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(q + 2) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:23: Warning:
out of bounds write. assert \valid(r);
[eva:alarm] tests/builtins/imprecise-malloc-free.c:23: Warning:
- pointer downcast. assert (unsigned int)r + 3 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(r + 3) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:25: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva] tests/builtins/imprecise-malloc-free.c:25: Call to builtin free
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 240ad0e4b03..f93b938207e 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -49,7 +49,7 @@
[eva] computing for function write_garbled <- main.
Called from tests/builtins/imprecise.c:145.
[eva:alarm] tests/builtins/imprecise.c:19: Warning:
- pointer downcast. assert (unsigned int)&k ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&k) ≤ 2147483647;
[eva] tests/builtins/imprecise.c:19:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/builtins/imprecise.c:19}
@@ -110,7 +110,7 @@
[eva:alarm] tests/builtins/imprecise.c:53: Warning:
out of bounds write. assert \valid(p2);
[eva:alarm] tests/builtins/imprecise.c:53: Warning:
- pointer downcast. assert (unsigned int)&addr ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&addr) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise.c:56: Warning:
out of bounds write. assert \valid(p4);
[eva:alarm] tests/builtins/imprecise.c:58: Warning:
@@ -625,7 +625,7 @@
[eva] computing for function write_garbled <- main.
Called from tests/builtins/imprecise.c:145.
[eva:alarm] tests/builtins/imprecise.c:19: Warning:
- pointer downcast. assert (unsigned int)&k ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&k) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise.c:20: Warning:
out of bounds write. assert \valid(p);
[eva] tests/builtins/imprecise.c:21:
@@ -686,7 +686,7 @@
[eva:alarm] tests/builtins/imprecise.c:53: Warning:
out of bounds write. assert \valid(p2);
[eva:alarm] tests/builtins/imprecise.c:53: Warning:
- pointer downcast. assert (unsigned int)&addr ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&addr) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise.c:56: Warning:
out of bounds write. assert \valid(p4);
[eva:alarm] tests/builtins/imprecise.c:58: Warning:
diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle
index 452e93e5b6d..4fbe20f941e 100644
--- a/tests/builtins/oracle/memchr.res.oracle
+++ b/tests/builtins/oracle/memchr.res.oracle
@@ -478,7 +478,7 @@
[eva] computing for function memchr_escaping <- main.
Called from tests/builtins/memchr.c:662.
[eva:alarm] tests/builtins/memchr.c:264: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/memchr.c:264: Warning:
locals {x} escaping the scope of a block of memchr_escaping through s
[eva] tests/builtins/memchr.c:267: Call to builtin memchr
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index b6358392e62..68da1692272 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -129,7 +129,7 @@
[eva] tests/builtins/memcpy.c:85:
function memcpy: precondition 'separation' got status valid.
[eva:alarm] tests/builtins/memcpy.c:87: Warning:
- pointer downcast. assert (unsigned int)(struct t1 *)t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
[eva] tests/builtins/memcpy.c:87: Call to builtin memcpy
[eva] tests/builtins/memcpy.c:87:
function memcpy: precondition 'valid_dest' got status valid.
@@ -138,7 +138,7 @@
[eva] tests/builtins/memcpy.c:87:
function memcpy: precondition 'separation' got status valid.
[eva:alarm] tests/builtins/memcpy.c:89: Warning:
- pointer downcast. assert (unsigned int)&v4 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&v4) ≤ 2147483647;
[eva] tests/builtins/memcpy.c:89: Call to builtin memcpy
[eva:alarm] tests/builtins/memcpy.c:89: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
@@ -150,9 +150,9 @@
writing somewhere in {NULL; v4} because of Arithmetic
{tests/builtins/memcpy.c:89}.
[eva:alarm] tests/builtins/memcpy.c:90: Warning:
- pointer downcast. assert (unsigned int)(struct t1 *)t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
[eva:alarm] tests/builtins/memcpy.c:91: Warning:
- pointer downcast. assert (unsigned int)&v5 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&v5) ≤ 2147483647;
[eva] tests/builtins/memcpy.c:91: Call to builtin memcpy
[eva:alarm] tests/builtins/memcpy.c:91: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index 11215767505..e2c14678865 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -26,7 +26,7 @@
[eva] share/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva:alarm] tests/builtins/memset.c:34: Warning:
- pointer downcast. assert (unsigned int)(int *)t2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int *)t2) ≤ 2147483647;
[eva] tests/builtins/memset.c:34: Call to builtin memset
[eva:alarm] tests/builtins/memset.c:34: Warning:
function memset: precondition 'valid_s' got status unknown.
@@ -45,7 +45,7 @@
[eva:alarm] tests/builtins/memset.c:38: Warning:
function memset: precondition 'valid_s' got status invalid.
[eva:alarm] tests/builtins/memset.c:41: Warning:
- pointer downcast. assert (unsigned int)(int *)t1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int *)t1) ≤ 2147483647;
[eva] tests/builtins/memset.c:41: Call to builtin memset
[eva] tests/builtins/memset.c:41:
function memset: precondition 'valid_s' got status valid.
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index 6139567781a..21fd920919a 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -317,7 +317,7 @@
[eva] computing for function strchr_escaping <- main.
Called from tests/builtins/strchr.c:556.
[eva:alarm] tests/builtins/strchr.c:258: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/strchr.c:258: Warning:
locals {x} escaping the scope of a block of strchr_escaping through s
[eva] tests/builtins/strchr.c:261: Call to builtin strchr
@@ -672,7 +672,7 @@
[eva] computing for function strchr_garbled_mix_in_char <- main.
Called from tests/builtins/strchr.c:562.
[eva:alarm] tests/builtins/strchr.c:541: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/builtins/strchr.c:541:
Assigning imprecise value to garbled.
The imprecision originates from Arithmetic {tests/builtins/strchr.c:541}
diff --git a/tests/builtins/oracle/strlen.res.oracle b/tests/builtins/oracle/strlen.res.oracle
index 900d168bdba..dcc09a3de5d 100644
--- a/tests/builtins/oracle/strlen.res.oracle
+++ b/tests/builtins/oracle/strlen.res.oracle
@@ -262,7 +262,7 @@
[eva] computing for function escaping <- main.
Called from tests/builtins/strlen.c:342.
[eva:alarm] tests/builtins/strlen.c:222: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/strlen.c:222: Warning:
locals {x} escaping the scope of a block of escaping through s
[eva] tests/builtins/strlen.c:225: Call to builtin strlen
diff --git a/tests/builtins/oracle/strnlen2.res.oracle b/tests/builtins/oracle/strnlen2.res.oracle
index b04e6e5abe4..392940b6cb6 100644
--- a/tests/builtins/oracle/strnlen2.res.oracle
+++ b/tests/builtins/oracle/strnlen2.res.oracle
@@ -262,7 +262,7 @@
[eva] computing for function escaping <- main.
Called from tests/builtins/strnlen2.c:522.
[eva:alarm] tests/builtins/strnlen2.c:196: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/strnlen2.c:196: Warning:
locals {x} escaping the scope of a block of escaping through s
[eva] tests/builtins/strnlen2.c:199: Call to builtin strnlen
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index 0c9295b364c..784bf02c5cf 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -262,13 +262,13 @@
[eva] computing for function escaping <- main.
Called from tests/builtins/wcslen.c:347.
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/builtins/wcslen.c:222: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/wcslen.c:222: Warning:
locals {x} escaping the scope of a block of escaping through s
[eva] tests/builtins/wcslen.c:225: Call to builtin wcslen
diff --git a/tests/float/oracle/builtins.res.oracle b/tests/float/oracle/builtins.res.oracle
index 00d692def3c..66f30707d32 100644
--- a/tests/float/oracle/builtins.res.oracle
+++ b/tests/float/oracle/builtins.res.oracle
@@ -135,7 +135,7 @@
[eva] tests/float/builtins.c:104:
function exp: precondition 'finite_domain' got status valid.
[eva:alarm] tests/float/builtins.c:107: Warning:
- pointer downcast. assert (unsigned int)&d ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&d) ≤ 2147483647;
[eva:alarm] tests/float/builtins.c:107: Warning:
non-finite double value. assert \is_finite((double)((int)(&d)));
[eva] tests/float/builtins.c:107: Call to builtin log
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 6324ceb920c..5e60b7a32e5 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -231,9 +231,9 @@
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 + (int)(&x_0) ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 9f4864b2625..036f8d26e43 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -254,9 +254,9 @@
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 + (int)(&x_0) ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index a0b3a97b62f..112f643e881 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -241,9 +241,9 @@
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 + (int)(&x_0) ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva] tests/float/nonlin.c:98:
Assigning imprecise value to a_0.
The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index 52fc170f4f8..f791b980831 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -231,9 +231,9 @@
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 + (int)(&x_0) ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index 2d45c975ffb..ba58150afaf 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -254,9 +254,9 @@
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 + (int)(&x_0) ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 667b1228b96..36e1a671ef6 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -241,9 +241,9 @@
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
- pointer downcast. assert (unsigned int)&x_0 + (int)(&x_0) ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva] tests/float/nonlin.c:98:
Assigning imprecise value to a_0.
The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index 81d6deca427..1fe41a6755a 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -60,45 +60,47 @@
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {tests/value/addition.i:34}
[eva:alarm] tests/value/addition.i:36: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva] tests/value/addition.i:36:
Assigning imprecise value to p2.
The imprecision originates from Arithmetic {tests/value/addition.i:36}
[eva:alarm] tests/value/addition.i:38: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:38: Warning:
- pointer downcast. assert (unsigned int)&t[(char)(&p1)] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t[(char)(&p1)]) ≤ 2147483647;
[eva] tests/value/addition.i:38:
Assigning imprecise value to p3.
The imprecision originates from Arithmetic {tests/value/addition.i:38}
[eva:alarm] tests/value/addition.i:40: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:40: Warning:
- pointer downcast. assert (unsigned int)&tt[(char)(&p1)].a ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&tt[(char)(&p1)].a) ≤ 2147483647;
[eva] tests/value/addition.i:40:
Assigning imprecise value to p4.
The imprecision originates from Arithmetic {tests/value/addition.i:40}
[eva:alarm] tests/value/addition.i:42: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:42: Warning:
- pointer downcast. assert (unsigned int)&p2 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
[eva:alarm] tests/value/addition.i:42: Warning:
pointer downcast.
- assert (unsigned int)&ttt[(char)(&p1)][(char)(&p2)] ≤ 2147483647;
+ assert (unsigned int)(&ttt[(char)(&p1)][(char)(&p2)]) ≤ 2147483647;
[eva] tests/value/addition.i:42:
Assigning imprecise value to p5.
The imprecision originates from Arithmetic {tests/value/addition.i:42}
[eva:alarm] tests/value/addition.i:44: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:44: Warning:
- pointer downcast. assert (unsigned int)&ttt[(char)(&p1)][u2] ≤ 2147483647;
+ pointer downcast.
+ assert (unsigned int)(&ttt[(char)(&p1)][u2]) ≤ 2147483647;
[eva] tests/value/addition.i:44:
Assigning imprecise value to p6.
The imprecision originates from Arithmetic {tests/value/addition.i:44}
[eva:alarm] tests/value/addition.i:46: Warning:
- pointer downcast. assert (unsigned int)&p2 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
[eva:alarm] tests/value/addition.i:46: Warning:
- pointer downcast. assert (unsigned int)&ttt[u2][(char)(&p2)] ≤ 2147483647;
+ pointer downcast.
+ assert (unsigned int)(&ttt[u2][(char)(&p2)]) ≤ 2147483647;
[eva] tests/value/addition.i:46:
Assigning imprecise value to p7.
The imprecision originates from Arithmetic {tests/value/addition.i:46}
@@ -106,7 +108,7 @@
pointer comparison.
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
[eva:alarm] tests/value/addition.i:50: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
[eva:alarm] tests/value/addition.i:50: Warning:
@@ -115,14 +117,14 @@
Assigning imprecise value to p9.
The imprecision originates from Arithmetic {tests/value/addition.i:50}
[eva:alarm] tests/value/addition.i:52: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva] tests/value/addition.i:52:
Assigning imprecise value to p10.
The imprecision originates from Arithmetic {tests/value/addition.i:52}
[eva:alarm] tests/value/addition.i:56: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:56: Warning:
- pointer downcast. assert (unsigned int)&p2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p2) ≤ 2147483647;
[eva] tests/value/addition.i:56:
Assigning imprecise value to p12.
The imprecision originates from Arithmetic {tests/value/addition.i:56}
@@ -357,45 +359,47 @@
[eva:alarm] tests/value/addition.i:34: Warning:
signed overflow. assert &p2 - &p3 ≤ 2147483647;
[eva:alarm] tests/value/addition.i:36: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:38: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:38: Warning:
- pointer downcast. assert (unsigned int)&t[(char)(&p1)] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t[(char)(&p1)]) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:40: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:40: Warning:
- pointer downcast. assert (unsigned int)&tt[(char)(&p1)].a ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&tt[(char)(&p1)].a) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:42: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:42: Warning:
- pointer downcast. assert (unsigned int)&p2 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
[eva:alarm] tests/value/addition.i:42: Warning:
pointer downcast.
- assert (unsigned int)&ttt[(char)(&p1)][(char)(&p2)] ≤ 2147483647;
+ assert (unsigned int)(&ttt[(char)(&p1)][(char)(&p2)]) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:44: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] tests/value/addition.i:44: Warning:
- pointer downcast. assert (unsigned int)&ttt[(char)(&p1)][u2] ≤ 2147483647;
+ pointer downcast.
+ assert (unsigned int)(&ttt[(char)(&p1)][u2]) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:46: Warning:
- pointer downcast. assert (unsigned int)&p2 ≤ 127;
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
[eva:alarm] tests/value/addition.i:46: Warning:
- pointer downcast. assert (unsigned int)&ttt[u2][(char)(&p2)] ≤ 2147483647;
+ pointer downcast.
+ assert (unsigned int)(&ttt[u2][(char)(&p2)]) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:48: Warning:
pointer comparison.
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
[eva:alarm] tests/value/addition.i:50: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
[eva:alarm] tests/value/addition.i:50: Warning:
signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
[eva:alarm] tests/value/addition.i:52: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:56: Warning:
- pointer downcast. assert (unsigned int)&p1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:56: Warning:
- pointer downcast. assert (unsigned int)&p2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p2) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:59: Warning:
signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
[eva:alarm] tests/value/addition.i:59: Warning:
diff --git a/tests/value/oracle/align_char_array.res.oracle b/tests/value/oracle/align_char_array.res.oracle
index c84e281414a..3383a7f5af1 100644
--- a/tests/value/oracle/align_char_array.res.oracle
+++ b/tests/value/oracle/align_char_array.res.oracle
@@ -16,33 +16,33 @@
overlapread3 ∈ {0}
overlapread4 ∈ {0}
[eva:alarm] tests/value/align_char_array.c:21: Warning:
- pointer downcast. assert (unsigned int)&S.a ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&S.a) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:21: Warning:
- pointer downcast. assert (unsigned int)&S.c ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&S.c) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:23: Warning:
- pointer downcast. assert (unsigned int)&t[2][2] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t[2][2]) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:23: Warning:
- pointer downcast. assert (unsigned int)&t[0][0] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t[0][0]) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:25: Warning:
- pointer downcast. assert (unsigned int)(char (*)[10])t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:25: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 3;
[eva:alarm] tests/value/align_char_array.c:25: Warning:
signed overflow. assert (int)((char (*)[10])t) + 3 ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:26: Warning:
- pointer downcast. assert (unsigned int)(char (*)[10])t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:26: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 3;
[eva:alarm] tests/value/align_char_array.c:26: Warning:
signed overflow. assert (int)((char (*)[10])t) + 3 ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:27: Warning:
- pointer downcast. assert (unsigned int)(char (*)[10])t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:27: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 2;
[eva:alarm] tests/value/align_char_array.c:27: Warning:
signed overflow. assert (int)((char (*)[10])t) + 2 ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:28: Warning:
- pointer downcast. assert (unsigned int)(char (*)[10])t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:28: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 2;
[eva:alarm] tests/value/align_char_array.c:28: Warning:
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index b8a89b48a6c..a09c922b6d3 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -23,7 +23,7 @@
pointer subtraction. assert \base_addr(p2) ≡ \base_addr(p2);
[eva] tests/value/arith_pointer.c:52: Frama_C_show_each: {0}
[eva:alarm] tests/value/arith_pointer.c:54: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/value/arith_pointer.c:54:
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {tests/value/arith_pointer.c:54}
@@ -151,7 +151,7 @@
{{ garbled mix of &{x; y}
(origin: Arithmetic {tests/value/arith_pointer.c:51}) }}
[eva:alarm] tests/value/arith_pointer.c:54: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/arith_pointer.c:56: Warning:
signed overflow. assert -2147483648 ≤ p2 - p1;
[eva:alarm] tests/value/arith_pointer.c:56: Warning:
diff --git a/tests/value/oracle/array_ptr.res.oracle b/tests/value/oracle/array_ptr.res.oracle
index 2d14be30289..8599de4e4af 100644
--- a/tests/value/oracle/array_ptr.res.oracle
+++ b/tests/value/oracle/array_ptr.res.oracle
@@ -7,7 +7,7 @@
l[0] ∈ {1}
[1..19] ∈ {0}
[eva:alarm] tests/value/array_ptr.i:14: Warning:
- pointer downcast. assert (unsigned int)&l ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&l) ≤ 2147483647;
[eva] computing for function f <- main.
Called from tests/value/array_ptr.i:15.
[eva] Recording results for f
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index 40501b7b144..4cfd1aeca7a 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -45,7 +45,7 @@
Called from tests/value/assigns.i:49.
[eva] Done for function f
[eva:alarm] tests/value/assigns.i:51: Warning:
- pointer downcast. assert (unsigned int)&T ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&T) ≤ 2147483647;
[eva:alarm] tests/value/assigns.i:51: Warning:
signed overflow. assert -2147483648 ≤ 2 * (int)(&T);
[eva:alarm] tests/value/assigns.i:51: Warning:
@@ -55,7 +55,7 @@
[eva] using specification for function g
[eva] Done for function g
[eva:alarm] tests/value/assigns.i:52: Warning:
- pointer downcast. assert (unsigned int)&t3 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t3) ≤ 2147483647;
[eva:alarm] tests/value/assigns.i:52: Warning:
signed overflow. assert -2147483648 ≤ 2 * (int)(&t3);
[eva:alarm] tests/value/assigns.i:52: Warning:
@@ -935,11 +935,11 @@ void main1(void)
i ++;
}
}
- /*@ assert Eva: pointer_downcast: (unsigned int)&T ≤ 2147483647; */
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&T) ≤ 2147483647; */
/*@ assert Eva: signed_overflow: -2147483648 ≤ 2 * (int)(&T); */
/*@ assert Eva: signed_overflow: 2 * (int)(&T) ≤ 2147483647; */
g(2 * (int)(& T));
- /*@ assert Eva: pointer_downcast: (unsigned int)&t3 ≤ 2147483647; */
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&t3) ≤ 2147483647; */
/*@ assert Eva: signed_overflow: -2147483648 ≤ 2 * (int)(&t3); */
/*@ assert Eva: signed_overflow: 2 * (int)(&t3) ≤ 2147483647; */
h((int *)(2 * (int)(& t3)));
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 54cf0bfdba6..0ae5f039460 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -29,12 +29,12 @@
[eva] tests/value/bitfield.i:113: Frama_C_show_each: {1}
[eva] tests/value/bitfield.i:117: Frama_C_show_each: {3}
[eva:alarm] tests/value/bitfield.i:123: Warning:
- pointer downcast. assert (unsigned int)&v ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&v) ≤ 2147483647;
[eva] tests/value/bitfield.i:123:
Assigning imprecise value to v.c.
The imprecision originates from Arithmetic {tests/value/bitfield.i:123}
[eva:alarm] tests/value/bitfield.i:124: Warning:
- pointer downcast. assert (unsigned int)&v + 1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&v + 1) ≤ 2147483647;
[eva:alarm] tests/value/bitfield.i:125: Warning:
signed overflow. assert -2147483648 ≤ (int)v.d + 1;
[eva:alarm] tests/value/bitfield.i:125: Warning:
@@ -82,7 +82,7 @@
[eva:alarm] tests/value/bitfield.i:129: Warning:
signed overflow. assert foo + foo ≤ 2147483647;
[eva:alarm] tests/value/bitfield.i:130: Warning:
- pointer downcast. assert (unsigned int)&v + 1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&v + 1) ≤ 2147483647;
[eva] tests/value/bitfield.i:130:
Assigning imprecise value to h.c.
The imprecision originates from Arithmetic {tests/value/bitfield.i:130}
@@ -557,9 +557,9 @@ void main_old(void)
else Frama_C_show_each(3);
VV = (unsigned int)h.a;
h.a = (unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))))VV;
- /*@ assert Eva: pointer_downcast: (unsigned int)&v ≤ 2147483647; */
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&v) ≤ 2147483647; */
v.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))((int)(& v));
- /*@ assert Eva: pointer_downcast: (unsigned int)&v + 1 ≤ 2147483647; */
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&v + 1) ≤ 2147483647; */
v.d = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(32))))((int)(& v + 1));
/*@ assert Eva: signed_overflow: -2147483648 ≤ (int)v.d + 1; */
/*@ assert Eva: signed_overflow: (int)v.d + 1 ≤ 2147483647; */
@@ -570,7 +570,7 @@ void main_old(void)
/*@ assert Eva: signed_overflow: -2147483648 ≤ foo + foo; */
/*@ assert Eva: signed_overflow: foo + foo ≤ 2147483647; */
h.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))(((foo + foo) + (int)h.a) + (int)h.b);
- /*@ assert Eva: pointer_downcast: (unsigned int)&v + 1 ≤ 2147483647; */
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&v + 1) ≤ 2147483647; */
h.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))((int)(& v + 1));
k8.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))8;
tmp = return_8();
diff --git a/tests/value/oracle/bitwise_pointer.res.oracle b/tests/value/oracle/bitwise_pointer.res.oracle
index a0538f60c8e..878fa04174a 100644
--- a/tests/value/oracle/bitwise_pointer.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.res.oracle
@@ -30,14 +30,14 @@
p1 ∈ {0}
x1 ∈ {0}
[eva:alarm] tests/value/bitwise_pointer.i:18: Warning:
- pointer downcast. assert (unsigned int)&t[7] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t[7]) ≤ 2147483647;
[eva] tests/value/bitwise_pointer.i:18:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:18}
[eva:alarm] tests/value/bitwise_pointer.i:19: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] tests/value/bitwise_pointer.i:22: Warning:
- pointer downcast. assert (unsigned int)&t1[mask] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t1[mask]) ≤ 2147483647;
[eva] tests/value/bitwise_pointer.i:22:
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:22}
diff --git a/tests/value/oracle/cmp_ptr.0.res.oracle b/tests/value/oracle/cmp_ptr.0.res.oracle
index 08d4b95eafc..47a1035cc56 100644
--- a/tests/value/oracle/cmp_ptr.0.res.oracle
+++ b/tests/value/oracle/cmp_ptr.0.res.oracle
@@ -46,7 +46,7 @@
[eva:alarm] tests/value/cmp_ptr.i:22: Warning:
pointer comparison. assert \pointer_comparable((void *)0, (void *)(&y + 2));
[eva:alarm] tests/value/cmp_ptr.i:23: Warning:
- pointer downcast. assert (unsigned int)&y + 2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y + 2) ≤ 2147483647;
[eva:pointer-comparison] tests/value/cmp_ptr.i:24:
invalid pointer comparison: invalid pointer(s)
[eva:alarm] tests/value/cmp_ptr.i:24: Warning:
diff --git a/tests/value/oracle/cmp_ptr.1.res.oracle b/tests/value/oracle/cmp_ptr.1.res.oracle
index ea6793941d4..182c5433339 100644
--- a/tests/value/oracle/cmp_ptr.1.res.oracle
+++ b/tests/value/oracle/cmp_ptr.1.res.oracle
@@ -60,7 +60,7 @@
[eva:alarm] tests/value/cmp_ptr.i:22: Warning:
pointer comparison. assert \pointer_comparable((void *)0, (void *)(&y + 2));
[eva:alarm] tests/value/cmp_ptr.i:23: Warning:
- pointer downcast. assert (unsigned int)&y + 2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y + 2) ≤ 2147483647;
[eva:pointer-comparison] tests/value/cmp_ptr.i:24:
invalid pointer comparison: invalid pointer(s)
[eva:alarm] tests/value/cmp_ptr.i:24: Warning:
diff --git a/tests/value/oracle/context_free.res.oracle b/tests/value/oracle/context_free.res.oracle
index f8869049442..f1220992e0b 100644
--- a/tests/value/oracle/context_free.res.oracle
+++ b/tests/value/oracle/context_free.res.oracle
@@ -102,7 +102,7 @@
[eva:alarm] tests/value/context_free.i:61: Warning:
out of bounds write. assert \valid(pvoid);
[eva:alarm] tests/value/context_free.i:61: Warning:
- pointer downcast. assert (unsigned int)&pvoid ≤ 127;
+ pointer downcast. assert (unsigned int)(&pvoid) ≤ 127;
[eva:alarm] tests/value/context_free.i:62: Warning:
pointer to function with incompatible type. assert \valid_function(g);
[eva] Recording results for f
diff --git a/tests/value/oracle/conversion.res.oracle b/tests/value/oracle/conversion.res.oracle
index 26374aad66f..954fdab07b4 100644
--- a/tests/value/oracle/conversion.res.oracle
+++ b/tests/value/oracle/conversion.res.oracle
@@ -58,7 +58,7 @@
l ∈ UNINITIALIZED
==END OF DUMP==
[eva:alarm] tests/value/conversion.i:38: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/value/conversion.i:40:
Frama_C_dump_each:
# Cvalue domain:
@@ -164,7 +164,7 @@
l ∈ UNINITIALIZED
==END OF DUMP==
[eva:alarm] tests/value/conversion.i:38: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/conversion.i:39: Warning:
non-finite float value. assert \is_finite(*((float *)(&x)));
[eva] tests/value/conversion.i:39:
diff --git a/tests/value/oracle/deps_addr.res.oracle b/tests/value/oracle/deps_addr.res.oracle
index 0c2afa4364c..59f4ac5f0f9 100644
--- a/tests/value/oracle/deps_addr.res.oracle
+++ b/tests/value/oracle/deps_addr.res.oracle
@@ -7,7 +7,7 @@
a ∈ {0}
tt[0..4][0..4] ∈ {0}
[eva:alarm] tests/value/deps_addr.i:6: Warning:
- pointer downcast. assert (unsigned int)&a ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&a) ≤ 2147483647;
[eva:alarm] tests/value/deps_addr.i:6: Warning:
out of bounds read. assert \valid_read(t + (int)(&a));
[eva] Recording results for main
diff --git a/tests/value/oracle/deps_mixed.res.oracle b/tests/value/oracle/deps_mixed.res.oracle
index e7af15348e5..6631dfe4e46 100644
--- a/tests/value/oracle/deps_mixed.res.oracle
+++ b/tests/value/oracle/deps_mixed.res.oracle
@@ -31,7 +31,7 @@
[eva:alarm] tests/value/deps_mixed.i:24: Warning:
pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] tests/value/deps_mixed.i:24: Warning:
- pointer downcast. assert (unsigned int)p + (int)q ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(p + (int)q) ≤ 2147483647;
[eva] tests/value/deps_mixed.i:24:
Assigning imprecise value to __retres.
The imprecision originates from Arithmetic {tests/value/deps_mixed.i:24}
diff --git a/tests/value/oracle/div.0.res.oracle b/tests/value/oracle/div.0.res.oracle
index 4f8b786e02d..2f95483430e 100644
--- a/tests/value/oracle/div.0.res.oracle
+++ b/tests/value/oracle/div.0.res.oracle
@@ -36,7 +36,7 @@
[eva:alarm] tests/value/div.i:32: Warning: division by zero. assert Z2 ≢ 0;
[eva:alarm] tests/value/div.i:33: Warning: division by zero. assert Z2 ≢ 0;
[eva:alarm] tests/value/div.i:33: Warning:
- pointer downcast. assert (unsigned int)&Z2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:33: Warning:
signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
[eva:alarm] tests/value/div.i:33: Warning:
@@ -45,7 +45,7 @@
Assigning imprecise value to b.
The imprecision originates from Arithmetic {tests/value/div.i:33}
[eva:alarm] tests/value/div.i:34: Warning:
- pointer downcast. assert (unsigned int)&X + 2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:34: Warning:
division by zero. assert (int)(&X + 2) ≢ 0;
[eva:alarm] tests/value/div.i:34: Warning:
@@ -56,7 +56,7 @@
Assigning imprecise value to d2.
The imprecision originates from Arithmetic {tests/value/div.i:34}
[eva:alarm] tests/value/div.i:35: Warning:
- pointer downcast. assert (unsigned int)&X + 1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
[eva:alarm] tests/value/div.i:35: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
[eva:alarm] tests/value/div.i:35: Warning:
@@ -65,7 +65,7 @@
Assigning imprecise value to d1.
The imprecision originates from Arithmetic {tests/value/div.i:35}
[eva:alarm] tests/value/div.i:36: Warning:
- pointer downcast. assert (unsigned int)&X ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:36: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
[eva:alarm] tests/value/div.i:36: Warning:
@@ -74,7 +74,7 @@
Assigning imprecise value to d0.
The imprecision originates from Arithmetic {tests/value/div.i:36}
[eva:alarm] tests/value/div.i:37: Warning:
- pointer downcast. assert (unsigned int)&X ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:37: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&X));
[eva:alarm] tests/value/div.i:37: Warning:
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
index d052fa034e4..bb2cbef1753 100644
--- a/tests/value/oracle/div.1.res.oracle
+++ b/tests/value/oracle/div.1.res.oracle
@@ -58,7 +58,7 @@
assertion 'rte,signed_overflow' got status unknown.
[eva:alarm] tests/value/div.i:33: Warning: division by zero. assert Z2 ≢ 0;
[eva:alarm] tests/value/div.i:33: Warning:
- pointer downcast. assert (unsigned int)&Z2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:33: Warning:
signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
[eva:alarm] tests/value/div.i:33: Warning:
@@ -71,7 +71,7 @@
[eva:alarm] tests/value/div.i:34: Warning:
assertion 'rte,division_by_zero' got status unknown.
[eva:alarm] tests/value/div.i:34: Warning:
- pointer downcast. assert (unsigned int)&X + 2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:34: Warning:
division by zero. assert (int)(&X + 2) ≢ 0;
[eva:alarm] tests/value/div.i:34: Warning:
@@ -85,7 +85,7 @@
assertion 'rte,pointer_downcast' got status unknown.
[eva] tests/value/div.i:35: assertion 'rte,division_by_zero' got status valid.
[eva:alarm] tests/value/div.i:35: Warning:
- pointer downcast. assert (unsigned int)&X + 1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
[eva:alarm] tests/value/div.i:35: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
[eva:alarm] tests/value/div.i:35: Warning:
@@ -97,7 +97,7 @@
assertion 'rte,pointer_downcast' got status unknown.
[eva] tests/value/div.i:36: assertion 'rte,division_by_zero' got status valid.
[eva:alarm] tests/value/div.i:36: Warning:
- pointer downcast. assert (unsigned int)&X ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:36: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
[eva:alarm] tests/value/div.i:36: Warning:
@@ -110,7 +110,7 @@
[eva:alarm] tests/value/div.i:37: Warning:
assertion 'rte,signed_overflow' got status unknown.
[eva:alarm] tests/value/div.i:37: Warning:
- pointer downcast. assert (unsigned int)&X ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:37: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&X));
[eva:alarm] tests/value/div.i:37: Warning:
diff --git a/tests/value/oracle/eval_separated.res.oracle b/tests/value/oracle/eval_separated.res.oracle
index 60f0db91f1e..ba49fd5aff7 100644
--- a/tests/value/oracle/eval_separated.res.oracle
+++ b/tests/value/oracle/eval_separated.res.oracle
@@ -12,7 +12,7 @@
[eva] tests/value/eval_separated.c:8: assertion got status valid.
[eva] tests/value/eval_separated.c:9: assertion got status valid.
[eva:alarm] tests/value/eval_separated.c:11: Warning:
- pointer downcast. assert (unsigned int)&q ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&q) ≤ 2147483647;
[eva:alarm] tests/value/eval_separated.c:11: Warning:
signed overflow. assert -2147483648 ≤ (int)(&q) + (int)(&q);
[eva:alarm] tests/value/eval_separated.c:11: Warning:
@@ -21,7 +21,7 @@
Assigning imprecise value to q.
The imprecision originates from Arithmetic {tests/value/eval_separated.c:11}
[eva:alarm] tests/value/eval_separated.c:12: Warning:
- pointer downcast. assert (unsigned int)&r ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&r) ≤ 2147483647;
[eva:alarm] tests/value/eval_separated.c:12: Warning:
signed overflow. assert -2147483648 ≤ (int)(&r) + (int)(&r);
[eva:alarm] tests/value/eval_separated.c:12: Warning:
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index f06f8231e21..90af155562b 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -2,9 +2,9 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/value/from_call.i:70: Warning:
- pointer downcast. assert (unsigned int)&AA ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
[eva:alarm] tests/value/from_call.i:71: Warning:
- pointer downcast. assert (unsigned int)&AA ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index a11fbdf9fa2..eb4493ddfd3 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -2,9 +2,9 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/value/from_call.i:70: Warning:
- pointer downcast. assert (unsigned int)&AA ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
[eva:alarm] tests/value/from_call.i:71: Warning:
- pointer downcast. assert (unsigned int)&AA ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
diff --git a/tests/value/oracle/from_ptr.0.res.oracle b/tests/value/oracle/from_ptr.0.res.oracle
index f58c5770d44..7261a1cb811 100644
--- a/tests/value/oracle/from_ptr.0.res.oracle
+++ b/tests/value/oracle/from_ptr.0.res.oracle
@@ -16,9 +16,9 @@
p[0..9][0..9][0..9] ∈ {0}
q ∈ {0}
[eva:alarm] tests/value/from_ptr.i:12: Warning:
- pointer downcast. assert (unsigned int)&p[11] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p[11]) ≤ 2147483647;
[eva:alarm] tests/value/from_ptr.i:13: Warning:
- pointer downcast. assert (unsigned int)&p[10] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p[10]) ≤ 2147483647;
[eva:alarm] tests/value/from_ptr.i:17: Warning:
out of bounds write. assert \valid((int *)i);
[kernel] tests/value/from_ptr.i:17: Warning:
diff --git a/tests/value/oracle/from_ptr.1.res.oracle b/tests/value/oracle/from_ptr.1.res.oracle
index d1824131817..1cde862a4b6 100644
--- a/tests/value/oracle/from_ptr.1.res.oracle
+++ b/tests/value/oracle/from_ptr.1.res.oracle
@@ -16,9 +16,9 @@
p[0..9][0..9][0..9] ∈ {0}
q ∈ {0}
[eva:alarm] tests/value/from_ptr.i:24: Warning:
- pointer downcast. assert (unsigned int)&p[1] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&p[1]) ≤ 2147483647;
[eva:alarm] tests/value/from_ptr.i:25: Warning:
- pointer downcast. assert (unsigned int)(int (*)[10][10])p ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int (*)[10][10])p) ≤ 2147483647;
[eva] Recording results for main1
[eva] done for function main1
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/fun_ptr.1.res.oracle b/tests/value/oracle/fun_ptr.1.res.oracle
index f99360712b5..3e7b008426e 100644
--- a/tests/value/oracle/fun_ptr.1.res.oracle
+++ b/tests/value/oracle/fun_ptr.1.res.oracle
@@ -9,9 +9,9 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/value/fun_ptr.i:21: Warning:
- pointer downcast. assert (unsigned __int64)&f ≤ 9223372036854775807;
+ pointer downcast. assert (unsigned __int64)(&f) ≤ 9223372036854775807;
[eva:alarm] tests/value/fun_ptr.i:21: Warning:
- pointer downcast. assert (unsigned __int64)&g ≤ 9223372036854775807;
+ pointer downcast. assert (unsigned __int64)(&g) ≤ 9223372036854775807;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
t[0] ∈ {{ (__int64)&f }}
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 611d2093add..338f79ddc5e 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -22,7 +22,7 @@
[eva] computing for function main2 <- main.
Called from tests/value/imprecise_invalid_write.i:25.
[eva:alarm] tests/value/imprecise_invalid_write.i:9: Warning:
- pointer downcast. assert (unsigned int)&main1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&main1) ≤ 2147483647;
[eva] tests/value/imprecise_invalid_write.i:9:
Assigning imprecise value to p.
The imprecision originates from Arithmetic
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index 8ca94ab19cf..b57ddb23b52 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -67,7 +67,7 @@
[eva] computing for function g2 <- main.
Called from tests/value/initialized.c:194.
[eva:alarm] tests/value/initialized.c:50: Warning:
- pointer downcast. assert (unsigned int)&b4 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&b4) ≤ 2147483647;
[eva:alarm] tests/value/initialized.c:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&b4) + (int)(&b4);
[eva:alarm] tests/value/initialized.c:50: Warning:
diff --git a/tests/value/oracle/join_misaligned.res.oracle b/tests/value/oracle/join_misaligned.res.oracle
index 2194180b285..111aa1c6f07 100644
--- a/tests/value/oracle/join_misaligned.res.oracle
+++ b/tests/value/oracle/join_misaligned.res.oracle
@@ -15,9 +15,9 @@
a ∈ {0}
va ∈ [--..--]
[eva:alarm] tests/value/join_misaligned.i:23: Warning:
- pointer downcast. assert (unsigned int)&t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&t) ≤ 2147483647;
[eva:alarm] tests/value/join_misaligned.i:37: Warning:
- pointer downcast. assert (unsigned int)&u ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&u) ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
[eva:garbled-mix] Warning:
diff --git a/tests/value/oracle/label.res.oracle b/tests/value/oracle/label.res.oracle
index 3c3c61be0c2..a87f0773b6e 100644
--- a/tests/value/oracle/label.res.oracle
+++ b/tests/value/oracle/label.res.oracle
@@ -11,7 +11,7 @@
p ∈ {0}
q ∈ {0}
[eva:alarm] tests/value/label.i:14: Warning:
- pointer downcast. assert (unsigned int)&d + 1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&d + 1) ≤ 2147483647;
[eva] tests/value/label.i:18:
Assigning imprecise value to *((char *)(& p) + i)
(pointing to p with offsets {0}).
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 41082946d0a..96ab8ffd9b4 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -7,7 +7,7 @@
H ∈ {0}
I ∈ {0}
[eva:alarm] tests/value/leaf2.i:6: Warning:
- pointer downcast. assert (unsigned int)&I ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&I) ≤ 2147483647;
[eva] computing for function f <- main.
Called from tests/value/leaf2.i:6.
[kernel:annot:missing-spec] tests/value/leaf2.i:6: Warning:
diff --git a/tests/value/oracle/mini_pointrer.res.oracle b/tests/value/oracle/mini_pointrer.res.oracle
index 65092ae89c4..0cc72335a3a 100644
--- a/tests/value/oracle/mini_pointrer.res.oracle
+++ b/tests/value/oracle/mini_pointrer.res.oracle
@@ -12,7 +12,7 @@
[eva:alarm] tests/value/mini_pointrer.i:6: Warning:
accessing out of bounds index. assert c1 < 2;
[eva:alarm] tests/value/mini_pointrer.i:6: Warning:
- pointer downcast. assert (unsigned int)&T[c1] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&T[c1]) ≤ 2147483647;
[eva:alarm] tests/value/mini_pointrer.i:8: Warning:
out of bounds read. assert \valid_read(ppp);
[eva:alarm] tests/value/mini_pointrer.i:8: Warning:
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index b5be0d8bcaa..433ce49eaa0 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -64,7 +64,7 @@
[eva:alarm] tests/value/nonlin.c:21: Warning:
out of bounds read. assert \valid_read((p + i) - i);
[eva:alarm] tests/value/nonlin.c:23: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/nonlin.c:24: Warning:
out of bounds read. assert \valid_read((p + i) - i);
[eva] Recording results for subdivide_pointer
diff --git a/tests/value/oracle/not_ct_array_arg.res.oracle b/tests/value/oracle/not_ct_array_arg.res.oracle
index 776fa403f15..8be78fd49c0 100644
--- a/tests/value/oracle/not_ct_array_arg.res.oracle
+++ b/tests/value/oracle/not_ct_array_arg.res.oracle
@@ -25,7 +25,7 @@
[eva:alarm] tests/value/not_ct_array_arg.i:12: Warning:
out of bounds write. assert \valid(&(*(tb + 9))[100]);
[eva:alarm] tests/value/not_ct_array_arg.i:12: Warning:
- pointer downcast. assert (unsigned int)&tb ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&tb) ≤ 2147483647;
[eva] tests/value/not_ct_array_arg.i:13:
Frama_C_dump_each:
# Cvalue domain:
diff --git a/tests/value/oracle/offset_top.res.oracle b/tests/value/oracle/offset_top.res.oracle
index 6c6287b4bff..8dbc430d5ee 100644
--- a/tests/value/oracle/offset_top.res.oracle
+++ b/tests/value/oracle/offset_top.res.oracle
@@ -7,7 +7,7 @@
T ∈ {0}
TAB[0..9] ∈ {0}
[eva:alarm] tests/value/offset_top.i:10: Warning:
- pointer downcast. assert (unsigned int)&TAB[*T] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&TAB[*T]) ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index 2a076ba31dc..572459f644a 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -28,7 +28,7 @@
[eva] tests/value/offsetmap.i:19: starting to merge loop iterations
[eva] tests/value/offsetmap.i:29: starting to merge loop iterations
[eva:alarm] tests/value/offsetmap.i:51: Warning:
- pointer downcast. assert (unsigned int)&x2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x2) ≤ 2147483647;
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index 115819f9674..d4ac4533187 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -28,7 +28,7 @@
[eva] tests/value/offsetmap.i:19: starting to merge loop iterations
[eva] tests/value/offsetmap.i:29: starting to merge loop iterations
[eva:alarm] tests/value/offsetmap.i:51: Warning:
- pointer downcast. assert (unsigned int)&x2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x2) ≤ 2147483647;
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index cd433bd1e2f..2bdd5becc39 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -55,7 +55,7 @@
[eva] computing for function origin_arithmetic_1 <- main.
Called from tests/value/origin.i:94.
[eva:alarm] tests/value/origin.i:14: Warning:
- pointer downcast. assert (unsigned int)(int *)ta1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int *)ta1) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:14: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)ta1));
[eva:alarm] tests/value/origin.i:14: Warning:
@@ -70,7 +70,7 @@
[eva] computing for function origin_arithmetic_2 <- main.
Called from tests/value/origin.i:95.
[eva:alarm] tests/value/origin.i:19: Warning:
- pointer downcast. assert (unsigned int)(int *)ta2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int *)ta2) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:19: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)ta2));
[eva:alarm] tests/value/origin.i:19: Warning:
@@ -82,7 +82,7 @@
Assigning imprecise value to qa2.
The imprecision originates from Arithmetic {tests/value/origin.i:19}
[eva:alarm] tests/value/origin.i:20: Warning:
- pointer downcast. assert (unsigned int)(int *)tta2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int *)tta2) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:20: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)tta2));
[eva:alarm] tests/value/origin.i:20: Warning:
@@ -93,13 +93,13 @@
[eva:alarm] tests/value/origin.i:21: Warning:
out of bounds write. assert \valid(qa2);
[eva:alarm] tests/value/origin.i:21: Warning:
- pointer downcast. assert (unsigned int)&aa2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&aa2) ≤ 2147483647;
[eva] Recording results for origin_arithmetic_2
[eva] Done for function origin_arithmetic_2
[eva] computing for function origin_arithmetic_3 <- main.
Called from tests/value/origin.i:96.
[eva:alarm] tests/value/origin.i:25: Warning:
- pointer downcast. assert (unsigned int)(int *)ta3 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((int *)ta3) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:25: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)ta3));
[eva:alarm] tests/value/origin.i:25: Warning:
@@ -159,7 +159,7 @@
[eva:alarm] tests/value/origin.i:56: Warning:
out of bounds write. assert \valid(qm2);
[eva:alarm] tests/value/origin.i:56: Warning:
- pointer downcast. assert (unsigned int)&a ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&a) ≤ 2147483647;
[eva] Recording results for origin_misalign_2
[eva] Done for function origin_misalign_2
[eva] computing for function origin_uninitialized_1 <- main.
@@ -179,11 +179,11 @@
[eva] computing for function local_escape_1 <- main.
Called from tests/value/origin.i:108.
[eva:alarm] tests/value/origin.i:83: Warning:
- pointer downcast. assert (unsigned int)&arg ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&arg) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:84: Warning:
- pointer downcast. assert (unsigned int)&local1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&local1) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:85: Warning:
- pointer downcast. assert (unsigned int)&arg ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&arg) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:85: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&arg));
[eva:alarm] tests/value/origin.i:85: Warning:
@@ -192,9 +192,9 @@
Assigning imprecise value to esc3.
The imprecision originates from Arithmetic {tests/value/origin.i:85}
[eva:alarm] tests/value/origin.i:87: Warning:
- pointer downcast. assert (unsigned int)&local1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&local1) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:88: Warning:
- pointer downcast. assert (unsigned int)&esc1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&esc1) ≤ 2147483647;
[eva] Recording results for local_escape_1
[eva] Done for function local_escape_1
[eva:locals-escaping] tests/value/origin.i:108: Warning:
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index 6e3283d9304..0b3195a5397 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -65,7 +65,7 @@
Assigning imprecise value to r.t[0].
The imprecision originates from Merge {tests/value/origin.i:129}
[eva:alarm] tests/value/origin.i:130: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:130: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&x));
[eva:alarm] tests/value/origin.i:130: Warning:
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index 156c9148c10..2af9a46bd2a 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -79,21 +79,21 @@
Ht ∈ {1}
==END OF DUMP==
[eva:alarm] tests/value/period.c:51: Warning:
- pointer downcast. assert (unsigned int)&g ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
[eva] tests/value/period.c:51:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/period.c:51}
[eva:alarm] tests/value/period.c:52: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] tests/value/period.c:53: Warning:
- pointer downcast. assert (unsigned int)&g ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
[eva] tests/value/period.c:53:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/period.c:53}
[eva:alarm] tests/value/period.c:54: Warning:
out of bounds read. assert \valid_read(p);
[eva:alarm] tests/value/period.c:55: Warning:
- pointer downcast. assert (unsigned int)&vg ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&vg) ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
[scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle/pointer_comparison.0.res.oracle b/tests/value/oracle/pointer_comparison.0.res.oracle
index fcd954b8df5..6ac5900dc2e 100644
--- a/tests/value/oracle/pointer_comparison.0.res.oracle
+++ b/tests/value/oracle/pointer_comparison.0.res.oracle
@@ -21,7 +21,7 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:pointer-comparison] tests/value/pointer_comparison.c:18:
@@ -61,7 +61,7 @@
assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
- assert Eva: pointer_downcast: (unsigned int)&y ≤ 2147483647;
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
tried with Eva.
--------------------------------------------------------------------------------
@@ -96,7 +96,7 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:alarm] tests/value/pointer_comparison.c:18: Warning:
@@ -152,7 +152,7 @@
assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
- assert Eva: pointer_downcast: (unsigned int)&y ≤ 2147483647;
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
assert
@@ -192,7 +192,7 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)(&y));
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
@@ -250,7 +250,7 @@
assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
- assert Eva: pointer_downcast: (unsigned int)&y ≤ 2147483647;
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
assert
diff --git a/tests/value/oracle/pointer_comparison.1.res.oracle b/tests/value/oracle/pointer_comparison.1.res.oracle
index af00458ed51..cd63714dccc 100644
--- a/tests/value/oracle/pointer_comparison.1.res.oracle
+++ b/tests/value/oracle/pointer_comparison.1.res.oracle
@@ -36,7 +36,7 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:pointer-comparison] tests/value/pointer_comparison.c:18:
@@ -81,7 +81,7 @@
assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
- assert Eva: pointer_downcast: (unsigned int)&y ≤ 2147483647;
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
tried with Eva.
--------------------------------------------------------------------------------
@@ -119,7 +119,7 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:alarm] tests/value/pointer_comparison.c:18: Warning:
@@ -176,7 +176,7 @@
assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
- assert Eva: pointer_downcast: (unsigned int)&y ≤ 2147483647;
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
assert
@@ -219,7 +219,7 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)(&y));
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
@@ -278,7 +278,7 @@
assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
- assert Eva: pointer_downcast: (unsigned int)&y ≤ 2147483647;
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
assert
diff --git a/tests/value/oracle/pointer_int_cast.res.oracle b/tests/value/oracle/pointer_int_cast.res.oracle
index 75c12b7d3ab..cad14cc1bd0 100644
--- a/tests/value/oracle/pointer_int_cast.res.oracle
+++ b/tests/value/oracle/pointer_int_cast.res.oracle
@@ -9,7 +9,7 @@
x ∈ {0}
y ∈ {0}
[eva:alarm] tests/value/pointer_int_cast.i:9: Warning:
- pointer downcast. assert (unsigned int)&y ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] Recording results for g
[eva] done for function g
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index 4e0d35dc30a..b2838250a6d 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -45,7 +45,7 @@
Assigning imprecise value to r.
The imprecision originates from Arithmetic {tests/value/shift.i:52}
[eva:alarm] tests/value/shift.i:53: Warning:
- pointer downcast. assert (unsigned int)(char *)t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((char *)t) ≤ 2147483647;
[eva:alarm] tests/value/shift.i:53: Warning:
invalid LHS operand for left shift. assert 0 ≤ (long)((char *)t);
[eva:alarm] tests/value/shift.i:53: Warning:
diff --git a/tests/value/oracle/shift.1.res.oracle b/tests/value/oracle/shift.1.res.oracle
index 46103bb62cc..9862244f180 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -39,7 +39,7 @@
Assigning imprecise value to r.
The imprecision originates from Arithmetic {tests/value/shift.i:52}
[eva:alarm] tests/value/shift.i:53: Warning:
- pointer downcast. assert (unsigned int)(char *)t ≤ 2147483647;
+ pointer downcast. assert (unsigned int)((char *)t) ≤ 2147483647;
[eva:alarm] tests/value/shift.i:53: Warning:
signed overflow. assert -2147483648 ≤ (long)((char *)t) << 8;
[eva:alarm] tests/value/shift.i:53: Warning:
diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index 23b0674bd22..adc483ff665 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -19,7 +19,7 @@
[eva] computing for function main2 <- main.
Called from tests/value/sizeof.i:41.
[eva:alarm] tests/value/sizeof.i:32: Warning:
- pointer downcast. assert (unsigned int)&s1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&s1) ≤ 2147483647;
[eva] tests/value/sizeof.i:32:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/sizeof.i:32}
@@ -126,7 +126,7 @@ struct s s1;
int volatile i;
void main2(void)
{
- /*@ assert Eva: pointer_downcast: (unsigned int)&s1 ≤ 2147483647; */
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&s1) ≤ 2147483647; */
struct s *p = (& s1 + (int)(& s1)) - (int)(& s1);
/*@ assert
Eva: index_bound: (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
diff --git a/tests/value/oracle/struct3.res.oracle b/tests/value/oracle/struct3.res.oracle
index 44c891f6674..4cbcaa45fec 100644
--- a/tests/value/oracle/struct3.res.oracle
+++ b/tests/value/oracle/struct3.res.oracle
@@ -22,7 +22,7 @@
[eva:alarm] tests/value/struct3.i:46: Warning:
pointer downcast. assert (unsigned int)s2.c ≤ 2147483647;
[eva:alarm] tests/value/struct3.i:46: Warning:
- pointer downcast. assert (unsigned int)s2.c + (int)s2.c ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(s2.c + (int)s2.c) ≤ 2147483647;
[eva] tests/value/struct3.i:46:
Assigning imprecise value to s2.a.
The imprecision originates from Arithmetic {tests/value/struct3.i:46}
diff --git a/tests/value/oracle/struct_array.res.oracle b/tests/value/oracle/struct_array.res.oracle
index c0df48148db..05ac2f16880 100644
--- a/tests/value/oracle/struct_array.res.oracle
+++ b/tests/value/oracle/struct_array.res.oracle
@@ -2,11 +2,11 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/value/struct_array.i:15: Warning:
- pointer downcast. assert (unsigned int)&z1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&z1) ≤ 2147483647;
[eva:alarm] tests/value/struct_array.i:15: Warning:
- pointer downcast. assert (unsigned int)&z2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&z2) ≤ 2147483647;
[eva:alarm] tests/value/struct_array.i:15: Warning:
- pointer downcast. assert (unsigned int)&z4 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&z4) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
@@ -241,11 +241,11 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/value/struct_array.i:15: Warning:
- pointer downcast. assert (unsigned int)&z1 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&z1) ≤ 2147483647;
[eva:alarm] tests/value/struct_array.i:15: Warning:
- pointer downcast. assert (unsigned int)&z2 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&z2) ≤ 2147483647;
[eva:alarm] tests/value/struct_array.i:15: Warning:
- pointer downcast. assert (unsigned int)&z4 ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&z4) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
diff --git a/tests/value/oracle/struct_incl.res.oracle b/tests/value/oracle/struct_incl.res.oracle
index e8e83a5e446..3eb4f598ee5 100644
--- a/tests/value/oracle/struct_incl.res.oracle
+++ b/tests/value/oracle/struct_incl.res.oracle
@@ -23,11 +23,11 @@
t ∈ {0}
v ∈ [--..--]
[eva:alarm] tests/value/struct_incl.i:28: Warning:
- pointer downcast. assert (unsigned int)&s1.d[9] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&s1.d[9]) ≤ 2147483647;
[eva:alarm] tests/value/struct_incl.i:29: Warning:
- pointer downcast. assert (unsigned int)&s1.d[10] ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&s1.d[10]) ≤ 2147483647;
[eva:alarm] tests/value/struct_incl.i:30: Warning:
- pointer downcast. assert (unsigned int)&s1.b ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&s1.b) ≤ 2147483647;
[eva:alarm] tests/value/struct_incl.i:48: Warning:
accessing out of bounds index. assert 10 < 10;
[kernel] tests/value/struct_incl.i:48: Warning:
diff --git a/tests/value/oracle/symbolic_locs.res.oracle b/tests/value/oracle/symbolic_locs.res.oracle
index 744e5e6a72f..eb325482dff 100644
--- a/tests/value/oracle/symbolic_locs.res.oracle
+++ b/tests/value/oracle/symbolic_locs.res.oracle
@@ -65,7 +65,7 @@
[eva:alarm] tests/value/symbolic_locs.i:51: Warning:
assertion got status unknown.
[eva:alarm] tests/value/symbolic_locs.i:54: Warning:
- pointer downcast. assert (unsigned int)&x ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/value/symbolic_locs.i:55:
Frama_C_dump_each:
# Cvalue domain:
diff --git a/tests/value/oracle/volatile.res.oracle b/tests/value/oracle/volatile.res.oracle
index 5298041bed3..8cfa94fed9d 100644
--- a/tests/value/oracle/volatile.res.oracle
+++ b/tests/value/oracle/volatile.res.oracle
@@ -91,7 +91,7 @@
[eva] computing for function main2 <- main.
Called from tests/value/volatile.c:177.
[eva:alarm] tests/value/volatile.c:83: Warning:
- pointer downcast. assert (unsigned int)&X ≤ 2147483647;
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
--
GitLab