Commit bf9c0a96 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] update oracles

parent 804a29ee
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/array.i:13: Warning: assertion got status unknown.
[eva:alarm] tests/arith/array.i:13: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/array.i:14: Warning: assertion got status unknown.
[eva:alarm] tests/arith/array.i:14: Warning:
function __e_acsl_assert: precondition got status unknown.
......@@ -11,8 +11,6 @@
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:28: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
......@@ -20,7 +18,7 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:31: Warning:
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:33: Warning:
accessing uninitialized left-value.
......@@ -29,9 +27,9 @@
((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:37: Warning:
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:31: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:37: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
accessing uninitialized left-value.
......@@ -40,7 +38,7 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:44: Warning:
accessing uninitialized left-value.
......@@ -49,6 +47,8 @@
((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
......@@ -63,8 +63,6 @@
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:8: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
......@@ -72,7 +70,7 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:54: Warning:
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:56: Warning:
accessing uninitialized left-value.
......@@ -81,6 +79,8 @@
((__gen_e_acsl_u_5 - 10) * 300 +
(((__gen_e_acsl_v_5 - -10) - 1) * 100 +
((__gen_e_acsl_w - 100) - 1))));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:54: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:63: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:65: Warning:
......
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/functions_rec.c:22: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:22: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:23: Warning:
[eva:alarm] tests/arith/functions_rec.c:22: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:23: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
[eva:alarm] tests/arith/functions_rec.c:23: Warning:
assertion got status unknown.
[eva] tests/arith/functions_rec.c:7: Warning:
recursive call during value analysis
......@@ -18,7 +16,7 @@
Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:26: Warning:
[eva:alarm] tests/arith/functions_rec.c:24: Warning:
assertion got status unknown.
[eva] tests/arith/functions_rec.c:10: Warning:
recursive call during value analysis
......@@ -67,7 +65,7 @@
2147483647;
[eva:alarm] tests/arith/functions_rec.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:28: Warning:
[eva:alarm] tests/arith/functions_rec.c:26: Warning:
assertion got status unknown.
[eva] tests/arith/functions_rec.c:14: Warning:
recursive call during value analysis
......@@ -75,7 +73,7 @@
__gen_e_acsl_f3 :: tests/arith/functions_rec.c:28 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
[eva:alarm] tests/arith/functions_rec.c:28: Warning:
assertion got status unknown.
[eva] tests/arith/functions_rec.c:17: Warning:
recursive call during value analysis
......@@ -85,3 +83,5 @@
Assuming the call has no effect. The analysis will be unsound.
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
assertion got status unknown.
......@@ -8,27 +8,26 @@ int main(void)
int x = -3;
int y = 2;
long z = 2L;
/*@ assert -3 ≡ x; */
__e_acsl_assert(-3 == x,(char *)"Assertion",(char *)"main",
(char *)"-3 == x",10);
/*@ assert x-3; */
/*@ assert -3x; */ ;
__e_acsl_assert(x == -3,(char *)"Assertion",(char *)"main",
(char *)"x == -3",11);
/*@ assert 0 ≢ ~0; */
/*@ assert x ≡ -3; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 != ~0",12);
/*@ assert x + 1 ≡ -2; */
/*@ assert 0 ≢ ~0; */ ;
__e_acsl_assert(x + 1L == -2L,(char *)"Assertion",(char *)"main",
(char *)"x + 1 == -2",14);
/*@ assert x - 1 ≡ -4; */
/*@ assert x + 1 ≡ -2; */ ;
__e_acsl_assert(x - 1L == -4L,(char *)"Assertion",(char *)"main",
(char *)"x - 1 == -4",15);
/*@ assert x * 3 ≡ -9; */
/*@ assert x - 1 ≡ -4; */ ;
__e_acsl_assert(x * 3L == -9L,(char *)"Assertion",(char *)"main",
(char *)"x * 3 == -9",16);
/*@ assert x / 3 ≡ -1; */
/*@ assert x * 3 ≡ -9; */ ;
__e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
(char *)"x / 3 == -1",17);
/*@ assert 0xffffffffffffffffffffff / 0xffffffffffffffffffffff ≡ 1; */
/*@ assert x / 3-1; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl__2;
......@@ -55,42 +54,40 @@ int main(void)
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_div);
}
/*@ assert x % 2-1; */
/*@ assert 0xffffffffffffffffffffff / 0xffffffffffffffffffffff ≡ 1; */ ;
__e_acsl_assert(x % 2 == -1,(char *)"Assertion",(char *)"main",
(char *)"x % 2 == -1",19);
/*@ assert -3 % -2 ≡ -1; */
/*@ assert x % 2 ≡ -1; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-3 % -2 == -1",20);
/*@ assert 3 % -2 ≡ 1; */
/*@ assert -3 % -2 ≡ -1; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"3 % -2 == 1",
21);
/*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */
/*@ assert 3 % -2 ≡ 1; */ ;
__e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10L,
(char *)"Assertion",(char *)"main",
(char *)"((x * 2 + (3 + y)) - 4) + (x - y) == -10",23);
/*@ assert (0 ≡ 1) ≡ !(0 ≡ 0); */
/*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 == 1) == !(0 == 0)",25);
/*@ assert (0 ≤ -1) ≡ (0 > 0); */
/*@ assert (0 1) ≡ !(0 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 <= -1) == (0 > 0)",26);
/*@ assert (0 -1) ≡ (0 0); */
/*@ assert (0 -1) ≡ (0 > 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 >= -1) == (0 <= 0)",27);
/*@ assert (0 1) ≡ !(0 0); */
/*@ assert (0 ≥ -1) ≡ (0 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 1) == !(0 != 0)",28);
/*@ assert (0 ≢ 0) ≡ !(1 ≢ 0); */
/*@ assert (0 ≢ 1) ≡ !(0 ≢ 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 0) == !(1 != 0)",30);
/*@ assert 4 / y ≡ 2; */
{
__e_acsl_assert(y != 0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: y != 0",31);
__e_acsl_assert(4 / y == 2,(char *)"Assertion",(char *)"main",
(char *)"4 / y == 2",31);
}
/*@ assert 1 + (z + 1) / (y - 123456789123456789) ≡ 1; */
/*@ assert (0 ≢ 0) ≡ !(1 ≢ 0); */ ;
__e_acsl_assert(y != 0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: y != 0",31);
__e_acsl_assert(4 / y == 2,(char *)"Assertion",(char *)"main",
(char *)"4 / y == 2",31);
/*@ assert 4 / y ≡ 2; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_z;
__e_acsl_mpz_t __gen_e_acsl__4;
......@@ -130,9 +127,10 @@ int main(void)
__gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_div_2);
}
/*@ assert 1 - x ≡ -x + 1; */
/*@ assert 1 + (z + 1) / (y - 123456789123456789) ≡ 1; */ ;
__e_acsl_assert(1L - x == - ((long)x) + 1L,(char *)"Assertion",
(char *)"main",(char *)"1 - x == -x + 1",36);
/*@ assert 1 - x ≡ -x + 1; */ ;
__retres = 0;
return __retres;
}
......
......@@ -21,12 +21,12 @@ int main(void)
i_0 ++;
}
}
/*@ assert T1[0] ≡ T2[0]; */
__e_acsl_assert(T1[0] == T2[0],(char *)"Assertion",(char *)"main",
(char *)"T1[0] == T2[0]",13);
/*@ assert T1[1] T2[1]; */
/*@ assert T1[0] T2[0]; */ ;
__e_acsl_assert(T1[1] != T2[1],(char *)"Assertion",(char *)"main",
(char *)"T1[1] != T2[1]",14);
/*@ assert T1[1] ≢ T2[1]; */ ;
__retres = 0;
return __retres;
}
......
......@@ -21,18 +21,18 @@ void f(void)
__gen_e_acsl_at_2 = A;
A = 2;
}
/*@ assert \at(A,Pre) ≡ 0; */
__e_acsl_assert(__gen_e_acsl_at == 0,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,Pre) == 0",11);
/*@ assert \at(A,F) ≡ 1; */
/*@ assert \at(A,Pre) ≡ 0; */ ;
__e_acsl_assert(__gen_e_acsl_at_2 == 1,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,F) == 1",12);
/*@ assert \at(A,Here) ≡ 2; */
/*@ assert \at(A,F) ≡ 1; */ ;
__e_acsl_assert(A == 2,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,Here) == 2",13);
/*@ assert \at(\at(A,Pre),F) ≡ 0; */
/*@ assert \at(A,Here) ≡ 2; */ ;
__e_acsl_assert(__gen_e_acsl_at_4 == 0,(char *)"Assertion",(char *)"f",
(char *)"\\at(\\at(A,Pre),F) == 0",14);
/*@ assert \at(\at(A,Pre),F) ≡ 0; */ ;
A = 3;
return;
}
......@@ -90,11 +90,11 @@ void g(int *p, int *q)
}
A = 4;
}
/*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
__e_acsl_assert(__gen_e_acsl_at_2 == 2,(char *)"Assertion",(char *)"g",
(char *)"\\at(*(p + \\at(*q,L1)),L2) == 2",26);
(char *)"\\at(*(p + \\at(*q,__invalid_label)),L2) == 2",26);
/*@ assert \at(*(p + \at(*q,__invalid_label)),L2) ≡ 2; */ ;
L3:
/*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
/*@ assert \at(*(p + \at(*q,__invalid_label)),Here) ≡ 2; */
{
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
......@@ -104,7 +104,8 @@ void g(int *p, int *q)
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
28);
__e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,(char *)"Assertion",
(char *)"g",(char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",
(char *)"g",
(char *)"\\at(*(p + \\at(*q,__invalid_label)),Here) == 2",
28);
}
__e_acsl_delete_block((void *)(& q));
......@@ -149,15 +150,16 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = 2;
__gen_e_acsl_f();
/*@ assert \at(x,L) ≡ 0; */
__e_acsl_assert(__gen_e_acsl_at == 0,(char *)"Assertion",(char *)"main",
(char *)"\\at(x,L) == 0",48);
/*@ assert \at(x + 1,L) ≡ 1; */
(char *)"\\at(x,__invalid_label) == 0",48);
/*@ assert \at(x,__invalid_label) ≡ 0; */ ;
__e_acsl_assert(__gen_e_acsl_at_2 == 1L,(char *)"Assertion",(char *)"main",
(char *)"\\at(x + 1,L) == 1",49);
/*@ assert \at(x,L) + 1 ≡ 1; */
(char *)"\\at(x + 1,__invalid_label) == 1",49);
/*@ assert \at(x + 1,__invalid_label) ≡ 1; */ ;
__e_acsl_assert(__gen_e_acsl_at_3 + 1L == 1L,(char *)"Assertion",
(char *)"main",(char *)"\\at(x,L) + 1 == 1",50);
(char *)"main",(char *)"\\at(x,__invalid_label) + 1 == 1",
50);
/*@ assert \at(x,__invalid_label) + 1 ≡ 1; */ ;
g(t,& x);
__retres = 0;
__e_acsl_delete_block((void *)(t));
......@@ -172,8 +174,8 @@ int __gen_e_acsl_h(int x)
int __gen_e_acsl_at;
int __retres;
__e_acsl_store_block((void *)(& __retres),(size_t)4);
__gen_e_acsl_at = x;
__e_acsl_store_block((void *)(& x),(size_t)4);
__gen_e_acsl_at = x;
__retres = h(x);
__e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
(char *)"h",(char *)"\\result == \\old(x)",35);
......
......@@ -37,7 +37,6 @@ void g(void)
;
}
m = 10;
/*@ assert ∃ ℤ w; 3 ≤ w < 6 ∧ \at(m + w ≡ 12,Q); */
{
int __gen_e_acsl_exists;
int __gen_e_acsl_w;
......@@ -72,6 +71,7 @@ void g(void)
(char *)"\\exists integer w; 3 <= w < 6 && \\at(m + w == 12,Q)",
16);
}
/*@ assert ∃ ℤ w; 3 ≤ w < 6 ∧ \at(m + w ≡ 12,Q); */ ;
free((void *)__gen_e_acsl_at);
return;
}
......@@ -205,7 +205,6 @@ int main(void)
}
__e_acsl_full_init((void *)(& n));
n = 666;
/*@ assert \let i = 3; \at(n + i ≡ 10,L); */
{
int __gen_e_acsl_i;
int __gen_e_acsl_valid_read;
......@@ -221,7 +220,7 @@ int main(void)
(char *)"main",
(char *)"\\let i = 3; \\at(n + i == 10,L)",28);
}
/*@ assert ∃ ℤ j; 2 ≤ j < 5 ∧ \at(n + j ≡ 11,L); */
/*@ assert \let i = 3; \at(n + i ≡ 10,L); */ ;
{
int __gen_e_acsl_exists;
int __gen_e_acsl_j;
......@@ -257,11 +256,7 @@ int main(void)
(char *)"\\exists integer j; 2 <= j < 5 && \\at(n + j == 11,L)",
29);
}
/*@ assert \let k = -7;
∃ ℤ u;
9 ≤ u < 21 ∧
(∀ ℤ v; -5 < v ≤ 6 ⇒ \at((u > 0? n + k: u + v) > 0,K));
*/
/*@ assert ∃ ℤ j; 2 ≤ j < 5 ∧ \at(n + j ≡ 11,L); */ ;
{
int __gen_e_acsl_k;
int __gen_e_acsl_exists_2;
......@@ -323,7 +318,13 @@ int main(void)
(char *)"\\let k = -7;\n\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= 6 ==> \\at((u > 0? n + k: u + v) > 0,K))",
31);
}
/*@ assert \let i = 3; \at(n + i,L) ≡ 10; */
/*@
assert \let k = -7;
∃ ℤ u;
9 ≤ u < 21 ∧
(∀ ℤ v; -5 < v ≤ 6 ⇒ \at((u > 0? n + k: u + v) > 0,K));
*/
;
{
int __gen_e_acsl_i_3;
int __gen_e_acsl_valid_read_4;
......@@ -339,6 +340,7 @@ int main(void)
(char *)"main",
(char *)"\\let i = 3; \\at(n + i,L) == 10",37);
}
/*@ assert \let i = 3; \at(n + i,L) ≡ 10; */ ;
unsigned int m = (unsigned int)3;
G:
{
......@@ -354,7 +356,6 @@ int main(void)
;
}
m = (unsigned int)(-3);
/*@ assert ∃ ℤ k; -9 < k < 0 ∧ \at(m + k,G) ≡ 0; */
{
int __gen_e_acsl_exists_3;
int __gen_e_acsl_k_3;
......@@ -392,11 +393,7 @@ int main(void)
(char *)"\\exists integer k; -9 < k < 0 && \\at(m + k,G) == 0",
41);
}
/*@ assert
∃ ℤ u;
9 ≤ u < 21 ∧
(∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
*/
/*@ assert ∃ ℤ k; -9 < k < 0 ∧ \at(m + k,G) ≡ 0; */ ;
{
int __gen_e_acsl_exists_4;
int __gen_e_acsl_u_3;
......@@ -461,20 +458,18 @@ int main(void)
(char *)"\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
43);
}
/*@
assert
∃ ℤ u;
9 ≤ u < 21 ∧
(∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
*/
;
int t[5] = {9, 12, 12, 12, -4};
__e_acsl_store_block((void *)(t),(size_t)20);
__e_acsl_full_init((void *)(& t));
__gen_e_acsl_f(t);
g();
/*@ assert
∃ ℤ u;
10 ≤ u < 20 ∧
(∃ ℤ v;
-10 < v ≤ -5 + (\let u = -2; u) ∧
(∃ ℤ w;
100 < w ≤ 200 ∧
\at((((n - u) + (\let u = 42; u)) + v) + w > 0,K)));
*/
{
int __gen_e_acsl_exists_5;
int __gen_e_acsl_u_5;
......@@ -561,6 +556,17 @@ int main(void)
(char *)"\\exists integer u;\n 10 <= u < 20 &&\n (\\exists integer v;\n -10 < v <= -5 + (\\let u = -2; u) &&\n (\\exists integer w;\n 100 < w <= 200 && \\at((((n - u) + (\\let u = 42; u)) + v) + w > 0,K)))",
54);
}
/*@
assert
∃ ℤ u;
10 ≤ u < 20 ∧
(∃ ℤ v;
-10 < v ≤ -5 + (\let u = -2; u) ∧
(∃ ℤ w;
100 < w ≤ 200 ∧
\at((((n - u) + (\let u = 42; u)) + v) + w > 0,K)));
*/
;
/*@ assert ∃ ℤ j; 2 ≤ j < 10000000000000000 ∧ \at(n + j ≡ 11,L);
*/
;
......@@ -594,6 +600,7 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_at_3 = (int *)malloc((size_t)4);
__gen_e_acsl_at_2 = (int *)malloc((size_t)8);
__gen_e_acsl_at = (int *)malloc((size_t)8);
__e_acsl_store_block((void *)(& t),(size_t)8);
{
int __gen_e_acsl_m_3;
__gen_e_acsl_m_3 = 4;
......@@ -622,7 +629,6 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_n_2 ++;
}
}
__e_acsl_store_block((void *)(& t),(size_t)8);
f(t);
{
int __gen_e_acsl_forall;
......
......@@ -7,26 +7,26 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
long x = (long)0;
int y = 0;
/*@ assert (int)x ≡ y; */
__e_acsl_assert((int)x == y,(char *)"Assertion",(char *)"main",
(char *)"(int)x == y",9);
/*@ assert x ≡ (long)y; */
/*@ assert (int)x ≡ y; */ ;
__e_acsl_assert(x == (long)y,(char *)"Assertion",(char *)"main",
(char *)"x == (long)y",10);
/*@ assert y ≡ (int)0; */
/*@ assert x ≡ (long)y; */ ;
__e_acsl_assert(y == 0,(char *)"Assertion",(char *)"main",
(char *)"y == (int)0",12);
/*@ assert (unsigned int)y ≡ (unsigned int)0; */
/*@ assert y ≡ (int)0; */ ;
__e_acsl_assert((unsigned int)y == 0U,(char *)"Assertion",(char *)"main",
(char *)"(unsigned int)y == (unsigned int)0",13);
/*@ assert y (int)0xfffffffffffffff; */
/*@ assert (unsigned int)y (unsigned int)0; */ ;
__e_acsl_assert(y != -1,(char *)"Assertion",(char *)"main",
(char *)"y != (int)0xfffffffffffffff",16);
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */
/*@ assert y ≢ (int)0xfffffffffffffff; */ ;
__e_acsl_assert((unsigned int)y != 4294967295U,(char *)"Assertion",
(char *)"main",
(char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
17);
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */ ;
int t[2] = {0, 1};
/*@ assert (float)x ≡ t[(int)0.1]; */ ;
__retres = 0;
......
......@@ -7,49 +7,49 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
int y = 1;
/*@ assert x < y; */
__e_acsl_assert(x < y,(char *)"Assertion",(char *)"main",(char *)"x < y",7);
/*@ assert y > x; */
/*@ assert x < y; */ ;
__e_acsl_assert(y > x,(char *)"Assertion",(char *)"main",(char *)"y > x",8);
/*@ assert x ≤ 0; */
/*@ assert y > x; */ ;
__e_acsl_assert(x <= 0,(char *)"Assertion",(char *)"main",(char *)"x <= 0",
9);
/*@ assert y ≥ 1; */
/*@ assert x ≤ 0; */ ;
__e_acsl_assert(y >= 1,(char *)"Assertion",(char *)"main",(char *)"y >= 1",
10);
/*@ assert y ≥ 1; */ ;
char *s = (char *)"toto";
/*@ assert s ≡ s; */
__e_acsl_assert(s == s,(char *)"Assertion",(char *)"main",(char *)"s == s",
12);
/*@ assert 5 < 18; */
/*@ assert s ≡ s; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"5 < 18",15);
/*@ assert 32 > 3; */
/*@ assert 5 < 18; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"32 > 3",16);
/*@ assert 12 ≤ 13; */
/*@ assert 32 > 3; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"12 <= 13",17);
/*@ assert 123 ≥ 12; */
/*@ assert 12 13; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"123 >= 12",
18);
/*@ assert 0xff ≡ 0xff; */
/*@ assert 123 ≥ 12; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"0xff == 0xff",19);
/*@ assert 1 ≢ 2; */
/*@ assert 0xff ≡ 0xff; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"1 != 2",20);
/*@ assert -5 < 18; */
/*@ assert 1 ≢ 2; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"-5 < 18",22);
/*@ assert 32 > -3; */
/*@ assert -5 < 18; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"32 > -3",23);
/*@ assert -12 ≤ 13; */
/*@ assert 32 > -3; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"-12 <= 13",
24);
/*@ assert 123 ≥ -12; */
/*@ assert -12 ≤ 13; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"123 >= -12",
25);
/*@ assert -0xff ≡ -0xff; */
/*@ assert 123 ≥ -12; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-0xff == -0xff",26);
/*@ assert 1 ≢ -2; */
/*@ assert -0xff ≡ -0xff; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"1 != -2",27);
/*@ assert 1 ≢ -2; */ ;
__retres = 0;
return __retres;
}
......
......@@ -88,21 +88,20 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 1;
int y = 2;
/*@ assert p1(x, y); */
{
int __gen_e_acsl_p1_2;
__gen_e_acsl_p1_2 = __gen_e_acsl_p1(x,y);
__e_acsl_assert(__gen_e_acsl_p1_2,(char *)"Assertion",(char *)"main",
(char *)"p1(x, y)",42);
}