update oracle wrt Frama-C master after merging E-ACSL v0.8

src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle

 tests/bts/bts1307.i:14:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
 tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
 tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float

src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/bts/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)

src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 tests/bts/bts1395.i:8:[value] warning: detected recursive call
                  (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:6 <-

src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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/bts/oracle/bts1399.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
 tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i - 1;

src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle

@@ -2,5 +2,6 @@
 [e-acsl] warning: annotating undefined function `atoi':
                   the generated program may miss memory instrumentation
                   if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 tests/bts/bts2231.i:8:[value] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c

@@ -38,13 +38,15 @@ int main(void)
   }
   /*@ assert \initialized((union msg *)((unsigned char *)buf)); */
   {
-    int __gen_e_acsl_initialized;
-    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(buf),
-                                                    sizeof(union msg));
-    __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
-                    (char *)"main",
-                    (char *)"\\initialized((union msg *)((unsigned char *)buf))",
-                    23);
+    {
+      int __gen_e_acsl_initialized;
+      __gen_e_acsl_initialized = __e_acsl_initialized((void *)(buf),
+                                                      sizeof(union msg));
+      __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
+                      (char *)"main",
+                      (char *)"\\initialized((union msg *)((unsigned char *)buf))",
+                      23);
+    }
   }
   __retres = 0;
   __e_acsl_delete_block((void *)(buf));

src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c

@@ -12,27 +12,31 @@ int main(void)
   __e_acsl_store_block((void *)(& s),0UL);
   /*@ assert \valid(&s); */
   {
-    int __gen_e_acsl_valid;
-    __gen_e_acsl_valid = __e_acsl_valid((void *)(& s),sizeof(struct toto));
-    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
-                    (char *)"\\valid(&s)",9);
+    {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)(& s),sizeof(struct toto));
+      __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+                      (char *)"\\valid(&s)",9);
+    }
   }
   __e_acsl_full_init((void *)(& p));
   p = & s;
   /*@ assert \valid(p); */
   {
-    int __gen_e_acsl_initialized;
-    int __gen_e_acsl_and;
-    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
-                                                    sizeof(struct toto *));
-    if (__gen_e_acsl_initialized) {
-      int __gen_e_acsl_valid_2;
-      __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(struct toto));
-      __gen_e_acsl_and = __gen_e_acsl_valid_2;
+    {
+      int __gen_e_acsl_initialized;
+      int __gen_e_acsl_and;
+      __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+                                                      sizeof(struct toto *));
+      if (__gen_e_acsl_initialized) {
+        int __gen_e_acsl_valid_2;
+        __gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(struct toto));
+        __gen_e_acsl_and = __gen_e_acsl_valid_2;
+      }
+      else __gen_e_acsl_and = 0;
+      __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+                      (char *)"\\valid(p)",12);
     }
-    else __gen_e_acsl_and = 0;
-    __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
-                    (char *)"\\valid(p)",12);
   }
   __retres = 0;
   __e_acsl_delete_block((void *)(& p));

src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c

@@ -13,18 +13,20 @@ int main(void)
   lbl_2:
     /*@ 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;
+      {
+        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 *)"main",
+                        (char *)"\\valid(p)",10);
       }
-      else __gen_e_acsl_and = 0;
-      __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
-                      (char *)"\\valid(p)",10);
     }
     __retres = 0;
     goto return_label;