From b8ce0e2a7311375bf449e13902faf1fa3ba5df1a Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 5 Aug 2014 13:44:05 +0200
Subject: [PATCH] fixed bug #1818 about initialization of globals
---
src/plugins/e-acsl/doc/Changelog | 1 +
src/plugins/e-acsl/gcc.sh | 4 +-
.../e-acsl/tests/e-acsl-runtime/init.c | 14 +++
.../oracle/bts1478.1.res.oracle | 1 +
.../e-acsl-runtime/oracle/bts1478.res.oracle | 1 +
.../tests/e-acsl-runtime/oracle/gen_bts1478.c | 5 +
.../e-acsl-runtime/oracle/gen_bts14782.c | 5 +
.../tests/e-acsl-runtime/oracle/gen_ghost.c | 2 +
.../tests/e-acsl-runtime/oracle/gen_ghost2.c | 2 +
.../tests/e-acsl-runtime/oracle/gen_init.c | 117 ++++++++++++++++++
.../tests/e-acsl-runtime/oracle/gen_init2.c | 117 ++++++++++++++++++
.../oracle/gen_literal_string.c | 3 +
.../oracle/gen_literal_string2.c | 3 +
.../e-acsl-runtime/oracle/gen_mainargs.c | 2 +-
.../e-acsl-runtime/oracle/gen_mainargs2.c | 2 +-
.../e-acsl-runtime/oracle/gen_ptr_init.c | 2 +
.../e-acsl-runtime/oracle/gen_ptr_init2.c | 2 +
.../tests/e-acsl-runtime/oracle/gen_stdout.c | 1 +
.../tests/e-acsl-runtime/oracle/gen_stdout2.c | 1 +
.../tests/e-acsl-runtime/oracle/gen_valid.c | 2 +
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 2 +
.../e-acsl-runtime/oracle/init.1.err.oracle | 0
.../e-acsl-runtime/oracle/init.1.res.oracle | 34 +++++
.../e-acsl-runtime/oracle/init.err.oracle | 0
.../e-acsl-runtime/oracle/init.res.oracle | 34 +++++
.../oracle/ptr_init.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/ptr_init.res.oracle | 2 +-
src/plugins/e-acsl/visit.ml | 11 +-
28 files changed, 365 insertions(+), 7 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/init.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 611e2eb01bd..a0cc7fef9f4 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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
diff --git a/src/plugins/e-acsl/gcc.sh b/src/plugins/e-acsl/gcc.sh
index 7e367a3f252..f30a5e020ab 100755
--- a/src/plugins/e-acsl/gcc.sh
+++ b/src/plugins/e-acsl/gcc.sh
@@ -1,3 +1,5 @@
#!/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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
new file mode 100644
index 00000000000..e7a5a17ddbb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
@@ -0,0 +1,14 @@
+/* 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) ; */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
index 44f5c5647e5..889dfbfd3a5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
index 76d0e9b7e0a..d794b166518 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index e521c474f04..591792094a6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index 45acef9f359..c6b0f7cd706 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index f5d1e8efd05..781784e4196 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index 37bdf66318a..d55d2cac36d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
new file mode 100644
index 00000000000..0bc419bf7d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
@@ -0,0 +1,117 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
new file mode 100644
index 00000000000..0bc419bf7d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
@@ -0,0 +1,117 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index ef102f88c41..6bf134e5636 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index e5d0a0280dd..d4c769e125a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index b741ebe03b2..f0adb7fbb68 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/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) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
index cf644234f2a..7159fdafd4d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
+++ b/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) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index ff3b77ce0e1..788567ae18f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index ff3b77ce0e1..788567ae18f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index bfb8ca6d0bb..711753c64e4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index bfb8ca6d0bb..711753c64e4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 2bdff399157..aad63973a32 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 2bdff399157..aad63973a32 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
new file mode 100644
index 00000000000..1818385f4b2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
@@ -0,0 +1,34 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/init.c"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ random_counter ∈ {0}
+ rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ a ∈ {0}
+ b ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid.
+[value] using specification for function __initialized
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
new file mode 100644
index 00000000000..1818385f4b2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
@@ -0,0 +1,34 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/init.c"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ random_counter ∈ {0}
+ rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ a ∈ {0}
+ b ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid.
+[value] using specification for function __initialized
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 68e6ea08da0..58fae9eeeb3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -33,11 +33,11 @@ FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic functio
A ∈ {0}
B ∈ {0}
[value] using specification for function __store_block
+[value] using specification for function __full_init
[value] using specification for function __malloc
[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[value] using specification for function __full_init
tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index c7d1ad4854c..361eba55b23 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -29,11 +29,11 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
A ∈ {0}
B ∈ {0}
[value] using specification for function __store_block
+[value] using specification for function __full_init
[value] using specification for function __malloc
[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[value] using specification for function __full_init
tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 2486578f1fc..21ded1b3e8d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -128,7 +128,14 @@ class e_acsl_visitor prj generate = object (self)
let new_vi = Cil.get_varinfo self#behavior old_vi in
let model blk =
if Pre_analysis.must_model_vi old_vi then
- Misc.mk_store_stmt new_vi :: blk
+ let blk =
+ if Kernel.LibEntry.get () then blk
+ else
+ Misc.mk_initialize ~loc:Location.unknown
+ (Cil.var new_vi)
+ :: blk
+ in
+ Misc.mk_store_stmt new_vi :: blk
else
stmts
in
@@ -203,7 +210,7 @@ class e_acsl_visitor prj generate = object (self)
f.globals <- new_globals
| None ->
Kernel.warning "@[no entry point specified:@ \
- you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
+you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
fname;
f.globals <- f.globals @ [ cil_fct ]
in
--
GitLab