diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle index 4d0f31c840e29ffd446647b4204edab473772c2c..845be00612efea9581746723802617b328a66215 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1740.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/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c index e165312e35df6395e032965ef0b650e3bc5fb0d7..7d1822a0543584b1951eae377aca95cd6a931aa6 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c @@ -1,13 +1,14 @@ /* Generated by Frama-C */ +#include "stdlib.h" int main(void) { int __retres; int *p; - __e_acsl_memory_init((int *)0,(char ***)0,8UL); - __e_acsl_store_block((void *)(& p),8UL); + __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8); + __e_acsl_store_block((void *)(& p),(size_t)8); { int a; - __e_acsl_store_block((void *)(& a),4UL); + __e_acsl_store_block((void *)(& a),(size_t)4); __e_acsl_full_init((void *)(& a)); a = 0; __e_acsl_full_init((void *)(& p)); diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle index f8de72eb5d5d0e28ae07a0359cb9943ffcf6a670..66bbcfdda0170d72969011310ad46adb416b2591 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.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/bypassed_var.c:16:[value] warning: accessing uninitialized left-value. assert \initialized(&p); diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle index 638dd2dcbe2764b3f19d5694fc591feb63e2899e..5c4f44cb7b170063e9201f3c9e7ecf22654ddd38 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.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/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c index a1eb4fce0d0bc3613b22ea9e939bb1a313fac8d0..acd909e18da7836611e10853460c8a67f296aab4 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c +++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c @@ -1,15 +1,16 @@ /* Generated by Frama-C */ +#include "stdlib.h" int bypassed_var(int i) { int lst[2]; - __e_acsl_store_block((void *)(lst),8UL); + __e_acsl_store_block((void *)(lst),(size_t)8); if (i) goto L; { int *p; - __e_acsl_store_block((void *)(& p),8UL); + __e_acsl_store_block((void *)(& p),(size_t)8); __e_acsl_full_init((void *)(& p)); p = (int *)(& lst); - L: __e_acsl_store_block_duplicate((void *)(& p),8UL); + L: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8); __e_acsl_full_init((void *)(& p)); /*@ assert Value: initialisation: \initialized(&p); */ p ++; @@ -60,7 +61,7 @@ int bypassed_var(int i) int main(int argc, char const **argv) { int __retres; - __e_acsl_memory_init(& argc,(char ***)(& argv),8UL); + __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8); bypassed_var(0); bypassed_var(1); __retres = 0; diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c index 4ec72b8a82d2037884266944d9a52ded91c5b693..897f45cce1a73daec858774c05a5077571ab97e6 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c +++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c @@ -1,12 +1,13 @@ /* Generated by Frama-C */ +#include "stdlib.h" int goto_bts(void) { int __retres; int *p; - __e_acsl_store_block((void *)(& p),8UL); + __e_acsl_store_block((void *)(& p),(size_t)8); { int a; - __e_acsl_store_block((void *)(& a),4UL); + __e_acsl_store_block((void *)(& a),(size_t)4); __e_acsl_full_init((void *)(& a)); a = 0; __e_acsl_full_init((void *)(& p)); @@ -63,27 +64,27 @@ int goto_valid(void) int *p; int *q; int *r; - __e_acsl_store_block((void *)(& r),8UL); - __e_acsl_store_block((void *)(& q),8UL); - __e_acsl_store_block((void *)(& p),8UL); + __e_acsl_store_block((void *)(& r),(size_t)8); + __e_acsl_store_block((void *)(& q),(size_t)8); + __e_acsl_store_block((void *)(& p),(size_t)8); a = 9; { int a1; - __e_acsl_store_block((void *)(& a1),4UL); + __e_acsl_store_block((void *)(& a1),(size_t)4); __e_acsl_full_init((void *)(& a1)); a1 = 0; __e_acsl_full_init((void *)(& p)); p = & a1; { int a2; - __e_acsl_store_block((void *)(& a2),4UL); + __e_acsl_store_block((void *)(& a2),(size_t)4); __e_acsl_full_init((void *)(& a2)); a2 = 0; __e_acsl_full_init((void *)(& q)); q = & a2; { int a3; - __e_acsl_store_block((void *)(& a3),4UL); + __e_acsl_store_block((void *)(& a3),(size_t)4); __e_acsl_full_init((void *)(& a3)); a3 = 0; __e_acsl_full_init((void *)(& r)); @@ -238,10 +239,10 @@ int switch_valid(void) int *p; int *q; int *s; - __e_acsl_store_block((void *)(& s),8UL); - __e_acsl_store_block((void *)(& q),8UL); - __e_acsl_store_block((void *)(& p),8UL); - __e_acsl_store_block((void *)(& i),4UL); + __e_acsl_store_block((void *)(& s),(size_t)8); + __e_acsl_store_block((void *)(& q),(size_t)8); + __e_acsl_store_block((void *)(& p),(size_t)8); + __e_acsl_store_block((void *)(& i),(size_t)4); __e_acsl_full_init((void *)(& i)); i = 1; __e_acsl_full_init((void *)(& s)); @@ -250,14 +251,14 @@ int switch_valid(void) default: ; { int a1; - __e_acsl_store_block((void *)(& a1),4UL); + __e_acsl_store_block((void *)(& a1),(size_t)4); __e_acsl_full_init((void *)(& a1)); a1 = 0; __e_acsl_full_init((void *)(& p)); p = & a1; { int a2; - __e_acsl_store_block((void *)(& a2),4UL); + __e_acsl_store_block((void *)(& a2),(size_t)4); __e_acsl_full_init((void *)(& a2)); a2 = 0; __e_acsl_full_init((void *)(& q)); @@ -397,13 +398,13 @@ int while_valid(void) int *q; int *r; int i; - __e_acsl_store_block((void *)(& r),8UL); - __e_acsl_store_block((void *)(& q),8UL); - __e_acsl_store_block((void *)(& p),8UL); + __e_acsl_store_block((void *)(& r),(size_t)8); + __e_acsl_store_block((void *)(& q),(size_t)8); + __e_acsl_store_block((void *)(& p),(size_t)8); i = 5; { int a0; - __e_acsl_store_block((void *)(& a0),4UL); + __e_acsl_store_block((void *)(& a0),(size_t)4); __e_acsl_full_init((void *)(& a0)); a0 = 0; __e_acsl_full_init((void *)(& r)); @@ -413,14 +414,14 @@ int while_valid(void) if (! i) break; { int a1; - __e_acsl_store_block((void *)(& a1),4UL); + __e_acsl_store_block((void *)(& a1),(size_t)4); __e_acsl_full_init((void *)(& a1)); a1 = 0; __e_acsl_full_init((void *)(& p)); p = & a1; { int a2; - __e_acsl_store_block((void *)(& a2),4UL); + __e_acsl_store_block((void *)(& a2),(size_t)4); __e_acsl_full_init((void *)(& a2)); a2 = 0; __e_acsl_full_init((void *)(& q)); @@ -555,8 +556,8 @@ void continue_valid(void) int i; int *p; int *q; - __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); i = 0; while (1) { int tmp; @@ -568,7 +569,7 @@ void continue_valid(void) if (! tmp) break; { int a1; - __e_acsl_store_block((void *)(& a1),4UL); + __e_acsl_store_block((void *)(& a1),(size_t)4); /*@ assert ¬\valid(p); */ { { @@ -643,7 +644,7 @@ void continue_valid(void) } { int a2; - __e_acsl_store_block((void *)(& a2),4UL); + __e_acsl_store_block((void *)(& a2),(size_t)4); __e_acsl_full_init((void *)(& a2)); a2 = 1; __e_acsl_full_init((void *)(& q)); @@ -738,7 +739,7 @@ void continue_valid(void) int main(int argc, char const **argv) { int __retres; - __e_acsl_memory_init(& argc,(char ***)(& argv),8UL); + __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8); goto_bts(); goto_valid(); switch_valid();