synchronize with frama-c/frama-c!1112

src/plugins/e-acsl/tests/bts/oracle/bts1304.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
+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".
 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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1326.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
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1390.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
+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/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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".
 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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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".

src/plugins/e-acsl/tests/bts/oracle/bts1399.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
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1478.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
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1700.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
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1717.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
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1718.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
+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.

src/plugins/e-acsl/tests/bts/oracle/bts1837.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
+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/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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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.

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

@@ -2,6 +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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+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.

src/plugins/e-acsl/tests/bts/oracle/bts2231.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
+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".
 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

 tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Old style K&R code?
 [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
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, 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

 /* Generated by Frama-C */
+#include "stdlib.h"
 struct msgA {
    int type ;
    int a[2] ;
@@ -17,7 +18,7 @@ union msg {
 };
 void read_sensor_4(unsigned int *m)
 {
-  __e_acsl_store_block((void *)(& m),8UL);
+  __e_acsl_store_block((void *)(& m),(size_t)8);
   __e_acsl_initialize((void *)m,sizeof(unsigned int));
   *m = (unsigned int)0;
   __e_acsl_delete_block((void *)(& m));
@@ -29,8 +30,8 @@ int main(void)
   int __retres;
   unsigned char buf[sizeof(union msg)];
   int i;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_store_block((void *)(buf),16UL);
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(buf),(size_t)16);
   i = 0;
   while ((unsigned long)i < sizeof(buf) / (unsigned long)4) {
     read_sensor_4((unsigned int *)(buf) + i);

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

 /* Generated by Frama-C */
+#include "stdlib.h"
 /*@ requires \valid(Mtmax_in);
     requires \valid(Mwmax);
     requires \valid(Mtmax_out);
@@ -23,9 +24,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out);
  */
 void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
 {
-  __e_acsl_store_block((void *)(& Mtmax_in),8UL);
-  __e_acsl_store_block((void *)(& Mwmax),8UL);
-  __e_acsl_store_block((void *)(& Mtmax_out),8UL);
+  __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
+  __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
+  __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
   __e_acsl_initialize((void *)Mtmax_out,sizeof(float));
   *Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
                                                                  5 / 80) * *Mwmax) * 0.4));
@@ -61,9 +62,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out);
  */
 void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
 {
-  __e_acsl_store_block((void *)(& Mtmin_in),8UL);
-  __e_acsl_store_block((void *)(& Mwmin),8UL);
-  __e_acsl_store_block((void *)(& Mtmin_out),8UL);
+  __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
+  __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
+  __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
   __e_acsl_initialize((void *)Mtmin_out,sizeof(float));
   *Mtmin_out = (float)(0.85 * (double)*Mwmin);
   __e_acsl_delete_block((void *)(& Mtmin_in));
@@ -78,10 +79,10 @@ int main(void)
   float f;
   float g;
   float h;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_store_block((void *)(& h),4UL);
-  __e_acsl_store_block((void *)(& g),4UL);
-  __e_acsl_store_block((void *)(& f),4UL);
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(& h),(size_t)4);
+  __e_acsl_store_block((void *)(& g),(size_t)4);
+  __e_acsl_store_block((void *)(& f),(size_t)4);
   __e_acsl_full_init((void *)(& f));
   f = (float)1.0;
   __e_acsl_full_init((void *)(& g));
@@ -119,9 +120,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
     int __gen_e_acsl_valid;
     int __gen_e_acsl_valid_2;
     int __gen_e_acsl_valid_3;
-    __e_acsl_store_block((void *)(& Mtmin_in),8UL);
-    __e_acsl_store_block((void *)(& Mwmin),8UL);
-    __e_acsl_store_block((void *)(& Mtmin_out),8UL);
+    __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
+    __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
+    __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
     __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float));
     __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"bar",
                     (char *)"\\valid(Mtmin_in)",17);
@@ -215,9 +216,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
     int __gen_e_acsl_valid;
     int __gen_e_acsl_valid_2;
     int __gen_e_acsl_valid_3;
-    __e_acsl_store_block((void *)(& Mtmax_in),8UL);
-    __e_acsl_store_block((void *)(& Mwmax),8UL);
-    __e_acsl_store_block((void *)(& Mtmax_out),8UL);
+    __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
+    __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
+    __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
     __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
     __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
                     (char *)"\\valid(Mtmax_in)",5);

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

 /* Generated by Frama-C */
+#include "stdlib.h"
 /*@ behavior yes:
       assumes ∀ int i; 0 < i < n ⇒ *(t + (i - 1)) ≤ *(t + i);
       ensures \result ≡ 1;
@@ -35,8 +36,8 @@ int main(void)
   int __retres;
   int t[7];
   int n;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_store_block((void *)(t),28UL);
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(t),(size_t)28);
   __e_acsl_initialize((void *)(t),sizeof(int));
   t[0] = 1;
   __e_acsl_initialize((void *)(& t[1]),sizeof(int));
@@ -69,7 +70,7 @@ int __gen_e_acsl_sorted(int *t, int n)
 {
   int __gen_e_acsl_at;
   int __retres;
-  __e_acsl_store_block((void *)(& t),8UL);
+  __e_acsl_store_block((void *)(& t),(size_t)8);
   {
     int __gen_e_acsl_forall;
     int __gen_e_acsl_i;