Merge branch 'feature/virgile/clean-print' into 'master'

synchronize with frama-c/frama-c!1112

See merge request !104

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

 /* 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;

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

 /* 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);

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

 /* Generated by Frama-C */
+#include "stdlib.h"
 /*@ requires n > 0; */
 int __gen_e_acsl_fact(int n);
 

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

 /* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
 int main(void)
 {
   int __retres;

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

 /* 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;

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

 /* 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); */
   {
     {

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

 /* 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;

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

 /* 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;

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

 /* 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); */

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

 /* 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); */
   {

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

 /* 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);

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

 /* Generated by Frama-C */
+#include "stdlib.h"
 long A = (long)0;
 int main(void)
 {

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

 /* 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;

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state

src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state

src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c

 /* 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; */

src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c

 /* 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();

src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state

src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state

src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle

 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state