diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8ed6f140b79aa8506a52fb6d13ab96325215339e..0b2daa15c1a05accb04715db8528e9816ce15bb6 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,8 +15,9 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
--* E-ACSL [2012/12/13] Fix bug with complex term left-values
-- E-ACSL [2012/11/27] Support of \valid_read
+- E-ACSL [2012/12/20] Support of ghost variables and statements.
+-* E-ACSL [2012/12/13] Fix bug with complex term left-values.
+- E-ACSL [2012/11/27] Support of \valid_read.
- E-ACSL [2012/11/27] Prevent runtime errors in annotations.
- E-ACSL [2012/11/19] Support of floats in annotations. Approximate
reals by floats.
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf
index 4876dc2a746a4b55399fc9be7c799f064bd5518c..b6002a0014dd41ad909416fd00bce9453bdda6e7 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf
index bad7a68fec8cfe50a1634ece77344203ffef97a2..b7ed786018125b9cd5296675eac11e155f37c75e 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf
index 972c1e5271bff9f39e62893e08926efa1cc71899..b6002a0014dd41ad909416fd00bce9453bdda6e7 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl.pdf b/src/plugins/e-acsl/doc/refman/e-acsl.pdf
index 59e2d7a12f9e30d18038d0591e4f15954c5292e1..b7ed786018125b9cd5296675eac11e155f37c75e 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/ghost.tex b/src/plugins/e-acsl/doc/refman/ghost.tex
index b31bc876a08fd3ceedf966d51c255efb515ec53b..b3c24434126f2bcb1b3faa712e5de9ed57e21200 100644
--- a/src/plugins/e-acsl/doc/refman/ghost.tex
+++ b/src/plugins/e-acsl/doc/refman/ghost.tex
@@ -3,8 +3,7 @@
ghost-type-specifier ::= C-type-specifier ;
| { logic-type-name } \
declaration ::= C-declaration ;
- | { "/*@" "ghost" } ;
- { ghost-declaration "*/" } \
+ | "/*@" "ghost" ghost-declaration "*/" \
direct-declarator ::= C-direct-declarator ;
| direct-declarator ;
"(" parameter-type-list? ")";
@@ -20,9 +19,9 @@
{ "*/"} ; call with ghosts
\
statement ::= C-statement ;
- | { statements-ghost } \
- { statements-ghost } ::= { "/*@" "ghost" };
- { ghost-statement+ "*/" } \
+ | statements-ghost \
+ statements-ghost ::= "/*@" "ghost" ;
+ ghost-statement+ "*/" \
ghost-selection-statement ::= C-selection-statement ;
| "if" "(" expression ")";
statement;
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index d4228bfdaa1b5c3c07a08a79a081724966bc3aae..d57089afd1917808596084bf64e63ff694a00051 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -740,7 +740,7 @@ variables and fields.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{\notimplemented{Ghost variables and statements}}
+\section{Ghost variables and statements}
\label{sec:ghost}
\index{ghost}
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 79a6e49917d3b463ad61d9c551d18fd2bcecd31f..0cb9cd6079e0cd9169a4d4d29edf5dce3d348ca3 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -35,6 +35,13 @@ let init_mpz () =
end in
Cil.visitCilFileSameGlobals set_mpzt (Ast.get ())
+let get_rte_by_stmt =
+ Dynamic.get
+ ~plugin:"RteGen"
+ "stmt_annotations"
+ (Datatype.func2 Kernel_function.ty Stmt.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
+
module Env: sig
val default_varinfos: Varinfo.Set.t option -> Varinfo.Set.t
val apply: (kernel_function -> 'a) -> kernel_function -> 'a
@@ -273,6 +280,14 @@ module rec Transfer
Annotations.fold_code_annot
(fun _ -> register_code_annot kf) stmt state
in
+ let state =
+ if stmt.ghost then
+ let rtes = get_rte_by_stmt kf stmt in
+ List.fold_left
+ (fun state a -> register_code_annot kf a state) state rtes
+ else
+ state
+ in
Some state)
let rec register_exp varinfos e = match e.enode with
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i b/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..4f01d1804f8b183dc3d86c4f06dbca2b5d4b9702
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ghost.i
@@ -0,0 +1,20 @@
+/* run.config
+ COMMENT: ghost code
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ EXECNOW: LOG gen_ghost.c BIN gen_ghost.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost.c > /dev/null && ./gcc_test.sh ghost
+ EXECNOW: LOG gen_ghost2.c BIN gen_ghost2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/ghost.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_ghost2.c > /dev/null && ./gcc_test.sh ghost2
+*/
+
+/*@ ghost int G = 0; */
+/*@ ghost int *P; */
+
+// /*@ ghost int foo(int *x) { return *x + 1; } */
+
+int main(void) {
+ /*@ ghost P = &G; */ ;
+ /*@ ghost int *Q = P; */
+ /*@ ghost (*P)++; */
+ /*@ assert *Q == G; */
+ // /*@ ghost G = foo(&G); */
+ // /*@ assert G == 2; */
+}
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
new file mode 100644
index 0000000000000000000000000000000000000000..8c09b64fb7433816e01bffe0c8510e63662081f2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -0,0 +1,159 @@
+/* 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;
+typedef unsigned int ino_t;
+typedef unsigned int gid_t;
+typedef unsigned int uid_t;
+typedef long time_t;
+typedef unsigned int blkcnt_t;
+typedef unsigned int blksize_t;
+typedef unsigned int dev_t;
+typedef unsigned int mode_t;
+typedef unsigned int nlink_t;
+typedef unsigned int off_t;
+struct stat {
+ dev_t st_dev ;
+ ino_t st_ino ;
+ mode_t st_mode ;
+ nlink_t st_nlink ;
+ uid_t st_uid ;
+ gid_t st_gid ;
+ dev_t st_rdev ;
+ off_t st_size ;
+ time_t st_atime ;
+ time_t st_mtime ;
+ time_t st_ctime ;
+ blksize_t st_blksize ;
+ blkcnt_t st_blocks ;
+ char *__fc_real_data ;
+ int __fc_real_data_max_size ;
+};
+struct __fc_FILE {
+ unsigned int __fc_stdio_id ;
+ unsigned int __fc_maxsz ;
+ unsigned int __fc_writepos ;
+ unsigned int __fc_readpos ;
+ int __fc_is_a_socket ;
+ int __fc_mode ;
+ struct stat *__fc_inode ;
+};
+typedef struct __fc_FILE FILE;
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+extern int __fc_heap_status;
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+extern FILE *__fc_stdout;
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from *(format+(..)); */
+extern int printf(char const *format , ...);
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (! predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+/*@ assigns \nothing; */
+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 __initialize(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ assigns \nothing;
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+int G = 0;
+int *P;
+void e_acsl_global_init(void)
+{
+ __store_block((void *)(& P),4U);
+ __full_init((void *)(& P));
+ __store_block((void *)(& G),4U);
+ __full_init((void *)(& G));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int *Q;
+ e_acsl_global_init();
+ __store_block((void *)(& Q),4U);
+ __full_init((void *)(& P));
+ P = & G;
+ __full_init((void *)(& Q));
+ Q = P;
+ {
+ int __e_acsl_valid_read;
+ int __e_acsl_valid;
+ __initialize((void *)P,sizeof(int));
+ __e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
+ e_acsl_assert(__e_acsl_valid_read,(char *)"Precondition",
+ (char *)"mem_access: \\valid_read(P)",16);
+ __e_acsl_valid = __valid((void *)P,sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Precondition",
+ (char *)"mem_access: \\valid(P)",16);
+ (*P) ++;
+ }
+ /*@ assert *Q ≡ G; */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(& Q),sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid_read_2;
+ __e_acsl_valid_read_2 = __valid_read((void *)Q,sizeof(int));
+ __e_acsl_and = __e_acsl_valid_read_2;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",
+ (char *)"mem_access: \\valid_read(Q)",0);
+ e_acsl_assert(*Q == G,(char *)"Assertion",(char *)"*Q == G",17);
+ }
+ __retres = 0;
+ __delete_block((void *)(& P));
+ __delete_block((void *)(& G));
+ __delete_block((void *)(& Q));
+ __clean();
+ return __retres;
+}
+
+
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
new file mode 100644
index 0000000000000000000000000000000000000000..55ab6403b0dc6e8cfba1633937df8405097ac3e8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -0,0 +1,167 @@
+/* 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;
+typedef unsigned int ino_t;
+typedef unsigned int gid_t;
+typedef unsigned int uid_t;
+typedef long time_t;
+typedef unsigned int blkcnt_t;
+typedef unsigned int blksize_t;
+typedef unsigned int dev_t;
+typedef unsigned int mode_t;
+typedef unsigned int nlink_t;
+typedef unsigned int off_t;
+struct stat {
+ dev_t st_dev ;
+ ino_t st_ino ;
+ mode_t st_mode ;
+ nlink_t st_nlink ;
+ uid_t st_uid ;
+ gid_t st_gid ;
+ dev_t st_rdev ;
+ off_t st_size ;
+ time_t st_atime ;
+ time_t st_mtime ;
+ time_t st_ctime ;
+ blksize_t st_blksize ;
+ blkcnt_t st_blocks ;
+ char *__fc_real_data ;
+ int __fc_real_data_max_size ;
+};
+struct __fc_FILE {
+ unsigned int __fc_stdio_id ;
+ unsigned int __fc_maxsz ;
+ unsigned int __fc_writepos ;
+ unsigned int __fc_readpos ;
+ int __fc_is_a_socket ;
+ int __fc_mode ;
+ struct stat *__fc_inode ;
+};
+typedef struct __fc_FILE FILE;
+/*@
+model __mpz_struct { ℤ n };
+*/
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+/*@ requires \valid(x);
+ assigns *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+extern int __fc_heap_status;
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+extern FILE *__fc_stdout;
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from *(format+(..)); */
+extern int printf(char const *format , ...);
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (! predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+/*@ assigns \nothing; */
+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 __initialize(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+int G = 0;
+int *P;
+void e_acsl_global_init(void)
+{
+ __store_block((void *)(& P),4U);
+ __full_init((void *)(& P));
+ __store_block((void *)(& G),4U);
+ __full_init((void *)(& G));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int *Q;
+ e_acsl_global_init();
+ __store_block((void *)(& Q),4U);
+ __full_init((void *)(& P));
+ P = & G;
+ __full_init((void *)(& Q));
+ Q = P;
+ {
+ int __e_acsl_valid_read;
+ int __e_acsl_valid;
+ __initialize((void *)P,sizeof(int));
+ __e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
+ e_acsl_assert(__e_acsl_valid_read,(char *)"Precondition",
+ (char *)"mem_access: \\valid_read(P)",16);
+ __e_acsl_valid = __valid((void *)P,sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Precondition",
+ (char *)"mem_access: \\valid(P)",16);
+ (*P) ++;
+ }
+ /*@ assert *Q ≡ G; */
+ {
+ mpz_t __e_acsl;
+ mpz_t __e_acsl_G;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl,(long)*Q);
+ __gmpz_init_set_si(__e_acsl_G,(long)G);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl),
+ (__mpz_struct const *)(__e_acsl_G));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"*Q == G",17);
+ __gmpz_clear(__e_acsl);
+ __gmpz_clear(__e_acsl_G);
+ }
+ __retres = 0;
+ __delete_block((void *)(& P));
+ __delete_block((void *)(& G));
+ __delete_block((void *)(& Q));
+ __clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6b18f21a5e8c08c59d2446991ba55880f62666ec
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -0,0 +1,86 @@
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ G ∈ {0}
+ P ∈ {0}
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __initialize
+[value] using specification for function __valid_read
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function printf
+[value] using specification for function exit
+FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+[value] using specification for function __valid
+tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid.
+[value] using specification for function __initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __clean
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_global_init:
+[value] Values at end of function e_acsl_assert:
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+[value] Values at end of function main:
+ G ∈ {1}
+ P ∈ {{ &G }}
+ Q ∈ {{ &G }}
+ __retres ∈ {0}
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a935996b3c0d6a60a54a7ae5090ff9cf5e056207
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
@@ -0,0 +1,91 @@
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ G ∈ {0}
+ P ∈ {0}
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; } ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks; }; } ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __initialize
+[value] using specification for function __valid_read
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function printf
+[value] using specification for function exit
+FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+[value] using specification for function __valid
+tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid.
+[value] using specification for function __gmpz_init_set_si
+./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status unknown.
+[value] using specification for function __gmpz_cmp
+./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function __gmpz_clear
+./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __clean
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_global_init:
+[value] Values at end of function e_acsl_assert:
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+[value] Values at end of function main:
+ G ∈ {1}
+ P ∈ {{ &G }}
+ Q ∈ {{ &G }}
+ __retres ∈ {0}
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .__fc_mode; } ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli
index d039e51e84f42a00cb2b6ca0ee7db8d643190cc0..00bf26bf5a3dfa9adc7c1907acaf8be859622a8e 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/translate.mli
@@ -32,6 +32,8 @@ val translate_pre_code_annotation:
kernel_function -> Env.t -> code_annotation -> Env.t
val translate_post_code_annotation:
kernel_function -> Env.t -> code_annotation -> Env.t
+val translate_named_predicate:
+ kernel_function -> ?rte:bool -> Env.t -> predicate named -> Env.t
val predicate_to_exp: kernel_function -> predicate named -> exp
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index fc9e6b9856c28640353e0de1572fde9d4b2c897a..d28ce4c48a8b81dcbdf41b6938ddd5d4be3d6e84 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -23,6 +23,13 @@
open Cil_types
open Cil_datatype
+let get_rte_by_stmt =
+ Dynamic.get
+ ~plugin:"RteGen"
+ "stmt_annotations"
+ (Datatype.func2 Kernel_function.ty Stmt.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
+
(* move all labels of [stmt] onto [new_stmt] *)
let move_labels env stmt new_stmt =
let labels = stmt.labels in
@@ -242,31 +249,34 @@ you must call function `%s' by yourself"
| GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
when Misc.is_library_loc vi.vdecl ->
assert (not vi.vghost);
- if generate then
- Cil.JustCopyPost
- (fun l ->
- Misc.register_library_function (Cil.get_varinfo self#behavior vi);
- l)
- else begin
- Misc.register_library_function vi;
- Cil.SkipChildren
- end
+ if generate then
+ Cil.JustCopyPost
+ (fun l ->
+ Misc.register_library_function (Cil.get_varinfo self#behavior vi);
+ l)
+ else begin
+ Misc.register_library_function vi;
+ Cil.SkipChildren
+ end
| g when Misc.is_library_loc (Global.loc g) ->
if generate then Cil.JustCopy else Cil.SkipChildren
| g ->
- (* TODO: handle ghost declaration. Waiting for fixing bug #1328 *)
- let do_it = function
+ let do_it g =
+ match g with
| GVar(vi, i, _) ->
+ vi.vghost <- false;
(* remove initializers on need *)
- if Pre_analysis.old_must_model_vi self#behavior vi then
- (try
- let old_vi = Cil.get_original_varinfo self#behavior vi in
- match Varinfo.Hashtbl.find global_vars old_vi with
- | None -> ()
- | Some _ -> i.init <- None;
- with Not_found ->
- assert false)
+ if Pre_analysis.old_must_model_vi self#behavior vi then begin
+ try
+ let old_vi = Cil.get_original_varinfo self#behavior vi in
+ match Varinfo.Hashtbl.find global_vars old_vi with
+ | None -> ()
+ | Some _ -> i.init <- None
+ with Not_found ->
+ assert false
+ end
| GFun({ svar = vi } as fundec, _) ->
+ vi.vghost <- false;
(* remember that we have to remove the main later (see method
[vfile]) *)
if vi.vorig_name = Kernel.MainFunction.get ()
@@ -321,8 +331,10 @@ you must call function `%s' by yourself"
body.blocals
vars
- method vfunc _f =
- Cil.DoChildrenPost (fun f -> self#add_generated_variables_in_function f; f)
+ method vfunc f =
+ List.iter (fun vi -> vi.vghost <- false) f.slocals;
+ Cil.DoChildrenPost
+ (fun f -> self#add_generated_variables_in_function f; f)
method private is_return old_kf stmt =
let old_ret =
@@ -415,6 +427,21 @@ you must call function `%s' by yourself"
been modified from the time where pre actions have been executed.
Use [function_env] to get it back. *)
let env = !function_env in
+ let env =
+ if stmt.ghost then begin
+ stmt.ghost <- false;
+ (* translate potential RTEs of ghost code *)
+ let rtes = get_rte_by_stmt kf stmt in
+ List.fold_left
+ (fun env a -> match a.annot_content with
+ | AAssert(_, p) ->
+ Translate.translate_named_predicate kf ~rte:false env p
+ | _ -> assert false)
+ env
+ rtes
+ end else
+ env
+ in
let mk_block b =
let mk b = match b.bstmts with
| [] ->
@@ -494,7 +521,6 @@ you must call function `%s' by yourself"
(* TODO: must clear the local block anytime (?) *)
mk_block post_block, env
in
- (* if TODO HERE *)
function_env := env;
Options.debug ~level:3
"@[new stmt (from sid %d):@ %a@]" stmt.sid Cil.d_stmt new_stmt;
@@ -528,7 +554,6 @@ you must call function `%s' by yourself"
match new_blk.blocals with
| [] -> new_blk
| _ :: _ ->
- (* bstmts <- [store_locals] @ bstmts @ [delete_locals] *)
let kf = Extlib.the self#current_kf in
let add_locals stmts =
List.fold_left
@@ -558,9 +583,11 @@ you must call function `%s' by yourself"
insert_in_innermost_last_block new_blk (List.rev new_blk.bstmts);
new_blk.bstmts <-
List.fold_left
- (fun acc v ->
- if Pre_analysis.must_model_vi v
- then Misc.mk_store_stmt (Cil.get_varinfo self#behavior v) :: acc
+ (fun acc vi ->
+ if Pre_analysis.must_model_vi vi
+ then
+ let vi = Cil.get_varinfo self#behavior vi in
+ Misc.mk_store_stmt vi :: acc
else acc)
new_blk.bstmts
blk.blocals;