Skip to content
Snippets Groups Projects
Commit 15b6816e authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'cherry-pick-oracles' into 'stable/phosphorus' 

synchronize oracles

See merge request !137
parents f5239343 0ab988f4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+ 68
− 68
View file @ 15b6816e
...@@ -234,82 +234,82 @@ int switch_valid(void) ...@@ -234,82 +234,82 @@ int switch_valid(void)
__e_acsl_full_init((void *)(& s)); __e_acsl_full_init((void *)(& s));
s = & i; s = & i;
switch (i) { switch (i) {
default: ; 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 a2 = 0; int a1 = 0;
__e_acsl_store_block((void *)(& a2),(size_t)4); __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a2)); __e_acsl_full_init((void *)(& a1));
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& p));
q = & a2; p = & a1;
/*@ 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 a2 = 0;
int __gen_e_acsl_and_2; __e_acsl_store_block((void *)(& a2),(size_t)4);
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q), __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 *)); sizeof(int *));
if (__gen_e_acsl_initialized_2) { if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_2; int __gen_e_acsl_valid;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int), __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),
(void *)q,(void *)(& q)); (void *)p,(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2; __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);
} }
else __gen_e_acsl_and_2 = 0; /*@ assert \valid(q); */
__e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion", {
(char *)"switch_valid",(char *)"\\valid(q)",77); int __gen_e_acsl_initialized_2;
} int __gen_e_acsl_and_2;
/*@ assert \valid(s); */ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& q),
{ sizeof(int *));
int __gen_e_acsl_initialized_3; if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_and_3; int __gen_e_acsl_valid_2;
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& s), __gen_e_acsl_valid_2 = __e_acsl_valid((void *)q,sizeof(int),
sizeof(int *)); (void *)q,(void *)(& q));
if (__gen_e_acsl_initialized_3) { __gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
int __gen_e_acsl_valid_3; }
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)s,sizeof(int), else __gen_e_acsl_and_2 = 0;
(void *)s,(void *)(& s)); __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
__gen_e_acsl_and_3 = __gen_e_acsl_valid_3; (char *)"switch_valid",(char *)"\\valid(q)",77);
} }
else __gen_e_acsl_and_3 = 0; /*@ assert \valid(s); */
__e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion", {
(char *)"switch_valid",(char *)"\\valid(s)",78); 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_delete_block((void *)(& a1));
__e_acsl_delete_block((void *)(& a2));
break;
__e_acsl_delete_block((void *)(& a2));
}
{ /* sequence */
__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)); __e_acsl_delete_block((void *)(& a1));
__e_acsl_delete_block((void *)(& a2));
break;
__e_acsl_delete_block((void *)(& a2));
} }
{ /* sequence */
__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); */ /*@ assert ¬\valid(q); */
{ {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment