diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
new file mode 100644
index 0000000000000000000000000000000000000000..c2306b33bd28b649bdd59e27c6ecfc3b8acbf8fc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
@@ -0,0 +1,22 @@
+/* run.config
+ COMMENT: frama-c/e-acsl#40, test for initialized memory after a call to fread
+ on /dev/urandom.
+*/
+
+#include <stdio.h>
+
+int main() {
+ char buf[4];
+ FILE *f = fopen("/dev/urandom", "r");
+ if (f) {
+ char buf[4];
+ int res = fread(buf, 1, 4, f);
+ if (res == 4) {
+ //@ assert \initialized(&buf[3]);
+ buf[0] = buf[3];
+ } else
+ return 2;
+ } else
+ return 1;
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
new file mode 100644
index 0000000000000000000000000000000000000000..559ef66c07d1b3649d063335a8f41b015fe6f4e8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
@@ -0,0 +1,362 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+char *__gen_e_acsl_literal_string;
+char *__gen_e_acsl_literal_string_2;
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_fopen(char const * restrict filename,
+ char const * restrict mode);
+
+/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_read: \result ≤ \old(nmemb);
+ ensures
+ initialization:
+ \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1))
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
+ */
+size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
+ FILE * restrict stream);
+
+/*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1));
+ requires valid_stream: \valid(stream);
+ ensures size_read: \result ≤ \old(nmemb);
+ ensures
+ initialization:
+ \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1));
+ assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result;
+ assigns *((char *)ptr + (0 .. nmemb * size - 1))
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns *stream
+ \from (indirect: size), (indirect: nmemb), (indirect: *stream);
+ assigns \result \from size, (indirect: *stream);
+ */
+size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
+ FILE * restrict stream)
+{
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
+ void *__gen_e_acsl_at_2;
+ size_t __gen_e_acsl_at;
+ size_t __retres;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_nmemb;
+ __e_acsl_mpz_t __gen_e_acsl_size_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ int __gen_e_acsl_le;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le_2;
+ unsigned long __gen_e_acsl_size_3;
+ int __gen_e_acsl_valid;
+ int __gen_e_acsl_valid_2;
+ __e_acsl_store_block((void *)(& stream),(size_t)8);
+ __e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_nmemb,nmemb);
+ __gmpz_init_set_ui(__gen_e_acsl_size_2,size);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_nmemb),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_2));
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_init_set(__gen_e_acsl_size,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2));
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ else __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __gmpz_init_set_ui(__gen_e_acsl__4,18446744073709551615UL);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_le_2 <= 0,1,"RTE","fread",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(char) * (((nmemb * size - 1) - 0) + 1);\n size <= 0? 0: size)\n <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/stdio.h",351);
+ __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 1 * 0),
+ __gen_e_acsl_size_3,ptr,
+ (void *)(& ptr));
+ __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","fread",
+ "valid_ptr_block: \\valid((char *)ptr + (0 .. nmemb * size - 1))",
+ "FRAMAC_SHARE/libc/stdio.h",351);
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stream,sizeof(FILE),
+ (void *)stream,(void *)(& stream));
+ __e_acsl_assert(__gen_e_acsl_valid_2,1,"Precondition","fread",
+ "valid_stream: \\valid(stream)",
+ "FRAMAC_SHARE/libc/stdio.h",352);
+ __gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_nmemb);
+ __gmpz_clear(__gen_e_acsl_size_2);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl_if);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_7;
+ __gmpz_init_set_ui(__gen_e_acsl_size_7,size);
+ __gmpz_init_set(__gen_e_acsl_at_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_7));
+ __gmpz_clear(__gen_e_acsl_size_7);
+ }
+ __gen_e_acsl_at_2 = ptr;
+ __gen_e_acsl_at = nmemb;
+ __retres = fread(ptr,size,nmemb,stream);
+ {
+ __e_acsl_mpz_t __gen_e_acsl___retres;
+ __e_acsl_mpz_t __gen_e_acsl_size_4;
+ __e_acsl_mpz_t __gen_e_acsl_mul_3;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_le_3;
+ unsigned long __gen_e_acsl_size_5;
+ __gmpz_init_set_ui(__gen_e_acsl___retres,__retres);
+ __gmpz_init_set_ui(__gen_e_acsl_size_4,size);
+ __gmpz_init(__gen_e_acsl_mul_3);
+ __gmpz_mul(__gen_e_acsl_mul_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl___retres),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_4));
+ __gmpz_init_set_ui(__gen_e_acsl__5,18446744073709551615UL);
+ __gen_e_acsl_le_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __e_acsl_assert(__gen_e_acsl_le_3 <= 0,1,"RTE","fread",
+ "size_lesser_or_eq_than_SIZE_MAX: __retres * size <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/stdio.h",350);
+ __gen_e_acsl_size_5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3));
+ __e_acsl_initialize(ptr,__gen_e_acsl_size_5);
+ __gmpz_clear(__gen_e_acsl___retres);
+ __gmpz_clear(__gen_e_acsl_size_4);
+ __gmpz_clear(__gen_e_acsl_mul_3);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl_size_6;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof_2;
+ __e_acsl_mpz_t __gen_e_acsl_result;
+ __e_acsl_mpz_t __gen_e_acsl_mul_4;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl_mul_5;
+ int __gen_e_acsl_le_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_le_5;
+ unsigned long __gen_e_acsl_size_8;
+ int __gen_e_acsl_initialized;
+ __e_acsl_assert(__retres <= __gen_e_acsl_at,1,"Postcondition","fread",
+ "size_read: \\result <= \\old(nmemb)",
+ "FRAMAC_SHARE/libc/stdio.h",356);
+ __gmpz_init_set_si(__gen_e_acsl_sizeof_2,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_result,__retres);
+ __gmpz_init(__gen_e_acsl_mul_4);
+ __gmpz_mul(__gen_e_acsl_mul_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_mul_5);
+ __gmpz_mul(__gen_e_acsl_mul_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_init_set(__gen_e_acsl_size_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_5));
+ __gen_e_acsl_le_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ if (__gen_e_acsl_le_4 <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_clear(__gen_e_acsl__8);
+ }
+ else __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size_6));
+ __gmpz_init_set_ui(__gen_e_acsl__9,18446744073709551615UL);
+ __gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert(__gen_e_acsl_le_5 <= 0,1,"RTE","fread",
+ "offset_lesser_or_eq_than_SIZE_MAX:\n (\\let size = sizeof(char) * (((\\result * \\old(size) - 1) - 0) + 1);\n size <= 0? 0: size)\n <= 18446744073709551615",
+ "FRAMAC_SHARE/libc/stdio.h",357);
+ __gen_e_acsl_size_8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)((char *)__gen_e_acsl_at_2 +
+ 1 * 0),
+ __gen_e_acsl_size_8);
+ __e_acsl_assert(__gen_e_acsl_initialized,1,"Postcondition","fread",
+ "initialization:\n \\initialized((char *)\\old(ptr) + (0 .. \\result * \\old(size) - 1))",
+ "FRAMAC_SHARE/libc/stdio.h",357);
+ __e_acsl_delete_block((void *)(& stream));
+ __e_acsl_delete_block((void *)(& ptr));
+ __gmpz_clear(__gen_e_acsl_size_6);
+ __gmpz_clear(__gen_e_acsl_sizeof_2);
+ __gmpz_clear(__gen_e_acsl_result);
+ __gmpz_clear(__gen_e_acsl_mul_4);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_mul_5);
+ __gmpz_clear(__gen_e_acsl_if_2);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_at_3);
+ return __retres;
+ }
+}
+
+/*@ requires valid_filename: valid_read_string(filename);
+ requires valid_mode: valid_read_string(mode);
+ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(filename + (0 .. strlen{Old}(filename)))),
+ (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_fopen(char const * restrict filename,
+ char const * restrict mode)
+{
+ FILE *__retres;
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __retres = fopen(filename,mode);
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+}
+
+void __e_acsl_globals_init(void)
+{
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __gen_e_acsl_literal_string = "r";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("r"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ __gen_e_acsl_literal_string_2 = "/dev/urandom";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("/dev/urandom"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ }
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ char buf[4];
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ FILE *f =
+ __gen_e_acsl_fopen(__gen_e_acsl_literal_string_2,
+ __gen_e_acsl_literal_string);
+ __e_acsl_store_block((void *)(& f),(size_t)8);
+ __e_acsl_full_init((void *)(& f));
+ if (f) {
+ char buf_0[4];
+ size_t tmp_0;
+ __e_acsl_store_block((void *)(buf_0),(size_t)4);
+ tmp_0 = __gen_e_acsl_fread((void *)(buf_0),(unsigned long)1,
+ (unsigned long)4,f);
+ int res = (int)tmp_0;
+ if (res == 4) {
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& buf_0[3]),
+ sizeof(char));
+ __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
+ "\\initialized(&buf_0[3])",
+ "tests/bts/issue-eacsl-40.c",15);
+ }
+ /*@ assert \initialized(&buf_0[3]); */ ;
+ __e_acsl_initialize((void *)(buf_0),sizeof(char));
+ buf_0[0] = buf_0[3];
+ }
+ else {
+ __retres = 2;
+ __e_acsl_delete_block((void *)(buf_0));
+ goto return_label;
+ }
+ __e_acsl_delete_block((void *)(buf_0));
+ }
+ else {
+ __retres = 1;
+ goto return_label;
+ }
+ __retres = 0;
+ return_label:
+ {
+ __e_acsl_delete_block((void *)(& f));
+ __e_acsl_memory_clean();
+ return __retres;
+ }
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5900456a1004264539b2adf880dff6c5139b07c5
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
@@ -0,0 +1,37 @@
+[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `fopen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning:
+ E-ACSL construct `logic functions with labels' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:155: Warning:
+ E-ACSL construct `predicate with no definition nor reads clause'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning:
+ function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
+[eva:alarm] tests/bts/issue-eacsl-40.c:15: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-40.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-40.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391