diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index f64d25acbeb515fba21482229e017ca66e94bb22..98cad6513199bdb168fb729cb1fd4a44ba181d4e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -30,14 +30,18 @@ int main(void)
}
__retres = 0;
goto return_label;
- lbl_1: __e_acsl_full_init((void *)(& p));
- p = & a;
+ lbl_1: {
+ __e_acsl_full_init((void *)(& p));
+ p = & a;
+ }
goto lbl_2;
return_label:
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& a));
- __e_acsl_memory_clean();
- return __retres;
+ {
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+ }
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index a209e7ff76172c930e730061e159b4c84414873a..9390aede98cae4c5436ef701e426508af52292cb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -30,14 +30,18 @@ int main(void)
}
__retres = 0;
goto return_label;
- lbl_1: __e_acsl_full_init((void *)(& p));
- p = & a;
+ lbl_1: {
+ __e_acsl_full_init((void *)(& p));
+ p = & a;
+ }
goto lbl_2;
return_label:
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& a));
- __e_acsl_memory_clean();
- return __retres;
+ {
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+ }
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index e7eb39cd366c745e5b236888c46e69b4dde356e9..0fe323393c383c6ef4c610103292101021b5ada5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -14,9 +14,11 @@ void f(void)
__gen_e_acsl_at_3 = A;
__gen_e_acsl_at = A;
A = 1;
- F: __gen_e_acsl_at_4 = __gen_e_acsl_at_3;
- __gen_e_acsl_at_2 = A;
- A = 2;
+ F: {
+ __gen_e_acsl_at_4 = __gen_e_acsl_at_3;
+ __gen_e_acsl_at_2 = A;
+ A = 2;
+ }
/*@ assert \at(A,Pre) ≡ 0; */
__e_acsl_assert(__gen_e_acsl_at == 0,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,Pre) == 0",11);
@@ -48,39 +50,44 @@ void g(int *p, int *q)
*q = 0;
L1:
{
- int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,
+ (void *)(& q));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",28);
+ __gen_e_acsl_at_3 = *q;
+ }
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",28);
- __gen_e_acsl_at_3 = *q;
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",26);
+ __gen_e_acsl_at = *q;
+ }
+ __e_acsl_initialize((void *)p,sizeof(int));
+ *p = 2;
}
- {
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
- }
- __e_acsl_initialize((void *)p,sizeof(int));
- *p = 2;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__e_acsl_initialize((void *)q,sizeof(int));
*q = 1;
L2:
{
- int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
- 26);
- __gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
+ {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
+ 26);
+ __gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
+ }
+ A = 4;
}
- A = 4;
/*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
__e_acsl_assert(__gen_e_acsl_at_2 == 2,(char *)"Assertion",(char *)"g",
(char *)"\\at(*(p + \\at(*q,L1)),L2) == 2",26);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 1883d05a943788036e73245d57367347b8b8c737..817040d8a25ed8487bb3d0490e2298d7df15b710 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -26,16 +26,18 @@ void f(void)
}
A = 1;
F:
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
{
- __e_acsl_mpz_t __gen_e_acsl_A_2;
- __gmpz_init_set_si(__gen_e_acsl_A_2,(long)A);
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_2));
- __gmpz_clear(__gen_e_acsl_A_2);
+ __gmpz_init_set(__gen_e_acsl_at_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
+ {
+ __e_acsl_mpz_t __gen_e_acsl_A_2;
+ __gmpz_init_set_si(__gen_e_acsl_A_2,(long)A);
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_2));
+ __gmpz_clear(__gen_e_acsl_A_2);
+ }
+ A = 2;
}
- A = 2;
/*@ assert \at(A,Pre) ≡ 0; */
{
__e_acsl_mpz_t __gen_e_acsl_;
@@ -105,43 +107,48 @@ void g(int *p, int *q)
*q = 0;
L1:
{
- int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
+ (void *)q,
+ (void *)(& q));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",28);
+ __gen_e_acsl_at_3 = *q;
+ }
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",28);
- __gen_e_acsl_at_3 = *q;
- }
- {
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
- (void *)q,(void *)(& q));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(q)",26);
+ __gen_e_acsl_at = *q;
+ }
+ __e_acsl_initialize((void *)p,sizeof(int));
+ *p = 2;
}
- __e_acsl_initialize((void *)p,sizeof(int));
- *p = 2;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__e_acsl_initialize((void *)q,sizeof(int));
*q = 1;
L2:
{
- int __gen_e_acsl_valid_read_2;
- __e_acsl_mpz_t __gen_e_acsl_;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
- 26);
- __gmpz_init_set_si(__gen_e_acsl_,(long)*(p + __gen_e_acsl_at));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
+ {
+ int __gen_e_acsl_valid_read_2;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
+ 26);
+ __gmpz_init_set_si(__gen_e_acsl_,(long)*(p + __gen_e_acsl_at));
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ A = 4;
}
- A = 4;
/*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
{
__e_acsl_mpz_t __gen_e_acsl__2;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
index 55fddf6c64864b3db007736e01d33c4024db09ca..aa901fe0925501b3554fdd9e20528bbdb0e2005c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
@@ -17,8 +17,10 @@ int main(void)
__e_acsl_globals_init();
__e_acsl_store_block((void *)(& b),(size_t)8);
goto _LOR;
- _LOR: __e_acsl_full_init((void *)(& b));
- b = & a;
+ _LOR: {
+ __e_acsl_full_init((void *)(& b));
+ b = & a;
+ }
if (a) goto _LOR;
/*@ assert \initialized(b); */
{