diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
new file mode 100644
index 0000000000000000000000000000000000000000..886159e1d67611a4203924e4b7b49269a98975fd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
@@ -0,0 +1,66 @@
+/* run.config
+ COMMENT: Behaviours of the \initialized E-ACSL predicate
+*/
+
+#include <stdlib.h>
+
+int A = 0;
+int B;
+
+int main(void) {
+ /* All globals are initialized, even if the initializer is not given */
+ int *p = &A;
+ int *q = &B;
+ /*@assert \initialized(&A) ; */
+ /*@assert \initialized(&B) ; */
+ /*@assert \initialized(p) ; */
+ /*@assert \initialized(q) ; */
+
+ /* A local variable without an initializer is uninitialized */
+ int a = 0;
+ int b;
+ long c[2] = { 1, 1 };
+ long d[2];
+ p = &a;
+ q = &b;
+
+ /*@assert \initialized(&a) ; */
+ /*@assert ! \initialized(&b) ; */
+ /*@assert \initialized(p) ; */
+ /*@assert ! \initialized(q) ; */
+ /*@assert \initialized(&c) ; */
+ /*@assert ! \initialized(&d) ; */
+
+ /* Local variables also initialized by assignments */
+ b = 0;
+ d[0] = 1;
+ /*@assert \initialized(&b) ; */
+ /*@assert \initialized(q) ; */
+ /*@assert ! \initialized(&d) ; */
+ d[1] = 1;
+ /*@assert \initialized(&d) ; */
+
+ /* Malloc allocates un-initialized memory */
+ p = (int*)malloc(sizeof(int*));
+ /*@assert ! \initialized(p) ; */
+
+ /* Calloc allocates initialized memory */
+ q = (int*)calloc(1, sizeof(int));
+ /*@ assert \initialized(q) ; */
+
+ /* Block reallocared using `realloc' carries initialization of the of the
+ * existing fragment but does not initialize the newly allocated one */
+ q = (int*)realloc(q, 2*sizeof(int));
+ /*@assert \initialized(q) ; */
+ q++;
+ /*@assert ! \initialized(q) ; */
+ q--;
+
+ /* Initialized on un-allocated regions is always false. This does not lead
+ * to undefined bevaviours in production mode or assertion failures in debug
+ * mode. */
+ free(p);
+ free(q);
+ /*@assert ! \initialized(p) ; */
+ /*@assert ! \initialized(q) ; */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c b/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c
new file mode 100644
index 0000000000000000000000000000000000000000..0ef49fb786d9e4a0805fb6eba5b24222af95f808
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c
@@ -0,0 +1,30 @@
+/* run.config
+ COMMENT: Behaviours of the \offset E-ACSL predicate
+*/
+
+#include <stdlib.h>
+
+int main() {
+ /* Stack offsets */
+ char c;
+ /*@assert \offset(&c) == 0; */
+
+ short slist[3];
+ short *ps = slist;
+ /*@assert \offset(ps) == 0; */
+ /*@assert \offset(ps + 1) == 2; */
+ /*@assert \offset(ps + 2) == 4; */
+
+ int ilist [3];
+ int *pi = ilist;
+ /*@assert \offset(pi) == 0; */
+ /*@assert \offset(pi + 1) == 4; */
+ /*@assert \offset(pi + 2) == 8; */
+
+ /* Heap offsets */
+ long *p = (long*)malloc(sizeof(long)*12);
+ /*@assert \offset(p) == 0; */
+ /*@assert \offset(p+1) == 8; */
+ /*@assert \offset(p+2) == 16; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
new file mode 100644
index 0000000000000000000000000000000000000000..dd211269b422d37f9ceb8edde052bd70d606b28d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
@@ -0,0 +1,207 @@
+/* Generated by Frama-C */
+int A = 0;
+int B;
+void __e_acsl_globals_init(void)
+{
+ __store_block((void *)(& B),4UL);
+ __full_init((void *)(& B));
+ __store_block((void *)(& A),4UL);
+ __full_init((void *)(& A));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int *p;
+ int *q;
+ int a;
+ int b;
+ long c[2];
+ long d[2];
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_globals_init();
+ __store_block((void *)(d),16UL);
+ __store_block((void *)(c),16UL);
+ __store_block((void *)(& b),4UL);
+ __store_block((void *)(& a),4UL);
+ __store_block((void *)(& q),8UL);
+ __store_block((void *)(& p),8UL);
+ __full_init((void *)(& p));
+ p = & A;
+ __full_init((void *)(& q));
+ q = & B;
+ /*@ assert \initialized(&A); */
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(&A)",14);
+ /*@ assert \initialized(&B); */
+ __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(&B)",15);
+ /*@ assert \initialized(p); */
+ {
+ int __e_acsl_initialized;
+ __e_acsl_initialized = __initialized((void *)p,sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(p)",16);
+ }
+ /*@ assert \initialized(q); */
+ {
+ int __e_acsl_initialized_2;
+ __e_acsl_initialized_2 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(q)",17);
+ }
+ __full_init((void *)(& a));
+ a = 0;
+ __initialize((void *)(c),sizeof(long));
+ c[0] = (long)1;
+ __initialize((void *)(& c[1]),sizeof(long));
+ c[1] = (long)1;
+ __full_init((void *)(& p));
+ p = & a;
+ __full_init((void *)(& q));
+ q = & b;
+ /*@ assert \initialized(&a); */
+ {
+ int __e_acsl_initialized_3;
+ __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_3,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(&a)",27);
+ }
+ /*@ assert ¬\initialized(&b); */
+ {
+ int __e_acsl_initialized_4;
+ __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int));
+ __e_acsl_assert(! __e_acsl_initialized_4,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(&b)",28);
+ }
+ /*@ assert \initialized(p); */
+ {
+ int __e_acsl_initialized_5;
+ __e_acsl_initialized_5 = __initialized((void *)p,sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_5,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(p)",29);
+ }
+ /*@ assert ¬\initialized(q); */
+ {
+ int __e_acsl_initialized_6;
+ __e_acsl_initialized_6 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(! __e_acsl_initialized_6,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(q)",30);
+ }
+ /*@ assert \initialized(&c); */
+ {
+ int __e_acsl_initialized_7;
+ __e_acsl_initialized_7 = __initialized((void *)(& c),sizeof(long [2]));
+ __e_acsl_assert(__e_acsl_initialized_7,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(&c)",31);
+ }
+ /*@ assert ¬\initialized(&d); */
+ {
+ int __e_acsl_initialized_8;
+ __e_acsl_initialized_8 = __initialized((void *)(& d),sizeof(long [2]));
+ __e_acsl_assert(! __e_acsl_initialized_8,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(&d)",32);
+ }
+ __full_init((void *)(& b));
+ b = 0;
+ __initialize((void *)(d),sizeof(long));
+ d[0] = (long)1;
+ /*@ assert \initialized(&b); */
+ {
+ int __e_acsl_initialized_9;
+ __e_acsl_initialized_9 = __initialized((void *)(& b),sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_9,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(&b)",37);
+ }
+ /*@ assert \initialized(q); */
+ {
+ int __e_acsl_initialized_10;
+ __e_acsl_initialized_10 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_10,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(q)",38);
+ }
+ /*@ assert ¬\initialized(&d); */
+ {
+ int __e_acsl_initialized_11;
+ __e_acsl_initialized_11 = __initialized((void *)(& d),sizeof(long [2]));
+ __e_acsl_assert(! __e_acsl_initialized_11,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(&d)",39);
+ }
+ __initialize((void *)(& d[1]),sizeof(long));
+ d[1] = (long)1;
+ /*@ assert \initialized(&d); */
+ {
+ int __e_acsl_initialized_12;
+ __e_acsl_initialized_12 = __initialized((void *)(& d),sizeof(long [2]));
+ __e_acsl_assert(__e_acsl_initialized_12,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(&d)",41);
+ }
+ __full_init((void *)(& p));
+ p = (int *)__e_acsl_malloc(sizeof(int *));
+ /*@ assert ¬\initialized(p); */
+ {
+ int __e_acsl_initialized_13;
+ __e_acsl_initialized_13 = __initialized((void *)p,sizeof(int));
+ __e_acsl_assert(! __e_acsl_initialized_13,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(p)",45);
+ }
+ __full_init((void *)(& q));
+ q = (int *)__calloc((unsigned long)1,sizeof(int));
+ /*@ assert \initialized(q); */
+ {
+ int __e_acsl_initialized_14;
+ __e_acsl_initialized_14 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_14,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(q)",49);
+ }
+ __full_init((void *)(& q));
+ q = (int *)__e_acsl_realloc((void *)q,(unsigned long)2 * sizeof(int));
+ /*@ assert \initialized(q); */
+ {
+ int __e_acsl_initialized_15;
+ __e_acsl_initialized_15 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(__e_acsl_initialized_15,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(q)",54);
+ }
+ __full_init((void *)(& q));
+ q ++;
+ /*@ assert ¬\initialized(q); */
+ {
+ int __e_acsl_initialized_16;
+ __e_acsl_initialized_16 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(! __e_acsl_initialized_16,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(q)",56);
+ }
+ __full_init((void *)(& q));
+ q --;
+ __e_acsl_free((void *)p);
+ __e_acsl_free((void *)q);
+ /*@ assert ¬\initialized(p); */
+ {
+ int __e_acsl_initialized_17;
+ __e_acsl_initialized_17 = __initialized((void *)p,sizeof(int));
+ __e_acsl_assert(! __e_acsl_initialized_17,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(p)",64);
+ }
+ /*@ assert ¬\initialized(q); */
+ {
+ int __e_acsl_initialized_18;
+ __e_acsl_initialized_18 = __initialized((void *)q,sizeof(int));
+ __e_acsl_assert(! __e_acsl_initialized_18,(char *)"Assertion",
+ (char *)"main",(char *)"!\\initialized(q)",65);
+ }
+ __retres = 0;
+ __delete_block((void *)(& B));
+ __delete_block((void *)(& A));
+ __delete_block((void *)(d));
+ __delete_block((void *)(c));
+ __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_offset.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c
new file mode 100644
index 0000000000000000000000000000000000000000..3129aa3b85b7b2f6a32143ecd78edfa12c4e1b5a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c
@@ -0,0 +1,115 @@
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ char c;
+ short slist[3];
+ short *ps;
+ int ilist[3];
+ int *pi;
+ long *p;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& pi),8UL);
+ __store_block((void *)(ilist),12UL);
+ __store_block((void *)(& ps),8UL);
+ __store_block((void *)(slist),6UL);
+ __store_block((void *)(& c),1UL);
+ /*@ assert \offset(&c) ≡ 0; */
+ {
+ int __e_acsl_offset;
+ __e_acsl_offset = __offset((void *)(& c));
+ __e_acsl_assert((unsigned long)__e_acsl_offset == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(&c) == 0",10);
+ }
+ __full_init((void *)(& ps));
+ ps = slist;
+ /*@ assert \offset(ps) ≡ 0; */
+ {
+ int __e_acsl_offset_2;
+ __e_acsl_offset_2 = __offset((void *)ps);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_2 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(ps) == 0",14);
+ }
+ /*@ assert \offset(ps+1) ≡ 2; */
+ {
+ int __e_acsl_offset_3;
+ __e_acsl_offset_3 = __offset((void *)(ps + 1));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_3 == (unsigned long)2,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(ps+1) == 2",15);
+ }
+ /*@ assert \offset(ps+2) ≡ 4; */
+ {
+ int __e_acsl_offset_4;
+ __e_acsl_offset_4 = __offset((void *)(ps + 2));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_4 == (unsigned long)4,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(ps+2) == 4",16);
+ }
+ __full_init((void *)(& pi));
+ pi = ilist;
+ /*@ assert \offset(pi) ≡ 0; */
+ {
+ int __e_acsl_offset_5;
+ __e_acsl_offset_5 = __offset((void *)pi);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_5 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi) == 0",20);
+ }
+ /*@ assert \offset(pi+1) ≡ 4; */
+ {
+ int __e_acsl_offset_6;
+ __e_acsl_offset_6 = __offset((void *)(pi + 1));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_6 == (unsigned long)4,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi+1) == 4",21);
+ }
+ /*@ assert \offset(pi+2) ≡ 8; */
+ {
+ int __e_acsl_offset_7;
+ __e_acsl_offset_7 = __offset((void *)(pi + 2));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_7 == (unsigned long)8,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi+2) == 8",22);
+ }
+ __full_init((void *)(& p));
+ p = (long *)__e_acsl_malloc(sizeof(long) * (unsigned long)12);
+ /*@ assert \offset(p) ≡ 0; */
+ {
+ int __e_acsl_offset_8;
+ __e_acsl_offset_8 = __offset((void *)p);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_8 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p) == 0",26);
+ }
+ /*@ assert \offset(p+1) ≡ 8; */
+ {
+ int __e_acsl_offset_9;
+ __e_acsl_offset_9 = __offset((void *)(p + 1));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_9 == (unsigned long)8,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p+1) == 8",27);
+ }
+ /*@ assert \offset(p+2) ≡ 16; */
+ {
+ int __e_acsl_offset_10;
+ __e_acsl_offset_10 = __offset((void *)(p + 2));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_10 == (unsigned long)16,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p+2) == 16",28);
+ }
+ __retres = 0;
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& pi));
+ __delete_block((void *)(ilist));
+ __delete_block((void *)(& ps));
+ __delete_block((void *)(slist));
+ __delete_block((void *)(& c));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..843ddc6ecd98085e71b63586cba0c3c2774d8af0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
@@ -0,0 +1,60 @@
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `realloc':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/initialized.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/initialized.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/initialized.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:215:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:215:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:208:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:222:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/initialized.c:45:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:49:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:201:[value] warning: function __e_acsl_realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:216:[value] warning: function __e_acsl_realloc, behavior dealloc: precondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:211:[value] warning: function __e_acsl_realloc, behavior alloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:218:[value] warning: function __e_acsl_realloc, behavior dealloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:219:[value] warning: function __e_acsl_realloc, behavior dealloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:226:[value] warning: function __e_acsl_realloc, behavior fail: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/initialized.c:54:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:56:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:178:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
+FRAMAC_SHARE/libc/stdlib.h:177:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
+tests/e-acsl-runtime/initialized.c:64:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:65:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2a96bccb2378ab8a4b70d8911e0928dbfee9d2f0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle
@@ -0,0 +1,21 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/offset.c:7:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/offset.c:7:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/offset.c:7:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/offset.c:26:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/offset.c:27:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:28:[value] warning: assertion got status unknown.