[eacsl:codegen] Add tests for variables in switch tracking

src/plugins/e-acsl/known_bugs/decl_in_switch.c

-/* run.config_ci
-   DONTRUN:
-   COMMENT: Variables declared in the body of switch statements so far cannot
-   COMMENT: be tracked
-*/
-
-int main(int argc, char **argv) {
-  switch(argc) {
-    int *p;
-    default: {
-      p = &argc;
-      /*! assert \valid(p); */
-      break;
-    }
-  }
-  return 0;
-}

src/plugins/e-acsl/tests/bts/issue-eacsl-91.c

+/* run.config_ci
+   COMMENT: frama-c/e-acsl#91, test for misplaced delete_block of local variable
+   in switch.
+   STDOPT: #"-e-acsl-full-mmodel"
+*/
+short a;
+char b()
+{
+  switch (a)
+  {
+    int c = 0;
+  case 0:
+    goto d;
+    /* Empty if statement so that frama-c simplifies this in `int tmp = c;` */
+    if (c)
+      ;
+  }
+d:
+  return 2;
+}
+
+int main()
+{
+  b();
+  return 0;
+}

src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+void duffcopy(char *to, char *from, int count)
+{
+  __e_acsl_store_block((void *)(& from),(size_t)8);
+  __e_acsl_store_block((void *)(& to),(size_t)8);
+  int n = (count + 7) / 8;
+  switch (count % 8) 
+    case 0:
+    while (1) {
+      {
+        char *tmp;
+        char *tmp_0;
+        char *tmp_1;
+        char *tmp_2;
+        char *tmp_3;
+        char *tmp_4;
+        char *tmp_5;
+        char *tmp_6;
+        char *tmp_7;
+        char *tmp_8;
+        char *tmp_9;
+        char *tmp_10;
+        char *tmp_11;
+        char *tmp_12;
+        char *tmp_13;
+        char *tmp_14;
+        __e_acsl_store_block((void *)(& tmp_14),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block((void *)(& tmp),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp));
+        tmp = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_0));
+        tmp_0 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp,sizeof(char));
+        *tmp = *tmp_0;
+        case 7: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_1));
+        tmp_1 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_2));
+        tmp_2 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_1,sizeof(char));
+        *tmp_1 = *tmp_2;
+        case 6: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_3));
+        tmp_3 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_4));
+        tmp_4 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_3,sizeof(char));
+        *tmp_3 = *tmp_4;
+        case 5: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_5));
+        tmp_5 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_6));
+        tmp_6 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_5,sizeof(char));
+        *tmp_5 = *tmp_6;
+        case 4: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_7));
+        tmp_7 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_8));
+        tmp_8 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_7,sizeof(char));
+        *tmp_7 = *tmp_8;
+        case 3: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_9));
+        tmp_9 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_10));
+        tmp_10 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_9,sizeof(char));
+        *tmp_9 = *tmp_10;
+        case 2: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_11));
+        tmp_11 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_12));
+        tmp_12 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_11,sizeof(char));
+        *tmp_11 = *tmp_12;
+        case 1: __e_acsl_store_block_duplicate((void *)(& tmp),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_0),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_1),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_2),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_3),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_4),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_5),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_6),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_7),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_8),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_9),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_10),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_11),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_12),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_13),(size_t)8);
+        __e_acsl_store_block_duplicate((void *)(& tmp_14),(size_t)8);
+        __e_acsl_full_init((void *)(& tmp_13));
+        tmp_13 = to;
+        to ++;
+        __e_acsl_full_init((void *)(& tmp_14));
+        tmp_14 = from;
+        from ++;
+        __e_acsl_initialize((void *)tmp_13,sizeof(char));
+        *tmp_13 = *tmp_14;
+        __e_acsl_delete_block((void *)(& tmp_14));
+        __e_acsl_delete_block((void *)(& tmp_13));
+        __e_acsl_delete_block((void *)(& tmp_12));
+        __e_acsl_delete_block((void *)(& tmp_11));
+        __e_acsl_delete_block((void *)(& tmp_10));
+        __e_acsl_delete_block((void *)(& tmp_9));
+        __e_acsl_delete_block((void *)(& tmp_8));
+        __e_acsl_delete_block((void *)(& tmp_7));
+        __e_acsl_delete_block((void *)(& tmp_6));
+        __e_acsl_delete_block((void *)(& tmp_5));
+        __e_acsl_delete_block((void *)(& tmp_4));
+        __e_acsl_delete_block((void *)(& tmp_3));
+        __e_acsl_delete_block((void *)(& tmp_2));
+        __e_acsl_delete_block((void *)(& tmp_1));
+        __e_acsl_delete_block((void *)(& tmp_0));
+        __e_acsl_delete_block((void *)(& tmp));
+      }
+      n --;
+      if (! (n > 0)) break;
+    }
+  __e_acsl_delete_block((void *)(& from));
+  __e_acsl_delete_block((void *)(& to));
+  return;
+}
+
+void initialize(char *arr, int length)
+{
+  int i;
+  __e_acsl_store_block((void *)(& arr),(size_t)8);
+  i = 0;
+  while (i < length) {
+    __e_acsl_initialize((void *)(arr + i),sizeof(char));
+    *(arr + i) = (char)(length - i);
+    i ++;
+  }
+  __e_acsl_delete_block((void *)(& arr));
+  return;
+}
+
+char source[100];
+char target[100];
+void __e_acsl_globals_init(void)
+{
+  static char __e_acsl_already_run = 0;
+  if (! __e_acsl_already_run) {
+    __e_acsl_already_run = 1;
+    __e_acsl_store_block((void *)(target),(size_t)100);
+    __e_acsl_full_init((void *)(& target));
+    __e_acsl_store_block((void *)(source),(size_t)100);
+    __e_acsl_full_init((void *)(& source));
+  }
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  initialize(source,100);
+  duffcopy(source,target,43);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(target));
+  __e_acsl_delete_block((void *)(source));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+short a;
+char b(void)
+{
+  char __retres;
+  __e_acsl_store_block((void *)(& __retres),(size_t)1);
+  switch ((int)a) {
+    int c = 0;
+    __e_acsl_store_block((void *)(& c),(size_t)4);
+    __e_acsl_full_init((void *)(& c));
+    case 0: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+    __e_acsl_delete_block((void *)(& c));
+    goto d;
+    int tmp = c;
+    __e_acsl_store_block((void *)(& tmp),(size_t)4);
+    __e_acsl_full_init((void *)(& tmp));
+    __e_acsl_delete_block((void *)(& tmp));
+    __e_acsl_delete_block((void *)(& c));
+  }
+  d: {
+       __e_acsl_full_init((void *)(& __retres));
+       __retres = (char)2;
+     }
+  __e_acsl_delete_block((void *)(& __retres));
+  return __retres;
+}
+
+void __e_acsl_globals_init(void)
+{
+  static char __e_acsl_already_run = 0;
+  if (! __e_acsl_already_run) {
+    __e_acsl_already_run = 1;
+    __e_acsl_store_block((void *)(& b),(size_t)1);
+    __e_acsl_full_init((void *)(& b));
+    __e_acsl_store_block((void *)(& a),(size_t)2);
+    __e_acsl_full_init((void *)(& a));
+    __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_tmpnam));
+    __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
+    __e_acsl_full_init((void *)(& __fc_tmpnam));
+    __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_fopen));
+    __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+    __e_acsl_full_init((void *)(& __fc_fopen));
+    __e_acsl_store_block((void *)(& stdin),(size_t)8);
+    __e_acsl_full_init((void *)(& stdin));
+    __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_random48_counter));
+    __e_acsl_store_block((void *)(random48_counter),(size_t)6);
+    __e_acsl_full_init((void *)(& random48_counter));
+    __e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
+    __e_acsl_full_init((void *)(& __fc_random48_init));
+    __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_rand_max));
+  }
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  __e_acsl_store_block((void *)(& __retres),(size_t)4);
+  b();
+  __e_acsl_full_init((void *)(& __retres));
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& b));
+  __e_acsl_delete_block((void *)(& a));
+  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
+  __e_acsl_delete_block((void *)(__fc_tmpnam));
+  __e_acsl_delete_block((void *)(& __fc_p_fopen));
+  __e_acsl_delete_block((void *)(__fc_fopen));
+  __e_acsl_delete_block((void *)(& stdin));
+  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+  __e_acsl_delete_block((void *)(random48_counter));
+  __e_acsl_delete_block((void *)(& __fc_random48_init));
+  __e_acsl_delete_block((void *)(& __fc_rand_max));
+  __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/bts/oracle_dev/bts1386_complex_flowgraph.res.oracle

