Test case for bypassed variables

src/plugins/e-acsl/tests/runtime/bypassed_var.c

+/* run.config
+   COMMENT: Variable, which declaration is bypassed by a goto jump
+*/
+
+int bypassed_var(int i) {
+  int lst [2];
+  if (i)
+    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 */
+
+    if (!i) {
+      /*@ assert \valid(p); */
+    } else {
+      /*@ 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

+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] warning: Declaration of local variable p at tests/runtime/bypassed_var.c:11 is bypassed by agoto statement at tests/runtime/bypassed_var.c:8
+[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 */
+int bypassed_var(int i)
+{
+  int lst[2];
+  __e_acsl_store_block((void *)(lst),8UL);
+  if (i) goto L;
+  {
+    int *p;
+    __e_acsl_store_block((void *)(& p),8UL);
+    __e_acsl_full_init((void *)(& p));
+    p = (int *)(& lst);
+    L: __e_acsl_store_block_duplicate((void *)(& p),8UL);
+    __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); */
+      {
+        {
+          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);
+        }
+      }
+    }
+    __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),8UL);
+  bypassed_var(0);
+  bypassed_var(1);
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+