Fix bypassed_var test to remove undefined behaviours

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;
 }

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);

src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c

 /* 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;
 }