diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
new file mode 100644
index 0000000000000000000000000000000000000000..3752a6400545995ec4abd6a1f3cded19e85ac2d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -0,0 +1,141 @@
+/* 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;
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ fpos_t __fc_stdio_fpos ;
+ char *__fc_stdio_buffer ;
+ char __fc_stdio_error ;
+ char __fc_stdio_eof ;
+ long __fc_stdio_id ;
+};
+typedef struct __fc_FILE FILE;
+struct list {
+ int element ;
+ struct list *next ;
+};
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
+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__)) int _valid(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);
+/*@ behavior B1:
+ assumes l ≡ \null;
+ ensures \result ≡ \old(l);
+
+ behavior B2:
+ assumes \valid(l);
+ assumes l->next ≡ \null;
+ ensures \result ≡ \old(l);
+
+
+*/
+struct list *f(struct list *l)
+{
+ struct list *__e_acsl_at_4;
+ int __e_acsl_at_3;
+ struct list *__e_acsl_at_2;
+ int __e_acsl_at;
+ struct list *__retres;
+ __e_acsl_at_4 = l;
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ int __e_acsl_and_2;
+ __e_acsl_initialized = _initialized((void *)(& l),sizeof(struct list *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = _valid((void *)l,sizeof(struct list));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else { __e_acsl_and = 0; }
+ if (__e_acsl_and) { __e_acsl_and_2 = l->next == (void *)0; }
+ else { __e_acsl_and_2 = 0; }
+ __e_acsl_at_3 = __e_acsl_and_2;
+ }
+
+ __e_acsl_at_2 = l;
+ __e_acsl_at = l == (void *)0;
+ if (l == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ if (l->next == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ __retres = (struct list *)((void *)0);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = __retres == __e_acsl_at_2; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(l == \\null) ==>\n\\result == \\old(l)",18);
+ if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
+ else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(\\valid(l) && l->next == \\null) ==>\n\\result == \\old(l)",
+ 22);
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ f((struct list *)((void *)0));
+ __retres = 0;
+ __clean();
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
new file mode 100644
index 0000000000000000000000000000000000000000..3752a6400545995ec4abd6a1f3cded19e85ac2d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -0,0 +1,141 @@
+/* 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;
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ fpos_t __fc_stdio_fpos ;
+ char *__fc_stdio_buffer ;
+ char __fc_stdio_error ;
+ char __fc_stdio_eof ;
+ long __fc_stdio_id ;
+};
+typedef struct __fc_FILE FILE;
+struct list {
+ int element ;
+ struct list *next ;
+};
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
+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__)) int _valid(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);
+/*@ behavior B1:
+ assumes l ≡ \null;
+ ensures \result ≡ \old(l);
+
+ behavior B2:
+ assumes \valid(l);
+ assumes l->next ≡ \null;
+ ensures \result ≡ \old(l);
+
+
+*/
+struct list *f(struct list *l)
+{
+ struct list *__e_acsl_at_4;
+ int __e_acsl_at_3;
+ struct list *__e_acsl_at_2;
+ int __e_acsl_at;
+ struct list *__retres;
+ __e_acsl_at_4 = l;
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ int __e_acsl_and_2;
+ __e_acsl_initialized = _initialized((void *)(& l),sizeof(struct list *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = _valid((void *)l,sizeof(struct list));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else { __e_acsl_and = 0; }
+ if (__e_acsl_and) { __e_acsl_and_2 = l->next == (void *)0; }
+ else { __e_acsl_and_2 = 0; }
+ __e_acsl_at_3 = __e_acsl_and_2;
+ }
+
+ __e_acsl_at_2 = l;
+ __e_acsl_at = l == (void *)0;
+ if (l == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ if (l->next == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ __retres = (struct list *)((void *)0);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = __retres == __e_acsl_at_2; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(l == \\null) ==>\n\\result == \\old(l)",18);
+ if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
+ else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(\\valid(l) && l->next == \\null) ==>\n\\result == \\old(l)",
+ 22);
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ f((struct list *)((void *)0));
+ __retres = 0;
+ __clean();
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7d07b614b1707d70d7b12d08af4e2762c75343cb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -0,0 +1,212 @@
+[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"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid_in_contract.c"
+tests/e-acsl-runtime/valid_in_contract.c:21:[e-acsl] warning: missing guard for ensuring that l is a valid memory access
+[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 ∈ {2147483647}
+ __fc_heap_status ∈ [--..--]
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+ S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] computing for function f <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:34.
+[value] computing for function _initialized <- f <- main.
+ Called from :0.
+[value] using specification for function _initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+[value] Done for function _initialized
+[value] computing for function _valid <- f <- main.
+ Called from :0.
+[value] using specification for function _valid
+[value] Done for function _valid
+:0:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
+[value] computing for function e_acsl_assert <- f <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:18.
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function e_acsl_assert <- f <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:22.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
+tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: assumes got status invalid; post-condition not evaluated.
+[value] Recording results for f
+[value] Done for function f
+[value] computing for function __clean <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:35.
+[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 __clean
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_assert:
+[value] Values at end of function f:
+ __retres ∈ {0}
+[value] Values at end of function main:
+ __retres ∈ {0}
+/* 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;
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ fpos_t __fc_stdio_fpos ;
+ char *__fc_stdio_buffer ;
+ char __fc_stdio_error ;
+ char __fc_stdio_eof ;
+ long __fc_stdio_id ;
+};
+typedef struct __fc_FILE FILE;
+struct list {
+ int element ;
+ struct list *next ;
+};
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
+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__)) int _valid(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);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+/*@ behavior B1:
+ assumes l ≡ \null;
+ ensures \result ≡ \old(l);
+
+ behavior B2:
+ assumes \valid(l);
+ assumes l->next ≡ \null;
+ ensures \result ≡ \old(l);
+
+
+*/
+struct list *f(struct list *l)
+{
+ struct list *__e_acsl_at_4;
+ int __e_acsl_at_3;
+ struct list *__e_acsl_at_2;
+ int __e_acsl_at;
+ struct list *__retres;
+ __e_acsl_at_4 = l;
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ int __e_acsl_and_2;
+ __e_acsl_initialized = _initialized((void *)(& l),sizeof(struct list *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = _valid((void *)l,sizeof(struct list));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else { __e_acsl_and = 0; }
+ if (__e_acsl_and) {
+ /*@ assert Value: mem_access: \valid_read(&l->next); */
+ __e_acsl_and_2 = l->next == (void *)0;
+ } else { __e_acsl_and_2 = 0; }
+ __e_acsl_at_3 = __e_acsl_and_2;
+ }
+
+ __e_acsl_at_2 = l;
+ __e_acsl_at = l == (void *)0;
+ if (l == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ if (l->next == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ __retres = (struct list *)((void *)0);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = __retres == __e_acsl_at_2; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(l == \\null) ==>\n\\result == \\old(l)",18);
+ if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
+ else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(\\valid(l) && l->next == \\null) ==>\n\\result == \\old(l)",
+ 22);
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ f((struct list *)((void *)0));
+ __retres = 0;
+ __clean();
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7d07b614b1707d70d7b12d08af4e2762c75343cb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -0,0 +1,212 @@
+[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"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid_in_contract.c"
+tests/e-acsl-runtime/valid_in_contract.c:21:[e-acsl] warning: missing guard for ensuring that l is a valid memory access
+[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 ∈ {2147483647}
+ __fc_heap_status ∈ [--..--]
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+ S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] computing for function f <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:34.
+[value] computing for function _initialized <- f <- main.
+ Called from :0.
+[value] using specification for function _initialized
+./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+[value] Done for function _initialized
+[value] computing for function _valid <- f <- main.
+ Called from :0.
+[value] using specification for function _valid
+[value] Done for function _valid
+:0:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
+[value] computing for function e_acsl_assert <- f <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:18.
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function e_acsl_assert <- f <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:22.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
+tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: assumes got status invalid; post-condition not evaluated.
+[value] Recording results for f
+[value] Done for function f
+[value] computing for function __clean <- main.
+ Called from tests/e-acsl-runtime/valid_in_contract.c:35.
+[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 __clean
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_assert:
+[value] Values at end of function f:
+ __retres ∈ {0}
+[value] Values at end of function main:
+ __retres ∈ {0}
+/* 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;
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ fpos_t __fc_stdio_fpos ;
+ char *__fc_stdio_buffer ;
+ char __fc_stdio_error ;
+ char __fc_stdio_eof ;
+ long __fc_stdio_id ;
+};
+typedef struct __fc_FILE FILE;
+struct list {
+ int element ;
+ struct list *next ;
+};
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
+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__)) int _valid(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);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+/*@ behavior B1:
+ assumes l ≡ \null;
+ ensures \result ≡ \old(l);
+
+ behavior B2:
+ assumes \valid(l);
+ assumes l->next ≡ \null;
+ ensures \result ≡ \old(l);
+
+
+*/
+struct list *f(struct list *l)
+{
+ struct list *__e_acsl_at_4;
+ int __e_acsl_at_3;
+ struct list *__e_acsl_at_2;
+ int __e_acsl_at;
+ struct list *__retres;
+ __e_acsl_at_4 = l;
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ int __e_acsl_and_2;
+ __e_acsl_initialized = _initialized((void *)(& l),sizeof(struct list *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = _valid((void *)l,sizeof(struct list));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else { __e_acsl_and = 0; }
+ if (__e_acsl_and) {
+ /*@ assert Value: mem_access: \valid_read(&l->next); */
+ __e_acsl_and_2 = l->next == (void *)0;
+ } else { __e_acsl_and_2 = 0; }
+ __e_acsl_at_3 = __e_acsl_and_2;
+ }
+
+ __e_acsl_at_2 = l;
+ __e_acsl_at = l == (void *)0;
+ if (l == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ if (l->next == (void *)0) {
+ __retres = l;
+ goto return_label; }
+ __retres = (struct list *)((void *)0);
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ int __e_acsl_implies_2;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = __retres == __e_acsl_at_2; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(l == \\null) ==>\n\\result == \\old(l)",18);
+ if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
+ else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
+ e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"\\old(\\valid(l) && l->next == \\null) ==>\n\\result == \\old(l)",
+ 22);
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ f((struct list *)((void *)0));
+ __retres = 0;
+ __clean();
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
new file mode 100644
index 0000000000000000000000000000000000000000..4fd31a0eed19d692cd498bf2a5638fcda710185f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
@@ -0,0 +1,36 @@
+/* run.config
+ COMMENT: function contract involving \valid
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+ EXECNOW: LOG gen_valid_in_contract.c BIN gen_valid_in_contract.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract.c > /dev/null && ./gcc_test.sh valid_in_contract
+ EXECNOW: LOG gen_valid_in_contract2.c BIN gen_valid_in_contract2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract2.c > /dev/null && ./gcc_test.sh valid_in_contract2
+*/
+
+#include <stdlib.h>
+
+struct list {
+ int element;
+ struct list * next;
+};
+
+/*@
+ @ behavior B1:
+ @ assumes l == \null;
+ @ ensures \result == l;
+ @ behavior B2:
+ @ assumes \valid(l);
+ @ assumes l->next == \null;
+ @ ensures \result == l;
+*/
+struct list * f(struct list * l) {
+ /* length = 0 */
+ if(l == NULL) return l;
+ /* length = 1 : already sorted */
+ if(l->next == NULL) return l;
+
+ return NULL;
+}
+
+int main() {
+ f(NULL);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 619ff6c782b75b19cce49d6e0af91fe93d5aea03..fa5049aeb0505c888e9be63649b0d95107714283 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -563,7 +563,7 @@ let rec named_predicate_to_exp ?name env p =
(label, Logic_const.taddrof ~loc tlv (Ctype (TPtr(ty, [])))),
p)
in
- Typing.type_named_predicate p;
+ Typing.type_named_predicate ~must_clear:false p;
named_predicate_to_exp env p
| _ -> assert false
end
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index cb578f17bea3d0ca887e20187a14ef2410a0fc29..fa3925ce87684d80d5add87d288b2b4044006fe0 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -233,12 +233,12 @@ let rec type_term t =
let div a b =
try BI.c_div a b
with Division_by_zero ->
- (* either the generated code will be dead (e.g. [false && 1/0])
- or it contains a potential RTE and thus it is actually equivalent
- to dead code. In any case, any type is correct at this point and
- we generate the less restrictive one (0 is always representable)
- in order to be as more precise as possible. *)
- BI.zero
+ (* either the generated code will be dead (e.g. [false && 1/0]) or
+ it contains a potential RTE and thus it is actually equivalent to
+ dead code. In any case, any type is correct at this point and we
+ generate the less restrictive one (0 is always representable) in
+ order to be as more precise as possible. *)
+ BI.zero
in
signed_rule div t1 t2
| TBinOp(Mod, t1, t2) ->
@@ -421,10 +421,10 @@ let rec type_predicate_named p = match p.content with
let type_term t = if not (Options.Gmp_only.get ()) then ignore (type_term t)
-let type_named_predicate p =
+let type_named_predicate ?(must_clear=true) p =
if not (Options.Gmp_only.get ()) then begin
Options.debug ~level:2 "typing predicate %a" Cil.d_predicate_named p;
- clear ();
+ if must_clear then clear ();
type_predicate_named p
end
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 84c1379178c8cce6743dbc11115350fe94e16f70..ca36d5b9333e282367891289fcc9de0588cad5f7 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -32,7 +32,7 @@ val typ_of_integer: My_bigint.t -> bool -> ikind
and [false] for signed.
@raise Not_representable if the integer does not fit in any C type. *)
-val type_named_predicate: predicate named -> unit
+val type_named_predicate: ?must_clear:bool -> predicate named -> unit
(** Compute the type of each term of the given predicate. *)
val type_term: term -> unit