From 84187b900c70e789d7bf20828f2c8af11fceef82 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 12 Apr 2017 18:59:12 +0200
Subject: [PATCH] update oracles
---
.../e-acsl/tests/bts/oracle/gen_bts1395.c | 6 +-
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 42 +-
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 42 +-
.../e-acsl/tests/bts/oracle/gen_bts1740.c | 40 +-
.../e-acsl/tests/bts/oracle/gen_bts1837.c | 10 +-
.../e-acsl/tests/bts/oracle/gen_bts2192.c | 6 +-
src/plugins/e-acsl/tests/gmp/oracle/gen_at.c | 103 +++--
src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c | 211 +++++-----
.../tests/runtime/oracle/gen_early_exit.c | 390 +++++++++---------
.../tests/runtime/oracle/gen_labeled_stmt.c | 26 +-
.../tests/runtime/oracle/gen_local_goto.c | 72 ++--
11 files changed, 466 insertions(+), 482 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index 4a502b1e822..ce014ccd5a2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -12,10 +12,8 @@ int fact(int n)
__retres = 1;
goto return_label;
}
- { /* sequence */
- tmp = __gen_e_acsl_fact(n - 1);
- ;
- }
+ tmp = __gen_e_acsl_fact(n - 1);
+ ;
__retres = n * tmp;
return_label: return __retres;
}
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 8849e28f584..c403fd5ceeb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -11,32 +11,32 @@ int main(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ assert \valid(p); */
- {
- int __gen_e_acsl_initialized;
- int __gen_e_acsl_and;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized) {
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
- (void *)(& p));
- __gen_e_acsl_and = __gen_e_acsl_valid;
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(p)",10);
+ /*@ assert \valid(p); */
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- __retres = 0;
- goto return_label;
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",10);
+ }
+ __retres = 0;
+ goto return_label;
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 6a1f4846740..bdf3b4a98f0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -11,32 +11,32 @@ int main(void)
__e_acsl_full_init((void *)(& a));
goto lbl_1;
lbl_2:
- /*@ assert \valid(p); */
- {
- int __gen_e_acsl_initialized;
- int __gen_e_acsl_and;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized) {
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
- (void *)(& p));
- __gen_e_acsl_and = __gen_e_acsl_valid;
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(p)",13);
+ /*@ assert \valid(p); */
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- __retres = 0;
- goto return_label;
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ goto return_label;
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_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 1be5aa98ba9..7421ceccaa3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -33,27 +33,27 @@ int main(void)
__e_acsl_delete_block((void *)(& a));
}
L:
- /*@ assert ¬\valid(p); */
- {
- int __gen_e_acsl_initialized_2;
- int __gen_e_acsl_and_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized_2) {
- int __gen_e_acsl_valid_2;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
- }
- else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
- (char *)"main",(char *)"!\\valid(p)",16);
+ /*@ assert ¬\valid(p); */
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_memory_clean();
- return __retres;
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"!\\valid(p)",16);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 26fe680be04..680fca00da0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -90,12 +90,10 @@ int main(void)
int i = 4;
while (1) {
int tmp;
- { /* sequence */
- tmp = i;
- /*@ assert Value: signed_overflow: -2147483648 ≤ i - 1; */
- i --;
- ;
- }
+ tmp = i;
+ /*@ assert Value: signed_overflow: -2147483648 ≤ i - 1; */
+ i --;
+ ;
if (! tmp) break;
{
char *s = (char *)__gen_e_acsl_literal_string_3;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
index c56a8ba6a99..db197044b28 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -19,10 +19,8 @@ int main(int argc, char **argv)
int __retres;
__e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
- { /* sequence */
- argc = __gen_e_acsl_atoi((char const *)n);
- a = argc;
- }
+ argc = __gen_e_acsl_atoi((char const *)n);
+ a = argc;
__retres = 0;
__e_acsl_delete_block((void *)(& n));
__e_acsl_memory_clean();
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 0be34f3867c..50e175fcb04 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -47,61 +47,60 @@ void g(int *p, int *q)
__e_acsl_initialize((void *)q,sizeof(int));
*q = 0;
L1:
- {
- 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),
+ {
+ 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,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
- }
- __e_acsl_initialize((void *)p,sizeof(int));
+ __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_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);
- }
- A = 4;
+ {
+ 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;
/*@ 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);
L3:
- /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
- {
- int __gen_e_acsl_valid_read_4;
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
- sizeof(int),(void *)p,
- (void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
- 28);
- __e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,(char *)"Assertion",
- (char *)"g",
- (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
- }
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- return;
+ /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
+ {
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
+ sizeof(int),(void *)p,
+ (void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
+ (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
+ 28);
+ __e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,(char *)"Assertion",
+ (char *)"g",(char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",
+ 28);
+ }
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ return;
}
/*@ ensures \result ≡ \old(x); */
@@ -129,14 +128,14 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- __gen_e_acsl_at_3 = (long)x;
- __gen_e_acsl_at_2 = x + 1L;
- __gen_e_acsl_at = x;
- /*@ assert x ≡ 0; */
- __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",
- (char *)"x == 0",43);
- __e_acsl_full_init((void *)(& x));
- x = 1;
+ __gen_e_acsl_at_3 = (long)x;
+ __gen_e_acsl_at_2 = x + 1L;
+ __gen_e_acsl_at = x;
+ /*@ assert x ≡ 0; */
+ __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
+ 43);
+ __e_acsl_full_init((void *)(& x));
+ x = 1;
__e_acsl_full_init((void *)(& x));
x = 2;
__gen_e_acsl_f();
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 832354a78aa..5b54cad0dde 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,16 @@ 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);
- }
- 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;
/*@ assert \at(A,Pre) ≡ 0; */
{
__e_acsl_mpz_t __gen_e_acsl_;
@@ -104,45 +104,44 @@ void g(int *p, int *q)
__e_acsl_initialize((void *)q,sizeof(int));
*q = 0;
L1:
- {
- 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),
+ {
+ 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,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(q)",26);
- __gen_e_acsl_at = *q;
- }
- __e_acsl_initialize((void *)p,sizeof(int));
+ __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_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_);
- }
- A = 4;
+ {
+ 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;
/*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
{
__e_acsl_mpz_t __gen_e_acsl__2;
@@ -155,24 +154,24 @@ void g(int *p, int *q)
__gmpz_clear(__gen_e_acsl__2);
}
L3:
- /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
- {
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
- __gmpz_init_set_si(__gen_e_acsl__4,2L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"g",
- (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl__4);
- }
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- __gmpz_clear(__gen_e_acsl_at_2);
- return;
+ /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
+ __gmpz_init_set_si(__gen_e_acsl__4,2L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"g",
+ (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ __gmpz_clear(__gen_e_acsl_at_2);
+ return;
}
/*@ ensures \result ≡ \old(x); */
@@ -199,52 +198,52 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- {
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __gmpz_init_set(__gen_e_acsl_at_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_add);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set(__gen_e_acsl_at,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
- __gmpz_clear(__gen_e_acsl_x_2);
- }
- /*@ assert x ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
- (char *)"main",(char *)"x == 0",43);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_);
- }
- __e_acsl_full_init((void *)(& x));
- x = 1;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set(__gen_e_acsl_at,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_init_set(__gen_e_acsl_at_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+ __gmpz_init_set(__gen_e_acsl_at,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
+ __gmpz_clear(__gen_e_acsl_x_2);
+ }
+ /*@ assert x ≡ 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"x == 0",43);
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ __e_acsl_full_init((void *)(& x));
+ x = 1;
__e_acsl_full_init((void *)(& x));
x = 2;
__gen_e_acsl_f();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
index f612e32bb61..84815259070 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -32,26 +32,26 @@ int goto_bts(void)
__e_acsl_delete_block((void *)(& a));
}
L:
- /*@ assert ¬\valid(p); */
- {
- int __gen_e_acsl_initialized_2;
- int __gen_e_acsl_and_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized_2) {
- int __gen_e_acsl_valid_2;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
- }
- else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
- (char *)"goto_bts",(char *)"!\\valid(p)",18);
+ /*@ assert ¬\valid(p); */
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& p));
- return __retres;
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"goto_bts",(char *)"!\\valid(p)",18);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& p));
+ return __retres;
}
int goto_valid(void)
@@ -87,136 +87,132 @@ int goto_valid(void)
goto FIRST;
__e_acsl_full_init((void *)(& p));
p = (int *)0;
- { /* sequence */
- __e_acsl_full_init((void *)(& q));
- q = & a;
- __e_acsl_full_init((void *)(& r));
- r = q;
- }
+ __e_acsl_full_init((void *)(& q));
+ q = & a;
+ __e_acsl_full_init((void *)(& r));
+ r = q;
__e_acsl_delete_block((void *)(& a3));
__e_acsl_delete_block((void *)(& a2));
}
}
FIRST:
- /*@ assert \valid(p); */
- {
- int __gen_e_acsl_initialized;
- int __gen_e_acsl_and;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized) {
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __gen_e_acsl_and = __gen_e_acsl_valid;
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
- (char *)"goto_valid",(char *)"\\valid(p)",46);
- }
- /*@ assert ¬\valid(q); */
- {
- int __gen_e_acsl_initialized_2;
- int __gen_e_acsl_and_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
- sizeof(int *));
- if (__gen_e_acsl_initialized_2) {
- int __gen_e_acsl_valid_2;
- /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q,(void *)(& q));
- __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
- }
- else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(q)",47);
- }
- /*@ assert ¬\valid(r); */
- {
- int __gen_e_acsl_initialized_3;
- int __gen_e_acsl_and_3;
- __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& r),
- sizeof(int *));
- if (__gen_e_acsl_initialized_3) {
- int __gen_e_acsl_valid_3;
- /*@ assert Value: dangling_pointer: ¬\dangling(&r); */
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
- (void *)r,(void *)(& r));
- __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
- }
- else __gen_e_acsl_and_3 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_3,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(r)",48);
- }
- __e_acsl_delete_block((void *)(& a1));
- goto SECOND;
- { /* sequence */
- __e_acsl_full_init((void *)(& q));
- q = & a;
- __e_acsl_full_init((void *)(& r));
- r = q;
- __e_acsl_full_init((void *)(& p));
- p = r;
- }
- __e_acsl_delete_block((void *)(& a1));
- }
- SECOND:
- /*@ assert ¬\valid(p); */
+ /*@ assert \valid(p); */
{
- int __gen_e_acsl_initialized_4;
- int __gen_e_acsl_and_4;
- __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized_4) {
- int __gen_e_acsl_valid_4;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- else __gen_e_acsl_and_4 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(p)",56);
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"\\valid(p)",46);
}
/*@ assert ¬\valid(q); */
{
- int __gen_e_acsl_initialized_5;
- int __gen_e_acsl_and_5;
- __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& q),
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
sizeof(int *));
- if (__gen_e_acsl_initialized_5) {
- int __gen_e_acsl_valid_5;
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
/*@ assert Value: dangling_pointer: ¬\dangling(&q); */
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
(void *)q,(void *)(& q));
- __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- else __gen_e_acsl_and_5 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_5,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(q)",57);
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(q)",47);
}
/*@ assert ¬\valid(r); */
{
- int __gen_e_acsl_initialized_6;
- int __gen_e_acsl_and_6;
- __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& r),
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& r),
sizeof(int *));
- if (__gen_e_acsl_initialized_6) {
- int __gen_e_acsl_valid_6;
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
/*@ assert Value: dangling_pointer: ¬\dangling(&r); */
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)r,sizeof(int),
(void *)r,(void *)(& r));
- __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
}
- else __gen_e_acsl_and_6 = 0;
- __e_acsl_assert(! __gen_e_acsl_and_6,(char *)"Assertion",
- (char *)"goto_valid",(char *)"!\\valid(r)",58);
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(r)",48);
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& r));
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- return __retres;
+ __e_acsl_delete_block((void *)(& a1));
+ goto SECOND;
+ __e_acsl_full_init((void *)(& q));
+ q = & a;
+ __e_acsl_full_init((void *)(& r));
+ r = q;
+ __e_acsl_full_init((void *)(& p));
+ p = r;
+ __e_acsl_delete_block((void *)(& a1));
+ }
+ SECOND:
+ /*@ assert ¬\valid(p); */
+ {
+ int __gen_e_acsl_initialized_4;
+ int __gen_e_acsl_and_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_4) {
+ int __gen_e_acsl_valid_4;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+ (void *)(& p));
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ }
+ else __gen_e_acsl_and_4 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_4,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(p)",56);
+ }
+ /*@ assert ¬\valid(q); */
+ {
+ int __gen_e_acsl_initialized_5;
+ int __gen_e_acsl_and_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_5) {
+ int __gen_e_acsl_valid_5;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)q,sizeof(int),(void *)q,
+ (void *)(& q));
+ __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ }
+ else __gen_e_acsl_and_5 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_5,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(q)",57);
+ }
+ /*@ assert ¬\valid(r); */
+ {
+ int __gen_e_acsl_initialized_6;
+ int __gen_e_acsl_and_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& r),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_6) {
+ int __gen_e_acsl_valid_6;
+ /*@ assert Value: dangling_pointer: ¬\dangling(&r); */
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)r,sizeof(int),(void *)r,
+ (void *)(& r));
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
+ }
+ else __gen_e_acsl_and_6 = 0;
+ __e_acsl_assert(! __gen_e_acsl_and_6,(char *)"Assertion",
+ (char *)"goto_valid",(char *)"!\\valid(r)",58);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& r));
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ return __retres;
}
int switch_valid(void)
@@ -235,81 +231,79 @@ int switch_valid(void)
s = & i;
switch (i) {
default:
+ {
+ int a1 = 0;
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
+ __e_acsl_full_init((void *)(& a1));
+ __e_acsl_full_init((void *)(& p));
+ p = & a1;
{
- int a1 = 0;
- __e_acsl_store_block((void *)(& a1),(size_t)4);
- __e_acsl_full_init((void *)(& a1));
- __e_acsl_full_init((void *)(& p));
- p = & a1;
+ int a2 = 0;
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
+ __e_acsl_full_init((void *)(& a2));
+ __e_acsl_full_init((void *)(& q));
+ q = & a2;
+ /*@ assert \valid(p); */
{
- int a2 = 0;
- __e_acsl_store_block((void *)(& a2),(size_t)4);
- __e_acsl_full_init((void *)(& a2));
- __e_acsl_full_init((void *)(& q));
- q = & a2;
- /*@ assert \valid(p); */
- {
- int __gen_e_acsl_initialized;
- int __gen_e_acsl_and;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
- sizeof(int *));
- if (__gen_e_acsl_initialized) {
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __gen_e_acsl_and = __gen_e_acsl_valid;
- }
- else __gen_e_acsl_and = 0;
- __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
- (char *)"switch_valid",(char *)"\\valid(p)",76);
- }
- /*@ assert \valid(q); */
- {
- int __gen_e_acsl_initialized_2;
- int __gen_e_acsl_and_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
- sizeof(int *));
- if (__gen_e_acsl_initialized_2) {
- int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
- (void *)q,(void *)(& q));
- __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
- }
- else __gen_e_acsl_and_2 = 0;
- __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
- (char *)"switch_valid",(char *)"\\valid(q)",77);
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- /*@ assert \valid(s); */
- {
- int __gen_e_acsl_initialized_3;
- int __gen_e_acsl_and_3;
- __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& s),
- sizeof(int *));
- if (__gen_e_acsl_initialized_3) {
- int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int),
- (void *)s,(void *)(& s));
- __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
- }
- else __gen_e_acsl_and_3 = 0;
- __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",
- (char *)"switch_valid",(char *)"\\valid(s)",78);
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(p)",76);
+ }
+ /*@ assert \valid(q); */
+ {
+ int __gen_e_acsl_initialized_2;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_2) {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
+ (void *)q,(void *)(& q));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
}
- __e_acsl_delete_block((void *)(& a1));
- __e_acsl_delete_block((void *)(& a2));
- break;
- __e_acsl_delete_block((void *)(& a2));
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(q)",77);
}
- { /* sequence */
- __e_acsl_full_init((void *)(& q));
- q = & i;
- __e_acsl_full_init((void *)(& p));
- p = q;
+ /*@ assert \valid(s); */
+ {
+ int __gen_e_acsl_initialized_3;
+ int __gen_e_acsl_and_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& s),
+ sizeof(int *));
+ if (__gen_e_acsl_initialized_3) {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int),
+ (void *)s,(void *)(& s));
+ __gen_e_acsl_and_3 = __gen_e_acsl_valid_3;
+ }
+ else __gen_e_acsl_and_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",
+ (char *)"switch_valid",(char *)"\\valid(s)",78);
}
- __e_acsl_full_init((void *)(& s));
- s = (int *)0;
__e_acsl_delete_block((void *)(& a1));
+ __e_acsl_delete_block((void *)(& a2));
+ break;
+ __e_acsl_delete_block((void *)(& a2));
}
+ __e_acsl_full_init((void *)(& q));
+ q = & i;
+ __e_acsl_full_init((void *)(& p));
+ p = q;
+ __e_acsl_full_init((void *)(& s));
+ s = (int *)0;
+ __e_acsl_delete_block((void *)(& a1));
+ }
}
/*@ assert ¬\valid(q); */
{
@@ -528,11 +522,9 @@ void continue_valid(void)
int i = 0;
while (1) {
int tmp;
- { /* sequence */
- tmp = i;
- i ++;
- ;
- }
+ tmp = i;
+ i ++;
+ ;
if (! tmp) break;
{
/*@ assert ¬\valid(p); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index 93c05dc46f7..f1c3f7afb6d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -10,21 +10,21 @@ int __gen_e_acsl_main(void)
int __retres;
goto L1;
L1:
- /*@ assert X ≡ 0; */
- __e_acsl_assert(X == 0,(char *)"Assertion",(char *)"main",
- (char *)"X == 0",10);
- X = 1;
+ /*@ assert X ≡ 0; */
+ __e_acsl_assert(X == 0,(char *)"Assertion",(char *)"main",(char *)"X == 0",
+ 10);
+ X = 1;
goto L2;
L2:
- /*@ requires X ≡ 1;
- ensures X ≡ 2; */
- {
- __e_acsl_assert(X == 1,(char *)"Precondition",(char *)"main",
- (char *)"X == 1",12);
- X = 2;
- __e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"main",
- (char *)"X == 2",12);
- }
+ /*@ requires X ≡ 1;
+ ensures X ≡ 2; */
+ {
+ __e_acsl_assert(X == 1,(char *)"Precondition",(char *)"main",
+ (char *)"X == 1",12);
+ X = 2;
+ __e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"main",
+ (char *)"X == 2",12);
+ }
if (X) {
X = 3;
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
index 9e517c9ce5a..30d11105244 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
@@ -40,45 +40,45 @@ int main(int argc, char const **argv)
goto RET;
}
AGAIN:
+ {
+ int a;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ a = 1;
+ /*@ assert \valid(&a); */
{
- int a;
- __e_acsl_store_block((void *)(& a),(size_t)4);
- __e_acsl_full_init((void *)(& a));
- a = 1;
- /*@ assert \valid(&a); */
- {
- int __gen_e_acsl_valid;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
- (void *)(& a),(void *)(& a));
- __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
- (char *)"main",(char *)"\\valid(&a)",25);
- }
- if (t == 2) {
- __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_3);
- __e_acsl_delete_block((void *)(& a));
- goto UP;
- }
- else t ++;
- int b = 15;
- __e_acsl_store_block((void *)(& b),(size_t)4);
- __e_acsl_full_init((void *)(& b));
- /*@ assert \valid(&b); */
- {
- int __gen_e_acsl_valid_2;
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
- (void *)(& b),(void *)(& b));
- __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
- (char *)"main",(char *)"\\valid(&b)",36);
- }
- __gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
- (char *)__gen_e_acsl_literal_string_4);
- __e_acsl_delete_block((void *)(& a));
- __e_acsl_delete_block((void *)(& b));
- goto AGAIN;
- __e_acsl_delete_block((void *)(& b));
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)(& a));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&a)",25);
+ }
+ if (t == 2) {
+ __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
+ (char *)__gen_e_acsl_literal_string_3);
__e_acsl_delete_block((void *)(& a));
+ goto UP;
}
+ else t ++;
+ int b = 15;
+ __e_acsl_store_block((void *)(& b),(size_t)4);
+ __e_acsl_full_init((void *)(& b));
+ /*@ assert \valid(&b); */
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+ (void *)(& b),(void *)(& b));
+ __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(&b)",36);
+ }
+ __gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
+ (char *)__gen_e_acsl_literal_string_4);
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_delete_block((void *)(& b));
+ goto AGAIN;
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_delete_block((void *)(& a));
+ }
RET: __retres = 0;
__e_acsl_memory_clean();
return __retres;
--
GitLab