Commit 37881680 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'bugfix/julien/mkBinOp' into 'master'

fix typing in presence of comparison operators (gitlab issue 49)

Closes #49

See merge request frama-c/e-acsl!191
parents 1f41a63f cb00dea6
Tests:
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL --cppo 07d2bcee50670aecae7e094d92f68fd18314073a
tags:
except:
- tags
context-from-precondition:
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition --cppo 07d2bcee50670aecae7e094d92f68fd18314073a
tags:
except:
- tags
Security:
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security --cppo 07d2bcee50670aecae7e094d92f68fd18314073a
tags:
except:
- tags
......@@ -19,6 +19,10 @@
# configure configure
###############################################################################
-* E-ACSL [2018/02/07] Fix incorrect typing in presence of
comparison operators (may only be visible when directly
analyzing the E-ACSL's generated code with Frama-C without
pretty-printing it).
-* runtime [2018/01/30] E-ACSL aborted when run on a machine with a
low hard limit on the stack size.
-* E-ACSL [2018/01/08] Fix a crash when translating a postcondition
......
......@@ -156,7 +156,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",
23);
__gen_e_acsl_and = *__gen_e_acsl_at_3 < 0.85 * *__gen_e_acsl_at_4;
__gen_e_acsl_and = (long double)*__gen_e_acsl_at_3 < 0.85 * *__gen_e_acsl_at_4;
}
else __gen_e_acsl_and = 0;
if (__gen_e_acsl_and) {
......@@ -168,7 +168,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"bar",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_5)",
23);
__gen_e_acsl_if = *__gen_e_acsl_at_5 != 0.;
__gen_e_acsl_if = (long double)*__gen_e_acsl_at_5 != 0.;
}
else {
int __gen_e_acsl_valid_read_6;
......@@ -254,9 +254,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
__e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 -
((long double)(
5 / 80) * *__gen_e_acsl_at_3) * 0.4),
__e_acsl_assert((long double)*__gen_e_acsl_at == *__gen_e_acsl_at_2 + (
(long double)5 -
((long double)0 * *__gen_e_acsl_at_3) * 0.4),
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)",
11);
......
......@@ -20,7 +20,7 @@ int main(void) {
/* heterogeneous casts from/to integers */
int t[2] = { 0, 1 };
/*@ assert (float)x == (float)t[(int)0.1]; */
/*@ assert (float)x == t[(int)0.1]; */
return 0;
}
......@@ -14,16 +14,15 @@ int main(void)
__e_acsl_assert(x == -3,(char *)"Assertion",(char *)"main",
(char *)"x == -3",11);
/*@ assert 0 ≢ ~0; */
__e_acsl_assert(0 != ~ 0,(char *)"Assertion",(char *)"main",
(char *)"0 != ~0",12);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 != ~0",12);
/*@ assert x + 1 ≡ -2; */
__e_acsl_assert(x + 1L == -2,(char *)"Assertion",(char *)"main",
__e_acsl_assert(x + 1L == -2L,(char *)"Assertion",(char *)"main",
(char *)"x + 1 == -2",14);
/*@ assert x - 1 ≡ -4; */
__e_acsl_assert(x - 1L == -4,(char *)"Assertion",(char *)"main",
__e_acsl_assert(x - 1L == -4L,(char *)"Assertion",(char *)"main",
(char *)"x - 1 == -4",15);
/*@ assert x * 3 ≡ -9; */
__e_acsl_assert(x * 3L == -9,(char *)"Assertion",(char *)"main",
__e_acsl_assert(x * 3L == -9L,(char *)"Assertion",(char *)"main",
(char *)"x * 3 == -9",16);
/*@ assert x / 3 ≡ -1; */
__e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
......@@ -48,7 +47,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gen_e_acsl__3 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
__e_acsl_assert(__gen_e_acsl__3 == 1,(char *)"Assertion",(char *)"main",
__e_acsl_assert(__gen_e_acsl__3 == 1L,(char *)"Assertion",(char *)"main",
(char *)"0xffffffffffffffffffffff / 0xffffffffffffffffffffff == 1",
18);
__gmpz_clear(__gen_e_acsl_);
......@@ -59,29 +58,29 @@ int main(void)
__e_acsl_assert(x % 2 == -1,(char *)"Assertion",(char *)"main",
(char *)"x % 2 == -1",19);
/*@ assert -3 % -2 ≡ -1; */
__e_acsl_assert(-3 % -2 == -1,(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-3 % -2 == -1",20);
/*@ assert 3 % -2 ≡ 1; */
__e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
(char *)"3 % -2 == 1",21);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"3 % -2 == 1",
21);
/*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */
__e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10,
__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); */
__e_acsl_assert((0 == 1) == ! (0 == 0),(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 == 1) == !(0 == 0)",25);
/*@ assert (0 ≤ -1) ≡ (0 > 0); */
__e_acsl_assert((0 <= -1) == (0 > 0),(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 <= -1) == (0 > 0)",26);
/*@ assert (0 ≥ -1) ≡ (0 ≤ 0); */
__e_acsl_assert((0 >= -1) == (0 <= 0),(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 >= -1) == (0 <= 0)",27);
/*@ assert (0 ≢ 1) ≡ !(0 ≢ 0); */
__e_acsl_assert((0 != 1) == ! (0 != 0),(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 1) == !(0 != 0)",28);
/*@ assert (0 ≢ 0) ≡ !(1 ≢ 0); */
__e_acsl_assert((0 != 0) == ! (1 != 0),(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 0) == !(1 != 0)",30);
/*@ assert 4 / y ≡ 2; */
{
......
......@@ -21,41 +21,34 @@ int main(void)
__e_acsl_assert(s == s,(char *)"Assertion",(char *)"main",(char *)"s == s",
12);
/*@ assert 5 < 18; */
__e_acsl_assert(5 < 18,(char *)"Assertion",(char *)"main",(char *)"5 < 18",
15);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"5 < 18",15);
/*@ assert 32 > 3; */
__e_acsl_assert(32 > 3,(char *)"Assertion",(char *)"main",(char *)"32 > 3",
16);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"32 > 3",16);
/*@ assert 12 ≤ 13; */
__e_acsl_assert(12 <= 13,(char *)"Assertion",(char *)"main",
(char *)"12 <= 13",17);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"12 <= 13",17);
/*@ assert 123 ≥ 12; */
__e_acsl_assert(123 >= 12,(char *)"Assertion",(char *)"main",
(char *)"123 >= 12",18);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"123 >= 12",
18);
/*@ assert 0xff ≡ 0xff; */
__e_acsl_assert(255 == 255,(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"0xff == 0xff",19);
/*@ assert 1 ≢ 2; */
__e_acsl_assert(1 != 2,(char *)"Assertion",(char *)"main",(char *)"1 != 2",
20);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"1 != 2",20);
/*@ assert -5 < 18; */
__e_acsl_assert(-5 < 18,(char *)"Assertion",(char *)"main",
(char *)"-5 < 18",22);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"-5 < 18",22);
/*@ assert 32 > -3; */
__e_acsl_assert(32 > -3,(char *)"Assertion",(char *)"main",
(char *)"32 > -3",23);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"32 > -3",23);
/*@ assert -12 ≤ 13; */
__e_acsl_assert(-12 <= 13,(char *)"Assertion",(char *)"main",
(char *)"-12 <= 13",24);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"-12 <= 13",
24);
/*@ assert 123 ≥ -12; */
__e_acsl_assert(123 >= -12,(char *)"Assertion",(char *)"main",
(char *)"123 >= -12",25);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"123 >= -12",
25);
/*@ assert -0xff ≡ -0xff; */
__e_acsl_assert(-255 == -255,(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-0xff == -0xff",26);
/*@ assert 1 ≢ -2; */
__e_acsl_assert(1 != -2,(char *)"Assertion",(char *)"main",
(char *)"1 != -2",27);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"1 != -2",27);
__retres = 0;
return __retres;
}
......
......@@ -6,16 +6,13 @@ int main(void)
int x;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
/*@ assert 0 ≡ 0; */
__e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"main",(char *)"0 == 0",
6);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 == 0",6);
x = 0;
x ++;
/*@ assert 0 ≢ 1; */
__e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"main",(char *)"0 != 1",
8);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 != 1",8);
/*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
__e_acsl_assert(1152921504606846975UL == 1152921504606846975UL,
(char *)"Assertion",(char *)"main",
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"1152921504606846975 == 0xfffffffffffffff",9);
/*@ assert
0xffffffffffffffffffffffffffffffff ≡
......
......@@ -43,7 +43,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_3;
__gen_e_acsl_block_length_3 = __e_acsl_block_length((void *)(A));
__e_acsl_assert(__gen_e_acsl_block_length_3 == 16,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_3 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length((int *)A) == sizeof(A)",20);
}
......@@ -51,7 +51,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_4;
__gen_e_acsl_block_length_4 = __e_acsl_block_length((void *)(& A[3]));
__e_acsl_assert(__gen_e_acsl_block_length_4 == 16,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_4 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&A[3]) == sizeof(A)",21);
}
......@@ -59,7 +59,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_5;
__gen_e_acsl_block_length_5 = __e_acsl_block_length((void *)PA);
__e_acsl_assert(__gen_e_acsl_block_length_5 == 16,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_5 == 16UL,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(PA) == sizeof(A)",
22);
}
......@@ -85,7 +85,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_8;
__gen_e_acsl_block_length_8 = __e_acsl_block_length((void *)(a));
__e_acsl_assert(__gen_e_acsl_block_length_8 == 16,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_8 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length((int *)a) == sizeof(a)",29);
}
......@@ -93,7 +93,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_9;
__gen_e_acsl_block_length_9 = __e_acsl_block_length((void *)(& a[3]));
__e_acsl_assert(__gen_e_acsl_block_length_9 == 16,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_9 == 16UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&a[3]) == sizeof(a)",30);
}
......@@ -101,7 +101,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_10;
__gen_e_acsl_block_length_10 = __e_acsl_block_length((void *)pa);
__e_acsl_assert(__gen_e_acsl_block_length_10 == 16,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_10 == 16UL,(char *)"Assertion",
(char *)"main",(char *)"\\block_length(pa) == sizeof(a)",
31);
}
......@@ -128,7 +128,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_13;
__gen_e_acsl_block_length_13 = __e_acsl_block_length((void *)(& l));
__e_acsl_assert(__gen_e_acsl_block_length_13 == 8,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_13 == 8UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(&l) == sizeof(long)",39);
}
......@@ -136,7 +136,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_14;
__gen_e_acsl_block_length_14 = __e_acsl_block_length((void *)pl);
__e_acsl_assert(__gen_e_acsl_block_length_14 == 8,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_14 == 8UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl) == sizeof(long)",40);
}
......@@ -144,7 +144,7 @@ int main(void)
{
unsigned long __gen_e_acsl_block_length_15;
__gen_e_acsl_block_length_15 = __e_acsl_block_length((void *)(pl + 7));
__e_acsl_assert(__gen_e_acsl_block_length_15 == 8,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_block_length_15 == 8UL,(char *)"Assertion",
(char *)"main",
(char *)"\\block_length(pl + 7) == sizeof(long)",41);
}
......
......@@ -219,7 +219,7 @@ void __gen_e_acsl_m(void)
(char *)"m",(char *)"\\old(X == 5 && Y == 2) ==> X == 7",
60);
if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_3 = 1;
else __gen_e_acsl_implies_3 = X == __gen_e_acsl_at_4 + Y;
else __gen_e_acsl_implies_3 = (long)X == __gen_e_acsl_at_4 + Y;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Postcondition",
(char *)"m",
(char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X) + Y",
......@@ -288,14 +288,14 @@ void __gen_e_acsl_j(void)
{
__e_acsl_assert(X == 5,(char *)"Precondition",(char *)"j",(char *)"X == 5",
27);
__e_acsl_assert(X == 3L + Y,(char *)"Precondition",(char *)"j",
__e_acsl_assert((long)X == 3L + Y,(char *)"Precondition",(char *)"j",
(char *)"X == 3 + Y",30);
__e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"j",(char *)"Y == 2",
31);
j();
__e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"j",
(char *)"X == 3",28);
__e_acsl_assert(X == Y + 1L,(char *)"Postcondition",(char *)"j",
__e_acsl_assert((long)X == Y + 1L,(char *)"Postcondition",(char *)"j",
(char *)"X == Y + 1",32);
return;
}
......
......@@ -17,7 +17,7 @@ int main(void)
{
int __gen_e_acsl_and_2;
if (x != 0) {
__e_acsl_assert(0 != 0,(char *)"RTE",(char *)"main",
__e_acsl_assert(0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: 0 != 0",10);
__gen_e_acsl_and_2 = y == 1 / 0;
}
......@@ -37,7 +37,7 @@ int main(void)
int __gen_e_acsl_or_2;
if (x == 0) __gen_e_acsl_or_2 = 1;
else {
__e_acsl_assert(0 != 0,(char *)"RTE",(char *)"main",
__e_acsl_assert(0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: 0 != 0",12);
__gen_e_acsl_or_2 = y == 1 / 0;
}
......@@ -57,7 +57,7 @@ int main(void)
int __gen_e_acsl_implies_2;
if (! (x == 1)) __gen_e_acsl_implies_2 = 1;
else {
__e_acsl_assert(0 != 0,(char *)"RTE",(char *)"main",
__e_acsl_assert(0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: 0 != 0",14);
__gen_e_acsl_implies_2 = y == 1 / 0;
}
......
......@@ -20,7 +20,7 @@ void f(void)
(void *)(& T));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(T + G)",11);
__e_acsl_assert(*(T + G) == 'b',(char *)"Assertion",(char *)"f",
__e_acsl_assert((int)*(T + G) == 98,(char *)"Assertion",(char *)"f",
(char *)"*(T + G) == \'b\'",11);
}
G ++;
......@@ -91,7 +91,7 @@ int main(void)
(void *)(& S));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(S + G2)",25);
__e_acsl_assert(*(S + G2) == 'o',(char *)"Assertion",(char *)"main",
__e_acsl_assert((int)*(S + G2) == 111,(char *)"Assertion",(char *)"main",
(char *)"*(S + G2) == \'o\'",25);
}
/*@ assert \initialized(S); */
......
......@@ -63,7 +63,7 @@ int __gen_e_acsl_main(int argc, char **argv)
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",15);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
__e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
__e_acsl_assert(*(argv + argc) == (char *)0,(char *)"Assertion",
(char *)"main",(char *)"*(argv + argc) == \\null",15);
}
/*@ assert ¬\valid(*(argv + argc)); */
......@@ -131,7 +131,7 @@ int __gen_e_acsl_main(int argc, char **argv)
__gen_e_acsl_forall_2 = 1;
__gen_e_acsl_k_2 = 0;
while (1) {
if (__gen_e_acsl_k_2 <= len) ; else break;
if (__gen_e_acsl_k_2 <= (long)len) ; else break;
{
int __gen_e_acsl_valid_read_4;
int __gen_e_acsl_valid_4;
......
......@@ -66,22 +66,22 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)256,(unsigned long)12);
/*@ assert a ≡ \null; */
__e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
__e_acsl_assert(a == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a == \\null",23);
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)255,(unsigned long)512);
/*@ assert a ≡ \null; */
__e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
__e_acsl_assert(a == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a == \\null",26);
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)0,(unsigned long)512);
/*@ assert a ≡ \null; */
__e_acsl_assert(a == (void *)0,(char *)"Assertion",(char *)"main",
__e_acsl_assert(a == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a == \\null",29);
__e_acsl_full_init((void *)(& a));
a = (char *)aligned_alloc((unsigned long)256,(unsigned long)512);
/*@ assert a ≢ \null; */
__e_acsl_assert(a != (void *)0,(char *)"Assertion",(char *)"main",
__e_acsl_assert(a != (char *)0,(char *)"Assertion",(char *)"main",
(char *)"a != \\null",32);
/*@ assert \valid(a); */
{
......
......@@ -21,30 +21,34 @@ int main(void)
{
int __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset((void *)(A));
__e_acsl_assert(__gen_e_acsl_offset == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset((int *)A) == 0",13);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset == 0UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset((int *)A) == 0",13);
}
/*@ assert \offset(&A[3]) ≡ 12; */
{
int __gen_e_acsl_offset_2;
__gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3]));
__e_acsl_assert(__gen_e_acsl_offset_2 == 12UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(&A[3]) == 12",14);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_2 == 12UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(&A[3]) == 12",14);
}
/*@ assert \offset(PA) ≡ 0; */
{
int __gen_e_acsl_offset_3;
__gen_e_acsl_offset_3 = __e_acsl_offset((void *)PA);
__e_acsl_assert(__gen_e_acsl_offset_3 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(PA) == 0",15);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_3 == 0UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(PA) == 0",15);
}
PA ++;
/*@ assert \offset(PA + 1) ≡ 8; */
{
int __gen_e_acsl_offset_4;
__gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1));
__e_acsl_assert(__gen_e_acsl_offset_4 == 8UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(PA + 1) == 8",17);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_4 == 8UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(PA + 1) == 8",17);
}
int a[4] = {1, 2, 3, 4};
__e_acsl_store_block((void *)(a),(size_t)16);
......@@ -53,22 +57,25 @@ int main(void)
{
int __gen_e_acsl_offset_5;
__gen_e_acsl_offset_5 = __e_acsl_offset((void *)(a));
__e_acsl_assert(__gen_e_acsl_offset_5 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset((int *)a) == 0",21);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_5 == 0UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset((int *)a) == 0",21);
}
/*@ assert \offset(&a[1]) ≡ 4; */
{
int __gen_e_acsl_offset_6;
__gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1]));
__e_acsl_assert(__gen_e_acsl_offset_6 == 4UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(&a[1]) == 4",22);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_6 == 4UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(&a[1]) == 4",22);
}
/*@ assert \offset(&a[3]) ≡ 12; */
{
int __gen_e_acsl_offset_7;
__gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3]));
__e_acsl_assert(__gen_e_acsl_offset_7 == 12UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(&a[3]) == 12",23);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_7 == 12UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(&a[3]) == 12",23);
}
long l = (long)4;
__e_acsl_store_block((void *)(& l),(size_t)8);
......@@ -80,29 +87,33 @@ int main(void)
{
int __gen_e_acsl_offset_8;
__gen_e_acsl_offset_8 = __e_acsl_offset((void *)(& l));
__e_acsl_assert(__gen_e_acsl_offset_8 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(&l) == 0",28);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_8 == 0UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(&l) == 0",28);
}
/*@ assert \offset(pl) ≡ 0; */
{
int __gen_e_acsl_offset_9;
__gen_e_acsl_offset_9 = __e_acsl_offset((void *)pl);
__e_acsl_assert(__gen_e_acsl_offset_9 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pl) == 0",29);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_9 == 0UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(pl) == 0",29);
}
/*@ assert \offset(pl + 1) ≡ 1; */
{
int __gen_e_acsl_offset_10;
__gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1));
__e_acsl_assert(__gen_e_acsl_offset_10 == 1UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pl + 1) == 1",30);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_10 == 1UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(pl + 1) == 1",30);
}
/*@ assert \offset(pl + 7) ≡ 7; */
{
int __gen_e_acsl_offset_11;
__gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7));
__e_acsl_assert(__gen_e_acsl_offset_11 == 7UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pl + 7) == 7",31);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_11 == 7UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(pl + 7) == 7",31);
}
int *pi = (int *)(& l);
__e_acsl_store_block((void *)(& pi),(size_t)8);
......@@ -111,8 +122,9 @@ int main(void)
{
int __gen_e_acsl_offset_12;
__gen_e_acsl_offset_12 = __e_acsl_offset((void *)pi);
__e_acsl_assert(__gen_e_acsl_offset_12 == 0UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pi) == 0",33);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_12 == 0UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(pi) == 0",33);
}
__e_acsl_full_init((void *)(& pi));
pi ++;
......@@ -120,8 +132,9 @@ int main(void)
{
int __gen_e_acsl_offset_13;
__gen_e_acsl_offset_13 = __e_acsl_offset((void *)pi);
__e_acsl_assert(__gen_e_acsl_offset_13 == 4UL,(char *)"Assertion",
(char *)"main",(char *)"\\offset(pi) == 4",35);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_13 == 4UL,
(char *)"Assertion",(char *)"main",
(char *)"\\offset(pi) == 4",35);
}
char *p = malloc((unsigned long)12);
__e_acsl_store_block((void *)(& p),(size_t)8);
......@@ -130,22 +143,25 @@ int main(void)
{