+[kernel] Parsing tests/bts/bts1386_complex_flowgraph.c (with preprocessing)

src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-91.res.oracle

+[kernel] Parsing tests/bts/issue-eacsl-91.c (with preprocessing)

src/plugins/e-acsl/tests/memory/decl_in_switch.c

+/* run.config_ci
+   COMMENT: Check that variables declared in the body of switch statements are
+   correctly tracked.
+*/
+
+/// Simple declaration in switch
+void decl_in_switch(int value)
+{
+  switch (value)
+  {
+    int *p;
+  default:
+  {
+    p = &value;
+    /*! assert \valid(p); */
+    break;
+  }
+  }
+}
+
+/// Declaration and initialization in a single statement
+/// (local initializer)
+void compound_decl_and_init(int value)
+{
+  int a = 0;
+  /*@ assert \valid(&a); */
+
+  switch (value)
+  {
+    int b = 2;
+    /*@ assert \valid(&b); */
+
+  case 0:;
+    int c = 3;
+    /*@ assert \valid(&c); */
+    break;
+
+  case 1:;
+    int d = 4;
+    /*@ assert \valid(&d); */
+    break;
+  }
+}
+
+/// Separate statements for declaration and initialization
+/// (no local initializer)
+void separate_decl_and_init(int value)
+{
+  int a;
+  a = 1;
+  /*@ assert \valid(&a); */
+
+  switch (value)
+  {
+    int b;
+    b = 2;
+    /*@ assert \valid(&b); */
+
+  case 0:;
+    int c;
+    c = 3;
+    /*@ assert \valid(&c); */
+    break;
+
+  case 1:;
+    int d;
+    d = 4;
+    /*@ assert \valid(&d); */
+    break;
+  }
+}
+
+/// Check label in switch
+void label_in_switch(int value)
+{
+  int done = 0;
+
+  switch (value)
+  {
+  /* standalone label */
+  K:;
+    int d = 0;
+    /*@ assert \valid(&d); */
+
+  /* Label and case on the same statement */
+  L:
+  case 0:;
+    int e = 1;
+    /*@ assert \valid(&e); */
+    break;
+  case 1:;
+    int ff = 2;
+    /*@ assert \valid(&ff); */
+    break;
+  }
+
+  if (!done)
+  {
+    done = 1;
+    if (value < 10)
+    {
+      goto L;
+    }
+    else
+    {
+      goto K;
+    }
+  }
+}
+
+int main(int argc, char **argv)
+{
+  decl_in_switch(argc);
+  compound_decl_and_init(argc);
+  separate_decl_and_init(argc);
+  label_in_switch(argc);
+  return 0;
+}

src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.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] translation done in project "e-acsl".

src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c

 /* Generated by Frama-C */
-typedef unsigned long size_t;
-struct __e_acsl_mpz_struct {
-   int _mp_alloc ;
-   int _mp_size ;
-   unsigned long *_mp_d ;
-};
-typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
-typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
-struct __e_acsl_mpq_struct {
-   __e_acsl_mpz_struct _mp_num ;
-   __e_acsl_mpz_struct _mp_den ;
-};
-typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
-typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
-typedef struct _IO_FILE FILE;
-/*@ ghost extern int __e_acsl_init; */
-
-extern size_t __e_acsl_heap_allocation_size;
-
-typedef unsigned short __uint16_t;
-typedef unsigned int __uint32_t;
-typedef unsigned long __uint64_t;
-typedef long __off_t;
-typedef long __off64_t;
-struct _IO_FILE;
-typedef void _IO_lock_t;
-struct _IO_marker {
-   struct _IO_marker *_next ;
-   struct _IO_FILE *_sbuf ;
-   int _pos ;
-};
-struct _IO_FILE {
-   int _flags ;
-   char *_IO_read_ptr ;
-   char *_IO_read_end ;
-   char *_IO_read_base ;
-   char *_IO_write_base ;
-   char *_IO_write_ptr ;
-   char *_IO_write_end ;
-   char *_IO_buf_base ;
-   char *_IO_buf_end ;
-   char *_IO_save_base ;
-   char *_IO_backup_base ;
-   char *_IO_save_end ;
-   struct _IO_marker *_markers ;
-   struct _IO_FILE *_chain ;
-   int _fileno ;
-   int _flags2 ;
-   __off_t _old_offset ;
-   unsigned short _cur_column ;
-   signed char _vtable_offset ;
-   char _shortbuf[1] ;
-   _IO_lock_t *_lock ;
-   __off64_t _offset ;
-   void *__pad1 ;
-   void *__pad2 ;
-   void *__pad3 ;
-   void *__pad4 ;
-   size_t __pad5 ;
-   int _mode ;
-   char _unused2[((unsigned long)15 * sizeof(int) - (unsigned long)4 * sizeof(void *)) - sizeof(size_t)] ;
-};
-/* compiler builtin: 
-   unsigned int __builtin_bswap32(unsigned int);   */
-/* compiler builtin: 
-   unsigned long __builtin_bswap64(unsigned long);   */
-__inline static unsigned int __bswap_32(unsigned int __bsx)
-{
-  unsigned int tmp;
-  tmp = __builtin_bswap32(__bsx);
-  return tmp;
-}
-
-__inline static __uint64_t __bswap_64(__uint64_t __bsx)
+#include "stdio.h"
+#include "stdlib.h"
+void decl_in_switch(int value)
 {
-  __uint64_t tmp;
-  tmp = __builtin_bswap64(__bsx);
-  return tmp;
+  __e_acsl_store_block((void *)(& value),(size_t)4);
+  switch (value) {
+    int *p;
+    __e_acsl_store_block((void *)(& p),(size_t)8);
+    default: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
+    __e_acsl_full_init((void *)(& p));
+    p = & value;
+    __e_acsl_delete_block((void *)(& p));
+    break;
+    __e_acsl_delete_block((void *)(& p));
+  }
+  __e_acsl_delete_block((void *)(& value));
+  return;
 }
 
