fixed bug #1818 about initialization of globals

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2014/08/05] Fix bug #1818 about initialization of globals.
 -* E-ACSL       [2014/08/04] Fix bug #1696 by clarifying the manual.
 -* E-ACSL       [2014/08/04] Fix bug #1831 about argc and argv.
 -* E-ACSL       [2014/07/19] Fix bug #1836 about one-off error when

src/plugins/e-acsl/gcc.sh

 #!/bin/sh
 
-gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o $1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c $1 -lgmp && $1.out
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o $1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c $1 -lgmp
+
+./$1.out

src/plugins/e-acsl/tests/e-acsl-runtime/init.c

+/* run.config
+   COMMENT: initialization of globals (bts #1818)
+   EXECNOW: LOG gen_init.c BIN gen_init.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init.c > /dev/null && ./gcc_test.sh init
+   EXECNOW: LOG gen_init2.c BIN gen_init2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init2.c > /dev/null && ./gcc_test.sh init2
+*/
+
+int a = 0, b;
+
+int main(void) {
+  int *p = &a, *q = &b;
+  /*@assert \initialized(&b) ; */
+  /*@assert \initialized(q) ; */
+  /*@assert \initialized(p) ; */
+}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle

@@ -20,6 +20,7 @@
   global_i ∈ {0}
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
+[value] using specification for function __full_init
 tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.

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

@@ -20,6 +20,7 @@
   global_i ∈ {0}
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
+[value] using specification for function __full_init
 tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.

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

@@ -40,6 +40,9 @@ extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
 /*@ ensures \result ≡ 0 ∨ \result ≡ 1;
     ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
     assigns \result;
@@ -94,7 +97,9 @@ void __e_acsl_loop(void)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& global_i_ptr),4U);
+  __full_init((void *)(& global_i_ptr));
   __store_block((void *)(& global_i),4U);
+  __full_init((void *)(& global_i));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c

@@ -63,6 +63,9 @@ extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
 /*@ ensures \result ≡ 0 ∨ \result ≡ 1;
     ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
     assigns \result;
@@ -126,7 +129,9 @@ void __e_acsl_loop(void)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& global_i_ptr),4U);
+  __full_init((void *)(& global_i_ptr));
   __store_block((void *)(& global_i),4U);
+  __full_init((void *)(& global_i));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c

@@ -90,7 +90,9 @@ int *P;
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& P),4U);
+  __full_init((void *)(& P));
   __store_block((void *)(& G),4U);
+  __full_init((void *)(& G));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c

@@ -104,7 +104,9 @@ int *P;
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& P),4U);
+  __full_init((void *)(& P));
   __store_block((void *)(& G),4U);
+  __full_init((void *)(& G));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c

+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+   int _mp_alloc ;
+   int _mp_size ;
+   unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+    assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+                                                           char *kind,
+                                                           char *fct,
+                                                           char *pred_txt,
+                                                           int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+  dynamic_allocation {
+  predicate is_allocable{L}(size_t n) 
+    reads __fc_heap_status;
+  
+  }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures
+      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+    assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+                                                          size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+    assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int a = 0;
+int b;
+void __e_acsl_memory_init(void)
+{
+  __store_block((void *)(& b),4U);
+  __full_init((void *)(& b));
+  __store_block((void *)(& a),4U);
+  __full_init((void *)(& a));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int *p;
+  int *q;
+  __e_acsl_memory_init();
+  __store_block((void *)(& q),8U);
+  __store_block((void *)(& p),8U);
+  __full_init((void *)(& p));
+  p = & a;
+  __full_init((void *)(& q));
+  q = & b;
+  /*@ assert \initialized(&b); */
+  e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+                (char *)"\\initialized(&b)",11);
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)q,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(q)",12);
+  }
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized_2;
+    __e_acsl_initialized_2 = __initialized((void *)p,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(p)",13);
+  }
+  __retres = 0;
+  __delete_block((void *)(& b));
+  __delete_block((void *)(& a));
+  __delete_block((void *)(& q));
+  __delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c

+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+   int _mp_alloc ;
+   int _mp_size ;
+   unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+    assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+                                                           char *kind,
+                                                           char *fct,
+                                                           char *pred_txt,
+                                                           int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+  dynamic_allocation {
+  predicate is_allocable{L}(size_t n) 
+    reads __fc_heap_status;
+  
+  }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures
+      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+    assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+                                                          size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+    assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int a = 0;
+int b;
+void __e_acsl_memory_init(void)
+{
+  __store_block((void *)(& b),4U);
+  __full_init((void *)(& b));
+  __store_block((void *)(& a),4U);
+  __full_init((void *)(& a));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int *p;
+  int *q;
+  __e_acsl_memory_init();
+  __store_block((void *)(& q),8U);
+  __store_block((void *)(& p),8U);
+  __full_init((void *)(& p));
+  p = & a;
+  __full_init((void *)(& q));
+  q = & b;
+  /*@ assert \initialized(&b); */
+  e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+                (char *)"\\initialized(&b)",11);
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)q,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(q)",12);
+  }
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized_2;
+    __e_acsl_initialized_2 = __initialized((void *)p,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(p)",13);
+  }
+  __retres = 0;
+  __delete_block((void *)(& b));
+  __delete_block((void *)(& a));
+  __delete_block((void *)(& q));
+  __delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c

@@ -126,10 +126,13 @@ void __e_acsl_memory_init(void)
   __store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __full_init((void *)(& S2));
   S2 = (char *)__e_acsl_literal_string_3;
   __store_block((void *)(& S),4U);
+  __full_init((void *)(& S));
   S = (char *)__e_acsl_literal_string_2;
   __store_block((void *)(& T),4U);
+  __full_init((void *)(& T));
   T = (char *)__e_acsl_literal_string;
   return;
 }

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c

@@ -154,10 +154,13 @@ void __e_acsl_memory_init(void)
   __store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __full_init((void *)(& S2));
   S2 = (char *)__e_acsl_literal_string_3;
   __store_block((void *)(& S),4U);
+  __full_init((void *)(& S));
   S = (char *)__e_acsl_literal_string_2;
   __store_block((void *)(& T),4U);
+  __full_init((void *)(& T));
   T = (char *)__e_acsl_literal_string;
   return;
 }

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c

@@ -83,7 +83,7 @@ extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
  */
 extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
 
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
 
 /*@
 predicate diffSize{L1, L2}(ℤ i) =

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c

@@ -157,7 +157,7 @@ extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
  */
 extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
 
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
 
 /*@
 predicate diffSize{L1, L2}(ℤ i) =

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c

@@ -142,7 +142,9 @@ void g(int *C, int *D)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& B),4U);
+  __full_init((void *)(& B));
   __store_block((void *)(& A),4U);
+  __full_init((void *)(& A));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c

@@ -142,7 +142,9 @@ void g(int *C, int *D)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& B),4U);
+  __full_init((void *)(& B));
   __store_block((void *)(& A),4U);
+  __full_init((void *)(& A));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c

@@ -100,6 +100,7 @@ FILE const *_p__fc_fopen = (FILE const *)(fopen);
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& stdout),8U);
+  __full_init((void *)(& stdout));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c

@@ -100,6 +100,7 @@ FILE const *_p__fc_fopen = (FILE const *)(fopen);
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& stdout),8U);
+  __full_init((void *)(& stdout));
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c

@@ -299,7 +299,9 @@ void g(void)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& Z),4U);
+  __full_init((void *)(& Z));
   __store_block((void *)(& X),8U);
+  __full_init((void *)(& X));
   return;
 }