Merge branch 'fix/virgile/325-do-not-clean-globals-too-early' into 'master'

Update tests and oracles against kernel modifications

See merge request !165

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

@@ -124,7 +124,7 @@ int while_valid() {
  * are not recorded twice. */
 void continue_valid() {
   int i = 0;
-  int *p, *q, *r;
+  int *p, *q;
 
   while (i++) {
     /*@ assert ! \valid(p); */

src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle

-[variadic] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
 [e-acsl] beginning translation.
 [e-acsl] warning: annotating undefined function `printf_va_1':
                   the generated program may miss memory instrumentation

src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c

@@ -16,6 +16,7 @@ int main(void)
   int __retres;
   temporal t1;
   temporal t2;
+  temporal *tp;
   temporal tarr[2];
   larger l;
   larger *lp;
@@ -67,7 +68,7 @@ int main(void)
     }
     else __gen_e_acsl_and_3 = 0;
     __e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",(char *)"main",
-                    (char *)"\\valid(t1.p) && \\valid(t1.q)",37);
+                    (char *)"\\valid(t1.p) && \\valid(t1.q)",31);
   }
   /*@ assert ¬\valid(t2.p) ∧ ¬\valid(t2.q); */
   {
@@ -99,7 +100,7 @@ int main(void)
     }
     else __gen_e_acsl_and_6 = 0;
     __e_acsl_assert(__gen_e_acsl_and_6,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(t2.p) && !\\valid(t2.q)",38);
+                    (char *)"!\\valid(t2.p) && !\\valid(t2.q)",32);
   }
   __e_acsl_temporal_memcpy((void *)(& t2),(void *)(& t1),(size_t)16);
   __e_acsl_full_init((void *)(& t2));
@@ -134,7 +135,7 @@ int main(void)
     }
     else __gen_e_acsl_and_9 = 0;
     __e_acsl_assert(__gen_e_acsl_and_9,(char *)"Assertion",(char *)"main",
-                    (char *)"\\valid(t2.p) && \\valid(t2.q)",41);
+                    (char *)"\\valid(t2.p) && \\valid(t2.q)",35);
   }
   __e_acsl_temporal_store_nblock((void *)(& t2.p),(void *)0);
   __e_acsl_initialize((void *)(& t2.p),sizeof(char *));
@@ -174,7 +175,7 @@ int main(void)
     }
     else __gen_e_acsl_and_12 = 0;
     __e_acsl_assert(__gen_e_acsl_and_12,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(t2.p) && \\valid(t2.q)",45);
+                    (char *)"!\\valid(t2.p) && \\valid(t2.q)",39);
   }
   __e_acsl_temporal_memcpy((void *)(& l.t),(void *)(& t2),(size_t)16);
   __e_acsl_initialize((void *)(& l.t),sizeof(struct temporal_t));
@@ -210,7 +211,7 @@ int main(void)
     }
     else __gen_e_acsl_and_15 = 0;
     __e_acsl_assert(__gen_e_acsl_and_15,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(l.t.p) && \\valid(l.t.q)",48);
+                    (char *)"!\\valid(l.t.p) && \\valid(l.t.q)",42);
   }
   __e_acsl_temporal_store_nblock((void *)(& lp),(void *)(& l));
   __e_acsl_full_init((void *)(& lp));
@@ -229,7 +230,7 @@ int main(void)
                                                     (void *)(& lp->t.p),
                                                     (void *)0);
       __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
-                      (char *)"mem_access: \\valid_read(&lp->t.p)",51);
+                      (char *)"mem_access: \\valid_read(&lp->t.p)",45);
       __gen_e_acsl_valid_11 = __e_acsl_valid((void *)lp->t.p,sizeof(char),
                                              (void *)lp->t.p,
                                              (void *)(& lp->t.p));
@@ -237,7 +238,7 @@ int main(void)
     }
     else __gen_e_acsl_and_16 = 0;
     __e_acsl_assert(! __gen_e_acsl_and_16,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(lp->t.p)",51);
+                    (char *)"!\\valid(lp->t.p)",45);
   }
   __e_acsl_temporal_memcpy((void *)(tarr),(void *)(& t2),(size_t)16);
   __e_acsl_initialize((void *)(tarr),sizeof(temporal));
@@ -275,7 +276,7 @@ int main(void)
     }
     else __gen_e_acsl_and_19 = 0;
     __e_acsl_assert(__gen_e_acsl_and_19,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(tarr[0].p) && \\valid(tarr[0].q)",54);
+                    (char *)"!\\valid(tarr[0].p) && \\valid(tarr[0].q)",48);
   }
   __e_acsl_temporal_memcpy((void *)(larr),(void *)(& l),(size_t)32);
   __e_acsl_initialize((void *)(larr),sizeof(larger));
@@ -315,7 +316,7 @@ int main(void)
     else __gen_e_acsl_and_22 = 0;
     __e_acsl_assert(__gen_e_acsl_and_22,(char *)"Assertion",(char *)"main",
                     (char *)"!\\valid(larr[0].t.p) && \\valid(larr[0].t.q)",
-                    57);
+                    51);
   }
   __retres = 0;
   __e_acsl_delete_block((void *)(larr));

src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle

-[variadic] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
 [e-acsl] beginning translation.
 [e-acsl] warning: annotating undefined function `printf_va_1':
                   the generated program may miss memory instrumentation

src/plugins/e-acsl/tests/temporal/t_struct.c

@@ -16,19 +16,13 @@ struct larger_t {
   struct temporal_t t;
 };
 
-struct smaller_t {
-  char c;
-};
-
 typedef struct temporal_t temporal;
 typedef struct larger_t larger;
-typedef struct smaller_t smaller;
 /* }}} */
 
 int main(void) {
   int  a = 1,
        b = 2;
-  smaller s1, s2;
   temporal t1, t2, *tp, tarr[2];
   larger l, *lp, larr[2];