-__inline static __uint16_t __uint16_identity(__uint16_t __x)
+void compound_decl_and_init(int value)
 {
-  return __x;
+  int a = 0;
+  __e_acsl_store_block((void *)(& a),(size_t)4);
+  __e_acsl_full_init((void *)(& a));
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+                                        (void *)(& a),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid,"Assertion","compound_decl_and_init",
+                    "\\valid(&a)","tests/memory/decl_in_switch.c",26);
+  }
+  /*@ assert \valid(&a); */ ;
+  switch (value) {
+    int b = 2;
+    {
+      int __gen_e_acsl_valid_2;
+      __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+                                            (void *)(& b),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion",
+                      "compound_decl_and_init","\\valid(&b)",
+                      "tests/memory/decl_in_switch.c",31);
+    }
+    /*@ assert \valid(&b); */ ;
+    case 0: ;
+    int c = 3;
+    __e_acsl_store_block((void *)(& c),(size_t)4);
+    __e_acsl_full_init((void *)(& c));
+    {
+      int __gen_e_acsl_valid_3;
+      __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& c),sizeof(int),
+                                            (void *)(& c),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_3,"Assertion",
+                      "compound_decl_and_init","\\valid(&c)",
+                      "tests/memory/decl_in_switch.c",35);
+    }
+    /*@ assert \valid(&c); */ ;
+    __e_acsl_delete_block((void *)(& c));
+    break;
+    case 1: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+    ;
+    int d = 4;
+    __e_acsl_store_block((void *)(& d),(size_t)4);
+    __e_acsl_full_init((void *)(& d));
+    {
+      int __gen_e_acsl_valid_4;
+      __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& d),sizeof(int),
+                                            (void *)(& d),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_4,"Assertion",
+                      "compound_decl_and_init","\\valid(&d)",
+                      "tests/memory/decl_in_switch.c",40);
+    }
+    /*@ assert \valid(&d); */ ;
+    __e_acsl_delete_block((void *)(& c));
+    __e_acsl_delete_block((void *)(& d));
+    break;
+    __e_acsl_delete_block((void *)(& d));
+    __e_acsl_delete_block((void *)(& c));
+  }
+  __e_acsl_delete_block((void *)(& a));
+  return;
 }
 
