Commit 48f0beaf authored by David Bühler's avatar David Bühler
Browse files

[Kernel] Fixes alarm: uses TCastE instead of TLogic_coerce.

New smart constructor for TCastE in logic_const.
parent 91b6a4d9
......@@ -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
| _ ->
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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:
......
......@@ -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
......
......@@ -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.
......
......@@ -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.
......
......@@ -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}
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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))));
......
......@@ -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))));
......
......@@ -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}
......
......@@ -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))));
......
......@@ -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))));
......
......@@ -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}
......
......@@ -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:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment