diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
index ec3e89c44a7ab617224670a924ba85351b7c16a1..cee0e88b084e3cc36747e8419637d720e9d18484 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
@@ -1,5 +1,5 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index f2bae8ef88f912808c1881370fc97938448ea63d..d7e404049c577aa955e9640b278bab1162d20e96 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -1,6 +1,6 @@
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
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index 881eb5ae793d5b3f2307ffd5ab9d1c30158f449f..fe811626ae55d4f4cad9b36c80d6b2cd10c966bb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,5 +1,5 @@
[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.)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
index 4e70dabff69357da657149b7b37e368e74a051a3..32524547d5aaeca47698e230d962315131d5776c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
@@ -1,5 +1,5 @@
[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 <-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
index d67894727844413b6bd41676ac1996f0e295bee5..a5cae9217c8e9879837112570eef37312fa75c63 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -1,5 +1,5 @@
[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;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
index f949e40637a83d73ea23dc09343c5dc12ee04d02..ed365527f42e276456b2d4bffd4e5f4980500740 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
index 4346efc85c36363c6c5916a885483ea1ed4f0b5f..079242c90780eac76acf0d6a8ca7844a3273b85b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
@@ -1,5 +1,5 @@
[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index 3e7b66c55fac4ab43c317b9b34c90f04a6ea19b8..a65de6cfc50394b511347f57c99445b5868d5ffb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,6 +1,6 @@
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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 9393af7ffa7edd36a1ee6d67dc1787087096afc0..e6561a3073fcb83a5da8e0a1813344a9195892b8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -1,4 +1,5 @@
/* 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);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index ab8e3d95afd83b5771c8d99c53e0bdd580d3882c..ccf51aabe3e61bb7666fba2f9d1f45dad23d3bdf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -1,4 +1,5 @@
/* 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);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index f9745849a2f6e98699ff8dc569b00fc4b5ccd13b..8a6f07863a3509b04d10f3086c74b4274174195b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -1,4 +1,5 @@
/* 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;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index 3b83bd403733f99d21d659c47f9f32ee69b61e5b..eb341729c74ff62536e0b0f39ef1e298608c6bd6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
typedef int ArrayInt[5];
/*@ ensures
*\old(AverageAccel) ≡
@@ -19,8 +20,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
*/
void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
{
- __e_acsl_store_block((void *)(& Accel),8UL);
- __e_acsl_store_block((void *)(& AverageAccel),8UL);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
+ __e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
__e_acsl_initialize((void *)AverageAccel,sizeof(int));
*AverageAccel = (((((*Accel)[4] + (*Accel)[3]) + (*Accel)[2]) + (*Accel)[1]) + (*Accel)[0]) / 5;
__e_acsl_delete_block((void *)(& Accel));
@@ -33,9 +34,9 @@ int main(void)
int __retres;
ArrayInt Accel;
int av;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& av),4UL);
- __e_acsl_store_block((void *)(Accel),20UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& av),(size_t)4);
+ __e_acsl_store_block((void *)(Accel),(size_t)20);
__e_acsl_initialize((void *)(Accel),sizeof(int));
Accel[0] = 1;
__e_acsl_initialize((void *)(& Accel[1]),sizeof(int));
@@ -70,8 +71,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
ArrayInt *__gen_e_acsl_at_3;
ArrayInt *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
- __e_acsl_store_block((void *)(& Accel),8UL);
- __e_acsl_store_block((void *)(& AverageAccel),8UL);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
+ __e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
__gen_e_acsl_at_6 = Accel;
__gen_e_acsl_at_5 = Accel;
__gen_e_acsl_at_4 = Accel;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 54750d7081e82ee7cdafd8f958007f9b0ce862b8..337f725608d6ad1426073dfa34a9aa7807954031 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
/*@ behavior exists:
@@ -30,9 +31,9 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
- __e_acsl_store_block((void *)(& s),8UL);
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& buf),8UL);
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_store_block((void *)(& buf),(size_t)8);
__e_acsl_full_init((void *)(& s));
s = (char *)buf;
i = 0;
@@ -74,8 +75,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
void const *__gen_e_acsl_at_2;
int __gen_e_acsl_at;
void *__retres;
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& buf),8UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_store_block((void *)(& buf),(size_t)8);
{
int __gen_e_acsl_forall_2;
unsigned int __gen_e_acsl_k;
@@ -200,7 +201,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
__gen_e_acsl_memchr((void const *)__gen_e_acsl_literal_string,'o',
(unsigned long)4);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index a6bdcd87f66153db4f988c98e08ed705f309361e..d6b5a8fee184c3b36cbe00c7919526950524ee0f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
/*@ requires n > 0; */
int __gen_e_acsl_fact(int n);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index e61c3232854b6664eca6470db61ee80eaccc021e..5fb9ec622cebdb86502e0b57dc3b5a29bbc2eb4c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 4e39439e16b29d871019d2cd11fa4f7f8143c5f9..6b0fb4d512e7d921fd31fe45a5d6486a8ccce33e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int global_i;
int *global_i_ptr = & global_i;
@@ -40,9 +41,9 @@ void __gen_e_acsl_loop(void)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& global_i_ptr),8UL);
+ __e_acsl_store_block((void *)(& global_i_ptr),(size_t)8);
__e_acsl_full_init((void *)(& global_i_ptr));
- __e_acsl_store_block((void *)(& global_i),4UL);
+ __e_acsl_store_block((void *)(& global_i),(size_t)4);
__e_acsl_full_init((void *)(& global_i));
return;
}
@@ -50,7 +51,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
__gen_e_acsl_loop();
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index ea16f514ee2e1a68581785744f8f8d65bf5afa87..b9274f28d4d28173855e9815100f64abb72b0a3a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
struct toto {
};
@@ -7,9 +8,9 @@ int main(void)
int __retres;
struct toto s;
struct toto *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& s),0UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& s),(size_t)0);
/*@ assert \valid(&s); */
{
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 0db5c8ad0f78fabf6b3ffdb86094e9c61ff3bd8b..5cc716098080d1cc9566b308e25817662455b372 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
int a;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
a = 10;
goto lbl_1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index d37ffae2b813a8609e2022f5c69791f6b6b033e5..a4cb99369930d1cc3eae7e3e2f3956bbcb0fe75c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
int a;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
a = 10;
goto lbl_1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index c26af6b5ae3123722b9c8df11a458c552e61d5d0..991bdf1b6a656e1de8c29f17967157bd7627ef96 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
@@ -8,8 +9,8 @@ int f(void)
int __retres;
char *s1;
char *s2;
- __e_acsl_store_block((void *)(& s2),8UL);
- __e_acsl_store_block((void *)(& s1),8UL);
+ __e_acsl_store_block((void *)(& s2),(size_t)8);
+ __e_acsl_store_block((void *)(& s1),(size_t)8);
__e_acsl_full_init((void *)(& s1));
s1 = (char *)__gen_e_acsl_literal_string;
__e_acsl_full_init((void *)(& s2));
@@ -79,7 +80,7 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("bar"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_store_block((void *)(& S),8UL);
+ __e_acsl_store_block((void *)(& S),(size_t)8);
__e_acsl_full_init((void *)(& S));
return;
}
@@ -88,7 +89,7 @@ int main(void)
{
int __retres;
int i;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
i = 4;
while (1) {
@@ -102,7 +103,7 @@ int main(void)
if (! tmp) break;
{
char *s;
- __e_acsl_store_block((void *)(& s),8UL);
+ __e_acsl_store_block((void *)(& s),(size_t)8);
__e_acsl_full_init((void *)(& s));
s = (char *)__gen_e_acsl_literal_string_3;
/*@ assert \valid_read(s); */
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index 8d2fa61eada818904459b33f4e093b01fab2ab79..89ea5ede7e28cfe3d2da5e040a47d5afb0d7736a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
struct ST {
@@ -20,7 +21,7 @@ void __e_acsl_globals_init(void)
sizeof("Struct_G[0]"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_store_block((void *)(_G),32UL);
+ __e_acsl_store_block((void *)(_G),(size_t)32);
__e_acsl_full_init((void *)(& _G));
return;
}
@@ -28,7 +29,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
/*@ assert \valid_read(_G[0].str); */
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
index 36fd0bd46ca8de8c1708942497262ea368242ed3..f4dad2e66aaa4366edad123fbc03886896b6ccea 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
int a;
char *n = (char *)"134";
@@ -8,7 +9,7 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("134"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string);
- __e_acsl_store_block((void *)(& n),8UL);
+ __e_acsl_store_block((void *)(& n),(size_t)8);
__e_acsl_full_init((void *)(& n));
return;
}
@@ -16,7 +17,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
{ /* sequence */
argc = __gen_e_acsl_atoi((char const *)n);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
index 174ad1a7f1f2e98f2b3065c046dffc6c281ac36b..cdf0350057f5ed3d31e47d20076816ae7efbd30c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
long A = (long)0;
int main(void)
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 17547beac1f1023c14821f42b8154d44bae42d1c..c6a8d88bbff61ad8f38c238db53028965d8b2e40 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..));
assigns \result \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
@@ -25,9 +26,9 @@ int main(void)
int loc;
char *destbuf;
char ch;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& srcbuf),8UL);
+ __e_acsl_store_block((void *)(& srcbuf),(size_t)8);
__e_acsl_full_init((void *)(& srcbuf));
srcbuf = (char *)__gen_e_acsl_literal_string;
loc = 1;
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
index b95faa854343f762a04eb0c96c4a996c769e2e9b..aa44777703fe9a869d03d1500996a55d92c15375 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
index b95faa854343f762a04eb0c96c4a996c769e2e9b..aa44777703fe9a869d03d1500996a55d92c15375 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
index 46d7ef3a5c194b698bbaf6d21f2781ba2e91d1bb..44756314152d32f74d2ed0eaa49863ec2c96ecfa 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(void)
{
int m;
int *u;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& u));
u = & m;
__e_acsl_full_init((void *)(& p));
@@ -32,7 +33,7 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
x = 0;
f();
/*@ assert &x ≡ &x; */
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
index 1b114dc836d35cb832b79a0dd4f8ddd2b3777a11..f966f94eb42d3380d5fc52657ee1da2313359458 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(void)
{
int m;
int *u;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& u));
u = & m;
__e_acsl_full_init((void *)(& p));
@@ -30,15 +31,15 @@ void f(void)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& __fc_wctomb_state),4UL);
+ __e_acsl_store_block((void *)(& __fc_wctomb_state),(size_t)4);
__e_acsl_full_init((void *)(& __fc_wctomb_state));
- __e_acsl_store_block((void *)(& __fc_mbtowc_state),4UL);
+ __e_acsl_store_block((void *)(& __fc_mbtowc_state),(size_t)4);
__e_acsl_full_init((void *)(& __fc_mbtowc_state));
- __e_acsl_store_block((void *)(& __fc_mblen_state),4UL);
+ __e_acsl_store_block((void *)(& __fc_mblen_state),(size_t)4);
__e_acsl_full_init((void *)(& __fc_mblen_state));
- __e_acsl_store_block((void *)(& __fc_rand_max),8UL);
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
__e_acsl_full_init((void *)(& __fc_rand_max));
- __e_acsl_store_block((void *)(& __fc_random_counter),4UL);
+ __e_acsl_store_block((void *)(& __fc_random_counter),(size_t)4);
__e_acsl_full_init((void *)(& __fc_random_counter));
return;
}
@@ -47,10 +48,10 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& x),4UL);
- __e_acsl_store_block((void *)(& __retres),4UL);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = 0;
f();
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index ef42a641f62119fbd93e0a78e78836cbad3f5a29..2e9ae22fd62363ad7346878981e2f237bac836d0 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
index 7cd3588f92f5b492bf7b55394c9d0e212e7101fd..8af3084fa20690d84c71505510d6772dc64f9311 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
index 1dc1420dc36b4479bde10caf5b85fd739adffa75..12c70c5e505b160bc46ceac3b3444ecfc195ab51 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
index abee4dc3c7a71ac96a286903d8979adf6699f8db..a6f7a745874c3826177e4ae20df967cf1334217b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
index 8a83d5c555e2abfcacc33f777b7b6d9ff5af5c9c..630deaa6d7d421f3bd3dccf34683eb1c738a93dd 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
index 6d02abba82808d0169a60118394903ed94c58d69..1e42f99d35351676f5ebb5c791df285db931cb75 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index 6518cc1154c4d89c1089bd61d500d1f24b9b2504..62cf4517ec4161f8f7b5400e1fdcb065a5222ca7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 9baa5e8c7204ecee26b3f8f3ad4a41e36e4c748a..422f1d17fe82242788a3c32ec696e7c02a7cd77e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
index 6518cc1154c4d89c1089bd61d500d1f24b9b2504..62cf4517ec4161f8f7b5400e1fdcb065a5222ca7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index e8c6147cea19c86bc2736082982591b9f33d5f58..9445ce1e9b9b5195ce9b711f3690d42b82286fe5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index c73057d06af41dc853049df7332779b0d64e0227..907f90fb59ee5d4fa2b8336505abb6878715efe0 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
index b092d8e8ad93c34d05743915c1c8681d875334af..353a05d7762a573e2aced6a5dda4812a16269606 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index ff2254d54665a3f37e39f4cce403ebec896364fa..51bb8fb04b67b3018b4835c3cd33d4a638b5fb4a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);
@@ -37,8 +38,8 @@ void g(int *p, int *q)
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_initialize((void *)p,sizeof(int));
*p = 0;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
@@ -106,7 +107,7 @@ int __gen_e_acsl_h(int x);
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_delete_block((void *)(& x));
return x;
}
@@ -119,9 +120,9 @@ int main(void)
int __retres;
int x;
int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(t),8UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
@@ -158,8 +159,8 @@ int __gen_e_acsl_h(int x)
{
int __gen_e_acsl_at;
int __retres;
- __e_acsl_store_block((void *)(& __retres),4UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__gen_e_acsl_at = x;
__retres = h(x);
__e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 05325507dda3d7c561e8e1517a3adf441ba7535c..76f52e27256a09e59fb476dc2b3eb6112cd8a397 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);
@@ -102,8 +103,8 @@ void g(int *p, int *q)
int __gen_e_acsl_at_3;
__e_acsl_mpz_t __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_initialize((void *)p,sizeof(int));
*p = 0;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
@@ -189,7 +190,7 @@ int __gen_e_acsl_h(int x);
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_delete_block((void *)(& x));
return x;
}
@@ -201,9 +202,9 @@ int main(void)
int __retres;
int x;
int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(t),8UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
@@ -318,8 +319,8 @@ int __gen_e_acsl_h(int x)
{
__e_acsl_mpz_t __gen_e_acsl_at;
int __retres;
- __e_acsl_store_block((void *)(& __retres),4UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
{
__e_acsl_mpz_t __gen_e_acsl_x;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
index 8b99036ca25f1864c3f9f79ec7f689278753f65b..c6cd92bed36f66319f74463f6e6fed690cc2e88c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
index af5d4476e5957f6d1a42fb721b842de18f610a18..0011c66b85a4cba4c86ee6e4f69ade9ebc91aa8b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
index efc79833e3f6ec59024123e3509ea265fb19a878..93d218442d30b76483b1e1dda713ac4c995a494e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
index 66fe6e49946dc8de5198003728773a5f1f6786a1..16f7236bcb4c7f26b4cdde71c694903c5253bcd2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
index a41c3aa317a7caa671865430e822c35ccfc76a89..a39e0d44f87f91171add8503324dabd1783a3f86 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
index 1d975679dd365934d6b78baef17fcbe0541a87c5..f870338038bdbcb4d3c2ff3a99852eb748cb22f8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index f4f995dc10218ad251429f3178f73352fa62b08c..cd49f58f7fe5da25d10664226c2abb5e4368a0e0 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index 553c26714151c5e2e4833c19681901a42b1fccb6..558fad0101c191e4585932d3e2b3a735b10dc670 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
index 772dc0983f6270ed87500f8736e78a29b6822605..e8297cbb920d6d28f5e5aced613c81812c050e06 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index 7f54b3889e737e1ab673a886364ec34490cc79a1..ae2a4fc2ad87eafb937a19f805d51c48630d472b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index e580bdf53e982d6e1be0d29987b028bb82e1573b..331bfe9e4a53bc92b18cd615451363716d5e043c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 0eee735afc36e10a8119ed4869f16d99a6e405a2..264bea4cd8ff7e36561fdaf3caf1c774e7b04ad4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
index 6518cc1154c4d89c1089bd61d500d1f24b9b2504..62cf4517ec4161f8f7b5400e1fdcb065a5222ca7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index 1d4d29db8024b423de546c7bddd8f4535c3ddce2..6c8ef42ae5b63404515a90fadff29ed3f6af69fc 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index 774cd469f6c06155636b3b9b45f082fb488953c2..ee86d9b6561cfff2f17d329fead0cbc47374e9c9 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 1c7ba24682cb42078a69ddaa8222b5a2ed1e6a12..5621b6492094bee92e8d32387de31f6ec5b785fa 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -1,5 +1,5 @@
[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".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
index af45ecaf0a38e7909bb7d3ebe5c6497f2d44c6c4..d3fd34d75bad2ee2f659a653d1765a5c7a634897 100644
--- a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
@@ -8,5 +8,5 @@
Please use option `-main' for specifying a valid entry point.
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".
diff --git a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
index b73b059804c977feb68386a43348e54a43da7ef7..c161e46326a1915d8267d4d5870af8f5719cf71a 100644
--- a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
@@ -3,7 +3,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing tests/reject/quantif.i (no preprocessing)
-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/reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
Ignoring annotation.
tests/reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
index 6b6527342b0b9a95afcef440939218f258a97a6e..4522e542c99e85e866bc24e10cc75f7ce0fb93d9 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/base_addr.c:44:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
index 48772f01703fa4c1ca48ac3047119ef24253ffdc..23012dfcdd07c38d32e0ac8725de873679487494 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/block_length.c:50:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
index ae7eacf4a88348422f940dc6ba68a4969948f63c..e4acdca2ce21f1ec74fe2cee7c88ed225416f8ca 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
@@ -2,11 +2,11 @@
[e-acsl] warning: annotating undefined function `isupper':
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
tests/runtime/ctype_macros.c:39:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/libc/ctype.h:163:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
+FRAMAC_SHARE/libc/ctype.h:164:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/libc/ctype.h:167:[value] warning: function __gen_e_acsl_isupper, behavior definitely_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/ctype.h:170:[value] warning: function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/ctype.h:168:[value] warning: function __gen_e_acsl_isupper, behavior definitely_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/ctype.h:171:[value] warning: function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
index 4c983b90f43e59493b9a14b3157c4d1fd1383326..90b97b057b40b2d20238306dea74b9a5a2ed2b59 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/freeable.c:15:[value] warning: assertion got status unknown.
tests/runtime/freeable.c:15:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
index 46d7ef3a5c194b698bbaf6d21f2781ba2e91d1bb..44756314152d32f74d2ed0eaa49863ec2c96ecfa 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(void)
{
int m;
int *u;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& u));
u = & m;
__e_acsl_full_init((void *)(& p));
@@ -32,7 +33,7 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
x = 0;
f();
/*@ assert &x ≡ &x; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
index 4fabf481163a3ae383652f77dec391b1992816c7..223753bbaf852bcdc66a1a44274fb270dad15a20 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
@@ -1,9 +1,10 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(int *dest, int val)
{
int *ptr;
- __e_acsl_store_block((void *)(& ptr),8UL);
- __e_acsl_store_block((void *)(& dest),8UL);
+ __e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
__e_acsl_full_init((void *)(& ptr));
ptr = dest;
__e_acsl_initialize((void *)ptr,sizeof(int));
@@ -17,8 +18,8 @@ int main(void)
{
int __retres;
int i;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& i),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& i),(size_t)4);
f(& i,255);
/*@ assert \initialized(&i); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
index df7cd29463475418f2c77d0c1bf1a76ed2b0cf9e..6cbfcdb5c04f8d5898cab1329fdee4e3d7504a71 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A[4] = {1, 2, 3, 4};
int *PA;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& PA),8UL);
+ __e_acsl_store_block((void *)(& PA),(size_t)8);
__e_acsl_full_init((void *)(& PA));
- __e_acsl_store_block((void *)(A),16UL);
+ __e_acsl_store_block((void *)(A),(size_t)16);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -22,17 +23,17 @@ int main(void)
char *pd;
long *q;
long *qd;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& qd),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& pd),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& pi),8UL);
- __e_acsl_store_block((void *)(& pl),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(& pa),8UL);
- __e_acsl_store_block((void *)(a),16UL);
+ __e_acsl_store_block((void *)(& qd),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& pd),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_store_block((void *)(& pa),(size_t)8);
+ __e_acsl_store_block((void *)(a),(size_t)16);
PA = (int *)(& A);
/*@ assert \base_addr((int *)A) ≡ \base_addr(PA); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
index dd82340cf0c148636cdf682c433445d175e8ded9..c39e410bde31f4e262404f98b4d06a629fe14199 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
struct Zero {
};
@@ -7,11 +8,11 @@ int *PA;
struct Zero ZERO;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& ZERO),0UL);
+ __e_acsl_store_block((void *)(& ZERO),(size_t)0);
__e_acsl_full_init((void *)(& ZERO));
- __e_acsl_store_block((void *)(& PA),8UL);
+ __e_acsl_store_block((void *)(& PA),(size_t)8);
__e_acsl_full_init((void *)(& PA));
- __e_acsl_store_block((void *)(A),16UL);
+ __e_acsl_store_block((void *)(A),(size_t)16);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -28,16 +29,16 @@ int main(void)
size_t size;
char *p;
long *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& pi),8UL);
- __e_acsl_store_block((void *)(& pl),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(& pa),8UL);
- __e_acsl_store_block((void *)(a),16UL);
- __e_acsl_store_block((void *)(& zero),0UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_store_block((void *)(& pa),(size_t)8);
+ __e_acsl_store_block((void *)(a),(size_t)16);
+ __e_acsl_store_block((void *)(& zero),(size_t)0);
/*@ assert \block_length(&ZERO) ≡ 0; */
{
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
index 146ccb703bc938b54b4c9e88e97bce0fdd4f0184..036561f38707d5805e58e895b560887aadc4ef7e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
@@ -41,19 +42,19 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,sizeof("First"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_store_block((void *)(_G),32UL);
+ __e_acsl_store_block((void *)(_G),(size_t)32);
__e_acsl_full_init((void *)(& _G));
- __e_acsl_store_block((void *)(& _E),4UL);
+ __e_acsl_store_block((void *)(& _E),(size_t)4);
__e_acsl_full_init((void *)(& _E));
- __e_acsl_store_block((void *)(_D),8UL);
+ __e_acsl_store_block((void *)(_D),(size_t)8);
__e_acsl_full_init((void *)(& _D));
- __e_acsl_store_block((void *)(& _C),8UL);
+ __e_acsl_store_block((void *)(& _C),(size_t)8);
__e_acsl_full_init((void *)(& _C));
- __e_acsl_store_block((void *)(& _B),8UL);
+ __e_acsl_store_block((void *)(& _B),(size_t)8);
__e_acsl_full_init((void *)(& _B));
- __e_acsl_store_block((void *)(_A),16UL);
+ __e_acsl_store_block((void *)(_A),(size_t)16);
__e_acsl_full_init((void *)(& _A));
- __e_acsl_store_block((void *)(& _F),4UL);
+ __e_acsl_store_block((void *)(& _F),(size_t)4);
__e_acsl_full_init((void *)(& _F));
return;
}
@@ -61,7 +62,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
/*@ assert \valid((char **)_A); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
index ca1c9e181ae47d513108bd3b5e1c968e8267def8..28d6aaa604cec07e6458a03c3b96e729dba04354 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
@@ -1,13 +1,15 @@
/* Generated by Frama-C */
+#include "ctype.h"
+#include "stdlib.h"
int main(int argc, char const **argv)
{
int __retres;
char c;
int tmp;
char *d;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
- __e_acsl_store_block((void *)(& d),8UL);
- __e_acsl_store_block((void *)(& c),1UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ __e_acsl_store_block((void *)(& d),(size_t)8);
+ __e_acsl_store_block((void *)(& c),(size_t)1);
tmp = __gen_e_acsl_isupper(argc);
__e_acsl_full_init((void *)(& c));
c = (char)tmp;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
index 272da24e99b5e98e634dfb8e37b632eaeed421a4..33c2ae302ddb6a95a94779c151aee819e7c6984c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
@@ -1,7 +1,10 @@
/* Generated by Frama-C */
+#include "errno.h"
+#include "stdio.h"
+#include "stdlib.h"
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& __FC_errno),4UL);
+ __e_acsl_store_block((void *)(& __FC_errno),(size_t)4);
__e_acsl_full_init((void *)(& __FC_errno));
return;
}
@@ -10,9 +13,9 @@ int main(int argc, char const **argv)
{
int __retres;
int *p;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & __FC_errno;
/*@ assert \valid(p); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
index 72116bfac3a7dcbade0aabc0f2ce1f57ac702241..3a77144b85af8c842b93821c33fb651ba0f3877f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index a27a3104873ffe16294aee8f1e98b1190c03a967..7b7b067ff37416636bcd53121428533ced6e242e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int X = 0;
int Y = 2;
/*@ ensures X ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
index 536af661a41e09bd2b3a0f4046349e4e99e46435..2527bb61fecb40e65a1df1682c33db43357e295a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int a = 0;
int b;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& b),4UL);
+ __e_acsl_store_block((void *)(& b),(size_t)4);
__e_acsl_full_init((void *)(& b));
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
return;
}
@@ -15,10 +16,10 @@ int main(void)
int __retres;
int *p;
int *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & a;
__e_acsl_full_init((void *)(& q));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
index 95cbaf4ad3242c36e9c9bbf363c9955bf49a0144..4027e89c9a0be2e542f2868eb91d9a1bb5d28cc3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
@@ -1,9 +1,10 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
char *a;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
a = (char *)malloc((unsigned long)7);
__retres = 0;
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
index b4827659ce9cd2b64ec24996531786fad3d0fcf3..1dd16e99a606fb8a8a485a20bba0e7864fd3d677 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A = 0;
int B;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& B),4UL);
+ __e_acsl_store_block((void *)(& B),(size_t)4);
__e_acsl_full_init((void *)(& B));
- __e_acsl_store_block((void *)(& A),4UL);
+ __e_acsl_store_block((void *)(& A),(size_t)4);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -24,15 +25,15 @@ int main(void)
char *partsc;
char *partsi;
int dup[2];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(d),16UL);
- __e_acsl_store_block((void *)(c),16UL);
- __e_acsl_store_block((void *)(& r),8UL);
- __e_acsl_store_block((void *)(& b),4UL);
- __e_acsl_store_block((void *)(& a),4UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(d),(size_t)16);
+ __e_acsl_store_block((void *)(c),(size_t)16);
+ __e_acsl_store_block((void *)(& r),(size_t)8);
+ __e_acsl_store_block((void *)(& b),(size_t)4);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & A;
__e_acsl_full_init((void *)(& q));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index 3b9f5a7636169dfb72dbbcdcb736473b372a54f2..93c05dc46f74f6be4e4da41a339acf6a2638c0c7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int X = 0;
/*@ ensures X ≡ 3; */
int main(void);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
index b672dc9cb33a79c90f060ed17754dd6e52515673..8994337c5ba2525d95fb7935af8848c5eb102162 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 3d22d25c102ef8f008bd7dd6c8fe37f4444a0eba..40d9186eb2fbdfc076b9b92e8abe4f44f43bfef1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A[10];
/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i + 1];
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
index a0c21dc44907a875d3d3ac488ac7d86da7872160..7acb15a3d46b373a05fbd038e9aed0cd7fe75657 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_6;
char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string;
@@ -62,15 +63,15 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("bar"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_store_block((void *)(& l_str),8UL);
+ __e_acsl_store_block((void *)(& l_str),(size_t)8);
__e_acsl_full_init((void *)(& l_str));
- __e_acsl_store_block((void *)(& s_str),8UL);
+ __e_acsl_store_block((void *)(& s_str),(size_t)8);
__e_acsl_full_init((void *)(& s_str));
- __e_acsl_store_block((void *)(& S2),8UL);
+ __e_acsl_store_block((void *)(& S2),(size_t)8);
__e_acsl_full_init((void *)(& S2));
- __e_acsl_store_block((void *)(& S),8UL);
+ __e_acsl_store_block((void *)(& S),(size_t)8);
__e_acsl_full_init((void *)(& S));
- __e_acsl_store_block((void *)(& T),8UL);
+ __e_acsl_store_block((void *)(& T),(size_t)8);
__e_acsl_full_init((void *)(& T));
return;
}
@@ -79,9 +80,9 @@ int main(void)
{
int __retres;
char *SS;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& SS),8UL);
+ __e_acsl_store_block((void *)(& SS),(size_t)8);
__e_acsl_full_init((void *)(& SS));
SS = (char *)__gen_e_acsl_literal_string;
/*@ assert *(S + G2) ≡ 'o'; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index ba7bf4973a970baae825726246fe22c12a5d35bb..11048b4a56331b283cf2683c65fc5b836646bd3c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -1,15 +1,17 @@
/* Generated by Frama-C */
+#include "stdlib.h"
+#include "string.h"
int main(int argc, char **argv)
{
int __retres;
int i;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
/*@ assert \valid(&argc); */
{
{
int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& argc),4UL);
- __e_acsl_store_block((void *)(& argv),8UL);
+ __e_acsl_store_block((void *)(& argc),(size_t)4);
+ __e_acsl_store_block((void *)(& argv),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argc)",10);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index af96acce120a7333a2dcb04c1f2c7f512c56b714..7d0cc5b85038eed0def594cec836ae524662f0ab 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(int argc, char const **argv)
{
int __retres;
@@ -6,10 +7,10 @@ int main(int argc, char const **argv)
int res2;
char *p;
char *a;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
- __e_acsl_store_block((void *)(& a),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& memptr),8UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& memptr),(size_t)8);
__e_acsl_full_init((void *)(& memptr));
memptr = (char **)malloc(sizeof(void *));
res2 = posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
index c8dd172c9567096afe19ba398e4056bb3a423c1b..c9146a3bbc6a4ee7cb76377e8cb6260dadb07095 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
@@ -1,10 +1,12 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(int argc, char **argv)
{
int __retres;
char *a;
char *b;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
a = (char *)malloc((unsigned long)7);
/*@ assert __e_acsl_heap_allocation_size ≡ 7; */
__e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,(char *)"Assertion",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
index 902a394a3332b5c66c7051a59b232a3de8fd5877..6a5bdd3bf97a87626d8173372175dbb8dbdde81f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
index 884218a24a664455043e94b25e2c4b9f735da232..411d9156a849d35841f3248b168f7579169b4910 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
index fd2d4ee168db229c2d590e37f7f0f8bb460bc51f..e5b27f8a5c0cb2794ef93671a9023ee58f58557a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A[4] = {1, 2, 3, 4};
int *PA;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& PA),8UL);
+ __e_acsl_store_block((void *)(& PA),(size_t)8);
__e_acsl_full_init((void *)(& PA));
- __e_acsl_store_block((void *)(A),16UL);
+ __e_acsl_store_block((void *)(A),(size_t)16);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -19,14 +20,14 @@ int main(void)
int *pi;
char *p;
long *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& pi),8UL);
- __e_acsl_store_block((void *)(& pl),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(a),16UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_store_block((void *)(a),(size_t)16);
PA = (int *)(& A);
/*@ assert \offset((int *)A) ≡ 0; */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
index 8189abbe6a27209fe7b0d41ca72103c68c4f91e5..64f20c885816b1144ee810e16013b50121a58179 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
enum bool {
false = 0,
true = 1
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index 1147d35f960fa3d7d8f7c6a7d3397e7b5f6402f3..dbbbe9eb9421f319ff6580d1c38c334ea51396b3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
@@ -6,10 +7,10 @@ int main(void)
int t[3];
int *p;
int k;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(t),12UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)12);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = 1;
__e_acsl_initialize((void *)(t),sizeof(int));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
index 50bc97ca19e77a78dbb7058866a3c3dc1aa0ed32..773aa7e4a8cdae46988f9c7f23c1dfa991e84e0f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int *A;
int *B;
void f(void)
@@ -11,7 +12,7 @@ void g(int *C, int *D)
{
/*@ assert \initialized(&C); */
{
- __e_acsl_store_block((void *)(& C),8UL);
+ __e_acsl_store_block((void *)(& C),(size_t)8);
__e_acsl_assert(1,(char *)"Assertion",(char *)"g",
(char *)"\\initialized(&C)",16);
}
@@ -21,9 +22,9 @@ void g(int *C, int *D)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& B),8UL);
+ __e_acsl_store_block((void *)(& B),(size_t)8);
__e_acsl_full_init((void *)(& B));
- __e_acsl_store_block((void *)(& A),8UL);
+ __e_acsl_store_block((void *)(& A),(size_t)8);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -33,10 +34,10 @@ int main(void)
int __retres;
int *x;
int *y;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& y),8UL);
- __e_acsl_store_block((void *)(& x),8UL);
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
B = (int *)malloc(sizeof(int));
__e_acsl_full_init((void *)(& y));
y = (int *)malloc(sizeof(int));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 4b706094131500fea65fe8e1d68882cb5b16b853..3d0ab3670f7428dddcc2d911ed302fcae61df258 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
/*@ ensures \result ≡ (int)(\old(x) - \old(x)); */
int __gen_e_acsl_f(int x);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
index 7f98cb9e792ec665ecd10c03427839ccdad88173..f5f08230c81d849d70204e2cbf4e64e7815559c6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
index c37843ee2b6ac85d3b88a011eea279ce401f7545..b61258b90e22ac831e276a49b9477e3442ce4a3b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string;
void __e_acsl_globals_init(void)
@@ -12,7 +14,7 @@ void __e_acsl_globals_init(void)
sizeof("/tmp/foo"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string);
- __e_acsl_store_block((void *)(& stdout),8UL);
+ __e_acsl_store_block((void *)(& stdout),(size_t)8);
__e_acsl_full_init((void *)(& stdout));
return;
}
@@ -22,9 +24,9 @@ int main(void)
int __retres;
FILE *f;
FILE *f2;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& f),8UL);
+ __e_acsl_store_block((void *)(& f),(size_t)8);
__e_acsl_full_init((void *)(& f));
f = stdout;
f2 = __gen_e_acsl_fopen(__gen_e_acsl_literal_string,
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 820ed8e257187d129ec5adfb9d838270c0911b5c..8f08c272ea1a22a8972fe273eea45badb579018e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
index 18e197aaa6e2a1605daedf6c58bebfc1089bc87a..15d2e2842277d3c7397ffb490de8efa1e15757c3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
index d8f9bac5ef11947e613a85a2a06cb7094e01f6c5..fcab2ee8a3f14b6d4452a063558836581d1fedcd 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
typedef unsigned char uint8;
int main(void)
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index cb69e859fa568929f46f552447ef889cc18465cb..d12021ab09add4feea53d2e359ce024f7a9e8b07 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -1,14 +1,14 @@
[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/runtime/initialized.c:65:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:69:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:321:[value] warning: function realloc: precondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:336:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:322:[value] warning: function realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:337:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
tests/runtime/initialized.c:74:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:76:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:308:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:309:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
tests/runtime/initialized.c:84:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:93:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
index 71d668555df73bb608a44b51a80baeb87c06e0e7..9c737631c48bf697d1700058f47ff5aa11af0364 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/linear_search.i:7:[value] warning: function __gen_e_acsl_search: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
index 5d8e5b79f1fe634f80340c664b5ed2f77c75142e..ecb6e4154f0b223bb0d25e19a60d6769fe904cd3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/loop.i:19:[value] warning: loop invariant got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index c20a1a7faab3860d2d375671d7c2219f1e47784f..8992dcf45c90f41ba88f82837be75dbbedc011ba 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -2,12 +2,12 @@
[e-acsl] warning: annotating undefined function `strlen':
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/string.h:91:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
+FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
[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.
@@ -17,8 +17,8 @@ tests/runtime/mainargs.c:15:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_read(argv + argc);
tests/runtime/mainargs.c:16:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv + argc);
-FRAMAC_SHARE/libc/string.h:91:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:91:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:93:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
index 591e95a1f199dfd50cc920abd66496f12267809a..17ffda3bffd96628a620e8c75739b07a2bb40839 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
@@ -7,7 +7,7 @@ tests/runtime/memalign.c:15:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/memalign.c:16:[value] warning: assertion got status unknown.
tests/runtime/memalign.c:17:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:308:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:309:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
tests/runtime/memalign.c:19:[value] warning: assertion got status unknown.
tests/runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
tests/runtime/memalign.c:23:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
index f4e55dd11dc7dbedb07ea401bb3687a5462b096d..9d3a78ec407888c2e2ac2e44c10a451e516532da 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/memsize.c:14:[value] warning: assertion got status unknown.
tests/runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
index 225bdd10c278f641b97da18199967bd460adae61..5ca2406e948c5e184e8444191ec0eb8f8da69225 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/offset.c:39:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
index ee58349831c8f7c1985d2213bfcdf3d1acfe272c..5ad5fd174a025cb3c3966d13ee30f95458b727da 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/ptr.i:17:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
index 74b2c0f88667ff0dbd307a6474a57f57cb8b45b7..a0a8836bb7a329fc53da2da239850fee8b952dde 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
@@ -1,4 +1,4 @@
[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
index 8a5949c1d1c2f19bf16c59ec4e73020535f9a3f2..53d24663ffc0de50e36ce79d6669f42418b1df3a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
@@ -2,10 +2,10 @@
[e-acsl] warning: annotating undefined function `fopen':
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
tests/runtime/stdout.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdio.h:108:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdio.h:109:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/stdout.c:10:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
index c33737e3cac6e74853111a99a2a4002b6a9d7094..672ba3db925ded58b22571e4f739a5412a0ecda3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
@@ -1,3 +1,3 @@
[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".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
index 82dfbcc3f10f37dac685ca6b30bc26f3d3a77850..ed9c8d0031082d824be73f8f84c381370f499d9e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/valid.c:47:[value] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
index c9f6e2aa111e4e107a261500556917f2fd9c1b76..740a1e676f5eee2b7d04e2aabd8d7f41b6643168 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
index 2e0f0d717532809fed93fa4213385f9dba3de81d..bfca2174f9aa1c4655e436a27010c8ab2e57204f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/valid_in_contract.c:19:[value] warning: out of bounds read. assert \valid_read(&l->next);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
index 5cbb1b197feff365a115616b122ee2f69e048207..e9ae42d40815b8b800a70c5225d5560245b326b2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
@@ -1,5 +1,5 @@
[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/runtime/vector.c:26:[value] warning: accessing uninitialized left-value. assert \initialized(v2 + 2);