diff --git a/src/plugins/e-acsl/tests/runtime/bypassed_var.c b/src/plugins/e-acsl/tests/runtime/bypassed_var.c index 58b31bc39178a59e77ba52db4b18ffb3113d5d22..5201ef5f9cd6a62ba688ec1779d9c91deb5de918 100644 --- a/src/plugins/e-acsl/tests/runtime/bypassed_var.c +++ b/src/plugins/e-acsl/tests/runtime/bypassed_var.c @@ -2,31 +2,15 @@ COMMENT: Variable, which declaration is bypassed by a goto jump */ -int bypassed_var(int i) { - int lst [2]; - if (i) - goto L; - +int main(int argc, char const **argv) { + goto L; { int *p; - p = &lst; - /* assert \valid(p); */ - L: - p++; /* Important to keep this statement here to make sure - initialize is ran after store_block */ + p = &argc; /* Important to keep this statement here to make sure + initialize is ran after store_block */ - if (!i) { - /*@ assert \valid(p); */ - } else { - /*@ assert !\valid(p); */ - } + /*@ assert \valid(&p); */ } - return i; -} - -int main(int argc, char const **argv) { - bypassed_var(0); - bypassed_var(1); return 0; } diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle index 66bbcfdda0170d72969011310ad46adb416b2591..a0a8836bb7a329fc53da2da239850fee8b952dde 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle @@ -2,4 +2,3 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. -tests/runtime/bypassed_var.c:16:[value] warning: accessing uninitialized left-value. assert \initialized(&p); diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c index acd909e18da7836611e10853460c8a67f296aab4..7e1c554bd6a8077d99a6847b795e72bf054eb0fe 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c +++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c @@ -1,70 +1,30 @@ /* Generated by Frama-C */ #include "stdlib.h" -int bypassed_var(int i) +int main(int argc, char const **argv) { - int lst[2]; - __e_acsl_store_block((void *)(lst),(size_t)8); - if (i) goto L; + int __retres; + __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8); + __e_acsl_store_block((void *)(& argc),(size_t)4); + goto L; { int *p; __e_acsl_store_block((void *)(& p),(size_t)8); - __e_acsl_full_init((void *)(& p)); - p = (int *)(& lst); L: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8); __e_acsl_full_init((void *)(& p)); - /*@ assert Value: initialisation: \initialized(&p); */ - p ++; - if (! i) { - /*@ 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)); - __gen_e_acsl_and = __gen_e_acsl_valid; - } - else __gen_e_acsl_and = 0; - __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion", - (char *)"bypassed_var",(char *)"\\valid(p)",20); - } - } - } - else { - /*@ assert ¬\valid(p); */ + p = & argc; + /*@ 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; - __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int)); - __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 *)"bypassed_var",(char *)"!\\valid(p)",22); - } + int __gen_e_acsl_valid; + __gen_e_acsl_valid = __e_acsl_valid((void *)(& p),sizeof(int *)); + __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion", + (char *)"main",(char *)"\\valid(&p)",13); + __e_acsl_delete_block((void *)(& p)); } } - __e_acsl_delete_block((void *)(& p)); } - __e_acsl_delete_block((void *)(lst)); - return i; -} - -int main(int argc, char const **argv) -{ - int __retres; - __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8); - bypassed_var(0); - bypassed_var(1); __retres = 0; + __e_acsl_delete_block((void *)(& argc)); __e_acsl_memory_clean(); return __retres; }