diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 445efc3204dc7df33fb762f7d61bf317f854ec4e..2faab4979f1ef4dc46ae06fff1b2c4bf2fe77d1f 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 8da10c3cf6910de2ce69ffa4b223bd79679c70ca..e9417dd0256ab638e8fe3f476d30be8edbac6c0f 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 c3be4194f94c20ce9dafc1719ca405b9397f19ca..280661c522f5e0027260323c72bf8ba1eb32da41 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 c748e18da98971ae147bd2710178f05b0fbcf744..4d7ac635f76867055ff5101b207043750e18500c 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 240ad0e4b03588b814918ef3a45c64308919e0ec..f93b938207e84054d6ecd4daf5c6a9740816884a 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 452e93e5b6df1268adb70c3e211b33bbdea2c856..4fbe20f941e39805a6270ea36816a8f5df791524 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 b6358392e622d184e2ecc53b62c8009eb13401d6..68da16922725ebdd4a044ba722aef0cc200d86fe 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 11215767505a32b8d80f9f108fcdbeb4bf202f72..e2c146788658bd30ae5e489e1134b1800830daf9 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 6139567781a663fe4269a763404374a7d3a2a61a..21fd920919affc8afd1710f3d43042b975c924b3 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 900d168bdbac15b6e38d1f34294b7001cd73fbcc..dcc09a3de5d1cf947b9d8f050733884324be3c76 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 b04e6e5abe47799286276d94e4809a105a8a5215..392940b6cb6e3312cb5941f61892dfa13cb007c0 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 0c9295b364c5ce95afcac52dc04fb41c62bf5b3a..784bf02c5cf4f24b9aa67db81b8cf442ed7c0e06 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 00d692def3c0c19cb821f8e550ac45f2ce238938..66f30707d3259e2969df47d8e280f469eb3f74b4 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 6324ceb920cc95d1c5d24f618f9d50b0e1f0ba53..5e60b7a32e5ff2014f7a279f2b314b5969f31798 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 9f4864b2625277e60112e9d743849319ae1b5cd8..036f8d26e43e182434e95dcde6ced28107a6d3bb 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 a0b3a97b62ff806abb069f955eb7debfd417a618..112f643e8810a8acfb5c96421196df65e43d7fe5 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 52fc170f4f861183d4d8bbb7901db806fc9760cd..f791b980831bd6f9e0c61b1febfb6e83cba17dda 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 2d45c975ffbd99995a126ae5eacbe2573ba8399a..ba58150afafceddb7303e4ef4f35b0d438a7b2b4 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 667b1228b96a1a637554fda9f90bebdad352a23f..36e1a671ef649728d5f1a3b4b1ba0f00f12488ea 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 81d6deca4271f49a1de658bc2b94764e87329b08..1fe41a6755acb70d209f28f6fe3f44444cfd61d9 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 c84e281414a922e821f94dcf97a984f3da44bf88..3383a7f5af11c33a0b49deb33113bdbf7543ac0f 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 b8a89b48a6ca0dcded1e728d13aebe1bfd13eb07..a09c922b6d3924e3f74da13fa331a48dc6afe907 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 2d14be302898c017d2567ed3b0346bc4af60ddc5..8599de4e4af9da144bcf4e997d7be8c9348c5b49 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 40501b7b144081ba32b4a3a5cf89dac663cc580b..4cfd1aeca7a34e5f4825e3efdf9dade3a7e01e54 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 54cf0bfdba6fb87ca4b47e2ef086ad4ca6e4f91f..0ae5f0394606e216870ff0d5c5f4fe947f103d98 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 a0538f60c8e08dc0a6252b031bfcaffdc9d1ef09..878fa04174a2301232dcc5fab79671c8cfad0fe8 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 08d4b95eafc15bca565fc3ae18efe6e16ba5e964..47a1035cc56d34fcfaad83bf7bfc5cd2f7b50b2d 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 ea6793941d440476c137a927a02553cf8df9a45c..182c5433339e484a9db1a6187096ab716cc325a0 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 f8869049442b7febbbbbc8f19093c300bc865954..f1220992e0b2fe33b682cd14e1d308846df0d14a 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 26374aad66f732fefba10a9defba98a572dacf0c..954fdab07b419cf2a12ec881c37860546384ec36 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 0c2afa4364c8e9c7efa752316095e2c82e1f5735..59f4ac5f0f9e552e08318ac54231d9674780213f 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 e7af15348e5e1167fd5216005bce99f6b903c298..6631dfe4e46d5233ea557de069df72f64f96bec0 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 4f8b786e02d27cb794885b586e4764919d129eeb..2f95483430ee68b9fb2aee65ffad1ccfd202931a 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 d052fa034e4dc04e49f23648ea6732c0ed0bd286..bb2cbef17535dbdbf3cef47f6757b5ac4894ff6c 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 60f0db91f1eb37a41a0d47990246922172a5351d..ba49fd5aff7ed2c46847101b030c1578ba71f117 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 f06f8231e21afb23dd9484c6a087dea6ffbd09b7..90af155562b9b8797ae7bcbd68e0ee6bd42434e9 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 a11fbdf9fa2e356d9824d4364bc7f71ab22cbde1..eb4493ddfd3a65d3dfce413d96809353d388e0e9 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 f58c5770d4419a1b7dd7fd87e08d06e24f696c0c..7261a1cb811310c62ae52d2a8bf458e0b25f6de2 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 d1824131817510a65631bd75ee25b15b33cf6299..1cde862a4b6551a10c5c50fbf37f9edddcd36857 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 f99360712b50b3da7a0c90b75a77771fd80b6086..3e7b008426e2a3857f1506beccf02faeb6d98f7a 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 611d2093addba4f74739c394f82d14b79ce57b47..338f79ddc5e562248c7d3246b45271cb2c3c3945 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 8ca94ab19cfb6a60b0f17669f82b1aaef6d049e0..b57ddb23b52afcfe2fb43e41160db19dd1996f01 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 2194180b285684a3e10dc8d02b35628bf4d3aff6..111aa1c6f07269e57c40e05b830f78610e7d81e3 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 3c3c61be0c2992ab48a36011766298c20c7dbe1c..a87f0773b6eb65bac1d59beedb2c2d142fd94d48 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 41082946d0a7b5f6491017407af16c953a50ef46..96ab8ffd9b41e9562a73dd6afd3f244a6c403e5f 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 65092ae89c40c760a377afc0cd3a4fc94986e3bd..0cc72335a3a945d507756d104f6b9f40ca26ee8f 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 b5be0d8bcaa981ebb4db5e6f519315282b23cf97..433ce49eaa0ba5fe807e8a83e3c7550bb2c62d67 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 776fa403f152dd299f35687dece98b7611491945..8be78fd49c0cde02afd96f8c3a7f7345cee83b0b 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 6c6287b4bff13a00abe2461f9ab0de2c5e359b64..8dbc430d5ee96b88e1fdc11243dd643dbfaa6a2b 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 2a076ba31dc272800363263c588061468689bdb1..572459f644a8f9403d5f4f5cc1231c2b6bf93b2e 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 115819f96744ef2984fcf7e56afdbb34735d178d..d4ac4533187b26fcde94ffc2686f55870879fca3 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 cd433bd1e2f88f0ed5a2c28f47fa7701b4e0819e..2bdd5becc39c217a92386b0eec24bb4ac9ebdd71 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 6e3283d930451f984ee203d1a048187c100869ac..0b3195a5397b0126f8eed45040fafff00df4c125 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 156c9148c1069aae3ba3125b819fb974d29ca356..2af9a46bd2a738663bb66bde0768d88bc3967919 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 fcd954b8df5e93cd8b3a9752f9b8eb1220998e09..6ac5900dc2e425cc69bd9317d1baadd5b41e2e7f 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 af00458ed51a8777d335941791674b352af57512..cd63714dccccd315f1b03fddceefecccc8f7ddd8 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 75c12b7d3ab8ee1923eb538d819be491aab3c462..cad14cc1bd042de3a5b4ae42904551966dc6a151 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 4e0d35dc30a0a3814ddd6e174bc436e794dd15ac..b2838250a6d5104942a7d000707c740654d060e8 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 46103bb62cc5622b9c0e8d53b36a8082f662b849..9862244f180a9db29e4f8a675b3763cf0dc72b3d 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 23b0674bd229acec51385fc59969ea61590ce5d1..adc483ff665929f6a5ccbcac65eee15f7da03395 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 44c891f667456df7ada4894a6aec967d94ec2a8b..4cbcaa45fece740a5d003524f97f4d0e6c3bd565 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 c0df48148db9f31f81c08e38cb7de09d81b1eb3f..05ac2f16880175bd81d50810e8f58c82ee0a05a7 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 e8e83a5e4467962efed80607ccbc53b44d0670f8..3eb4f598ee5535e92806764dd7628d0d1bc3307c 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 744e5e6a72fb23ffb0dd20c5d028bd0899842c15..eb325482dff5626613b033e1a10ed1426e77a835 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 5298041bed3f69001dc239cd281e3901cfcbecbb..8cfa94fed9df507ba41a46c8921cf3b906e5eb20 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.