-__inline static __uint32_t __uint32_identity(__uint32_t __x)
+void separate_decl_and_init(int value)
 {
-  return __x;
+  int a;
+  __e_acsl_store_block((void *)(& a),(size_t)4);
+  __e_acsl_full_init((void *)(& a));
+  a = 1;
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+                                        (void *)(& a),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid,"Assertion","separate_decl_and_init",
+                    "\\valid(&a)","tests/memory/decl_in_switch.c",51);
+  }
+  /*@ assert \valid(&a); */ ;
+  switch (value) {
+    int b;
+    int c;
+    int d;
+    __e_acsl_store_block((void *)(& d),(size_t)4);
+    __e_acsl_store_block((void *)(& c),(size_t)4);
+    b = 2;
+    {
+      int __gen_e_acsl_valid_2;
+      __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
+                                            (void *)(& b),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion",
+                      "separate_decl_and_init","\\valid(&b)",
+                      "tests/memory/decl_in_switch.c",57);
+    }
+    /*@ assert \valid(&b); */ ;
+    case 0: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+    __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+    ;
+    __e_acsl_full_init((void *)(& c));
+    c = 3;
+    {
+      int __gen_e_acsl_valid_3;
+      __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& c),sizeof(int),
+                                            (void *)(& c),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_3,"Assertion",
+                      "separate_decl_and_init","\\valid(&c)",
+                      "tests/memory/decl_in_switch.c",62);
+    }
+    /*@ assert \valid(&c); */ ;
+    __e_acsl_delete_block((void *)(& c));
+    __e_acsl_delete_block((void *)(& d));
+    break;
+    case 1: __e_acsl_store_block_duplicate((void *)(& c),(size_t)4);
+    __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+    ;
+    __e_acsl_full_init((void *)(& d));
+    d = 4;
+    {
+      int __gen_e_acsl_valid_4;
+      __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& d),sizeof(int),
+                                            (void *)(& d),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_4,"Assertion",
+                      "separate_decl_and_init","\\valid(&d)",
+                      "tests/memory/decl_in_switch.c",68);
+    }
+    /*@ assert \valid(&d); */ ;
+    __e_acsl_delete_block((void *)(& c));
+    __e_acsl_delete_block((void *)(& d));
+    break;
+    __e_acsl_delete_block((void *)(& d));
+    __e_acsl_delete_block((void *)(& c));
+  }
+  __e_acsl_delete_block((void *)(& a));
+  return;
 }
 
