From bb75804d4c10bb9e24a2d88544c74c85f354cc44 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 10 Apr 2017 16:00:50 +0200
Subject: [PATCH] update oracle
---
.../tests/runtime/oracle/gen_early_exit.c | 256 +++++++++---------
1 file changed, 128 insertions(+), 128 deletions(-)
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 1cf55bb1773..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); */
+ /*@ 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);
+ __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,132 +87,132 @@ int goto_valid(void)
goto FIRST;
__e_acsl_full_init((void *)(& p));
p = (int *)0;
- __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;
- __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,
+ 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_4 = __gen_e_acsl_valid_4;
+ __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),(void *)q,
- (void *)(& q));
- __gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
+ __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_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_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;
+ __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);
+ __gen_e_acsl_and_6 = __gen_e_acsl_valid_6;
}
- __retres = 0;
- __e_acsl_delete_block((void *)(& r));
- __e_acsl_delete_block((void *)(& q));
- __e_acsl_delete_block((void *)(& p));
- return __retres;
+ 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)
@@ -296,10 +296,10 @@ int switch_valid(void)
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 *)(& 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));
@@ -522,9 +522,9 @@ void continue_valid(void)
int i = 0;
while (1) {
int tmp;
- tmp = i;
- i ++;
- ;
+ tmp = i;
+ i ++;
+ ;
if (! tmp) break;
{
/*@ assert ¬\valid(p); */
--
GitLab