diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index 4fe9c71cee4f113df2c108789b383cb290d559cb..9c975cf40a3bfac51dcbbe5093d76274d6c7cc38 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -62,7 +62,7 @@ int main(void)
e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"&x == &x",9);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
index 4fe9c71cee4f113df2c108789b383cb290d559cb..9c975cf40a3bfac51dcbbe5093d76274d6c7cc38 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
@@ -62,7 +62,7 @@ int main(void)
e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"&x == &x",9);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index e258cf1b07fb71d39d832e4efccbc5fd7a9c7cb0..cce8ed65b213091823de8625561196d5cb6ba9af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -112,7 +112,7 @@ int main(void)
e_acsl_assert(4 / y == 2,(char *)"Assertion",(char *)"4/y == 2",33);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
index 1f18e3648dbd55a4e25dcbb42eb2da0470f692b8..3865941f38981cf7cd0db81f4b88775e8f5eda37 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
@@ -169,7 +169,6 @@ int main(void)
__gmpz_clear(__e_acsl_neg);
__gmpz_clear(__e_acsl_x);
}
-
/*@ assert x ≡ -3; */
{
mpz_t __e_acsl_x_2;
@@ -188,7 +187,6 @@ int main(void)
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_neg_2);
}
-
/*@ assert 0 ≢ ~0; */
{
mpz_t __e_acsl_3;
@@ -203,7 +201,6 @@ int main(void)
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_bnot);
}
-
/*@ assert x+1 ≡ -2; */
{
mpz_t __e_acsl_x_3;
@@ -230,7 +227,6 @@ int main(void)
__gmpz_clear(__e_acsl_5);
__gmpz_clear(__e_acsl_neg_3);
}
-
/*@ assert x-1 ≡ -4; */
{
mpz_t __e_acsl_x_4;
@@ -257,7 +253,6 @@ int main(void)
__gmpz_clear(__e_acsl_7);
__gmpz_clear(__e_acsl_neg_4);
}
-
/*@ assert x*3 ≡ -9; */
{
mpz_t __e_acsl_x_5;
@@ -284,7 +279,6 @@ int main(void)
__gmpz_clear(__e_acsl_9);
__gmpz_clear(__e_acsl_neg_5);
}
-
/*@ assert x/3 ≡ -1; */
{
mpz_t __e_acsl_x_6;
@@ -320,7 +314,6 @@ int main(void)
__gmpz_clear(__e_acsl_12);
__gmpz_clear(__e_acsl_neg_6);
}
-
/*@ assert 0xfffffffffff/0xfffffffffff ≡ 1; */
{
mpz_t __e_acsl_13;
@@ -349,7 +342,6 @@ int main(void)
__gmpz_clear(__e_acsl_div_2);
__gmpz_clear(__e_acsl_15);
}
-
/*@ assert x%2 ≡ -1; */
{
mpz_t __e_acsl_x_7;
@@ -385,7 +377,6 @@ int main(void)
__gmpz_clear(__e_acsl_18);
__gmpz_clear(__e_acsl_neg_7);
}
-
/*@ assert -3%-2 ≡ -1; */
{
mpz_t __e_acsl_19;
@@ -429,7 +420,6 @@ int main(void)
__gmpz_clear(__e_acsl_22);
__gmpz_clear(__e_acsl_neg_10);
}
-
/*@ assert 3%-2 ≡ 1; */
{
mpz_t __e_acsl_23;
@@ -465,7 +455,6 @@ int main(void)
__gmpz_clear(__e_acsl_mod_3);
__gmpz_clear(__e_acsl_26);
}
-
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */
{
mpz_t __e_acsl_x_8;
@@ -526,7 +515,6 @@ int main(void)
__gmpz_clear(__e_acsl_30);
__gmpz_clear(__e_acsl_neg_12);
}
-
/*@ assert (0≡1) ≡ !(0≡0); */
{
mpz_t __e_acsl_31;
@@ -559,7 +547,6 @@ int main(void)
__gmpz_clear(__e_acsl_34);
__gmpz_clear(__e_acsl_35);
}
-
/*@ assert (0≤-1) ≡ (0>0); */
{
mpz_t __e_acsl_36;
@@ -590,7 +577,6 @@ int main(void)
__gmpz_clear(__e_acsl_38);
__gmpz_clear(__e_acsl_39);
}
-
/*@ assert (0≥-1) ≡ (0≤0); */
{
mpz_t __e_acsl_40;
@@ -621,7 +607,6 @@ int main(void)
__gmpz_clear(__e_acsl_42);
__gmpz_clear(__e_acsl_43);
}
-
/*@ assert (0≢1) ≡ !(0≢0); */
{
mpz_t __e_acsl_44;
@@ -654,7 +639,6 @@ int main(void)
__gmpz_clear(__e_acsl_47);
__gmpz_clear(__e_acsl_48);
}
-
/*@ assert (0≢0) ≡ !(1≢0); */
{
mpz_t __e_acsl_49;
@@ -687,7 +671,6 @@ int main(void)
__gmpz_clear(__e_acsl_52);
__gmpz_clear(__e_acsl_53);
}
-
/*@ assert 4/y ≡ 2; */
{
mpz_t __e_acsl_54;
@@ -719,10 +702,9 @@ int main(void)
__gmpz_clear(__e_acsl_div_3);
__gmpz_clear(__e_acsl_56);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index 0aa165a1d9b69b865a481703f671a766a12f3fb4..9727892edb47558fd30195233a2c78106d1f8877 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -58,18 +58,22 @@ int T2[4];
int main(void)
{
int __retres;
- { int i;
+ {
+ int i;
i = 0;
while (i < 3) {
T1[i] = i;
- i ++; } }
-
- { int i_0;
+ i ++;
+ }
+ }
+ {
+ int i_0;
i_0 = 0;
while (i_0 < 4) {
T2[i_0] = 2 * i_0;
- i_0 ++; } }
-
+ i_0 ++;
+ }
+ }
/*@ assert T1[0] ≡ T2[0]; */
e_acsl_assert(T1[0] == T2[0],(char *)"Assertion",(char *)"T1[0] == T2[0]",
15);
@@ -78,7 +82,7 @@ int main(void)
16);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
index 03a2e7f920ca827739d9d0b8f5fbae081ba9a555..7b8f9300f2fae871be796123bbaa7fa23988f798 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
@@ -75,18 +75,22 @@ int T2[4];
int main(void)
{
int __retres;
- { int i;
+ {
+ int i;
i = 0;
while (i < 3) {
T1[i] = i;
- i ++; } }
-
- { int i_0;
+ i ++;
+ }
+ }
+ {
+ int i_0;
i_0 = 0;
while (i_0 < 4) {
T2[i_0] = 2 * i_0;
- i_0 ++; } }
-
+ i_0 ++;
+ }
+ }
/*@ assert T1[0] ≡ T2[0]; */
{
mpz_t __e_acsl;
@@ -101,7 +105,6 @@ int main(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
}
-
/*@ assert T1[1] ≢ T2[1]; */
{
mpz_t __e_acsl_3;
@@ -116,10 +119,9 @@ int main(void)
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_4);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index b33883fc2489abef581d31b3e49c512f6d31487f..2b66b54c966910ac36afcdc4a1aeca3c8e1ebfdb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -76,10 +76,9 @@ void f(void)
__e_acsl_at_4 = A;
__e_acsl_at = A;
A = 1;
- F:
- __e_acsl_at_5 = __e_acsl_at_4;
- __e_acsl_at_2 = A;
- A = 2;
+ F: __e_acsl_at_5 = __e_acsl_at_4;
+ __e_acsl_at_2 = A;
+ A = 2;
/*@ assert \at(A,Pre) ≡ 0; */
e_acsl_assert(__e_acsl_at == 0,(char *)"Assertion",
(char *)"\\at(A,Pre) == 0",13);
@@ -117,36 +116,36 @@ void g(int *p, int *q)
__initialize((void *)q,sizeof(int));
*q = 0;
__initialize((void *)p,sizeof(int));
- L1:
- __store_block((void *)(& __e_acsl_at_3),4U);
- __full_init((void *)(& __e_acsl_at_3));
- __e_acsl_at_3 = *q;
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
- __e_acsl_at = *q;
- *p = 2;
+ L1:
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
+ __e_acsl_at_3 = *q;
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
+ __e_acsl_at = *q;
+ *p = 2;
__initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__initialize((void *)q,sizeof(int));
*q = 1;
- L2:
- __store_block((void *)(& __e_acsl_at_2),4U);
- __full_init((void *)(& __e_acsl_at_2));
- __e_acsl_at_2 = *(p + __e_acsl_at);
- A = 4;
+ L2:
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
+ __e_acsl_at_2 = *(p + __e_acsl_at);
+ A = 4;
/*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */
e_acsl_assert(__e_acsl_at_2 == 2,(char *)"Assertion",
(char *)"\\at(*(p+\\at(*q,L1)),L2) == 2",32);
- L3:
- /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */
- __store_block((void *)(& __e_acsl_at_4),4U);
- __full_init((void *)(& __e_acsl_at_4));
- __e_acsl_at_4 = *(p + __e_acsl_at_3);
- e_acsl_assert(__e_acsl_at_4 == 2,(char *)"Assertion",
- (char *)"\\at(*(p+\\at(*q,L1)),Here) == 2",34);
- __delete_block((void *)(& p));
- __delete_block((void *)(& q));
- return;
+ L3:
+ /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
+ __e_acsl_at_4 = *(p + __e_acsl_at_3);
+ e_acsl_assert(__e_acsl_at_4 == 2,(char *)"Assertion",
+ (char *)"\\at(*(p+\\at(*q,L1)),Here) == 2",34);
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& q));
+ return;
}
int main(void)
@@ -161,20 +160,20 @@ int main(void)
__store_block((void *)(& x),4U);
__full_init((void *)(& x));
x = 0;
- L:
- __store_block((void *)(& __e_acsl_at_3),4U);
- __full_init((void *)(& __e_acsl_at_3));
- __e_acsl_at_3 = x;
- __store_block((void *)(& __e_acsl_at_2),8U);
- __full_init((void *)(& __e_acsl_at_2));
- __e_acsl_at_2 = (long long)x + (long long)1;
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
- __e_acsl_at = x;
- /*@ assert x ≡ 0; */
- e_acsl_assert(x == 0,(char *)"Assertion",(char *)"x == 0",45);
- __full_init((void *)(& x));
- x = 1;
+ L:
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
+ __e_acsl_at_3 = x;
+ __store_block((void *)(& __e_acsl_at_2),8U);
+ __full_init((void *)(& __e_acsl_at_2));
+ __e_acsl_at_2 = (long long)x + (long long)1;
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
+ __e_acsl_at = x;
+ /*@ assert x ≡ 0; */
+ e_acsl_assert(x == 0,(char *)"Assertion",(char *)"x == 0",45);
+ __full_init((void *)(& x));
+ x = 1;
__full_init((void *)(& x));
x = 2;
f();
@@ -192,7 +191,7 @@ int main(void)
__delete_block((void *)(t));
__delete_block((void *)(& x));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index 525de6cdafcd1ef9a7b0e50b264e5819aec661fc..80ca4005974afab6e2638fbcc1d18304af2d448c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -117,10 +117,9 @@ void f(void)
__e_acsl_at_4 = A;
__e_acsl_at = A;
A = 1;
- F:
- __e_acsl_at_5 = __e_acsl_at_4;
- __e_acsl_at_2 = A;
- A = 2;
+ F: __e_acsl_at_5 = __e_acsl_at_4;
+ __e_acsl_at_2 = A;
+ A = 2;
/*@ assert \at(A,Pre) ≡ 0; */
{
mpz_t __e_acsl;
@@ -135,7 +134,6 @@ void f(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
}
-
/*@ assert \at(A,F) ≡ 1; */
{
mpz_t __e_acsl_3;
@@ -150,7 +148,6 @@ void f(void)
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_4);
}
-
/*@ assert \at(A,Here) ≡ 2; */
{
mpz_t __e_acsl_5;
@@ -166,7 +163,6 @@ void f(void)
__gmpz_clear(__e_acsl_5);
__gmpz_clear(__e_acsl_6);
}
-
/*@ assert \at(\at(A,Pre),F) ≡ 0; */
{
mpz_t __e_acsl_7;
@@ -181,7 +177,6 @@ void f(void)
__gmpz_clear(__e_acsl_7);
__gmpz_clear(__e_acsl_8);
}
-
A = 3;
{
mpz_t __e_acsl_9;
@@ -198,7 +193,6 @@ void f(void)
__gmpz_clear(__e_acsl_10);
return;
}
-
}
void g(int *p, int *q)
@@ -218,23 +212,23 @@ void g(int *p, int *q)
__initialize((void *)q,sizeof(int));
*q = 0;
__initialize((void *)p,sizeof(int));
- L1:
- __store_block((void *)(& __e_acsl_at_3),4U);
- __full_init((void *)(& __e_acsl_at_3));
- __e_acsl_at_3 = *q;
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
- __e_acsl_at = *q;
- *p = 2;
+ L1:
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
+ __e_acsl_at_3 = *q;
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
+ __e_acsl_at = *q;
+ *p = 2;
__initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__initialize((void *)q,sizeof(int));
*q = 1;
- L2:
- __store_block((void *)(& __e_acsl_at_2),4U);
- __full_init((void *)(& __e_acsl_at_2));
- __e_acsl_at_2 = *(p + (long)__e_acsl_at);
- A = 4;
+ L2:
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
+ __e_acsl_at_2 = *(p + (long)__e_acsl_at);
+ A = 4;
/*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */
{
mpz_t __e_acsl;
@@ -249,29 +243,27 @@ void g(int *p, int *q)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
}
-
- L3:
- /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */
- {
- mpz_t __e_acsl_3;
- mpz_t __e_acsl_4;
- int __e_acsl_eq_2;
- __store_block((void *)(& __e_acsl_at_4),4U);
- __full_init((void *)(& __e_acsl_at_4));
- __e_acsl_at_4 = *(p + (long)__e_acsl_at_3);
- __gmpz_init_set_si(__e_acsl_3,(long)__e_acsl_at_4);
- __gmpz_init_set_si(__e_acsl_4,(long)2);
- __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_3),
- (__mpz_struct const *)(__e_acsl_4));
- e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"\\at(*(p+\\at(*q,L1)),Here) == 2",34);
- __gmpz_clear(__e_acsl_3);
- __gmpz_clear(__e_acsl_4);
- }
-
- __delete_block((void *)(& p));
- __delete_block((void *)(& q));
- return;
+ L3:
+ /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */
+ {
+ mpz_t __e_acsl_3;
+ mpz_t __e_acsl_4;
+ int __e_acsl_eq_2;
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
+ __e_acsl_at_4 = *(p + (long)__e_acsl_at_3);
+ __gmpz_init_set_si(__e_acsl_3,(long)__e_acsl_at_4);
+ __gmpz_init_set_si(__e_acsl_4,(long)2);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_3),
+ (__mpz_struct const *)(__e_acsl_4));
+ e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
+ (char *)"\\at(*(p+\\at(*q,L1)),Here) == 2",34);
+ __gmpz_clear(__e_acsl_3);
+ __gmpz_clear(__e_acsl_4);
+ }
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& q));
+ return;
}
int main(void)
@@ -286,44 +278,42 @@ int main(void)
__store_block((void *)(& x),4U);
__full_init((void *)(& x));
x = 0;
- L:
- __store_block((void *)(& __e_acsl_at_3),4U);
- __full_init((void *)(& __e_acsl_at_3));
- __e_acsl_at_3 = x;
- {
- mpz_t __e_acsl_x_2;
- mpz_t __e_acsl_4;
- mpz_t __e_acsl_add;
- __gmpz_init_set_si(__e_acsl_x_2,(long)x);
- __gmpz_init_set_si(__e_acsl_4,(long)1);
- __gmpz_init(__e_acsl_add);
- __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_x_2),
- (__mpz_struct const *)(__e_acsl_4));
- __gmpz_init_set(__e_acsl_at_2,(__mpz_struct const *)(__e_acsl_add));
- __gmpz_clear(__e_acsl_x_2);
- __gmpz_clear(__e_acsl_4);
- __gmpz_clear(__e_acsl_add);
- }
-
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
- __e_acsl_at = x;
- /*@ assert x ≡ 0; */
- {
- mpz_t __e_acsl_x;
- mpz_t __e_acsl;
- int __e_acsl_eq;
- __gmpz_init_set_si(__e_acsl_x,(long)x);
- __gmpz_init_set_si(__e_acsl,(long)0);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x),
- (__mpz_struct const *)(__e_acsl));
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"x == 0",45);
- __gmpz_clear(__e_acsl_x);
- __gmpz_clear(__e_acsl);
- }
-
- __full_init((void *)(& x));
- x = 1;
+ L:
+ __store_block((void *)(& __e_acsl_at_3),4U);
+ __full_init((void *)(& __e_acsl_at_3));
+ __e_acsl_at_3 = x;
+ {
+ mpz_t __e_acsl_x_2;
+ mpz_t __e_acsl_4;
+ mpz_t __e_acsl_add;
+ __gmpz_init_set_si(__e_acsl_x_2,(long)x);
+ __gmpz_init_set_si(__e_acsl_4,(long)1);
+ __gmpz_init(__e_acsl_add);
+ __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_x_2),
+ (__mpz_struct const *)(__e_acsl_4));
+ __gmpz_init_set(__e_acsl_at_2,(__mpz_struct const *)(__e_acsl_add));
+ __gmpz_clear(__e_acsl_x_2);
+ __gmpz_clear(__e_acsl_4);
+ __gmpz_clear(__e_acsl_add);
+ }
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
+ __e_acsl_at = x;
+ /*@ assert x ≡ 0; */
+ {
+ mpz_t __e_acsl_x;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl_x,(long)x);
+ __gmpz_init_set_si(__e_acsl,(long)0);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"x == 0",45);
+ __gmpz_clear(__e_acsl_x);
+ __gmpz_clear(__e_acsl);
+ }
+ __full_init((void *)(& x));
+ x = 1;
__full_init((void *)(& x));
x = 2;
f();
@@ -341,7 +331,6 @@ int main(void)
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_3);
}
-
/*@ assert \at(x+1,L) ≡ 1; */
{
mpz_t __e_acsl_5;
@@ -353,7 +342,6 @@ int main(void)
(char *)"\\at(x+1,L) == 1",51);
__gmpz_clear(__e_acsl_5);
}
-
/*@ assert \at(x,L)+1 ≡ 1; */
{
mpz_t __e_acsl_6;
@@ -373,14 +361,13 @@ int main(void)
__gmpz_clear(__e_acsl_7);
__gmpz_clear(__e_acsl_add_2);
}
-
g(t,& x);
__retres = 0;
__gmpz_clear(__e_acsl_at_2);
__delete_block((void *)(t));
__delete_block((void *)(& x));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index c55f81da07a23d8d75c1e9fd425fd28882138d43..931da3698735f4fb9cf3036e707f0491acccdbcb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
@@ -114,11 +114,10 @@ int main(void)
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized((union msg *)buf)",25);
}
-
__retres = 0;
__delete_block((void *)(buf));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index c55f81da07a23d8d75c1e9fd425fd28882138d43..931da3698735f4fb9cf3036e707f0491acccdbcb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
@@ -114,11 +114,10 @@ int main(void)
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized((union msg *)buf)",25);
}
-
__retres = 0;
__delete_block((void *)(buf));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index aae8c9dd45a7ccd23578315f5d9c95050b268078..1185d08e199bb14e29de7402b72a517903dbe8f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -121,7 +121,6 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
}
-
{
int __e_acsl_initialized;
int __e_acsl_and;
@@ -136,7 +135,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_read = __valid_read((void *)__e_acsl_at_3,sizeof(float));
__e_acsl_and = __e_acsl_valid_read;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_3)",0);
__e_acsl_initialized_2 = __initialized((void *)(& __e_acsl_at_2),
@@ -147,7 +146,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
sizeof(float));
__e_acsl_and_2 = __e_acsl_valid_read_2;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_2)",0);
__e_acsl_initialized_3 = __initialized((void *)(& __e_acsl_at),
@@ -157,7 +156,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
__e_acsl_and_3 = __e_acsl_valid_read_3;
}
- else { __e_acsl_and_3 = 0; }
+ else __e_acsl_and_3 = 0;
e_acsl_assert(__e_acsl_and_3,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at)",0);
e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + (5 - ((5 / 80) * *__e_acsl_at_3) * 0.4),
@@ -169,7 +168,6 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__delete_block((void *)(& Mtmax_out));
return;
}
-
}
/*@ requires \valid(Mtmin_in);
@@ -232,16 +230,14 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_at = Mtmin_out;
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
}
-
{
int __e_acsl_and;
int __e_acsl_if;
- if (*__e_acsl_at == *__e_acsl_at_2) {
- __e_acsl_and = *__e_acsl_at_3 < 0.85 * *__e_acsl_at_4;
- }
- else { __e_acsl_and = 0; }
- if (__e_acsl_and) { __e_acsl_if = *__e_acsl_at_5 != 0.; }
- else { __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.; }
+ if (*__e_acsl_at == *__e_acsl_at_2) __e_acsl_and = *__e_acsl_at_3 <
+ 0.85 * *__e_acsl_at_4;
+ else __e_acsl_and = 0;
+ if (__e_acsl_and) __e_acsl_if = *__e_acsl_at_5 != 0.;
+ else __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.;
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",
(char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
25);
@@ -250,7 +246,6 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__delete_block((void *)(& Mtmin_out));
return;
}
-
}
int main(void)
@@ -273,7 +268,7 @@ int main(void)
__delete_block((void *)(& g));
__delete_block((void *)(& f));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index d16978e28bf70622f5e1b4af0f6393c0242a89d0..bc77efcd46514e45e61d8ea551a61b278ee46e1d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -165,7 +165,6 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
}
-
{
mpz_t __e_acsl;
mpz_t __e_acsl_2;
@@ -198,7 +197,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_read = __valid_read((void *)__e_acsl_at_3,sizeof(float));
__e_acsl_and = __e_acsl_valid_read;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_3)",0);
__e_acsl_initialized_2 = __initialized((void *)(& __e_acsl_at_2),
@@ -209,7 +208,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
sizeof(float));
__e_acsl_and_2 = __e_acsl_valid_read_2;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at_2)",0);
__e_acsl_initialized_3 = __initialized((void *)(& __e_acsl_at),
@@ -219,7 +218,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
__e_acsl_and_3 = __e_acsl_valid_read_3;
}
- else { __e_acsl_and_3 = 0; }
+ else __e_acsl_and_3 = 0;
e_acsl_assert(__e_acsl_and_3,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(__e_acsl_at)",0);
e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + (5 - (__e_acsl_4 * *__e_acsl_at_3) * 0.4),
@@ -235,7 +234,6 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gmpz_clear(__e_acsl_div);
return;
}
-
}
/*@ requires \valid(Mtmin_in);
@@ -298,7 +296,6 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_at = Mtmin_out;
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
}
-
{
mpz_t __e_acsl_and;
unsigned long __e_acsl_2;
@@ -310,10 +307,10 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gmpz_init_set(__e_acsl_and,(__mpz_struct const *)(__e_acsl));
__gmpz_clear(__e_acsl);
}
- else { __gmpz_init_set_si(__e_acsl_and,0L); }
+ else __gmpz_init_set_si(__e_acsl_and,0L);
__e_acsl_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_and));
- if (__e_acsl_2) { __e_acsl_if = *__e_acsl_at_5 != 0.; }
- else { __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.; }
+ if (__e_acsl_2) __e_acsl_if = *__e_acsl_at_5 != 0.;
+ else __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.;
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",
(char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
25);
@@ -323,7 +320,6 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__gmpz_clear(__e_acsl_and);
return;
}
-
}
int main(void)
@@ -346,7 +342,7 @@ int main(void)
__delete_block((void *)(& g));
__delete_block((void *)(& f));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 0c8681e9eda78d171753f4b457e3f5ac68a7c562..e76ce706a4b10d78e8f4898475039d7188151152 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -83,7 +83,7 @@ int sorted(int *t, int n)
__e_acsl_forall = 1;
__e_acsl_i = (long long)(0 + 1);
while (1) {
- if (__e_acsl_i < n) { ; } else { break; }
+ if (__e_acsl_i < n) ; else break;
{
int __e_acsl_valid_read;
int __e_acsl_valid_read_2;
@@ -96,42 +96,43 @@ int sorted(int *t, int n)
e_acsl_assert(__e_acsl_valid_read_2,(char *)"Postcondition",
(char *)"mem_access: \\valid_read(t+(long long)(__e_acsl_i-(long long)1))",
0);
- if (*(t + (__e_acsl_i - (long long)1)) <= *(t + __e_acsl_i)) { ; }
+ if (*(t + (__e_acsl_i - (long long)1)) <= *(t + __e_acsl_i))
+ ;
else {
__e_acsl_forall = 0;
- goto e_acsl_end_loop1; }
+ goto e_acsl_end_loop1;
+ }
}
-
__e_acsl_i ++;
}
e_acsl_end_loop1: /* internal */ ;
__e_acsl_at = __e_acsl_forall;
}
-
b = 1;
if (n <= 1) {
__retres = 1;
- goto return_label; }
+ goto return_label;
+ }
b = 1;
while (b < n) {
if (*(t + (b - 1)) > *(t + b)) {
__retres = 0;
- goto return_label; }
+ goto return_label;
+ }
b ++;
}
__retres = 1;
- return_label: /* internal */
- {
- int __e_acsl_implies;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = __retres == 1; }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(\\forall long long i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==>\n\\result == 1",
- 9);
- __delete_block((void *)(& t));
- return (__retres);
- }
-
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else __e_acsl_implies = __retres == 1;
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(\\forall long long i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==>\n\\result == 1",
+ 9);
+ __delete_block((void *)(& t));
+ return __retres;
+ }
}
int main(void)
@@ -160,7 +161,7 @@ int main(void)
__retres = 0;
__delete_block((void *)(t));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index c6aafbec4bcc6d75c730dc31415d52fda4436a8a..1bab1c557f72cf97b5947445c8d8677727a9d553 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -144,7 +144,6 @@ int sorted(int *t, int n)
__gmpz_clear(__e_acsl_6);
__gmpz_clear(__e_acsl_add);
}
-
while (1) {
{
mpz_t __e_acsl_n;
@@ -152,10 +151,9 @@ int sorted(int *t, int n)
__gmpz_init_set_si(__e_acsl_n,(long)n);
__e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_i),
(__mpz_struct const *)(__e_acsl_n));
- if (__e_acsl_lt < 0) { ; } else { break; }
+ if (__e_acsl_lt < 0) ; else break;
__gmpz_clear(__e_acsl_n);
}
-
{
mpz_t __e_acsl;
mpz_t __e_acsl_sub;
@@ -178,12 +176,12 @@ int sorted(int *t, int n)
__gmpz_clear(__e_acsl_sub);
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_4);
- if (__e_acsl_le <= 0) { ; }
+ if (__e_acsl_le <= 0) ;
else {
__e_acsl_forall = 0;
- goto e_acsl_end_loop1; }
+ goto e_acsl_end_loop1;
+ }
}
-
{
mpz_t __e_acsl_7;
mpz_t __e_acsl_add_2;
@@ -195,48 +193,47 @@ int sorted(int *t, int n)
__gmpz_clear(__e_acsl_7);
__gmpz_clear(__e_acsl_add_2);
}
-
}
e_acsl_end_loop1: /* internal */ ;
__e_acsl_at = __e_acsl_forall;
__gmpz_clear(__e_acsl_i);
}
-
b = 1;
if (n <= 1) {
__retres = 1;
- goto return_label; }
+ goto return_label;
+ }
b = 1;
while (b < n) {
if (*(t + (b - 1)) > *(t + b)) {
__retres = 0;
- goto return_label; }
+ goto return_label;
+ }
b ++;
}
__retres = 1;
- return_label: /* internal */
- {
- int __e_acsl_implies;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else {
- mpz_t __e_acsl_result;
- mpz_t __e_acsl_8;
- int __e_acsl_eq;
- __gmpz_init_set_si(__e_acsl_result,(long)__retres);
- __gmpz_init_set_si(__e_acsl_8,(long)1);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result),
- (__mpz_struct const *)(__e_acsl_8));
- __e_acsl_implies = __e_acsl_eq == 0;
- __gmpz_clear(__e_acsl_result);
- __gmpz_clear(__e_acsl_8);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else {
+ mpz_t __e_acsl_result;
+ mpz_t __e_acsl_8;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl_result,(long)__retres);
+ __gmpz_init_set_si(__e_acsl_8,(long)1);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result),
+ (__mpz_struct const *)(__e_acsl_8));
+ __e_acsl_implies = __e_acsl_eq == 0;
+ __gmpz_clear(__e_acsl_result);
+ __gmpz_clear(__e_acsl_8);
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(\\forall integer i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==>\n\\result == 1",
+ 9);
+ __delete_block((void *)(& t));
+ return __retres;
}
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(\\forall integer i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==>\n\\result == 1",
- 9);
- __delete_block((void *)(& t));
- return (__retres);
- }
-
}
int main(void)
@@ -273,11 +270,10 @@ int main(void)
__gmpz_clear(__e_acsl_n);
__gmpz_clear(__e_acsl);
}
-
__retres = 0;
__delete_block((void *)(t));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 516aa6bb8a3e0145edf768a431d12b77c6033a6a..36d64a59dace69ea91ff85b3b0010c7a8b7c9daa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -79,7 +79,7 @@ int main(void)
20);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
index fa4a18bac43081867fc24535304f5d4b67e14f87..2cf627edb332cec9ce7501fc9544e70b412d6cdf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
@@ -113,7 +113,6 @@ int main(void)
__gmpz_clear(__e_acsl_cast);
__gmpz_clear(__e_acsl_y);
}
-
/*@ assert x ≡ (long)y; */
{
mpz_t __e_acsl_x;
@@ -128,7 +127,6 @@ int main(void)
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl_cast_2);
}
-
/*@ assert y ≡ (int)0; */
{
mpz_t __e_acsl_y_2;
@@ -143,7 +141,6 @@ int main(void)
__gmpz_clear(__e_acsl_y_2);
__gmpz_clear(__e_acsl_cast_3);
}
-
/*@ assert (unsigned int)y ≡ (unsigned int)0; */
{
mpz_t __e_acsl_cast_4;
@@ -158,7 +155,6 @@ int main(void)
__gmpz_clear(__e_acsl_cast_4);
__gmpz_clear(__e_acsl_cast_5);
}
-
/*@ assert y ≢ (int)0xfffffffffffffff; */
{
mpz_t __e_acsl_y_3;
@@ -178,7 +174,6 @@ int main(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_cast_6);
}
-
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */
{
mpz_t __e_acsl_cast_7;
@@ -200,10 +195,9 @@ int main(void)
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_cast_8);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 37b420d66f827afb268441017ee538ad901918da..d3ee38f6b75a60541ac8935b322d2d23d5d7d9df 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -111,7 +111,7 @@ int main(void)
e_acsl_assert(1 != -2,(char *)"Assertion",(char *)"1 != -2",29);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index 909225b9ca8550f58699aee71e3ea4c4550b61a9..80854e2e1b1b38b1ed867801323de57239fe4fba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -112,7 +112,6 @@ int main(void)
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl_y);
}
-
/*@ assert y > x; */
{
mpz_t __e_acsl_y_2;
@@ -126,7 +125,6 @@ int main(void)
__gmpz_clear(__e_acsl_y_2);
__gmpz_clear(__e_acsl_x_2);
}
-
/*@ assert x ≤ 0; */
{
mpz_t __e_acsl_x_3;
@@ -140,7 +138,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_3);
__gmpz_clear(__e_acsl);
}
-
/*@ assert y ≥ 1; */
{
mpz_t __e_acsl_y_3;
@@ -154,7 +151,6 @@ int main(void)
__gmpz_clear(__e_acsl_y_3);
__gmpz_clear(__e_acsl_2);
}
-
__e_acsl_literal_string = "toto";
__store_block((void *)__e_acsl_literal_string,sizeof("toto"));
__full_init((void *)__e_acsl_literal_string);
@@ -175,7 +171,6 @@ int main(void)
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_4);
}
-
/*@ assert 32 > 3; */
{
mpz_t __e_acsl_5;
@@ -189,7 +184,6 @@ int main(void)
__gmpz_clear(__e_acsl_5);
__gmpz_clear(__e_acsl_6);
}
-
/*@ assert 12 ≤ 13; */
{
mpz_t __e_acsl_7;
@@ -204,7 +198,6 @@ int main(void)
__gmpz_clear(__e_acsl_7);
__gmpz_clear(__e_acsl_8);
}
-
/*@ assert 123 ≥ 12; */
{
mpz_t __e_acsl_9;
@@ -219,7 +212,6 @@ int main(void)
__gmpz_clear(__e_acsl_9);
__gmpz_clear(__e_acsl_10);
}
-
/*@ assert 0xff ≡ 0xff; */
{
mpz_t __e_acsl_11;
@@ -231,7 +223,6 @@ int main(void)
(char *)"0xff == 0xff",21);
__gmpz_clear(__e_acsl_11);
}
-
/*@ assert 1 ≢ 2; */
{
mpz_t __e_acsl_12;
@@ -245,7 +236,6 @@ int main(void)
__gmpz_clear(__e_acsl_12);
__gmpz_clear(__e_acsl_13);
}
-
/*@ assert -5 < 18; */
{
mpz_t __e_acsl_14;
@@ -263,7 +253,6 @@ int main(void)
__gmpz_clear(__e_acsl_neg);
__gmpz_clear(__e_acsl_15);
}
-
/*@ assert 32 > -3; */
{
mpz_t __e_acsl_16;
@@ -281,7 +270,6 @@ int main(void)
__gmpz_clear(__e_acsl_17);
__gmpz_clear(__e_acsl_neg_2);
}
-
/*@ assert -12 ≤ 13; */
{
mpz_t __e_acsl_18;
@@ -300,7 +288,6 @@ int main(void)
__gmpz_clear(__e_acsl_neg_3);
__gmpz_clear(__e_acsl_19);
}
-
/*@ assert 123 ≥ -12; */
{
mpz_t __e_acsl_20;
@@ -319,7 +306,6 @@ int main(void)
__gmpz_clear(__e_acsl_21);
__gmpz_clear(__e_acsl_neg_4);
}
-
/*@ assert -0xff ≡ -0xff; */
{
mpz_t __e_acsl_22;
@@ -335,7 +321,6 @@ int main(void)
__gmpz_clear(__e_acsl_22);
__gmpz_clear(__e_acsl_neg_5);
}
-
/*@ assert 1 ≢ -2; */
{
mpz_t __e_acsl_23;
@@ -354,10 +339,9 @@ int main(void)
__gmpz_clear(__e_acsl_24);
__gmpz_clear(__e_acsl_neg_6);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index 269d857ccad80d3e8b438778ab59ab990f2bdb63..4c44a28c32c835817dcf2c83a3b5a4ce14f50b8e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -58,13 +58,12 @@ int main(void)
int __retres;
int x;
x = 0;
- if (x) {
+ if (x)
/*@ assert \false; */
e_acsl_assert(0,(char *)"Assertion",(char *)"\\false",8);
- }
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
index 269d857ccad80d3e8b438778ab59ab990f2bdb63..4c44a28c32c835817dcf2c83a3b5a4ce14f50b8e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
@@ -58,13 +58,12 @@ int main(void)
int __retres;
int x;
x = 0;
- if (x) {
+ if (x)
/*@ assert \false; */
e_acsl_assert(0,(char *)"Assertion",(char *)"\\false",8);
- }
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index cd9b58ab0ff62674f928c7eadcb705f16aca7be3..c3906a3387c05ba3ad38e183ffdc831f0d2c0928 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -131,24 +131,21 @@ void k(void)
int __e_acsl_implies_2;
int __e_acsl_and_2;
int __e_acsl_implies_3;
- if (! (X == 1)) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = X == 0; }
+ if (! (X == 1)) __e_acsl_implies = 1; else __e_acsl_implies = X == 0;
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",
(char *)"X == 1 ==> X == 0",40);
- if (X == 3) { __e_acsl_and = Y == 2; } else { __e_acsl_and = 0; }
- if (! __e_acsl_and) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = X == 3; }
+ if (X == 3) __e_acsl_and = Y == 2; else __e_acsl_and = 0;
+ if (! __e_acsl_and) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = X == 3;
e_acsl_assert(__e_acsl_implies_2,(char *)"Precondition",
(char *)"X == 3 && Y == 2 ==> X == 3",44);
- if (X == 3) { __e_acsl_and_2 = Y == 2; } else { __e_acsl_and_2 = 0; }
- if (! __e_acsl_and_2) { __e_acsl_implies_3 = 1; }
- else { __e_acsl_implies_3 = (long long)X + (long long)Y == (long long)5;
- }
+ if (X == 3) __e_acsl_and_2 = Y == 2; else __e_acsl_and_2 = 0;
+ if (! __e_acsl_and_2) __e_acsl_implies_3 = 1;
+ else __e_acsl_implies_3 = (long long)X + (long long)Y == (long long)5;
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",
(char *)"X == 3 && Y == 2 ==> X+Y == 5",45);
X += Y;
}
-
return;
}
@@ -158,7 +155,7 @@ int l(void)
/*@ assert Y ≡ 2; */
e_acsl_assert(Y == 2,(char *)"Assertion",(char *)"Y == 2",51);
e_acsl_assert(X == 5,(char *)"Postcondition",(char *)"X == 5",49);
- return (X);
+ return X;
}
/*@ behavior b1:
@@ -180,39 +177,33 @@ void m(void)
__e_acsl_at_4 = X;
{
int __e_acsl_and_2;
- if (X == 5) { __e_acsl_and_2 = Y == 2; } else { __e_acsl_and_2 = 0; }
+ if (X == 5) __e_acsl_and_2 = Y == 2; else __e_acsl_and_2 = 0;
__e_acsl_at_3 = __e_acsl_and_2;
}
-
{
int __e_acsl_and;
- if (X == 5) { __e_acsl_and = Y == 2; } else { __e_acsl_and = 0; }
+ if (X == 5) __e_acsl_and = Y == 2; else __e_acsl_and = 0;
__e_acsl_at_2 = __e_acsl_and;
}
-
__e_acsl_at = X == 7;
X += Y;
{
int __e_acsl_implies;
int __e_acsl_implies_2;
int __e_acsl_implies_3;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = X == 95; }
+ if (! __e_acsl_at) __e_acsl_implies = 1; else __e_acsl_implies = X == 95;
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
(char *)"\\old(X == 7) ==> X == 95",58);
- if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = X == 7; }
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = X == 7;
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"\\old(X == 5 && Y == 2) ==> X == 7",62);
- if (! __e_acsl_at_3) { __e_acsl_implies_3 = 1; }
- else {
- __e_acsl_implies_3 = (long long)X == (long long)__e_acsl_at_4 + (long long)Y;
- }
+ if (! __e_acsl_at_3) __e_acsl_implies_3 = 1;
+ else __e_acsl_implies_3 = (long long)X == (long long)__e_acsl_at_4 + (long long)Y;
e_acsl_assert(__e_acsl_implies_3,(char *)"Postcondition",
(char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",63);
return;
}
-
}
/*@ requires X > 0;
@@ -238,17 +229,15 @@ void n(void)
{
int __e_acsl_implies;
int __e_acsl_implies_2;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = X == 8; }
+ if (! __e_acsl_at) __e_acsl_implies = 1; else __e_acsl_implies = X == 8;
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
(char *)"\\old(X == 7) ==> X == 8",71);
- if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = X == 98; }
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = X == 98;
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"\\old(X == 5) ==> X == 98",74);
return;
}
-
}
int main(void)
@@ -265,7 +254,7 @@ int main(void)
n();
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
index 6da7fdbc42480a693564e270d64ebb2827a69f00..8850c513f5309a6d39ee854095762f049ff7d332 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -105,7 +105,6 @@ void f(void)
__gmpz_clear(__e_acsl);
return;
}
-
}
/*@ ensures X ≡ 2;
@@ -135,7 +134,6 @@ void g(void)
__gmpz_clear(__e_acsl_Y);
return;
}
-
}
/*@ requires X ≡ 2; */
@@ -155,7 +153,6 @@ void h(void)
__gmpz_clear(__e_acsl);
X ++;
}
-
return;
}
@@ -188,7 +185,6 @@ void i(void)
__gmpz_clear(__e_acsl_2);
X += Y;
}
-
return;
}
@@ -241,7 +237,6 @@ void j(void)
__gmpz_clear(__e_acsl_3);
X = 3;
}
-
{
mpz_t __e_acsl_X_2;
mpz_t __e_acsl_4;
@@ -272,7 +267,6 @@ void j(void)
__gmpz_clear(__e_acsl_add_2);
return;
}
-
}
/*@ behavior b1:
@@ -303,7 +297,7 @@ void k(void)
__gmpz_init_set_si(__e_acsl,(long)1);
__e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
(__mpz_struct const *)(__e_acsl));
- if (! (__e_acsl_eq == 0)) { __e_acsl_implies = 1; }
+ if (! (__e_acsl_eq == 0)) __e_acsl_implies = 1;
else {
mpz_t __e_acsl_X_2;
mpz_t __e_acsl_2;
@@ -333,8 +327,8 @@ void k(void)
__gmpz_clear(__e_acsl_Y);
__gmpz_clear(__e_acsl_4);
}
- else { __e_acsl_and = 0; }
- if (! __e_acsl_and) { __e_acsl_implies_2 = 1; }
+ else __e_acsl_and = 0;
+ if (! __e_acsl_and) __e_acsl_implies_2 = 1;
else {
mpz_t __e_acsl_X_3;
mpz_t __e_acsl_5;
@@ -363,8 +357,8 @@ void k(void)
__gmpz_clear(__e_acsl_Y_2);
__gmpz_clear(__e_acsl_6);
}
- else { __e_acsl_and_2 = 0; }
- if (! __e_acsl_and_2) { __e_acsl_implies_3 = 1; }
+ else __e_acsl_and_2 = 0;
+ if (! __e_acsl_and_2) __e_acsl_implies_3 = 1;
else {
mpz_t __e_acsl_X_4;
mpz_t __e_acsl_Y_3;
@@ -392,7 +386,6 @@ void k(void)
__gmpz_clear(__e_acsl_3);
X += Y;
}
-
return;
}
@@ -412,7 +405,6 @@ int l(void)
__gmpz_clear(__e_acsl_Y);
__gmpz_clear(__e_acsl);
}
-
{
mpz_t __e_acsl_X;
mpz_t __e_acsl_2;
@@ -425,9 +417,8 @@ int l(void)
(char *)"X == 5",49);
__gmpz_clear(__e_acsl_X);
__gmpz_clear(__e_acsl_2);
- return (X);
+ return X;
}
-
}
/*@ behavior b1:
@@ -468,12 +459,11 @@ void m(void)
__gmpz_clear(__e_acsl_Y_2);
__gmpz_clear(__e_acsl_7);
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_at_3 = __e_acsl_and_2;
__gmpz_clear(__e_acsl_X_5);
__gmpz_clear(__e_acsl_6);
}
-
{
mpz_t __e_acsl_X_3;
mpz_t __e_acsl_3;
@@ -495,12 +485,11 @@ void m(void)
__gmpz_clear(__e_acsl_Y);
__gmpz_clear(__e_acsl_4);
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
__e_acsl_at_2 = __e_acsl_and;
__gmpz_clear(__e_acsl_X_3);
__gmpz_clear(__e_acsl_3);
}
-
{
mpz_t __e_acsl_X;
mpz_t __e_acsl;
@@ -513,13 +502,12 @@ void m(void)
__gmpz_clear(__e_acsl_X);
__gmpz_clear(__e_acsl);
}
-
X += Y;
{
int __e_acsl_implies;
int __e_acsl_implies_2;
int __e_acsl_implies_3;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ if (! __e_acsl_at) __e_acsl_implies = 1;
else {
mpz_t __e_acsl_X_2;
mpz_t __e_acsl_2;
@@ -534,7 +522,7 @@ void m(void)
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
(char *)"\\old(X == 7) ==> X == 95",58);
- if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
else {
mpz_t __e_acsl_X_4;
mpz_t __e_acsl_5;
@@ -549,7 +537,7 @@ void m(void)
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"\\old(X == 5 && Y == 2) ==> X == 7",62);
- if (! __e_acsl_at_3) { __e_acsl_implies_3 = 1; }
+ if (! __e_acsl_at_3) __e_acsl_implies_3 = 1;
else {
mpz_t __e_acsl_X_6;
mpz_t __e_acsl_8;
@@ -574,7 +562,6 @@ void m(void)
(char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",63);
return;
}
-
}
/*@ requires X > 0;
@@ -622,7 +609,6 @@ void n(void)
__gmpz_clear(__e_acsl_X_4);
__gmpz_clear(__e_acsl_5);
}
-
{
mpz_t __e_acsl_X_2;
mpz_t __e_acsl_3;
@@ -635,14 +621,12 @@ void n(void)
__gmpz_clear(__e_acsl_X_2);
__gmpz_clear(__e_acsl_3);
}
-
X ++;
}
-
{
int __e_acsl_implies;
int __e_acsl_implies_2;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ if (! __e_acsl_at) __e_acsl_implies = 1;
else {
mpz_t __e_acsl_X_3;
mpz_t __e_acsl_4;
@@ -657,7 +641,7 @@ void n(void)
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
(char *)"\\old(X == 7) ==> X == 8",71);
- if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
else {
mpz_t __e_acsl_X_5;
mpz_t __e_acsl_6;
@@ -674,7 +658,6 @@ void n(void)
(char *)"\\old(X == 5) ==> X == 98",74);
return;
}
-
}
int main(void)
@@ -691,7 +674,7 @@ int main(void)
n();
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 7f62a62af5b18e4a2939bf7e878c56165fed28b4..5f1b6b27afa6fa58c03b4e741e6d6053079d67e9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -100,10 +100,9 @@ int main(void)
13);
__gmpz_clear(__e_acsl);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index bed5fafffe4203d086d1455a920b009e8c1e0124..fb73f92a1d2946911a9a6a891353ca7151e40955 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -94,7 +94,6 @@ int main(void)
e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",8);
__gmpz_clear(__e_acsl);
}
-
x = 0;
x ++;
/*@ assert 0 ≢ 1; */
@@ -110,7 +109,6 @@ int main(void)
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_3);
}
-
/*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
{
mpz_t __e_acsl_4;
@@ -122,7 +120,6 @@ int main(void)
(char *)"1152921504606846975 == 0xfffffffffffffff",11);
__gmpz_clear(__e_acsl_4);
}
-
/*@ assert
0xffffffffffffffffffffffffffffffff ≡
0xffffffffffffffffffffffffffffffff;
@@ -139,10 +136,9 @@ int main(void)
13);
__gmpz_clear(__e_acsl_5);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index 514a0f203f536b15af488c470d412e07e2453bcd..2413b7391249e78325f198ff6bb47eb60036e407 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
@@ -65,21 +65,19 @@ int main(void)
/*@ invariant 0 ≤ i ∧ i < 10; */
{
int __e_acsl_and;
- if (0 <= i) { __e_acsl_and = i < 10; } else { __e_acsl_and = 0; }
+ if (0 <= i) __e_acsl_and = i < 10; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",
(char *)"0 <= i && i < 10",9);
}
-
x += i;
/*@ invariant i ≤ x; */
e_acsl_assert(i <= x,(char *)"Invariant",(char *)"i <= x",11);
i ++;
}
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
index f2f2b377680c303466354d3a1710e3a7b3711378..23e88aaa0e4a6de7f8481b818cab7c43687020f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
@@ -101,13 +101,12 @@ int main(void)
__gmpz_clear(__e_acsl_i_2);
__gmpz_clear(__e_acsl_2);
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",
(char *)"0 <= i && i < 10",9);
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_i);
}
-
x += i;
/*@ invariant i ≤ x; */
{
@@ -123,14 +122,12 @@ int main(void)
__gmpz_clear(__e_acsl_i_3);
__gmpz_clear(__e_acsl_x);
}
-
i ++;
}
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index dc42cb828f61519558357966f7369b251c691e3f..90363b430163fa865908cd0fc6819563b76dc74e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -59,29 +59,29 @@ int main(void)
{
int __retres;
goto L1;
- L1:
- /*@ assert X ≡ 0; */
- e_acsl_assert(X == 0,(char *)"Assertion",(char *)"X == 0",12);
- X = 1;
+ L1:
+ /*@ assert X ≡ 0; */
+ e_acsl_assert(X == 0,(char *)"Assertion",(char *)"X == 0",12);
+ X = 1;
goto L2;
- L2:
- /*@ requires X ≡ 1;
- ensures X ≡ 2; */
- {
- e_acsl_assert(X == 1,(char *)"Precondition",(char *)"X == 1",14);
- X = 2;
- e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"X == 2",14);
- }
-
+ L2:
+ /*@ requires X ≡ 1;
+ ensures X ≡ 2; */
+ {
+ e_acsl_assert(X == 1,(char *)"Precondition",(char *)"X == 1",14);
+ X = 2;
+ e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"X == 2",14);
+ }
if (X) {
X = 3;
__retres = 0;
- goto return_label; }
+ goto return_label;
+ }
__retres = 0;
- return_label: /* internal */
- e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"X == 3",9);
- __clean();
- return (__retres);
+ return_label: /* internal */
+ e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"X == 3",9);
+ __clean();
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
index 59880e9df060171b9449cd0504944d6a50020fd3..b123f842db0f24d169184c75c9ade308d54498ae 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -76,77 +76,74 @@ int main(void)
{
int __retres;
goto L1;
- L1:
- /*@ assert X ≡ 0; */
- {
- mpz_t __e_acsl_X;
- mpz_t __e_acsl;
- int __e_acsl_eq;
- __gmpz_init_set_si(__e_acsl_X,(long)X);
- __gmpz_init_set_si(__e_acsl,(long)0);
- __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
- (__mpz_struct const *)(__e_acsl));
- e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"X == 0",12);
- __gmpz_clear(__e_acsl_X);
- __gmpz_clear(__e_acsl);
- }
-
- X = 1;
+ L1:
+ /*@ assert X ≡ 0; */
+ {
+ mpz_t __e_acsl_X;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl_X,(long)X);
+ __gmpz_init_set_si(__e_acsl,(long)0);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"X == 0",12);
+ __gmpz_clear(__e_acsl_X);
+ __gmpz_clear(__e_acsl);
+ }
+ X = 1;
goto L2;
- L2:
- /*@ requires X ≡ 1;
- ensures X ≡ 2; */
- {
- mpz_t __e_acsl_X_3;
- mpz_t __e_acsl_3;
- int __e_acsl_eq_3;
+ L2:
+ /*@ requires X ≡ 1;
+ ensures X ≡ 2; */
{
- mpz_t __e_acsl_X_2;
- mpz_t __e_acsl_2;
- int __e_acsl_eq_2;
- __gmpz_init_set_si(__e_acsl_X_2,(long)X);
- __gmpz_init_set_si(__e_acsl_2,(long)1);
- __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_2),
- (__mpz_struct const *)(__e_acsl_2));
- e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Precondition",
- (char *)"X == 1",14);
- __gmpz_clear(__e_acsl_X_2);
- __gmpz_clear(__e_acsl_2);
- X = 2;
+ mpz_t __e_acsl_X_3;
+ mpz_t __e_acsl_3;
+ int __e_acsl_eq_3;
+ {
+ mpz_t __e_acsl_X_2;
+ mpz_t __e_acsl_2;
+ int __e_acsl_eq_2;
+ __gmpz_init_set_si(__e_acsl_X_2,(long)X);
+ __gmpz_init_set_si(__e_acsl_2,(long)1);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_2),
+ (__mpz_struct const *)(__e_acsl_2));
+ e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Precondition",
+ (char *)"X == 1",14);
+ __gmpz_clear(__e_acsl_X_2);
+ __gmpz_clear(__e_acsl_2);
+ X = 2;
+ }
+ __gmpz_init_set_si(__e_acsl_X_3,(long)X);
+ __gmpz_init_set_si(__e_acsl_3,(long)2);
+ __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_3),
+ (__mpz_struct const *)(__e_acsl_3));
+ e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Postcondition",
+ (char *)"X == 2",14);
+ __gmpz_clear(__e_acsl_X_3);
+ __gmpz_clear(__e_acsl_3);
}
-
- __gmpz_init_set_si(__e_acsl_X_3,(long)X);
- __gmpz_init_set_si(__e_acsl_3,(long)2);
- __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_3),
- (__mpz_struct const *)(__e_acsl_3));
- e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Postcondition",
- (char *)"X == 2",14);
- __gmpz_clear(__e_acsl_X_3);
- __gmpz_clear(__e_acsl_3);
- }
-
if (X) {
X = 3;
__retres = 0;
- goto return_label; }
- __retres = 0;
- return_label: /* internal */
- {
- mpz_t __e_acsl_X_4;
- mpz_t __e_acsl_4;
- int __e_acsl_eq_4;
- __gmpz_init_set_si(__e_acsl_X_4,(long)X);
- __gmpz_init_set_si(__e_acsl_4,(long)3);
- __e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_4),
- (__mpz_struct const *)(__e_acsl_4));
- e_acsl_assert(__e_acsl_eq_4 == 0,(char *)"Postcondition",
- (char *)"X == 3",9);
- __gmpz_clear(__e_acsl_X_4);
- __gmpz_clear(__e_acsl_4);
- __clean();
- return (__retres);
+ goto return_label;
}
-
+ __retres = 0;
+ return_label: /* internal */
+ {
+ mpz_t __e_acsl_X_4;
+ mpz_t __e_acsl_4;
+ int __e_acsl_eq_4;
+ __gmpz_init_set_si(__e_acsl_X_4,(long)X);
+ __gmpz_init_set_si(__e_acsl_4,(long)3);
+ __e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X_4),
+ (__mpz_struct const *)(__e_acsl_4));
+ e_acsl_assert(__e_acsl_eq_4 == 0,(char *)"Postcondition",
+ (char *)"X == 3",9);
+ __gmpz_clear(__e_acsl_X_4);
+ __gmpz_clear(__e_acsl_4);
+ __clean();
+ return __retres;
+ }
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index bf25d56191fa396ba62d94bc7a11ef604f2b8f1b..54a7466540d0d78adee3c6ef9ee936cb1356760e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -63,160 +63,139 @@ int main(void)
/*@ assert x ≡ 0 ∧ y ≡ 1; */
{
int __e_acsl_and;
- if (x == 0) { __e_acsl_and = y == 1; } else { __e_acsl_and = 0; }
+ if (x == 0) __e_acsl_and = y == 1; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",
(char *)"x == 0 && y == 1",11);
}
-
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */
{
int __e_acsl_and_2;
- if (x != 0) { __e_acsl_and_2 = y == 1 / 0; } else { __e_acsl_and_2 = 0; }
+ if (x != 0) __e_acsl_and_2 = y == 1 / 0; else __e_acsl_and_2 = 0;
e_acsl_assert(! __e_acsl_and_2,(char *)"Assertion",
(char *)"!(x != 0 && y == 1/0)",12);
}
-
/*@ assert y ≡ 1 ∨ x ≡ 1; */
{
int __e_acsl_or;
- if (y == 1) { __e_acsl_or = 1; } else { __e_acsl_or = x == 1; }
+ if (y == 1) __e_acsl_or = 1; else __e_acsl_or = x == 1;
e_acsl_assert(__e_acsl_or,(char *)"Assertion",(char *)"y == 1 || x == 1",
13);
}
-
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */
{
int __e_acsl_or_2;
- if (x == 0) { __e_acsl_or_2 = 1; } else { __e_acsl_or_2 = y == 1 / 0; }
+ if (x == 0) __e_acsl_or_2 = 1; else __e_acsl_or_2 = y == 1 / 0;
e_acsl_assert(__e_acsl_or_2,(char *)"Assertion",
(char *)"x == 0 || y == 1/0",14);
}
-
/*@ assert x ≡ 0 ⇒ y ≡ 1; */
{
int __e_acsl_implies;
- if (! (x == 0)) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = y == 1; }
+ if (! (x == 0)) __e_acsl_implies = 1; else __e_acsl_implies = y == 1;
e_acsl_assert(__e_acsl_implies,(char *)"Assertion",
(char *)"x == 0 ==> y == 1",15);
}
-
/*@ assert x ≡ 1 ⇒ y ≡ 1/0; */
{
int __e_acsl_implies_2;
- if (! (x == 1)) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = y == 1 / 0; }
+ if (! (x == 1)) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = y == 1 / 0;
e_acsl_assert(__e_acsl_implies_2,(char *)"Assertion",
(char *)"x == 1 ==> y == 1/0",16);
}
-
/*@ assert x≢0? x ≢ 0: y ≢ 0; */
{
int __e_acsl_if;
- if (x != 0) { __e_acsl_if = x != 0; } else { __e_acsl_if = y != 0; }
+ if (x != 0) __e_acsl_if = x != 0; else __e_acsl_if = y != 0;
e_acsl_assert(__e_acsl_if,(char *)"Assertion",
(char *)"x!=0? x != 0: y != 0",17);
}
-
/*@ assert y≢0? y ≢ 0: x ≢ 0; */
{
int __e_acsl_if_2;
- if (y != 0) { __e_acsl_if_2 = y != 0; } else { __e_acsl_if_2 = x != 0; }
+ if (y != 0) __e_acsl_if_2 = y != 0; else __e_acsl_if_2 = x != 0;
e_acsl_assert(__e_acsl_if_2,(char *)"Assertion",
(char *)"y!=0? y != 0: x != 0",18);
}
-
/*@ assert x≡1? x ≡ 18: x ≡ 0; */
{
int __e_acsl_if_3;
- if (x == 1) { __e_acsl_if_3 = x == 18; } else { __e_acsl_if_3 = x == 0; }
+ if (x == 1) __e_acsl_if_3 = x == 18; else __e_acsl_if_3 = x == 0;
e_acsl_assert(__e_acsl_if_3,(char *)"Assertion",
(char *)"x==1? x == 18: x == 0",19);
}
-
/*@ assert x ≡ 2 ⇔ y ≡ 3; */
{
int __e_acsl_implies_3;
int __e_acsl_equiv;
- if (! (x == 2)) { __e_acsl_implies_3 = 1; }
- else { __e_acsl_implies_3 = y == 3; }
+ if (! (x == 2)) __e_acsl_implies_3 = 1; else __e_acsl_implies_3 = y == 3;
if (__e_acsl_implies_3) {
int __e_acsl_implies_4;
- if (! (y == 3)) { __e_acsl_implies_4 = 1; }
- else { __e_acsl_implies_4 = x == 2; }
+ if (! (y == 3)) __e_acsl_implies_4 = 1;
+ else __e_acsl_implies_4 = x == 2;
__e_acsl_equiv = __e_acsl_implies_4;
}
- else { __e_acsl_equiv = 0; }
+ else __e_acsl_equiv = 0;
e_acsl_assert(__e_acsl_equiv,(char *)"Assertion",
(char *)"x == 2 <==> y == 3",22);
}
-
/*@ assert x ≡ 0 ⇔ y ≡ 1; */
{
int __e_acsl_implies_5;
int __e_acsl_equiv_2;
- if (! (x == 0)) { __e_acsl_implies_5 = 1; }
- else { __e_acsl_implies_5 = y == 1; }
+ if (! (x == 0)) __e_acsl_implies_5 = 1; else __e_acsl_implies_5 = y == 1;
if (__e_acsl_implies_5) {
int __e_acsl_implies_6;
- if (! (y == 1)) { __e_acsl_implies_6 = 1; }
- else { __e_acsl_implies_6 = x == 0; }
+ if (! (y == 1)) __e_acsl_implies_6 = 1;
+ else __e_acsl_implies_6 = x == 0;
__e_acsl_equiv_2 = __e_acsl_implies_6;
}
- else { __e_acsl_equiv_2 = 0; }
+ else __e_acsl_equiv_2 = 0;
e_acsl_assert(__e_acsl_equiv_2,(char *)"Assertion",
(char *)"x == 0 <==> y == 1",23);
}
-
/*@ assert ((x≢0? x: y)≢0) ≡ (x≡0); */
{
int __e_acsl_if_4;
- if (x != 0) { __e_acsl_if_4 = x; } else { __e_acsl_if_4 = y; }
+ if (x != 0) __e_acsl_if_4 = x; else __e_acsl_if_4 = y;
e_acsl_assert((__e_acsl_if_4 != 0) == (x == 0),(char *)"Assertion",
(char *)"((x!=0? x: y)!=0) == (x==0)",26);
}
-
/*@ assert (x ≢ 0 ∧ y ≢ 0) ∨ y ≢ 0; */
{
int __e_acsl_and_3;
int __e_acsl_or_3;
- if (x != 0) { __e_acsl_and_3 = y != 0; } else { __e_acsl_and_3 = 0; }
- if (__e_acsl_and_3) { __e_acsl_or_3 = 1; }
- else { __e_acsl_or_3 = y != 0; }
+ if (x != 0) __e_acsl_and_3 = y != 0; else __e_acsl_and_3 = 0;
+ if (__e_acsl_and_3) __e_acsl_or_3 = 1; else __e_acsl_or_3 = y != 0;
e_acsl_assert(__e_acsl_or_3,(char *)"Assertion",
(char *)"(x != 0 && y != 0) || y != 0",27);
}
-
/*@ assert (x ≢ 0 ∨ y ≢ 0) ∧ y ≡ 1; */
{
int __e_acsl_or_4;
int __e_acsl_and_4;
- if (x != 0) { __e_acsl_or_4 = 1; } else { __e_acsl_or_4 = y != 0; }
- if (__e_acsl_or_4) { __e_acsl_and_4 = y == 1; }
- else { __e_acsl_and_4 = 0; }
+ if (x != 0) __e_acsl_or_4 = 1; else __e_acsl_or_4 = y != 0;
+ if (__e_acsl_or_4) __e_acsl_and_4 = y == 1; else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
(char *)"(x != 0 || y != 0) && y == 1",28);
}
-
/*@ assert (x≢0∨y≢0) ≡ (y≢0); */
{
int __e_acsl_or_5;
- if (x != 0) { __e_acsl_or_5 = 1; } else { __e_acsl_or_5 = y != 0; }
+ if (x != 0) __e_acsl_or_5 = 1; else __e_acsl_or_5 = y != 0;
e_acsl_assert(__e_acsl_or_5 == (y != 0),(char *)"Assertion",
(char *)"(x!=0||y!=0) == (y!=0)",29);
}
-
/*@ assert (x≢0∧y≢0) ≡ (x≢0); */
{
int __e_acsl_and_5;
- if (x != 0) { __e_acsl_and_5 = y != 0; } else { __e_acsl_and_5 = 0; }
+ if (x != 0) __e_acsl_and_5 = y != 0; else __e_acsl_and_5 = 0;
e_acsl_assert(__e_acsl_and_5 == (x != 0),(char *)"Assertion",
(char *)"(x!=0&&y!=0) == (x!=0)",30);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
index a5c8c7253400c62d2c08bb0167a1ea95584cf39a..da8b7fe824dca269f0ad3ce941ef31f45ac9abb7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
@@ -123,13 +123,12 @@ int main(void)
__gmpz_clear(__e_acsl_y);
__gmpz_clear(__e_acsl_2);
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",
(char *)"x == 0 && y == 1",11);
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl);
}
-
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */
{
mpz_t __e_acsl_x_2;
@@ -166,13 +165,12 @@ int main(void)
__gmpz_clear(__e_acsl_5);
__gmpz_clear(__e_acsl_div);
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
e_acsl_assert(! __e_acsl_and_2,(char *)"Assertion",
(char *)"!(x != 0 && y == 1/0)",12);
__gmpz_clear(__e_acsl_x_2);
__gmpz_clear(__e_acsl_3);
}
-
/*@ assert y ≡ 1 ∨ x ≡ 1; */
{
mpz_t __e_acsl_y_3;
@@ -183,7 +181,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_6,(long)1);
__e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y_3),
(__mpz_struct const *)(__e_acsl_6));
- if (__e_acsl_eq_4 == 0) { __e_acsl_or = 1; }
+ if (__e_acsl_eq_4 == 0) __e_acsl_or = 1;
else {
mpz_t __e_acsl_x_3;
mpz_t __e_acsl_7;
@@ -201,7 +199,6 @@ int main(void)
__gmpz_clear(__e_acsl_y_3);
__gmpz_clear(__e_acsl_6);
}
-
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */
{
mpz_t __e_acsl_x_4;
@@ -212,7 +209,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_8,(long)0);
__e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_4),
(__mpz_struct const *)(__e_acsl_8));
- if (__e_acsl_eq_6 == 0) { __e_acsl_or_2 = 1; }
+ if (__e_acsl_eq_6 == 0) __e_acsl_or_2 = 1;
else {
mpz_t __e_acsl_y_4;
mpz_t __e_acsl_9;
@@ -244,7 +241,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_4);
__gmpz_clear(__e_acsl_8);
}
-
/*@ assert x ≡ 0 ⇒ y ≡ 1; */
{
mpz_t __e_acsl_x_5;
@@ -255,7 +251,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_11,(long)0);
__e_acsl_eq_8 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_5),
(__mpz_struct const *)(__e_acsl_11));
- if (! (__e_acsl_eq_8 == 0)) { __e_acsl_implies = 1; }
+ if (! (__e_acsl_eq_8 == 0)) __e_acsl_implies = 1;
else {
mpz_t __e_acsl_y_5;
mpz_t __e_acsl_12;
@@ -273,7 +269,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_5);
__gmpz_clear(__e_acsl_11);
}
-
/*@ assert x ≡ 1 ⇒ y ≡ 1/0; */
{
mpz_t __e_acsl_x_6;
@@ -284,7 +279,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_13,(long)1);
__e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_6),
(__mpz_struct const *)(__e_acsl_13));
- if (! (__e_acsl_eq_10 == 0)) { __e_acsl_implies_2 = 1; }
+ if (! (__e_acsl_eq_10 == 0)) __e_acsl_implies_2 = 1;
else {
mpz_t __e_acsl_y_6;
mpz_t __e_acsl_14;
@@ -316,7 +311,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_6);
__gmpz_clear(__e_acsl_13);
}
-
/*@ assert x≢0? x ≢ 0: y ≢ 0; */
{
mpz_t __e_acsl_x_7;
@@ -356,7 +350,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_7);
__gmpz_clear(__e_acsl_16);
}
-
/*@ assert y≢0? y ≢ 0: x ≢ 0; */
{
mpz_t __e_acsl_y_8;
@@ -396,7 +389,6 @@ int main(void)
__gmpz_clear(__e_acsl_y_8);
__gmpz_clear(__e_acsl_19);
}
-
/*@ assert x≡1? x ≡ 18: x ≡ 0; */
{
mpz_t __e_acsl_x_10;
@@ -436,7 +428,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_10);
__gmpz_clear(__e_acsl_22);
}
-
/*@ assert x ≡ 2 ⇔ y ≡ 3; */
{
mpz_t __e_acsl_x_13;
@@ -448,7 +439,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_25,(long)2);
__e_acsl_eq_15 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_13),
(__mpz_struct const *)(__e_acsl_25));
- if (! (__e_acsl_eq_15 == 0)) { __e_acsl_implies_3 = 1; }
+ if (! (__e_acsl_eq_15 == 0)) __e_acsl_implies_3 = 1;
else {
mpz_t __e_acsl_y_10;
mpz_t __e_acsl_26;
@@ -470,7 +461,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_27,(long)3);
__e_acsl_eq_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y_11),
(__mpz_struct const *)(__e_acsl_27));
- if (! (__e_acsl_eq_17 == 0)) { __e_acsl_implies_4 = 1; }
+ if (! (__e_acsl_eq_17 == 0)) __e_acsl_implies_4 = 1;
else {
mpz_t __e_acsl_x_14;
mpz_t __e_acsl_28;
@@ -487,13 +478,12 @@ int main(void)
__gmpz_clear(__e_acsl_y_11);
__gmpz_clear(__e_acsl_27);
}
- else { __e_acsl_equiv = 0; }
+ else __e_acsl_equiv = 0;
e_acsl_assert(__e_acsl_equiv,(char *)"Assertion",
(char *)"x == 2 <==> y == 3",22);
__gmpz_clear(__e_acsl_x_13);
__gmpz_clear(__e_acsl_25);
}
-
/*@ assert x ≡ 0 ⇔ y ≡ 1; */
{
mpz_t __e_acsl_x_15;
@@ -505,7 +495,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_29,(long)0);
__e_acsl_eq_19 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_15),
(__mpz_struct const *)(__e_acsl_29));
- if (! (__e_acsl_eq_19 == 0)) { __e_acsl_implies_5 = 1; }
+ if (! (__e_acsl_eq_19 == 0)) __e_acsl_implies_5 = 1;
else {
mpz_t __e_acsl_y_12;
mpz_t __e_acsl_30;
@@ -527,7 +517,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_31,(long)1);
__e_acsl_eq_21 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y_13),
(__mpz_struct const *)(__e_acsl_31));
- if (! (__e_acsl_eq_21 == 0)) { __e_acsl_implies_6 = 1; }
+ if (! (__e_acsl_eq_21 == 0)) __e_acsl_implies_6 = 1;
else {
mpz_t __e_acsl_x_16;
mpz_t __e_acsl_32;
@@ -544,13 +534,12 @@ int main(void)
__gmpz_clear(__e_acsl_y_13);
__gmpz_clear(__e_acsl_31);
}
- else { __e_acsl_equiv_2 = 0; }
+ else __e_acsl_equiv_2 = 0;
e_acsl_assert(__e_acsl_equiv_2,(char *)"Assertion",
(char *)"x == 0 <==> y == 1",23);
__gmpz_clear(__e_acsl_x_15);
__gmpz_clear(__e_acsl_29);
}
-
/*@ assert ((x≢0? x: y)≢0) ≡ (x≡0); */
{
mpz_t __e_acsl_x_17;
@@ -594,7 +583,6 @@ int main(void)
__gmpz_clear(__e_acsl_34);
__gmpz_clear(__e_acsl_35);
}
-
/*@ assert (x ≢ 0 ∧ y ≢ 0) ∨ y ≢ 0; */
{
mpz_t __e_acsl_x_19;
@@ -618,8 +606,8 @@ int main(void)
__gmpz_clear(__e_acsl_y_15);
__gmpz_clear(__e_acsl_37);
}
- else { __e_acsl_and_3 = 0; }
- if (__e_acsl_and_3) { __e_acsl_or_3 = 1; }
+ else __e_acsl_and_3 = 0;
+ if (__e_acsl_and_3) __e_acsl_or_3 = 1;
else {
mpz_t __e_acsl_y_16;
mpz_t __e_acsl_38;
@@ -637,7 +625,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_19);
__gmpz_clear(__e_acsl_36);
}
-
/*@ assert (x ≢ 0 ∨ y ≢ 0) ∧ y ≡ 1; */
{
mpz_t __e_acsl_x_20;
@@ -649,7 +636,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_39,0L);
__e_acsl_ne_13 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_20),
(__mpz_struct const *)(__e_acsl_39));
- if (__e_acsl_ne_13 != 0) { __e_acsl_or_4 = 1; }
+ if (__e_acsl_ne_13 != 0) __e_acsl_or_4 = 1;
else {
mpz_t __e_acsl_y_17;
mpz_t __e_acsl_40;
@@ -674,13 +661,12 @@ int main(void)
__gmpz_clear(__e_acsl_y_18);
__gmpz_clear(__e_acsl_41);
}
- else { __e_acsl_and_4 = 0; }
+ else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
(char *)"(x != 0 || y != 0) && y == 1",28);
__gmpz_clear(__e_acsl_x_20);
__gmpz_clear(__e_acsl_39);
}
-
/*@ assert (x≢0∨y≢0) ≡ (y≢0); */
{
mpz_t __e_acsl_x_21;
@@ -695,7 +681,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_42,0L);
__e_acsl_ne_15 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_21),
(__mpz_struct const *)(__e_acsl_42));
- if (__e_acsl_ne_15 != 0) { __gmpz_init_set_si(__e_acsl_or_5,1L); }
+ if (__e_acsl_ne_15 != 0) __gmpz_init_set_si(__e_acsl_or_5,1L);
else {
mpz_t __e_acsl_y_19;
mpz_t __e_acsl_43;
@@ -725,7 +711,6 @@ int main(void)
__gmpz_clear(__e_acsl_y_20);
__gmpz_clear(__e_acsl_45);
}
-
/*@ assert (x≢0∧y≢0) ≡ (x≢0); */
{
mpz_t __e_acsl_x_22;
@@ -754,7 +739,7 @@ int main(void)
__gmpz_clear(__e_acsl_47);
__gmpz_clear(__e_acsl_48);
}
- else { __gmpz_init_set_si(__e_acsl_and_5,0L); }
+ else __gmpz_init_set_si(__e_acsl_and_5,0L);
__e_acsl_ne_20 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_22),
(__mpz_struct const *)(__e_acsl_46));
__gmpz_init_set_si(__e_acsl_49,(long)(__e_acsl_ne_20 != 0));
@@ -767,10 +752,9 @@ int main(void)
__gmpz_clear(__e_acsl_and_5);
__gmpz_clear(__e_acsl_49);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 6a3f7f640dfe44de1a3ea682952b87b8d8ef97fc..215c74c3727495a422afc90c3e5520abde660f37 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -76,7 +76,7 @@ int search(int elt)
__e_acsl_forall = 1;
__e_acsl_i = 0;
while (1) {
- if (__e_acsl_i < 9) { ; } else { break; }
+ if (__e_acsl_i < 9) ; else break;
e_acsl_assert(__e_acsl_i + 1 < 10,(char *)"Precondition",
(char *)"index_bound: (int)(__e_acsl_i+1) < 10",9);
e_acsl_assert(0 <= __e_acsl_i + 1,(char *)"Precondition",
@@ -85,10 +85,11 @@ int search(int elt)
(char *)"index_bound: __e_acsl_i < 10",9);
e_acsl_assert(0 <= __e_acsl_i,(char *)"Precondition",
(char *)"index_bound: 0 <= __e_acsl_i",9);
- if (A[__e_acsl_i] <= A[__e_acsl_i + 1]) { ; }
+ if (A[__e_acsl_i] <= A[__e_acsl_i + 1]) ;
else {
__e_acsl_forall = 0;
- goto e_acsl_end_loop1; }
+ goto e_acsl_end_loop1;
+ }
__e_acsl_i ++;
}
e_acsl_end_loop1: /* internal */ ;
@@ -101,88 +102,90 @@ int search(int elt)
__e_acsl_forall_2 = 1;
__e_acsl_j_2 = 0;
while (1) {
- if (__e_acsl_j_2 < 10) { ; } else { break; }
+ if (__e_acsl_j_2 < 10) ; else break;
e_acsl_assert(__e_acsl_j_2 < 10,(char *)"Postcondition",
(char *)"index_bound: __e_acsl_j_2 < 10",14);
e_acsl_assert(0 <= __e_acsl_j_2,(char *)"Postcondition",
(char *)"index_bound: 0 <= __e_acsl_j_2",14);
- if (A[__e_acsl_j_2] != elt) { ; }
+ if (A[__e_acsl_j_2] != elt) ;
else {
__e_acsl_forall_2 = 0;
- goto e_acsl_end_loop3; }
+ goto e_acsl_end_loop3;
+ }
__e_acsl_j_2 ++;
}
e_acsl_end_loop3: /* internal */ ;
__e_acsl_at_2 = __e_acsl_forall_2;
}
-
{
int __e_acsl_exists;
int __e_acsl_j;
__e_acsl_exists = 0;
__e_acsl_j = 0;
while (1) {
- if (__e_acsl_j < 10) { ; } else { break; }
+ if (__e_acsl_j < 10) ; else break;
e_acsl_assert(__e_acsl_j < 10,(char *)"Postcondition",
(char *)"index_bound: __e_acsl_j < 10",11);
e_acsl_assert(0 <= __e_acsl_j,(char *)"Postcondition",
(char *)"index_bound: 0 <= __e_acsl_j",11);
- if (! (A[__e_acsl_j] == elt)) { ; }
+ if (! (A[__e_acsl_j] == elt)) ;
else {
__e_acsl_exists = 1;
- goto e_acsl_end_loop2; }
+ goto e_acsl_end_loop2;
+ }
__e_acsl_j ++;
}
e_acsl_end_loop2: /* internal */ ;
__e_acsl_at = __e_acsl_exists;
}
-
k = 0;
}
-
/*@ loop invariant 0 ≤ k ∧ k ≤ 10;
loop invariant ∀ ℤ i; 0 ≤ i ∧ i < k ⇒ A[i] < elt;
*/
while (k < 10) {
if (A[k] == elt) {
__retres = 1;
- goto return_label; }
- else {
+ goto return_label;
+ }
+ else
if (A[k] > elt) {
__retres = 0;
- goto return_label; } }
+ goto return_label;
+ }
k ++;
}
__retres = 0;
- return_label: /* internal */
- {
- int __e_acsl_implies;
- int __e_acsl_implies_2;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = __retres == 1; }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(\\exists int j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
- 12);
- if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = __retres == 0; }
- e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(\\forall int j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0",
- 15);
- return (__retres);
- }
-
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else __e_acsl_implies = __retres == 1;
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(\\exists int j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
+ 12);
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = __retres == 0;
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(\\forall int j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0",
+ 15);
+ return __retres;
+ }
}
int main(void)
{
int __retres;
int found;
- { int i;
+ {
+ int i;
i = 0;
while (i < 10) {
A[i] = i * i;
- i ++; } }
-
+ i ++;
+ }
+ }
found = search(36);
/*@ assert found ≡ 1; */
e_acsl_assert(found == 1,(char *)"Assertion",(char *)"found == 1",33);
@@ -191,7 +194,7 @@ int main(void)
e_acsl_assert(found == 0,(char *)"Assertion",(char *)"found == 0",36);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
index f32718628069a7fbb5bdf96fd78a978c164f102b..1fc26c7fe58be2533c04fe1a3556c279080b4cc6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -123,7 +123,6 @@ int search(int elt)
__gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl_5));
__gmpz_clear(__e_acsl_5);
}
-
while (1) {
{
mpz_t __e_acsl_6;
@@ -131,10 +130,9 @@ int search(int elt)
__gmpz_init_set_si(__e_acsl_6,(long)9);
__e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_i),
(__mpz_struct const *)(__e_acsl_6));
- if (__e_acsl_lt < 0) { ; } else { break; }
+ if (__e_acsl_lt < 0) ; else break;
__gmpz_clear(__e_acsl_6);
}
-
{
unsigned long __e_acsl_i_2;
mpz_t __e_acsl;
@@ -157,12 +155,12 @@ int search(int elt)
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_add);
__gmpz_clear(__e_acsl_4);
- if (__e_acsl_le <= 0) { ; }
+ if (__e_acsl_le <= 0) ;
else {
__e_acsl_forall = 0;
- goto e_acsl_end_loop1; }
+ goto e_acsl_end_loop1;
+ }
}
-
{
mpz_t __e_acsl_7;
mpz_t __e_acsl_add_2;
@@ -174,7 +172,6 @@ int search(int elt)
__gmpz_clear(__e_acsl_7);
__gmpz_clear(__e_acsl_add_2);
}
-
}
e_acsl_end_loop1: /* internal */ ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",
@@ -192,7 +189,6 @@ int search(int elt)
__gmpz_set(__e_acsl_j_3,(__mpz_struct const *)(__e_acsl_14));
__gmpz_clear(__e_acsl_14);
}
-
while (1) {
{
mpz_t __e_acsl_15;
@@ -200,10 +196,9 @@ int search(int elt)
__gmpz_init_set_si(__e_acsl_15,(long)10);
__e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_j_3),
(__mpz_struct const *)(__e_acsl_15));
- if (__e_acsl_lt_3 < 0) { ; } else { break; }
+ if (__e_acsl_lt_3 < 0) ; else break;
__gmpz_clear(__e_acsl_15);
}
-
{
unsigned long __e_acsl_j_4;
mpz_t __e_acsl_13;
@@ -216,12 +211,12 @@ int search(int elt)
(__mpz_struct const *)(__e_acsl_elt_2));
__gmpz_clear(__e_acsl_13);
__gmpz_clear(__e_acsl_elt_2);
- if (__e_acsl_ne != 0) { ; }
+ if (__e_acsl_ne != 0) ;
else {
__e_acsl_forall_2 = 0;
- goto e_acsl_end_loop3; }
+ goto e_acsl_end_loop3;
+ }
}
-
{
mpz_t __e_acsl_16;
mpz_t __e_acsl_add_4;
@@ -233,13 +228,11 @@ int search(int elt)
__gmpz_clear(__e_acsl_16);
__gmpz_clear(__e_acsl_add_4);
}
-
}
e_acsl_end_loop3: /* internal */ ;
__e_acsl_at_2 = __e_acsl_forall_2;
__gmpz_clear(__e_acsl_j_3);
}
-
{
int __e_acsl_exists;
mpz_t __e_acsl_j;
@@ -251,7 +244,6 @@ int search(int elt)
__gmpz_set(__e_acsl_j,(__mpz_struct const *)(__e_acsl_9));
__gmpz_clear(__e_acsl_9);
}
-
while (1) {
{
mpz_t __e_acsl_10;
@@ -259,10 +251,9 @@ int search(int elt)
__gmpz_init_set_si(__e_acsl_10,(long)10);
__e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_j),
(__mpz_struct const *)(__e_acsl_10));
- if (__e_acsl_lt_2 < 0) { ; } else { break; }
+ if (__e_acsl_lt_2 < 0) ; else break;
__gmpz_clear(__e_acsl_10);
}
-
{
unsigned long __e_acsl_j_2;
mpz_t __e_acsl_8;
@@ -275,12 +266,12 @@ int search(int elt)
(__mpz_struct const *)(__e_acsl_elt));
__gmpz_clear(__e_acsl_8);
__gmpz_clear(__e_acsl_elt);
- if (! (__e_acsl_eq == 0)) { ; }
+ if (! (__e_acsl_eq == 0)) ;
else {
__e_acsl_exists = 1;
- goto e_acsl_end_loop2; }
+ goto e_acsl_end_loop2;
+ }
}
-
{
mpz_t __e_acsl_11;
mpz_t __e_acsl_add_3;
@@ -292,81 +283,81 @@ int search(int elt)
__gmpz_clear(__e_acsl_11);
__gmpz_clear(__e_acsl_add_3);
}
-
}
e_acsl_end_loop2: /* internal */ ;
__e_acsl_at = __e_acsl_exists;
__gmpz_clear(__e_acsl_j);
}
-
k = 0;
}
-
/*@ loop invariant 0 ≤ k ∧ k ≤ 10;
loop invariant ∀ ℤ i; 0 ≤ i ∧ i < k ⇒ A[i] < elt;
*/
while (k < 10) {
if (A[k] == elt) {
__retres = 1;
- goto return_label; }
- else {
+ goto return_label;
+ }
+ else
if (A[k] > elt) {
__retres = 0;
- goto return_label; } }
+ goto return_label;
+ }
k ++;
}
__retres = 0;
- return_label: /* internal */
- {
- int __e_acsl_implies;
- int __e_acsl_implies_2;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else {
- mpz_t __e_acsl_result;
- mpz_t __e_acsl_12;
- int __e_acsl_eq_2;
- __gmpz_init_set_si(__e_acsl_result,(long)__retres);
- __gmpz_init_set_si(__e_acsl_12,(long)1);
- __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result),
- (__mpz_struct const *)(__e_acsl_12));
- __e_acsl_implies = __e_acsl_eq_2 == 0;
- __gmpz_clear(__e_acsl_result);
- __gmpz_clear(__e_acsl_12);
- }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
- 12);
- if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
- else {
- mpz_t __e_acsl_result_2;
- mpz_t __e_acsl_17;
- int __e_acsl_eq_3;
- __gmpz_init_set_si(__e_acsl_result_2,(long)__retres);
- __gmpz_init_set_si(__e_acsl_17,(long)0);
- __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result_2),
- (__mpz_struct const *)(__e_acsl_17));
- __e_acsl_implies_2 = __e_acsl_eq_3 == 0;
- __gmpz_clear(__e_acsl_result_2);
- __gmpz_clear(__e_acsl_17);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else {
+ mpz_t __e_acsl_result;
+ mpz_t __e_acsl_12;
+ int __e_acsl_eq_2;
+ __gmpz_init_set_si(__e_acsl_result,(long)__retres);
+ __gmpz_init_set_si(__e_acsl_12,(long)1);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result),
+ (__mpz_struct const *)(__e_acsl_12));
+ __e_acsl_implies = __e_acsl_eq_2 == 0;
+ __gmpz_clear(__e_acsl_result);
+ __gmpz_clear(__e_acsl_12);
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
+ 12);
+ if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
+ else {
+ mpz_t __e_acsl_result_2;
+ mpz_t __e_acsl_17;
+ int __e_acsl_eq_3;
+ __gmpz_init_set_si(__e_acsl_result_2,(long)__retres);
+ __gmpz_init_set_si(__e_acsl_17,(long)0);
+ __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result_2),
+ (__mpz_struct const *)(__e_acsl_17));
+ __e_acsl_implies_2 = __e_acsl_eq_3 == 0;
+ __gmpz_clear(__e_acsl_result_2);
+ __gmpz_clear(__e_acsl_17);
+ }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0",
+ 15);
+ return __retres;
}
- e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0",
- 15);
- return (__retres);
- }
-
}
int main(void)
{
int __retres;
int found;
- { int i;
+ {
+ int i;
i = 0;
while (i < 10) {
A[i] = i * i;
- i ++; } }
-
+ i ++;
+ }
+ }
found = search(36);
/*@ assert found ≡ 1; */
{
@@ -382,7 +373,6 @@ int main(void)
__gmpz_clear(__e_acsl_found);
__gmpz_clear(__e_acsl);
}
-
found = search(5);
/*@ assert found ≡ 0; */
{
@@ -398,10 +388,9 @@ int main(void)
__gmpz_clear(__e_acsl_found_2);
__gmpz_clear(__e_acsl_2);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 815c8b0a5c21804d915e00120367371102ec6f9d..188b595eba5c897f1680cbd6253d6ac06e2c9527 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -88,7 +88,6 @@ void f(void)
e_acsl_assert((int)*(T + G) == 'b',(char *)"Assertion",
(char *)"*(T+G) == \'b\'",13);
}
-
G ++;
return;
}
@@ -153,7 +152,6 @@ int main(void)
e_acsl_assert((int)*(S + G2) == 'o',(char *)"Assertion",
(char *)"*(S+G2) == \'o\'",24);
}
-
/*@ assert \initialized(S); */
{
int __e_acsl_initialized;
@@ -161,7 +159,6 @@ int main(void)
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized(S)",25);
}
-
/*@ assert \valid_read(S2); */
{
int __e_acsl_valid_read_2;
@@ -169,7 +166,6 @@ int main(void)
e_acsl_assert(__e_acsl_valid_read_2,(char *)"Assertion",
(char *)"\\valid_read(S2)",26);
}
-
/*@ assert ¬\valid(SS); */
{
int __e_acsl_initialized_2;
@@ -180,11 +176,10 @@ int main(void)
__e_acsl_valid = __valid((void *)SS,sizeof(char));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"!\\valid(SS)",
27);
}
-
__retres = 0;
__delete_block((void *)(& G2));
__delete_block((void *)(& S2));
@@ -193,7 +188,7 @@ int main(void)
__delete_block((void *)(& T));
__delete_block((void *)(& SS));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index 643eabb51e63a14d23bd76454a9ca9cf714a5ecb..324d43b95e0fa9472ff7d97a815d728b5632fed6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -110,7 +110,6 @@ void f(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
}
-
G ++;
return;
}
@@ -180,7 +179,6 @@ int main(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
}
-
/*@ assert \initialized(S); */
{
int __e_acsl_initialized;
@@ -188,7 +186,6 @@ int main(void)
e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",
(char *)"\\initialized(S)",25);
}
-
/*@ assert \valid_read(S2); */
{
int __e_acsl_valid_read;
@@ -196,7 +193,6 @@ int main(void)
e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",
(char *)"\\valid_read(S2)",26);
}
-
/*@ assert ¬\valid(SS); */
{
int __e_acsl_initialized_2;
@@ -207,11 +203,10 @@ int main(void)
__e_acsl_valid = __valid((void *)SS,sizeof(char));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"!\\valid(SS)",
27);
}
-
__retres = 0;
__delete_block((void *)(& G2));
__delete_block((void *)(& S2));
@@ -220,7 +215,7 @@ int main(void)
__delete_block((void *)(& T));
__delete_block((void *)(& SS));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 9feba2ca0bab83e8de607255c9a4ef2fddee3816..f263ef08d9ffe38d33a0a14ce922a327103b057b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -112,14 +112,13 @@ struct list *add(struct list *l, int i)
__e_acsl_valid = __valid((void *)new,sizeof(struct list));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"\\valid(new)",20);
}
-
new->element = i;
new->next = l;
__delete_block((void *)(& new));
- return (new);
+ return new;
}
int main(void)
@@ -131,7 +130,7 @@ int main(void)
l = add(l,7);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 9feba2ca0bab83e8de607255c9a4ef2fddee3816..f263ef08d9ffe38d33a0a14ce922a327103b057b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -112,14 +112,13 @@ struct list *add(struct list *l, int i)
__e_acsl_valid = __valid((void *)new,sizeof(struct list));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"\\valid(new)",20);
}
-
new->element = i;
new->next = l;
__delete_block((void *)(& new));
- return (new);
+ return new;
}
int main(void)
@@ -131,7 +130,7 @@ int main(void)
l = add(l,7);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index bb92a143361fd7ab5869f32aaaf1a9c13a358e67..b7498aab92c1c0455bf8a6a2e4724da8c381d906 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -66,10 +66,9 @@ int main(void)
ensures x ≥ 1; */
{
e_acsl_assert(x == 0,(char *)"Precondition",(char *)"x == 0",10);
- if (x) {
+ if (x)
/*@ assert \false; */
e_acsl_assert(0,(char *)"Assertion",(char *)"\\false",13);
- }
else {
/*@ requires x ≡ 0;
ensures x ≡ 1; */
@@ -78,7 +77,6 @@ int main(void)
x ++;
e_acsl_assert(x == 1,(char *)"Postcondition",(char *)"x == 1",16);
}
-
if (x) {
/*@ requires x ≡ 1;
ensures x ≡ 2; */
@@ -87,19 +85,16 @@ int main(void)
x ++;
e_acsl_assert(x == 2,(char *)"Postcondition",(char *)"x == 2",20);
}
-
}
- else {
+ else
/*@ assert \false; */
e_acsl_assert(0,(char *)"Assertion",(char *)"\\false",23);
- }
}
e_acsl_assert(x >= 1,(char *)"Postcondition",(char *)"x >= 1",11);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
index 4aeea4b3b6ca5df06b9ab5f1f255312ae780cbe0..bfc47bca237367be23ffaeeedf2a5ed03ec1e8a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
@@ -90,7 +90,6 @@ int main(void)
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl_y);
}
-
/*@ requires x ≡ 0;
ensures x ≥ 1; */
{
@@ -109,10 +108,9 @@ int main(void)
10);
__gmpz_clear(__e_acsl_x_2);
__gmpz_clear(__e_acsl);
- if (x) {
+ if (x)
/*@ assert \false; */
e_acsl_assert(0,(char *)"Assertion",(char *)"\\false",13);
- }
else {
/*@ requires x ≡ 0;
ensures x ≡ 1; */
@@ -134,7 +132,6 @@ int main(void)
__gmpz_clear(__e_acsl_2);
x ++;
}
-
__gmpz_init_set_si(__e_acsl_x_4,(long)x);
__gmpz_init_set_si(__e_acsl_3,(long)1);
__e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_4),
@@ -144,7 +141,6 @@ int main(void)
__gmpz_clear(__e_acsl_x_4);
__gmpz_clear(__e_acsl_3);
}
-
if (x) {
/*@ requires x ≡ 1;
ensures x ≡ 2; */
@@ -166,7 +162,6 @@ int main(void)
__gmpz_clear(__e_acsl_4);
x ++;
}
-
__gmpz_init_set_si(__e_acsl_x_6,(long)x);
__gmpz_init_set_si(__e_acsl_5,(long)2);
__e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_6),
@@ -176,15 +171,12 @@ int main(void)
__gmpz_clear(__e_acsl_x_6);
__gmpz_clear(__e_acsl_5);
}
-
}
- else {
+ else
/*@ assert \false; */
e_acsl_assert(0,(char *)"Assertion",(char *)"\\false",23);
- }
}
}
-
__gmpz_init_set_si(__e_acsl_x_7,(long)x);
__gmpz_init_set_si(__e_acsl_6,(long)1);
__e_acsl_ge = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_7),
@@ -194,10 +186,9 @@ int main(void)
__gmpz_clear(__e_acsl_x_7);
__gmpz_clear(__e_acsl_6);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index f15ad255c8611c98443b2d0e0a798d0f601bd134..76953ef713123430aa46d11fbe4c0828b29081d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -60,13 +60,12 @@ int main(void)
x = 0;
/*@ assert x ≡ 0; */
e_acsl_assert(x == 0,(char *)"Assertion",(char *)"x == 0",8);
- if (x) {
+ if (x)
/*@ assert x ≢ 0; */
e_acsl_assert(x != 0,(char *)"Assertion",(char *)"x != 0",9);
- }
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
index 78f473968c94b3112fc335f1339bceb75e9e44bf..ab08c786eec874f7c6a076efb493d5a70e5dd452 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
@@ -88,7 +88,6 @@ int main(void)
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl);
}
-
if (x) {
/*@ assert x ≢ 0; */
{
@@ -103,11 +102,10 @@ int main(void)
__gmpz_clear(__e_acsl_x_2);
__gmpz_clear(__e_acsl_2);
}
-
}
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index f42d74413e2b422a9540bda43e2bfeb1f2994ba1..870555842e584f5b257caf3c720dbc6bc3dd7af6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -61,7 +61,7 @@ int main(void)
(char *)"\\null == (void *)0",8);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
index f42d74413e2b422a9540bda43e2bfeb1f2994ba1..870555842e584f5b257caf3c720dbc6bc3dd7af6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
@@ -61,7 +61,7 @@ int main(void)
(char *)"\\null == (void *)0",8);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index e2677fe53e42d411e8cb07a7d089fffa1636a360..1de3918334db39f6281d6d0d1162f15c893cfa18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -66,7 +66,7 @@ int main(void)
e_acsl_assert(false != true,(char *)"Assertion",(char *)"false != true",13);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
index 8f87c901769f3263347cae8972869ed447e5078c..2a72f8d057be94f854dbd5e1ab5787514e25b1f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
@@ -88,7 +88,6 @@ int main(void)
(char *)"\'c\' == \'c\'",12);
__gmpz_clear(__e_acsl);
}
-
/*@ assert false ≢ true; */
{
mpz_t __e_acsl_2;
@@ -103,10 +102,9 @@ int main(void)
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_3);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index b160fb8ba936ff9f91577c27fa0e91ec2149da1e..98666e54acaac7c6962b3f0e232d0bbe852f19b3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -102,12 +102,11 @@ int main(void)
__e_acsl_valid_read = __valid_read((void *)p,sizeof(int));
__e_acsl_and = __e_acsl_valid_read;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",
(char *)"mem_access: \\valid_read(p)",0);
e_acsl_assert(*p == 1,(char *)"Assertion",(char *)"*p == 1",13);
}
-
/*@ assert t[0] ≡ 2; */
e_acsl_assert(t[0] == 2,(char *)"Assertion",(char *)"t[0] == 2",14);
/*@ assert t[2] ≡ 4; */
@@ -148,13 +147,11 @@ int main(void)
e_acsl_assert((long long)*(& t[2] - i) == (long long)4 - (long long)i,
(char *)"Assertion",(char *)"*(&t[2]-i) == 4-i",21);
}
-
__full_init((void *)(& i));
i ++;
}
__delete_block((void *)(& i));
}
-
__full_init((void *)(& p));
p = & t[2];
t[2] = 5;
@@ -168,18 +165,17 @@ int main(void)
__e_acsl_valid_read_3 = __valid_read((void *)p,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_read_3;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",
(char *)"mem_access: \\valid_read(p)",0);
e_acsl_assert(*p == 5,(char *)"Assertion",(char *)"*p == 5",27);
}
-
__retres = 0;
__delete_block((void *)(& p));
__delete_block((void *)(t));
__delete_block((void *)(& x));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index 1982eac838b991f9366e37f7954bec2cde9b7e50..791e5ede016b7bd7f1fe90001cd543c6bc628d54 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
@@ -157,7 +157,6 @@ int main(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_2);
}
-
/*@ assert t[0] ≡ 2; */
{
mpz_t __e_acsl_3;
@@ -172,7 +171,6 @@ int main(void)
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_4);
}
-
/*@ assert t[2] ≡ 4; */
{
mpz_t __e_acsl_5;
@@ -187,7 +185,6 @@ int main(void)
__gmpz_clear(__e_acsl_5);
__gmpz_clear(__e_acsl_6);
}
-
/*@ assert t[(2*sizeof(int))/sizeof((int)0x0)] ≡ 4; */
{
mpz_t __e_acsl_7;
@@ -232,7 +229,6 @@ int main(void)
__gmpz_clear(__e_acsl_10);
__gmpz_clear(__e_acsl_11);
}
-
{
int i;
__store_block((void *)(& i),4U);
@@ -261,7 +257,6 @@ int main(void)
__gmpz_clear(__e_acsl_13);
__gmpz_clear(__e_acsl_add);
}
-
/*@ assert t[2-i] ≡ 4-i; */
{
mpz_t __e_acsl_14;
@@ -294,7 +289,6 @@ int main(void)
__gmpz_clear(__e_acsl_17);
__gmpz_clear(__e_acsl_sub_2);
}
-
/*@ assert *(&t[2]-i) ≡ 4-i; */
{
mpz_t __e_acsl_18;
@@ -317,13 +311,11 @@ int main(void)
__gmpz_clear(__e_acsl_i_3);
__gmpz_clear(__e_acsl_sub_3);
}
-
__full_init((void *)(& i));
i ++;
}
__delete_block((void *)(& i));
}
-
__full_init((void *)(& p));
p = & t[2];
t[2] = 5;
@@ -341,13 +333,12 @@ int main(void)
__gmpz_clear(__e_acsl_20);
__gmpz_clear(__e_acsl_21);
}
-
__retres = 0;
__delete_block((void *)(& p));
__delete_block((void *)(t));
__delete_block((void *)(& x));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index bd567c9d4bf5af11756403348e7b6cbd458e3ad3..521c56b473b4c77561377d06a69285d023608104 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -63,17 +63,17 @@ int main(void)
__e_acsl_forall = 1;
__e_acsl_x = 0;
while (1) {
- if (__e_acsl_x <= 1) { ; } else { break; }
+ if (__e_acsl_x <= 1) ; else break;
{
int __e_acsl_or;
- if (__e_acsl_x == 0) { __e_acsl_or = 1; }
- else { __e_acsl_or = __e_acsl_x == 1; }
- if (__e_acsl_or) { ; }
+ if (__e_acsl_x == 0) __e_acsl_or = 1;
+ else __e_acsl_or = __e_acsl_x == 1;
+ if (__e_acsl_or) ;
else {
__e_acsl_forall = 0;
- goto e_acsl_end_loop1; }
+ goto e_acsl_end_loop1;
+ }
}
-
__e_acsl_x ++;
}
e_acsl_end_loop1: /* internal */ ;
@@ -81,7 +81,6 @@ int main(void)
(char *)"\\forall int x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
11);
}
-
/*@ assert ∀ int x; 0 < x ∧ x ≤ 1 ⇒ x ≡ 1; */
{
int __e_acsl_forall_2;
@@ -89,18 +88,18 @@ int main(void)
__e_acsl_forall_2 = 1;
__e_acsl_x_2 = 0 + 1;
while (1) {
- if (__e_acsl_x_2 <= 1) { ; } else { break; }
- if (__e_acsl_x_2 == 1) { ; }
+ if (__e_acsl_x_2 <= 1) ; else break;
+ if (__e_acsl_x_2 == 1) ;
else {
__e_acsl_forall_2 = 0;
- goto e_acsl_end_loop2; }
+ goto e_acsl_end_loop2;
+ }
__e_acsl_x_2 ++;
}
e_acsl_end_loop2: /* internal */ ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",
(char *)"\\forall int x; 0 < x && x <= 1 ==> x == 1",12);
}
-
/*@ assert ∀ int x; 0 < x ∧ x < 1 ⇒ \false; */
{
int __e_acsl_forall_3;
@@ -108,18 +107,18 @@ int main(void)
__e_acsl_forall_3 = 1;
__e_acsl_x_3 = 0 + 1;
while (1) {
- if (__e_acsl_x_3 < 1) { ; } else { break; }
- if (0) { ; }
+ if (__e_acsl_x_3 < 1) ; else break;
+ if (0) ;
else {
__e_acsl_forall_3 = 0;
- goto e_acsl_end_loop3; }
+ goto e_acsl_end_loop3;
+ }
__e_acsl_x_3 ++;
}
e_acsl_end_loop3: /* internal */ ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",
(char *)"\\forall int x; 0 < x && x < 1 ==> \\false",13);
}
-
/*@ assert ∀ int x; 0 ≤ x ∧ x < 1 ⇒ x ≡ 0; */
{
int __e_acsl_forall_4;
@@ -127,18 +126,18 @@ int main(void)
__e_acsl_forall_4 = 1;
__e_acsl_x_4 = 0;
while (1) {
- if (__e_acsl_x_4 < 1) { ; } else { break; }
- if (__e_acsl_x_4 == 0) { ; }
+ if (__e_acsl_x_4 < 1) ; else break;
+ if (__e_acsl_x_4 == 0) ;
else {
__e_acsl_forall_4 = 0;
- goto e_acsl_end_loop4; }
+ goto e_acsl_end_loop4;
+ }
__e_acsl_x_4 ++;
}
e_acsl_end_loop4: /* internal */ ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",
(char *)"\\forall int x; 0 <= x && x < 1 ==> x == 0",14);
}
-
/*@ assert
∀ int x, int y, int z;
((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧
@@ -152,17 +151,18 @@ int main(void)
__e_acsl_forall_5 = 1;
__e_acsl_x_5 = 0;
while (1) {
- if (__e_acsl_x_5 < 2) { ; } else { break; }
+ if (__e_acsl_x_5 < 2) ; else break;
__e_acsl_y = 0;
while (1) {
- if (__e_acsl_y < 5) { ; } else { break; }
+ if (__e_acsl_y < 5) ; else break;
__e_acsl_z = 0;
while (1) {
- if (__e_acsl_z <= __e_acsl_y) { ; } else { break; }
- if (__e_acsl_x_5 + __e_acsl_z <= __e_acsl_y + 1) { ; }
+ if (__e_acsl_z <= __e_acsl_y) ; else break;
+ if (__e_acsl_x_5 + __e_acsl_z <= __e_acsl_y + 1) ;
else {
__e_acsl_forall_5 = 0;
- goto e_acsl_end_loop5; }
+ goto e_acsl_end_loop5;
+ }
__e_acsl_z ++;
}
__e_acsl_y ++;
@@ -174,7 +174,6 @@ int main(void)
(char *)"\\forall int x, int y, int z;\n ((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\n x+z <= y+1",
18);
}
-
/*@ assert ∃ int x; (0 ≤ x ∧ x < 10) ∧ x ≡ 5; */
{
int __e_acsl_exists;
@@ -182,18 +181,18 @@ int main(void)
__e_acsl_exists = 0;
__e_acsl_x_6 = 0;
while (1) {
- if (__e_acsl_x_6 < 10) { ; } else { break; }
- if (! (__e_acsl_x_6 == 5)) { ; }
+ if (__e_acsl_x_6 < 10) ; else break;
+ if (! (__e_acsl_x_6 == 5)) ;
else {
__e_acsl_exists = 1;
- goto e_acsl_end_loop6; }
+ goto e_acsl_end_loop6;
+ }
__e_acsl_x_6 ++;
}
e_acsl_end_loop6: /* internal */ ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",
(char *)"\\exists int x; (0 <= x && x < 10) && x == 5",23);
}
-
/*@ assert
∀ int x;
0 ≤ x ∧ x < 10 ⇒
@@ -205,32 +204,33 @@ int main(void)
__e_acsl_forall_6 = 1;
__e_acsl_x_7 = 0;
while (1) {
- if (__e_acsl_x_7 < 10) { ; } else { break; }
+ if (__e_acsl_x_7 < 10) ; else break;
{
int __e_acsl_implies;
- if (! (__e_acsl_x_7 % 2 == 0)) { __e_acsl_implies = 1; }
+ if (! (__e_acsl_x_7 % 2 == 0)) __e_acsl_implies = 1;
else {
int __e_acsl_exists_2;
int __e_acsl_y_2;
__e_acsl_exists_2 = 0;
__e_acsl_y_2 = 0;
while (1) {
- if (__e_acsl_y_2 <= __e_acsl_x_7 / 2) { ; } else { break; }
- if (! (__e_acsl_x_7 == 2 * __e_acsl_y_2)) { ; }
+ if (__e_acsl_y_2 <= __e_acsl_x_7 / 2) ; else break;
+ if (! (__e_acsl_x_7 == 2 * __e_acsl_y_2)) ;
else {
__e_acsl_exists_2 = 1;
- goto e_acsl_end_loop7; }
+ goto e_acsl_end_loop7;
+ }
__e_acsl_y_2 ++;
}
e_acsl_end_loop7: /* internal */ ;
__e_acsl_implies = __e_acsl_exists_2;
}
- if (__e_acsl_implies) { ; }
+ if (__e_acsl_implies) ;
else {
__e_acsl_forall_6 = 0;
- goto e_acsl_end_loop8; }
+ goto e_acsl_end_loop8;
+ }
}
-
__e_acsl_x_7 ++;
}
e_acsl_end_loop8: /* internal */ ;
@@ -238,10 +238,9 @@ int main(void)
(char *)"\\forall int x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists int y; (0 <= y && y <= x/2) && x == 2*y))",
27);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
index a6d2368138e1bb5dfc9d92b4748a88c1161a7554..e942e11f7c78d7698446b9faf06c05392a6deff0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -134,7 +134,6 @@ int main(void)
__gmpz_set(__e_acsl_x,(__mpz_struct const *)(__e_acsl_3));
__gmpz_clear(__e_acsl_3);
}
-
while (1) {
{
mpz_t __e_acsl_4;
@@ -142,10 +141,9 @@ int main(void)
__gmpz_init_set_si(__e_acsl_4,(long)1);
__e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x),
(__mpz_struct const *)(__e_acsl_4));
- if (__e_acsl_le <= 0) { ; } else { break; }
+ if (__e_acsl_le <= 0) ; else break;
__gmpz_clear(__e_acsl_4);
}
-
{
mpz_t __e_acsl;
int __e_acsl_eq;
@@ -153,7 +151,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl,(long)0);
__e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x),
(__mpz_struct const *)(__e_acsl));
- if (__e_acsl_eq == 0) { __e_acsl_or = 1; }
+ if (__e_acsl_eq == 0) __e_acsl_or = 1;
else {
mpz_t __e_acsl_2;
int __e_acsl_eq_2;
@@ -164,12 +162,12 @@ int main(void)
__gmpz_clear(__e_acsl_2);
}
__gmpz_clear(__e_acsl);
- if (__e_acsl_or) { ; }
+ if (__e_acsl_or) ;
else {
__e_acsl_forall = 0;
- goto e_acsl_end_loop1; }
+ goto e_acsl_end_loop1;
+ }
}
-
{
mpz_t __e_acsl_5;
mpz_t __e_acsl_add;
@@ -181,7 +179,6 @@ int main(void)
__gmpz_clear(__e_acsl_5);
__gmpz_clear(__e_acsl_add);
}
-
}
e_acsl_end_loop1: /* internal */ ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",
@@ -189,7 +186,6 @@ int main(void)
11);
__gmpz_clear(__e_acsl_x);
}
-
/*@ assert ∀ ℤ x; 0 < x ∧ x ≤ 1 ⇒ x ≡ 1; */
{
int __e_acsl_forall_2;
@@ -210,7 +206,6 @@ int main(void)
__gmpz_clear(__e_acsl_8);
__gmpz_clear(__e_acsl_add_2);
}
-
while (1) {
{
mpz_t __e_acsl_9;
@@ -218,10 +213,9 @@ int main(void)
__gmpz_init_set_si(__e_acsl_9,(long)1);
__e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_2),
(__mpz_struct const *)(__e_acsl_9));
- if (__e_acsl_le_2 <= 0) { ; } else { break; }
+ if (__e_acsl_le_2 <= 0) ; else break;
__gmpz_clear(__e_acsl_9);
}
-
{
mpz_t __e_acsl_6;
int __e_acsl_eq_3;
@@ -229,12 +223,12 @@ int main(void)
__e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_2),
(__mpz_struct const *)(__e_acsl_6));
__gmpz_clear(__e_acsl_6);
- if (__e_acsl_eq_3 == 0) { ; }
+ if (__e_acsl_eq_3 == 0) ;
else {
__e_acsl_forall_2 = 0;
- goto e_acsl_end_loop2; }
+ goto e_acsl_end_loop2;
+ }
}
-
{
mpz_t __e_acsl_10;
mpz_t __e_acsl_add_3;
@@ -246,7 +240,6 @@ int main(void)
__gmpz_clear(__e_acsl_10);
__gmpz_clear(__e_acsl_add_3);
}
-
}
e_acsl_end_loop2: /* internal */ ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",
@@ -254,7 +247,6 @@ int main(void)
12);
__gmpz_clear(__e_acsl_x_2);
}
-
/*@ assert ∀ ℤ x; 0 < x ∧ x < 1 ⇒ \false; */
{
int __e_acsl_forall_3;
@@ -275,7 +267,6 @@ int main(void)
__gmpz_clear(__e_acsl_12);
__gmpz_clear(__e_acsl_add_4);
}
-
while (1) {
{
mpz_t __e_acsl_13;
@@ -283,14 +274,14 @@ int main(void)
__gmpz_init_set_si(__e_acsl_13,(long)1);
__e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_3),
(__mpz_struct const *)(__e_acsl_13));
- if (__e_acsl_lt < 0) { ; } else { break; }
+ if (__e_acsl_lt < 0) ; else break;
__gmpz_clear(__e_acsl_13);
}
-
- if (0) { ; }
+ if (0) ;
else {
__e_acsl_forall_3 = 0;
- goto e_acsl_end_loop3; }
+ goto e_acsl_end_loop3;
+ }
{
mpz_t __e_acsl_14;
mpz_t __e_acsl_add_5;
@@ -302,7 +293,6 @@ int main(void)
__gmpz_clear(__e_acsl_14);
__gmpz_clear(__e_acsl_add_5);
}
-
}
e_acsl_end_loop3: /* internal */ ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",
@@ -310,7 +300,6 @@ int main(void)
13);
__gmpz_clear(__e_acsl_x_3);
}
-
/*@ assert ∀ ℤ x; 0 ≤ x ∧ x < 1 ⇒ x ≡ 0; */
{
int __e_acsl_forall_4;
@@ -323,7 +312,6 @@ int main(void)
__gmpz_set(__e_acsl_x_4,(__mpz_struct const *)(__e_acsl_16));
__gmpz_clear(__e_acsl_16);
}
-
while (1) {
{
mpz_t __e_acsl_17;
@@ -331,10 +319,9 @@ int main(void)
__gmpz_init_set_si(__e_acsl_17,(long)1);
__e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_4),
(__mpz_struct const *)(__e_acsl_17));
- if (__e_acsl_lt_2 < 0) { ; } else { break; }
+ if (__e_acsl_lt_2 < 0) ; else break;
__gmpz_clear(__e_acsl_17);
}
-
{
mpz_t __e_acsl_15;
int __e_acsl_eq_4;
@@ -342,12 +329,12 @@ int main(void)
__e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_4),
(__mpz_struct const *)(__e_acsl_15));
__gmpz_clear(__e_acsl_15);
- if (__e_acsl_eq_4 == 0) { ; }
+ if (__e_acsl_eq_4 == 0) ;
else {
__e_acsl_forall_4 = 0;
- goto e_acsl_end_loop4; }
+ goto e_acsl_end_loop4;
+ }
}
-
{
mpz_t __e_acsl_18;
mpz_t __e_acsl_add_6;
@@ -359,7 +346,6 @@ int main(void)
__gmpz_clear(__e_acsl_18);
__gmpz_clear(__e_acsl_add_6);
}
-
}
e_acsl_end_loop4: /* internal */ ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",
@@ -367,7 +353,6 @@ int main(void)
14);
__gmpz_clear(__e_acsl_x_4);
}
-
/*@ assert
∀ ℤ x, ℤ y, ℤ z;
((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧
@@ -388,7 +373,6 @@ int main(void)
__gmpz_set(__e_acsl_x_5,(__mpz_struct const *)(__e_acsl_25));
__gmpz_clear(__e_acsl_25);
}
-
while (1) {
{
mpz_t __e_acsl_26;
@@ -396,17 +380,15 @@ int main(void)
__gmpz_init_set_si(__e_acsl_26,(long)2);
__e_acsl_lt_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_5),
(__mpz_struct const *)(__e_acsl_26));
- if (__e_acsl_lt_4 < 0) { ; } else { break; }
+ if (__e_acsl_lt_4 < 0) ; else break;
__gmpz_clear(__e_acsl_26);
}
-
{
mpz_t __e_acsl_22;
__gmpz_init_set_si(__e_acsl_22,(long)0);
__gmpz_set(__e_acsl_y,(__mpz_struct const *)(__e_acsl_22));
__gmpz_clear(__e_acsl_22);
}
-
while (1) {
{
mpz_t __e_acsl_23;
@@ -414,25 +396,22 @@ int main(void)
__gmpz_init_set_si(__e_acsl_23,(long)5);
__e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y),
(__mpz_struct const *)(__e_acsl_23));
- if (__e_acsl_lt_3 < 0) { ; } else { break; }
+ if (__e_acsl_lt_3 < 0) ; else break;
__gmpz_clear(__e_acsl_23);
}
-
{
mpz_t __e_acsl_20;
__gmpz_init_set_si(__e_acsl_20,(long)0);
__gmpz_set(__e_acsl_z,(__mpz_struct const *)(__e_acsl_20));
__gmpz_clear(__e_acsl_20);
}
-
while (1) {
{
int __e_acsl_le_4;
__e_acsl_le_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_z),
(__mpz_struct const *)(__e_acsl_y));
- if (__e_acsl_le_4 <= 0) { ; } else { break; }
+ if (__e_acsl_le_4 <= 0) ; else break;
}
-
{
mpz_t __e_acsl_add_7;
mpz_t __e_acsl_19;
@@ -450,12 +429,12 @@ int main(void)
__gmpz_clear(__e_acsl_add_7);
__gmpz_clear(__e_acsl_19);
__gmpz_clear(__e_acsl_add_8);
- if (__e_acsl_le_3 <= 0) { ; }
+ if (__e_acsl_le_3 <= 0) ;
else {
__e_acsl_forall_5 = 0;
- goto e_acsl_end_loop5; }
+ goto e_acsl_end_loop5;
+ }
}
-
{
mpz_t __e_acsl_21;
mpz_t __e_acsl_add_9;
@@ -467,7 +446,6 @@ int main(void)
__gmpz_clear(__e_acsl_21);
__gmpz_clear(__e_acsl_add_9);
}
-
}
{
mpz_t __e_acsl_24;
@@ -480,7 +458,6 @@ int main(void)
__gmpz_clear(__e_acsl_24);
__gmpz_clear(__e_acsl_add_10);
}
-
}
{
mpz_t __e_acsl_27;
@@ -493,7 +470,6 @@ int main(void)
__gmpz_clear(__e_acsl_27);
__gmpz_clear(__e_acsl_add_11);
}
-
}
e_acsl_end_loop5: /* internal */ ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",
@@ -503,7 +479,6 @@ int main(void)
__gmpz_clear(__e_acsl_y);
__gmpz_clear(__e_acsl_z);
}
-
/*@ assert ∃ ℤ x; (0 ≤ x ∧ x < 10) ∧ x ≡ 5; */
{
int __e_acsl_exists;
@@ -516,7 +491,6 @@ int main(void)
__gmpz_set(__e_acsl_x_6,(__mpz_struct const *)(__e_acsl_29));
__gmpz_clear(__e_acsl_29);
}
-
while (1) {
{
mpz_t __e_acsl_30;
@@ -524,10 +498,9 @@ int main(void)
__gmpz_init_set_si(__e_acsl_30,(long)10);
__e_acsl_lt_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_6),
(__mpz_struct const *)(__e_acsl_30));
- if (__e_acsl_lt_5 < 0) { ; } else { break; }
+ if (__e_acsl_lt_5 < 0) ; else break;
__gmpz_clear(__e_acsl_30);
}
-
{
mpz_t __e_acsl_28;
int __e_acsl_eq_5;
@@ -535,12 +508,12 @@ int main(void)
__e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_6),
(__mpz_struct const *)(__e_acsl_28));
__gmpz_clear(__e_acsl_28);
- if (! (__e_acsl_eq_5 == 0)) { ; }
+ if (! (__e_acsl_eq_5 == 0)) ;
else {
__e_acsl_exists = 1;
- goto e_acsl_end_loop6; }
+ goto e_acsl_end_loop6;
+ }
}
-
{
mpz_t __e_acsl_31;
mpz_t __e_acsl_add_12;
@@ -552,7 +525,6 @@ int main(void)
__gmpz_clear(__e_acsl_31);
__gmpz_clear(__e_acsl_add_12);
}
-
}
e_acsl_end_loop6: /* internal */ ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",
@@ -560,7 +532,6 @@ int main(void)
23);
__gmpz_clear(__e_acsl_x_6);
}
-
/*@ assert
∀ ℤ x;
0 ≤ x ∧ x < 10 ⇒
@@ -577,7 +548,6 @@ int main(void)
__gmpz_set(__e_acsl_x_7,(__mpz_struct const *)(__e_acsl_39));
__gmpz_clear(__e_acsl_39);
}
-
while (1) {
{
mpz_t __e_acsl_40;
@@ -585,10 +555,9 @@ int main(void)
__gmpz_init_set_si(__e_acsl_40,(long)10);
__e_acsl_lt_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_7),
(__mpz_struct const *)(__e_acsl_40));
- if (__e_acsl_lt_6 < 0) { ; } else { break; }
+ if (__e_acsl_lt_6 < 0) ; else break;
__gmpz_clear(__e_acsl_40);
}
-
{
mpz_t __e_acsl_32;
mpz_t __e_acsl_33;
@@ -608,7 +577,7 @@ int main(void)
(__mpz_struct const *)(__e_acsl_32));
__e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_mod),
(__mpz_struct const *)(__e_acsl_33));
- if (! (__e_acsl_eq_6 == 0)) { __e_acsl_implies = 1; }
+ if (! (__e_acsl_eq_6 == 0)) __e_acsl_implies = 1;
else {
int __e_acsl_exists_2;
mpz_t __e_acsl_y_2;
@@ -620,7 +589,6 @@ int main(void)
__gmpz_set(__e_acsl_y_2,(__mpz_struct const *)(__e_acsl_35));
__gmpz_clear(__e_acsl_35);
}
-
while (1) {
{
mpz_t __e_acsl_36;
@@ -641,12 +609,11 @@ int main(void)
(__mpz_struct const *)(__e_acsl_36));
__e_acsl_le_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y_2),
(__mpz_struct const *)(__e_acsl_div));
- if (__e_acsl_le_5 <= 0) { ; } else { break; }
+ if (__e_acsl_le_5 <= 0) ; else break;
__gmpz_clear(__e_acsl_36);
__gmpz_clear(__e_acsl_37);
__gmpz_clear(__e_acsl_div);
}
-
{
mpz_t __e_acsl_34;
mpz_t __e_acsl_mul;
@@ -659,12 +626,12 @@ int main(void)
(__mpz_struct const *)(__e_acsl_mul));
__gmpz_clear(__e_acsl_34);
__gmpz_clear(__e_acsl_mul);
- if (! (__e_acsl_eq_7 == 0)) { ; }
+ if (! (__e_acsl_eq_7 == 0)) ;
else {
__e_acsl_exists_2 = 1;
- goto e_acsl_end_loop7; }
+ goto e_acsl_end_loop7;
+ }
}
-
{
mpz_t __e_acsl_38;
mpz_t __e_acsl_add_13;
@@ -678,7 +645,6 @@ int main(void)
__gmpz_clear(__e_acsl_38);
__gmpz_clear(__e_acsl_add_13);
}
-
}
e_acsl_end_loop7: /* internal */ ;
__e_acsl_implies = __e_acsl_exists_2;
@@ -687,12 +653,12 @@ int main(void)
__gmpz_clear(__e_acsl_32);
__gmpz_clear(__e_acsl_33);
__gmpz_clear(__e_acsl_mod);
- if (__e_acsl_implies) { ; }
+ if (__e_acsl_implies) ;
else {
__e_acsl_forall_6 = 0;
- goto e_acsl_end_loop8; }
+ goto e_acsl_end_loop8;
+ }
}
-
{
mpz_t __e_acsl_41;
mpz_t __e_acsl_add_14;
@@ -704,7 +670,6 @@ int main(void)
__gmpz_clear(__e_acsl_41);
__gmpz_clear(__e_acsl_add_14);
}
-
}
e_acsl_end_loop8: /* internal */ ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",
@@ -712,10 +677,9 @@ int main(void)
27);
__gmpz_clear(__e_acsl_x_7);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index 998780a9701795bfb3f39f2abb68fcee281b6509..317c8de96995cfc2748e5b706c8e258ca1cfcbf8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -72,7 +72,7 @@ int f(int x)
e_acsl_assert(x == (int)((long long)__e_acsl_at - (long long)__e_acsl_at_2),
(char *)"Postcondition",
(char *)"\\result == (int)(\\old(x)-\\old(x))",7);
- return (x);
+ return x;
}
int Y = 1;
@@ -80,7 +80,7 @@ int Y = 1;
int g(int x)
{
e_acsl_assert(x == Y,(char *)"Postcondition",(char *)"\\result == Y",18);
- return (x);
+ return x;
}
/*@ ensures \result ≡ 0; */
@@ -90,7 +90,7 @@ int h(void)
__retres = 0;
e_acsl_assert(__retres == 0,(char *)"Postcondition",
(char *)"\\result == 0",23);
- return (__retres);
+ return __retres;
}
int main(void)
@@ -101,7 +101,7 @@ int main(void)
h();
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
index e0facaf62be23630249f8436ca62c7975fdc2052..1adae8592d93132acbc940e27d03444080c9c1af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
@@ -118,9 +118,8 @@ int f(int x)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_sub);
__gmpz_clear(__e_acsl_cast);
- return (x);
+ return x;
}
-
}
int Y = 1;
@@ -139,9 +138,8 @@ int g(int x)
(char *)"\\result == Y",18);
__gmpz_clear(__e_acsl_result);
__gmpz_clear(__e_acsl_Y);
- return (x);
+ return x;
}
-
}
/*@ ensures \result ≡ 0; */
@@ -161,9 +159,8 @@ int h(void)
(char *)"\\result == 0",23);
__gmpz_clear(__e_acsl_result);
__gmpz_clear(__e_acsl);
- return (__retres);
+ return __retres;
}
-
}
int main(void)
@@ -174,7 +171,7 @@ int main(void)
h();
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index c174e68f74385036aa1f62ab8c037d9cee780957..cf7517dfbeb57f6a55811050c284ebd8f6d4c7d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -64,7 +64,7 @@ int main(void)
(char *)"sizeof(int) == sizeof(x)",10);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
index 6a35a11f4714bb186ab9cd6aa2f1edeb9aa4995c..46b0bdc966cfff4678276c01d6f010d37d6fa0b7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
@@ -90,10 +90,9 @@ int main(void)
__gmpz_clear(__e_acsl_sizeof);
__gmpz_clear(__e_acsl_sizeof_2);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index d0b02f172bb52ab1c8be8fa2473d79ddbf2051cc..66d0c63a5d6608dae23c37ee7f282423bbe6b80c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -61,9 +61,10 @@ int main(void)
x = 0;
y = 2;
/*@ ensures x ≡ 1; */
- { x = 1;
- e_acsl_assert(x == 1,(char *)"Postcondition",(char *)"x == 1",9); }
-
+ {
+ x = 1;
+ e_acsl_assert(x == 1,(char *)"Postcondition",(char *)"x == 1",9);
+ }
/*@ ensures x ≡ 2;
ensures y ≡ 2; */
{
@@ -71,7 +72,6 @@ int main(void)
e_acsl_assert(x == 2,(char *)"Postcondition",(char *)"x == 2",12);
e_acsl_assert(y == 2,(char *)"Postcondition",(char *)"y == 2",13);
}
-
/*@ requires x ≡ 2; */
e_acsl_assert(x == 2,(char *)"Precondition",(char *)"x == 2",16);
x ++;
@@ -99,7 +99,6 @@ int main(void)
e_acsl_assert((long long)x == (long long)y + (long long)1,
(char *)"Postcondition",(char *)"x == y+1",29);
}
-
/*@ behavior b1:
assumes x ≡ 1;
requires x ≡ 0;
@@ -116,24 +115,21 @@ int main(void)
int __e_acsl_implies_2;
int __e_acsl_and_2;
int __e_acsl_implies_3;
- if (! (x == 1)) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = x == 0; }
+ if (! (x == 1)) __e_acsl_implies = 1; else __e_acsl_implies = x == 0;
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",
(char *)"x == 1 ==> x == 0",34);
- if (x == 3) { __e_acsl_and = y == 2; } else { __e_acsl_and = 0; }
- if (! __e_acsl_and) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = x == 3; }
+ if (x == 3) __e_acsl_and = y == 2; else __e_acsl_and = 0;
+ if (! __e_acsl_and) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = x == 3;
e_acsl_assert(__e_acsl_implies_2,(char *)"Precondition",
(char *)"x == 3 && y == 2 ==> x == 3",38);
- if (x == 3) { __e_acsl_and_2 = y == 2; } else { __e_acsl_and_2 = 0; }
- if (! __e_acsl_and_2) { __e_acsl_implies_3 = 1; }
- else { __e_acsl_implies_3 = (long long)x + (long long)y == (long long)5;
- }
+ if (x == 3) __e_acsl_and_2 = y == 2; else __e_acsl_and_2 = 0;
+ if (! __e_acsl_and_2) __e_acsl_implies_3 = 1;
+ else __e_acsl_implies_3 = (long long)x + (long long)y == (long long)5;
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",
(char *)"x == 3 && y == 2 ==> x+y == 5",39);
x += y;
}
-
/*@ requires x ≡ 5; */
e_acsl_assert(x == 5,(char *)"Precondition",(char *)"x == 5",42);
/*@ requires y ≡ 2; */
@@ -146,9 +142,8 @@ int main(void)
__retres = 0;
e_acsl_assert(x == 7,(char *)"Postcondition",(char *)"x == 7",47);
}
-
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
index 772fdbcdc1a2ced20afe892252605788cbcbd8b5..89734b26793d9e932dc60466d39a892d501dc0da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
@@ -107,7 +107,6 @@ int main(void)
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl);
}
-
/*@ ensures x ≡ 2;
ensures y ≡ 2; */
{
@@ -132,7 +131,6 @@ int main(void)
__gmpz_clear(__e_acsl_2);
__gmpz_clear(__e_acsl_y);
}
-
/*@ requires x ≡ 2; */
{
mpz_t __e_acsl_x_3;
@@ -148,7 +146,6 @@ int main(void)
__gmpz_clear(__e_acsl_3);
x ++;
}
-
/*@ requires x ≡ 3;
requires y ≡ 2; */
{
@@ -176,7 +173,6 @@ int main(void)
__gmpz_clear(__e_acsl_5);
x += y;
}
-
/*@ behavior b1:
requires x ≡ 5;
ensures x ≡ 3;
@@ -232,7 +228,6 @@ int main(void)
__gmpz_clear(__e_acsl_8);
x = 3;
}
-
__gmpz_init_set_si(__e_acsl_x_6,(long)x);
__gmpz_init_set_si(__e_acsl_9,(long)3);
__e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_6),
@@ -254,7 +249,6 @@ int main(void)
__gmpz_clear(__e_acsl_10);
__gmpz_clear(__e_acsl_add_2);
}
-
/*@ behavior b1:
assumes x ≡ 1;
requires x ≡ 0;
@@ -281,7 +275,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_11,(long)1);
__e_acsl_eq_12 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_7),
(__mpz_struct const *)(__e_acsl_11));
- if (! (__e_acsl_eq_12 == 0)) { __e_acsl_implies = 1; }
+ if (! (__e_acsl_eq_12 == 0)) __e_acsl_implies = 1;
else {
mpz_t __e_acsl_x_8;
mpz_t __e_acsl_12;
@@ -311,8 +305,8 @@ int main(void)
__gmpz_clear(__e_acsl_y_5);
__gmpz_clear(__e_acsl_14);
}
- else { __e_acsl_and = 0; }
- if (! __e_acsl_and) { __e_acsl_implies_2 = 1; }
+ else __e_acsl_and = 0;
+ if (! __e_acsl_and) __e_acsl_implies_2 = 1;
else {
mpz_t __e_acsl_x_9;
mpz_t __e_acsl_15;
@@ -341,8 +335,8 @@ int main(void)
__gmpz_clear(__e_acsl_y_6);
__gmpz_clear(__e_acsl_16);
}
- else { __e_acsl_and_2 = 0; }
- if (! __e_acsl_and_2) { __e_acsl_implies_3 = 1; }
+ else __e_acsl_and_2 = 0;
+ if (! __e_acsl_and_2) __e_acsl_implies_3 = 1;
else {
mpz_t __e_acsl_x_10;
mpz_t __e_acsl_y_7;
@@ -370,7 +364,6 @@ int main(void)
__gmpz_clear(__e_acsl_13);
x += y;
}
-
/*@ requires x ≡ 5; */
{
mpz_t __e_acsl_x_11;
@@ -399,8 +392,7 @@ int main(void)
__gmpz_clear(__e_acsl_19);
x += y;
}
- }
-
+ }
/*@ requires x ≡ 7;
ensures x ≡ 7; */
{
@@ -421,7 +413,6 @@ int main(void)
__gmpz_clear(__e_acsl_20);
__retres = 0;
}
-
__gmpz_init_set_si(__e_acsl_x_13,(long)x);
__gmpz_init_set_si(__e_acsl_21,(long)7);
__e_acsl_eq_23 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_13),
@@ -431,9 +422,8 @@ int main(void)
__gmpz_clear(__e_acsl_x_13);
__gmpz_clear(__e_acsl_21);
}
-
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index 82e3cdb879fe148d574d059a6866eca7eae16555..4a6e11b7f01cb86bdf0535588b5a582a7b7b4ffa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -63,7 +63,7 @@ int main(void)
e_acsl_assert(1,(char *)"Assertion",(char *)"\\true",10);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
index 82e3cdb879fe148d574d059a6866eca7eae16555..4a6e11b7f01cb86bdf0535588b5a582a7b7b4ffa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
@@ -63,7 +63,7 @@ int main(void)
e_acsl_assert(1,(char *)"Assertion",(char *)"\\true",10);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
index f2204f36c8c4464fcd63a8a74b53a0182b5bba60..dd8bb786ec39fe736180083f6184e235ee950f16 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
@@ -63,7 +63,7 @@ int main(void)
e_acsl_assert((int)x == 0,(char *)"Assertion",(char *)"x == 0",11);
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
index bfdd29db4d7b618aec8cb9bb3212d0a735768591..8adfbdfd26b62417772774e041aba1b0882ea18b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
@@ -98,10 +98,9 @@ int main(void)
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl);
}
-
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index bc1f297a0f0eeb3ad30517200279d6a13eadee23..be871a3168f45c1fbe750bb0b7b150da237f8090 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -134,11 +134,10 @@ int *f(int *x)
__e_acsl_valid_2 = __valid((void *)y,sizeof(int));
__e_acsl_and = __e_acsl_valid_2;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"!\\valid(y)",
19);
}
-
__full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
@@ -148,7 +147,6 @@ int *f(int *x)
e_acsl_assert(__e_acsl_valid_3,(char *)"Assertion",(char *)"\\valid(x)",
21);
}
-
{
int __e_acsl_valid_4;
__e_acsl_valid_4 = __valid((void *)y,sizeof(int));
@@ -156,9 +154,8 @@ int *f(int *x)
(char *)"\\valid(\\result)",16);
__delete_block((void *)(& x));
__delete_block((void *)(& y));
- return (y);
+ return y;
}
-
}
void e_acsl_global_init(void)
@@ -192,7 +189,7 @@ int main(void)
__e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
@@ -202,20 +199,19 @@ int main(void)
__e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_and_3 = ! __e_acsl_and_2;
}
- else { __e_acsl_and_3 = 0; }
+ else __e_acsl_and_3 = 0;
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
__e_acsl_valid_3 = __valid((void *)X,sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
- else { __e_acsl_and_4 = 0; }
+ else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
(char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
}
-
__full_init((void *)(& a));
a = (int *)__malloc(sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
@@ -230,7 +226,7 @@ int main(void)
__e_acsl_valid_4 = __valid((void *)a,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
- else { __e_acsl_and_5 = 0; }
+ else __e_acsl_and_5 = 0;
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
@@ -240,20 +236,19 @@ int main(void)
__e_acsl_valid_5 = __valid((void *)b,sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
- else { __e_acsl_and_6 = 0; }
+ else __e_acsl_and_6 = 0;
__e_acsl_and_7 = ! __e_acsl_and_6;
}
- else { __e_acsl_and_7 = 0; }
+ else __e_acsl_and_7 = 0;
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
__e_acsl_valid_6 = __valid((void *)X,sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
- else { __e_acsl_and_8 = 0; }
+ else __e_acsl_and_8 = 0;
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",
(char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",29);
}
-
__full_init((void *)(& X));
X = a;
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
@@ -268,7 +263,7 @@ int main(void)
__e_acsl_valid_7 = __valid((void *)a,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
- else { __e_acsl_and_9 = 0; }
+ else __e_acsl_and_9 = 0;
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
@@ -278,20 +273,19 @@ int main(void)
__e_acsl_valid_8 = __valid((void *)b,sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
- else { __e_acsl_and_10 = 0; }
+ else __e_acsl_and_10 = 0;
__e_acsl_and_11 = ! __e_acsl_and_10;
}
- else { __e_acsl_and_11 = 0; }
+ else __e_acsl_and_11 = 0;
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
__e_acsl_valid_9 = __valid((void *)X,sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
- else { __e_acsl_and_12 = 0; }
+ else __e_acsl_and_12 = 0;
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",
(char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",31);
}
-
__full_init((void *)(& b));
b = f(& n);
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -306,7 +300,7 @@ int main(void)
__e_acsl_valid_10 = __valid((void *)a,sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
- else { __e_acsl_and_13 = 0; }
+ else __e_acsl_and_13 = 0;
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
@@ -316,20 +310,19 @@ int main(void)
__e_acsl_valid_11 = __valid((void *)b,sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
- else { __e_acsl_and_14 = 0; }
+ else __e_acsl_and_14 = 0;
__e_acsl_and_15 = __e_acsl_and_14;
}
- else { __e_acsl_and_15 = 0; }
+ else __e_acsl_and_15 = 0;
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
__e_acsl_valid_12 = __valid((void *)X,sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
- else { __e_acsl_and_16 = 0; }
+ else __e_acsl_and_16 = 0;
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",
(char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",33);
}
-
__full_init((void *)(& X));
X = b;
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -344,7 +337,7 @@ int main(void)
__e_acsl_valid_13 = __valid((void *)a,sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
- else { __e_acsl_and_17 = 0; }
+ else __e_acsl_and_17 = 0;
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
@@ -354,20 +347,19 @@ int main(void)
__e_acsl_valid_14 = __valid((void *)b,sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
- else { __e_acsl_and_18 = 0; }
+ else __e_acsl_and_18 = 0;
__e_acsl_and_19 = __e_acsl_and_18;
}
- else { __e_acsl_and_19 = 0; }
+ else __e_acsl_and_19 = 0;
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
__e_acsl_valid_15 = __valid((void *)X,sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
- else { __e_acsl_and_20 = 0; }
+ else __e_acsl_and_20 = 0;
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",
(char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",35);
}
-
__free((void *)a);
/*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
@@ -381,7 +373,7 @@ int main(void)
__e_acsl_valid_16 = __valid((void *)a,sizeof(int));
__e_acsl_and_21 = __e_acsl_valid_16;
}
- else { __e_acsl_and_21 = 0; }
+ else __e_acsl_and_21 = 0;
if (! __e_acsl_and_21) {
int __e_acsl_initialized_12;
int __e_acsl_and_22;
@@ -391,27 +383,26 @@ int main(void)
__e_acsl_valid_17 = __valid((void *)b,sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_17;
}
- else { __e_acsl_and_22 = 0; }
+ else __e_acsl_and_22 = 0;
__e_acsl_and_23 = __e_acsl_and_22;
}
- else { __e_acsl_and_23 = 0; }
+ else __e_acsl_and_23 = 0;
if (__e_acsl_and_23) {
int __e_acsl_valid_18;
__e_acsl_valid_18 = __valid((void *)X,sizeof(int));
__e_acsl_and_24 = __e_acsl_valid_18;
}
- else { __e_acsl_and_24 = 0; }
+ else __e_acsl_and_24 = 0;
e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",
(char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
}
-
__retres = 0;
__delete_block((void *)(& X));
__delete_block((void *)(& n));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index bc1f297a0f0eeb3ad30517200279d6a13eadee23..be871a3168f45c1fbe750bb0b7b150da237f8090 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -134,11 +134,10 @@ int *f(int *x)
__e_acsl_valid_2 = __valid((void *)y,sizeof(int));
__e_acsl_and = __e_acsl_valid_2;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"!\\valid(y)",
19);
}
-
__full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
@@ -148,7 +147,6 @@ int *f(int *x)
e_acsl_assert(__e_acsl_valid_3,(char *)"Assertion",(char *)"\\valid(x)",
21);
}
-
{
int __e_acsl_valid_4;
__e_acsl_valid_4 = __valid((void *)y,sizeof(int));
@@ -156,9 +154,8 @@ int *f(int *x)
(char *)"\\valid(\\result)",16);
__delete_block((void *)(& x));
__delete_block((void *)(& y));
- return (y);
+ return y;
}
-
}
void e_acsl_global_init(void)
@@ -192,7 +189,7 @@ int main(void)
__e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
@@ -202,20 +199,19 @@ int main(void)
__e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_and_3 = ! __e_acsl_and_2;
}
- else { __e_acsl_and_3 = 0; }
+ else __e_acsl_and_3 = 0;
if (__e_acsl_and_3) {
int __e_acsl_valid_3;
__e_acsl_valid_3 = __valid((void *)X,sizeof(int));
__e_acsl_and_4 = ! __e_acsl_valid_3;
}
- else { __e_acsl_and_4 = 0; }
+ else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
(char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
}
-
__full_init((void *)(& a));
a = (int *)__malloc(sizeof(int));
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
@@ -230,7 +226,7 @@ int main(void)
__e_acsl_valid_4 = __valid((void *)a,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
- else { __e_acsl_and_5 = 0; }
+ else __e_acsl_and_5 = 0;
if (__e_acsl_and_5) {
int __e_acsl_initialized_4;
int __e_acsl_and_6;
@@ -240,20 +236,19 @@ int main(void)
__e_acsl_valid_5 = __valid((void *)b,sizeof(int));
__e_acsl_and_6 = __e_acsl_valid_5;
}
- else { __e_acsl_and_6 = 0; }
+ else __e_acsl_and_6 = 0;
__e_acsl_and_7 = ! __e_acsl_and_6;
}
- else { __e_acsl_and_7 = 0; }
+ else __e_acsl_and_7 = 0;
if (__e_acsl_and_7) {
int __e_acsl_valid_6;
__e_acsl_valid_6 = __valid((void *)X,sizeof(int));
__e_acsl_and_8 = ! __e_acsl_valid_6;
}
- else { __e_acsl_and_8 = 0; }
+ else __e_acsl_and_8 = 0;
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",
(char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",29);
}
-
__full_init((void *)(& X));
X = a;
/*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
@@ -268,7 +263,7 @@ int main(void)
__e_acsl_valid_7 = __valid((void *)a,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_7;
}
- else { __e_acsl_and_9 = 0; }
+ else __e_acsl_and_9 = 0;
if (__e_acsl_and_9) {
int __e_acsl_initialized_6;
int __e_acsl_and_10;
@@ -278,20 +273,19 @@ int main(void)
__e_acsl_valid_8 = __valid((void *)b,sizeof(int));
__e_acsl_and_10 = __e_acsl_valid_8;
}
- else { __e_acsl_and_10 = 0; }
+ else __e_acsl_and_10 = 0;
__e_acsl_and_11 = ! __e_acsl_and_10;
}
- else { __e_acsl_and_11 = 0; }
+ else __e_acsl_and_11 = 0;
if (__e_acsl_and_11) {
int __e_acsl_valid_9;
__e_acsl_valid_9 = __valid((void *)X,sizeof(int));
__e_acsl_and_12 = __e_acsl_valid_9;
}
- else { __e_acsl_and_12 = 0; }
+ else __e_acsl_and_12 = 0;
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",
(char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",31);
}
-
__full_init((void *)(& b));
b = f(& n);
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -306,7 +300,7 @@ int main(void)
__e_acsl_valid_10 = __valid((void *)a,sizeof(int));
__e_acsl_and_13 = __e_acsl_valid_10;
}
- else { __e_acsl_and_13 = 0; }
+ else __e_acsl_and_13 = 0;
if (__e_acsl_and_13) {
int __e_acsl_initialized_8;
int __e_acsl_and_14;
@@ -316,20 +310,19 @@ int main(void)
__e_acsl_valid_11 = __valid((void *)b,sizeof(int));
__e_acsl_and_14 = __e_acsl_valid_11;
}
- else { __e_acsl_and_14 = 0; }
+ else __e_acsl_and_14 = 0;
__e_acsl_and_15 = __e_acsl_and_14;
}
- else { __e_acsl_and_15 = 0; }
+ else __e_acsl_and_15 = 0;
if (__e_acsl_and_15) {
int __e_acsl_valid_12;
__e_acsl_valid_12 = __valid((void *)X,sizeof(int));
__e_acsl_and_16 = __e_acsl_valid_12;
}
- else { __e_acsl_and_16 = 0; }
+ else __e_acsl_and_16 = 0;
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",
(char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",33);
}
-
__full_init((void *)(& X));
X = b;
/*@ assert (\valid(a) ∧ \valid(b)) ∧ \valid(X); */
@@ -344,7 +337,7 @@ int main(void)
__e_acsl_valid_13 = __valid((void *)a,sizeof(int));
__e_acsl_and_17 = __e_acsl_valid_13;
}
- else { __e_acsl_and_17 = 0; }
+ else __e_acsl_and_17 = 0;
if (__e_acsl_and_17) {
int __e_acsl_initialized_10;
int __e_acsl_and_18;
@@ -354,20 +347,19 @@ int main(void)
__e_acsl_valid_14 = __valid((void *)b,sizeof(int));
__e_acsl_and_18 = __e_acsl_valid_14;
}
- else { __e_acsl_and_18 = 0; }
+ else __e_acsl_and_18 = 0;
__e_acsl_and_19 = __e_acsl_and_18;
}
- else { __e_acsl_and_19 = 0; }
+ else __e_acsl_and_19 = 0;
if (__e_acsl_and_19) {
int __e_acsl_valid_15;
__e_acsl_valid_15 = __valid((void *)X,sizeof(int));
__e_acsl_and_20 = __e_acsl_valid_15;
}
- else { __e_acsl_and_20 = 0; }
+ else __e_acsl_and_20 = 0;
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",
(char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",35);
}
-
__free((void *)a);
/*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
{
@@ -381,7 +373,7 @@ int main(void)
__e_acsl_valid_16 = __valid((void *)a,sizeof(int));
__e_acsl_and_21 = __e_acsl_valid_16;
}
- else { __e_acsl_and_21 = 0; }
+ else __e_acsl_and_21 = 0;
if (! __e_acsl_and_21) {
int __e_acsl_initialized_12;
int __e_acsl_and_22;
@@ -391,27 +383,26 @@ int main(void)
__e_acsl_valid_17 = __valid((void *)b,sizeof(int));
__e_acsl_and_22 = __e_acsl_valid_17;
}
- else { __e_acsl_and_22 = 0; }
+ else __e_acsl_and_22 = 0;
__e_acsl_and_23 = __e_acsl_and_22;
}
- else { __e_acsl_and_23 = 0; }
+ else __e_acsl_and_23 = 0;
if (__e_acsl_and_23) {
int __e_acsl_valid_18;
__e_acsl_valid_18 = __valid((void *)X,sizeof(int));
__e_acsl_and_24 = __e_acsl_valid_18;
}
- else { __e_acsl_and_24 = 0; }
+ else __e_acsl_and_24 = 0;
e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",
(char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
}
-
__retres = 0;
__delete_block((void *)(& X));
__delete_block((void *)(& n));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 5c1967666ef9639f6baa033e52914ef39a5511a4..9ce841baac62c44fe643976522808878c7fc4dd4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -139,7 +139,7 @@ int main(void)
__e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
@@ -149,14 +149,13 @@ int main(void)
__e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_and_3 = ! __e_acsl_and_2;
}
- else { __e_acsl_and_3 = 0; }
+ else __e_acsl_and_3 = 0;
e_acsl_assert(__e_acsl_and_3,(char *)"Assertion",
(char *)"!\\valid(a) && !\\valid(b)",12);
}
-
__full_init((void *)(& a));
a = (int *)__malloc(sizeof(int));
__initialize((void *)a,sizeof(int));
@@ -174,7 +173,7 @@ int main(void)
__e_acsl_valid_3 = __valid((void *)a,sizeof(int));
__e_acsl_and_4 = __e_acsl_valid_3;
}
- else { __e_acsl_and_4 = 0; }
+ else __e_acsl_and_4 = 0;
if (__e_acsl_and_4) {
int __e_acsl_initialized_4;
int __e_acsl_and_5;
@@ -184,14 +183,13 @@ int main(void)
__e_acsl_valid_4 = __valid((void *)b,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
- else { __e_acsl_and_5 = 0; }
+ else __e_acsl_and_5 = 0;
__e_acsl_and_6 = __e_acsl_and_5;
}
- else { __e_acsl_and_6 = 0; }
+ else __e_acsl_and_6 = 0;
e_acsl_assert(__e_acsl_and_6,(char *)"Assertion",
(char *)"\\valid(a) && \\valid(b)",16);
}
-
/*@ assert *b ≡ n; */
{
int __e_acsl_initialized_5;
@@ -202,12 +200,11 @@ int main(void)
__e_acsl_valid_read = __valid_read((void *)b,sizeof(int));
__e_acsl_and_7 = __e_acsl_valid_read;
}
- else { __e_acsl_and_7 = 0; }
+ else __e_acsl_and_7 = 0;
e_acsl_assert(__e_acsl_and_7,(char *)"Assertion",
(char *)"mem_access: \\valid_read(b)",0);
e_acsl_assert(*b == n,(char *)"Assertion",(char *)"*b == n",17);
}
-
__free((void *)b);
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
@@ -220,7 +217,7 @@ int main(void)
__e_acsl_valid_5 = __valid((void *)a,sizeof(int));
__e_acsl_and_8 = __e_acsl_valid_5;
}
- else { __e_acsl_and_8 = 0; }
+ else __e_acsl_and_8 = 0;
if (! __e_acsl_and_8) {
int __e_acsl_initialized_7;
int __e_acsl_and_9;
@@ -230,20 +227,19 @@ int main(void)
__e_acsl_valid_6 = __valid((void *)b,sizeof(int));
__e_acsl_and_9 = __e_acsl_valid_6;
}
- else { __e_acsl_and_9 = 0; }
+ else __e_acsl_and_9 = 0;
__e_acsl_and_10 = ! __e_acsl_and_9;
}
- else { __e_acsl_and_10 = 0; }
+ else __e_acsl_and_10 = 0;
e_acsl_assert(__e_acsl_and_10,(char *)"Assertion",
(char *)"!\\valid(a) && !\\valid(b)",19);
}
-
__retres = 0;
__delete_block((void *)(& n));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 10cc3e9c09f1770691a9f26873326180b5f52e73..7fe560e39252caf7f75e32fad306b33884ebae55 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -153,7 +153,7 @@ int main(void)
__e_acsl_valid = __valid((void *)a,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
if (! __e_acsl_and) {
int __e_acsl_initialized_2;
int __e_acsl_and_2;
@@ -163,14 +163,13 @@ int main(void)
__e_acsl_valid_2 = __valid((void *)b,sizeof(int));
__e_acsl_and_2 = __e_acsl_valid_2;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_and_3 = ! __e_acsl_and_2;
}
- else { __e_acsl_and_3 = 0; }
+ else __e_acsl_and_3 = 0;
e_acsl_assert(__e_acsl_and_3,(char *)"Assertion",
(char *)"!\\valid(a) && !\\valid(b)",12);
}
-
__full_init((void *)(& a));
a = (int *)__malloc(sizeof(int));
__initialize((void *)a,sizeof(int));
@@ -188,7 +187,7 @@ int main(void)
__e_acsl_valid_3 = __valid((void *)a,sizeof(int));
__e_acsl_and_4 = __e_acsl_valid_3;
}
- else { __e_acsl_and_4 = 0; }
+ else __e_acsl_and_4 = 0;
if (__e_acsl_and_4) {
int __e_acsl_initialized_4;
int __e_acsl_and_5;
@@ -198,14 +197,13 @@ int main(void)
__e_acsl_valid_4 = __valid((void *)b,sizeof(int));
__e_acsl_and_5 = __e_acsl_valid_4;
}
- else { __e_acsl_and_5 = 0; }
+ else __e_acsl_and_5 = 0;
__e_acsl_and_6 = __e_acsl_and_5;
}
- else { __e_acsl_and_6 = 0; }
+ else __e_acsl_and_6 = 0;
e_acsl_assert(__e_acsl_and_6,(char *)"Assertion",
(char *)"\\valid(a) && \\valid(b)",16);
}
-
/*@ assert *b ≡ n; */
{
mpz_t __e_acsl;
@@ -219,7 +217,6 @@ int main(void)
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_n);
}
-
__free((void *)b);
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
{
@@ -232,7 +229,7 @@ int main(void)
__e_acsl_valid_5 = __valid((void *)a,sizeof(int));
__e_acsl_and_7 = __e_acsl_valid_5;
}
- else { __e_acsl_and_7 = 0; }
+ else __e_acsl_and_7 = 0;
if (! __e_acsl_and_7) {
int __e_acsl_initialized_6;
int __e_acsl_and_8;
@@ -242,20 +239,19 @@ int main(void)
__e_acsl_valid_6 = __valid((void *)b,sizeof(int));
__e_acsl_and_8 = __e_acsl_valid_6;
}
- else { __e_acsl_and_8 = 0; }
+ else __e_acsl_and_8 = 0;
__e_acsl_and_9 = ! __e_acsl_and_8;
}
- else { __e_acsl_and_9 = 0; }
+ else __e_acsl_and_9 = 0;
e_acsl_assert(__e_acsl_and_9,(char *)"Assertion",
(char *)"!\\valid(a) && !\\valid(b)",19);
}
-
__retres = 0;
__delete_block((void *)(& n));
__delete_block((void *)(& b));
__delete_block((void *)(& a));
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index b52dfeec5b45556c9d8bfdb3fe580143e09946c2..fd0f8641dd06cdee2fd7f7c1b569cab045365e43 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -108,13 +108,12 @@ struct list *f(struct list *l)
__e_acsl_valid_2 = __valid((void *)l->next,sizeof(struct list));
__e_acsl_and = __e_acsl_valid_2;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
__e_acsl_and_2 = ! __e_acsl_and;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_at_3 = __e_acsl_and_2;
}
-
__store_block((void *)(& __e_acsl_at_2),4U);
__full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = l;
@@ -123,28 +122,29 @@ struct list *f(struct list *l)
__e_acsl_at = l == (void *)0;
if (l == (void *)0) {
__retres = l;
- goto return_label; }
+ goto return_label;
+ }
if (l->next == (void *)0) {
__retres = l;
- goto return_label; }
- __retres = (struct list *)((void *)0);
- return_label: /* internal */
- {
- int __e_acsl_implies;
- int __e_acsl_implies_2;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = __retres == __e_acsl_at_2; }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(l == \\null) ==> \\result == \\old(l)",18);
- if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
- e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)",
- 22);
- __delete_block((void *)(& l));
- return (__retres);
+ goto return_label;
}
-
+ __retres = (struct list *)((void *)0);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else __e_acsl_implies = __retres == __e_acsl_at_2;
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(l == \\null) ==> \\result == \\old(l)",18);
+ if (! __e_acsl_at_3) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = __retres == __e_acsl_at_4;
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)",
+ 22);
+ __delete_block((void *)(& l));
+ return __retres;
+ }
}
int main(void)
@@ -153,7 +153,7 @@ int main(void)
f((struct list *)((void *)0));
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index b52dfeec5b45556c9d8bfdb3fe580143e09946c2..fd0f8641dd06cdee2fd7f7c1b569cab045365e43 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -108,13 +108,12 @@ struct list *f(struct list *l)
__e_acsl_valid_2 = __valid((void *)l->next,sizeof(struct list));
__e_acsl_and = __e_acsl_valid_2;
}
- else { __e_acsl_and = 0; }
+ else __e_acsl_and = 0;
__e_acsl_and_2 = ! __e_acsl_and;
}
- else { __e_acsl_and_2 = 0; }
+ else __e_acsl_and_2 = 0;
__e_acsl_at_3 = __e_acsl_and_2;
}
-
__store_block((void *)(& __e_acsl_at_2),4U);
__full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = l;
@@ -123,28 +122,29 @@ struct list *f(struct list *l)
__e_acsl_at = l == (void *)0;
if (l == (void *)0) {
__retres = l;
- goto return_label; }
+ goto return_label;
+ }
if (l->next == (void *)0) {
__retres = l;
- goto return_label; }
- __retres = (struct list *)((void *)0);
- return_label: /* internal */
- {
- int __e_acsl_implies;
- int __e_acsl_implies_2;
- if (! __e_acsl_at) { __e_acsl_implies = 1; }
- else { __e_acsl_implies = __retres == __e_acsl_at_2; }
- e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(l == \\null) ==> \\result == \\old(l)",18);
- if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
- else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
- e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)",
- 22);
- __delete_block((void *)(& l));
- return (__retres);
+ goto return_label;
}
-
+ __retres = (struct list *)((void *)0);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) __e_acsl_implies = 1;
+ else __e_acsl_implies = __retres == __e_acsl_at_2;
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(l == \\null) ==> \\result == \\old(l)",18);
+ if (! __e_acsl_at_3) __e_acsl_implies_2 = 1;
+ else __e_acsl_implies_2 = __retres == __e_acsl_at_4;
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)",
+ 22);
+ __delete_block((void *)(& l));
+ return __retres;
+ }
}
int main(void)
@@ -153,7 +153,7 @@ int main(void)
f((struct list *)((void *)0));
__retres = 0;
__clean();
- return (__retres);
+ return __retres;
}