-__inline static __uint64_t __uint64_identity(__uint64_t __x)
+void label_in_switch(int value)
 {
-  return __x;
+  int done = 0;
+  switch (value) {
+    K: ;
+    int d = 0;
+    __e_acsl_store_block((void *)(& d),(size_t)4);
+    __e_acsl_full_init((void *)(& d));
+    {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)(& d),sizeof(int),
+                                          (void *)(& d),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid,"Assertion","label_in_switch",
+                      "\\valid(&d)","tests/memory/decl_in_switch.c",83);
+    }
+    /*@ assert \valid(&d); */ ;
+    L: case 0: __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+    ;
+    int e = 1;
+    __e_acsl_store_block((void *)(& e),(size_t)4);
+    __e_acsl_full_init((void *)(& e));
+    {
+      int __gen_e_acsl_valid_2;
+      __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& e),sizeof(int),
+                                            (void *)(& e),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","label_in_switch",
+                      "\\valid(&e)","tests/memory/decl_in_switch.c",89);
+    }
+    /*@ assert \valid(&e); */ ;
+    __e_acsl_delete_block((void *)(& d));
+    __e_acsl_delete_block((void *)(& e));
+    break;
+    case 1: __e_acsl_store_block_duplicate((void *)(& d),(size_t)4);
+    __e_acsl_store_block_duplicate((void *)(& e),(size_t)4);
+    ;
+    int ff = 2;
+    __e_acsl_store_block((void *)(& ff),(size_t)4);
+    __e_acsl_full_init((void *)(& ff));
+    {
+      int __gen_e_acsl_valid_3;
+      __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& ff),sizeof(int),
+                                            (void *)(& ff),(void *)0);
+      __e_acsl_assert(__gen_e_acsl_valid_3,"Assertion","label_in_switch",
+                      "\\valid(&ff)","tests/memory/decl_in_switch.c",93);
+    }
+    /*@ assert \valid(&ff); */ ;
+    __e_acsl_delete_block((void *)(& d));
+    __e_acsl_delete_block((void *)(& e));
+    __e_acsl_delete_block((void *)(& ff));
+    break;
+    __e_acsl_delete_block((void *)(& ff));
+    __e_acsl_delete_block((void *)(& e));
+    __e_acsl_delete_block((void *)(& d));
+  }
+  if (! done) {
+    done = 1;
+    if (value < 10) goto L; else goto K;
+  }
+  return;
 }
 
-/*@
-predicate diffSize{L1, L2}(ℤ i) =
-  \at(__e_acsl_heap_allocation_size,L1) -
-  \at(__e_acsl_heap_allocation_size,L2) ≡ i;
-
-*/
-extern  __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_init)(
-int *x_0, char ***x_1, unsigned long x_2);
-
-extern  __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_store_block)(
-void *x_0, unsigned long x_1);
-
-extern  __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_full_init)(
-void *x_0);
-
-extern  __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_delete_block)(
-void *x_0);
-
-extern  __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_clean)(
-void);
-
 int main(int argc, char **argv)
 {
   int __retres;
-  __e_acsl_memory_init(& argc,& argv,8UL);
-  __e_acsl_memory_init(& argc,& argv,8UL);
-  __e_acsl_store_block((void *)(& argc),4UL);
-  {
-    int *p;
-    __e_acsl_store_block((void *)(& p),8UL);
-    __e_acsl_store_block((void *)(& p),8UL);
-    switch (argc) {
-      default: ;
-      __e_acsl_full_init((void *)(& p));
-      __e_acsl_full_init((void *)(& p));
-      p = & argc;
-      break;
-    }
-    __e_acsl_delete_block((void *)(& p));
-    __e_acsl_delete_block((void *)(& p));
-  }
+  __e_acsl_memory_init(& argc,& argv,(size_t)8);
+  decl_in_switch(argc);
+  compound_decl_and_init(argc);
+  separate_decl_and_init(argc);
+  label_in_switch(argc);
   __retres = 0;
   __e_acsl_delete_block((void *)(& argc));
   __e_acsl_memory_clean();
-  __e_acsl_delete_block((void *)(& argc));
-  __e_acsl_memory_clean();
   return __retres;
 }
 

src/plugins/e-acsl/tests/memory/oracle_dev/decl_in_switch.res.oracle

+[kernel] Parsing tests/memory/decl_in_switch.c (with preprocessing)