diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/base_addr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/base_addr.c
new file mode 100644
index 0000000000000000000000000000000000000000..cd0a17aa618ce73afe4939baaa8ecb66ac70f259
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/base_addr.c
@@ -0,0 +1,62 @@
+/* run.config
+ COMMENT: Behaviours of the \base_addr E-ACSL predicate
+*/
+
+#include <stdlib.h>
+
+int A[] = { 1, 2, 3, 4};
+int *PA;
+
+int main(void) {
+ /* Global memory */
+ PA = (int*)&A;
+ /*@ assert \base_addr(A) == \base_addr(PA); */
+ /*@ assert \base_addr(A+3) == \base_addr(PA); */
+ PA++;
+ /*@ assert \base_addr(PA) == \base_addr(A); */
+ /*@ assert \base_addr(PA+2) == \base_addr(A+3); */
+
+ /* Stack memory [long blocks] */
+ int a[] = { 1, 2, 3, 4 };
+ int *pa;
+ pa = (int*)&a;
+
+ /*@ assert \base_addr(a) == \base_addr(pa); */
+ /*@ assert \base_addr(a+3) == \base_addr(pa); */
+ pa++;
+ /*@ assert \base_addr(pa) == \base_addr(a); */
+ /*@ assert \base_addr(pa+2) == \base_addr(a); */
+
+ /* Stack memory [Short blocks] */
+ long l = 4;
+ char *pl = (char*)&l;
+ /*@ assert \base_addr(&l) == \base_addr(pl); */
+ /*@ assert \base_addr(pl+2) == \base_addr(&l); */
+ short *pi = (short*)&l;
+ pi++;
+ pl++;
+ /*@ assert \base_addr(pi) == \base_addr(pl); */
+ /*@ assert \base_addr(pl) == \base_addr(&l); */
+
+ /* Heap memory [single segment] */
+ char *p = malloc(12);
+ char *pd = p;
+ /*@ assert \base_addr(p) == \base_addr(pd); */
+ /*@ assert \base_addr(p+1) == \base_addr(pd+5); */
+ /*@ assert \base_addr(p+11) == \base_addr(pd+1); */
+ p += 5;
+ /*@ assert \base_addr(p+5) == \base_addr(p-5); */
+ /*@ assert \base_addr(p-5) == \base_addr(p+5); */
+
+ /* Heap memory [multiple segments] */
+ long *q = malloc(30*sizeof(long));
+ long *qd = q;
+
+ /*@ assert \base_addr(q) == \base_addr(qd); */
+ q++;
+ /*@ assert \base_addr(q) == \base_addr(qd); */
+ q += 2;
+ /*@ assert \base_addr(q) == \base_addr(qd); */
+ q += 4;
+ /*@ assert \base_addr(q) == \base_addr(qd); */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c b/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c
index 0ef49fb786d9e4a0805fb6eba5b24222af95f808..acc4f10d625524a00f313bbaee6cb69fde8561ec 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/offset.c
@@ -4,27 +4,53 @@
#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;
-}
+int A[] = { 1, 2, 3, 4};
+int *PA;
+
+int main(void) {
+ /* Global memory */
+ PA = (int*)&A;
+ /*@ assert \offset(A) == 0; */
+ /*@ assert \offset(A+3) == 12; */
+ /*@ assert \offset(PA) == 0; */
+ PA++;
+ /*@ assert \offset(PA+1) == 8; */
+
+ /* Stack memory [long blocks] */
+ int a[] = { 1, 2, 3, 4};
+ /*@ assert \offset(a) == 0; */
+ /*@ assert \offset(a+1) == 4; */
+ /*@ assert \offset(a+3) == 12; */
+
+ /* Stack memory [Short blocks] */
+ long l = 4;
+ char *pl = (char*)&l;
+ /*@ assert \offset(&l) == 0; */
+ /*@ assert \offset(pl) == 0; */
+ /*@ assert \offset(pl+1) == 1; */
+ /*@ assert \offset(pl+7) == 7; */
+ int *pi = (int*)&l;
+ /*@ assert \offset(pi) == 0; */
+ pi++;
+ /*@ assert \offset(pi) == 4; */
+
+ /* Heap memory [single segment] */
+ char *p = malloc(12);
+ /*@ assert \offset(p) == 0; */
+ /*@ assert \offset(p+1) == 1; */
+ /*@ assert \offset(p+11) == 11; */
+ p += 5;
+ /*@ assert \offset(p+5) == 10; */
+ /*@ assert \offset(p-5) == 0; */
+
+ /* Heap memory [multiple segments] */
+ long *q = malloc(30*sizeof(long));
+
+ /*@ assert \offset(q) == 0; */
+ q++;
+ /*@ assert \offset(q) == 8; */
+ q += 2;
+ /*@ assert \offset(q) == 24; */
+ q += 4;
+ /*@ assert \offset(q) == 56; */
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2879f19b5f84717a4e15786946db32e32c141c46
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle
@@ -0,0 +1,27 @@
+[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/base_addr.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/base_addr.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.
+[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/base_addr.c:44:[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/base_addr.c:45:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:46:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:48:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:49:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:55:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:57:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:59:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/base_addr.c:61:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
new file mode 100644
index 0000000000000000000000000000000000000000..c4ba017ba98805d0057d37c13e21e48428057c99
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
@@ -0,0 +1,302 @@
+/* Generated by Frama-C */
+int A[4] = {1, 2, 3, 4};
+int *PA;
+void __e_acsl_globals_init(void)
+{
+ __store_block((void *)(& PA),8UL);
+ __full_init((void *)(& PA));
+ __store_block((void *)(A),16UL);
+ __full_init((void *)(& A));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int a[4];
+ int *pa;
+ long l;
+ char *pl;
+ short *pi;
+ char *p;
+ char *pd;
+ long *q;
+ long *qd;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_globals_init();
+ __store_block((void *)(& qd),8UL);
+ __store_block((void *)(& q),8UL);
+ __store_block((void *)(& pd),8UL);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& pi),8UL);
+ __store_block((void *)(& pl),8UL);
+ __store_block((void *)(& l),8UL);
+ __store_block((void *)(& pa),8UL);
+ __store_block((void *)(a),16UL);
+ PA = (int *)(& A);
+ /*@ assert \base_addr((int *)A) ≡ \base_addr(PA); */
+ {
+ void *__e_acsl_base_addr;
+ void *__e_acsl_base_addr_2;
+ __e_acsl_base_addr = __base_addr((void *)(A));
+ __e_acsl_base_addr_2 = __base_addr((void *)PA);
+ __e_acsl_assert(__e_acsl_base_addr == __e_acsl_base_addr_2,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr((int *)A) == \\base_addr(PA)",13);
+ }
+ /*@ assert \base_addr(&A[3]) ≡ \base_addr(PA); */
+ {
+ void *__e_acsl_base_addr_3;
+ void *__e_acsl_base_addr_4;
+ __e_acsl_base_addr_3 = __base_addr((void *)(& A[3]));
+ __e_acsl_base_addr_4 = __base_addr((void *)PA);
+ __e_acsl_assert(__e_acsl_base_addr_3 == __e_acsl_base_addr_4,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(&A[3]) == \\base_addr(PA)",14);
+ }
+ PA ++;
+ /*@ assert \base_addr(PA) ≡ \base_addr((int *)A); */
+ {
+ void *__e_acsl_base_addr_5;
+ void *__e_acsl_base_addr_6;
+ __e_acsl_base_addr_5 = __base_addr((void *)PA);
+ __e_acsl_base_addr_6 = __base_addr((void *)(A));
+ __e_acsl_assert(__e_acsl_base_addr_5 == __e_acsl_base_addr_6,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(PA) == \\base_addr((int *)A)",16);
+ }
+ /*@ assert \base_addr(PA+2) ≡ \base_addr(&A[3]); */
+ {
+ void *__e_acsl_base_addr_7;
+ void *__e_acsl_base_addr_8;
+ __e_acsl_base_addr_7 = __base_addr((void *)(PA + 2));
+ __e_acsl_base_addr_8 = __base_addr((void *)(& A[3]));
+ __e_acsl_assert(__e_acsl_base_addr_7 == __e_acsl_base_addr_8,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(PA+2) == \\base_addr(&A[3])",17);
+ }
+ __initialize((void *)(a),sizeof(int));
+ a[0] = 1;
+ __initialize((void *)(& a[1]),sizeof(int));
+ a[1] = 2;
+ __initialize((void *)(& a[2]),sizeof(int));
+ a[2] = 3;
+ __initialize((void *)(& a[3]),sizeof(int));
+ a[3] = 4;
+ __full_init((void *)(& pa));
+ pa = (int *)(& a);
+ /*@ assert \base_addr((int *)a) ≡ \base_addr(pa); */
+ {
+ void *__e_acsl_base_addr_9;
+ void *__e_acsl_base_addr_10;
+ __e_acsl_base_addr_9 = __base_addr((void *)(a));
+ __e_acsl_base_addr_10 = __base_addr((void *)pa);
+ __e_acsl_assert(__e_acsl_base_addr_9 == __e_acsl_base_addr_10,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr((int *)a) == \\base_addr(pa)",24);
+ }
+ /*@ assert \base_addr(&a[3]) ≡ \base_addr(pa); */
+ {
+ void *__e_acsl_base_addr_11;
+ void *__e_acsl_base_addr_12;
+ __e_acsl_base_addr_11 = __base_addr((void *)(& a[3]));
+ __e_acsl_base_addr_12 = __base_addr((void *)pa);
+ __e_acsl_assert(__e_acsl_base_addr_11 == __e_acsl_base_addr_12,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(&a[3]) == \\base_addr(pa)",25);
+ }
+ __full_init((void *)(& pa));
+ pa ++;
+ /*@ assert \base_addr(pa) ≡ \base_addr((int *)a); */
+ {
+ void *__e_acsl_base_addr_13;
+ void *__e_acsl_base_addr_14;
+ __e_acsl_base_addr_13 = __base_addr((void *)pa);
+ __e_acsl_base_addr_14 = __base_addr((void *)(a));
+ __e_acsl_assert(__e_acsl_base_addr_13 == __e_acsl_base_addr_14,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(pa) == \\base_addr((int *)a)",27);
+ }
+ /*@ assert \base_addr(pa+2) ≡ \base_addr((int *)a); */
+ {
+ void *__e_acsl_base_addr_15;
+ void *__e_acsl_base_addr_16;
+ __e_acsl_base_addr_15 = __base_addr((void *)(pa + 2));
+ __e_acsl_base_addr_16 = __base_addr((void *)(a));
+ __e_acsl_assert(__e_acsl_base_addr_15 == __e_acsl_base_addr_16,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(pa+2) == \\base_addr((int *)a)",28);
+ }
+ __full_init((void *)(& l));
+ l = (long)4;
+ __full_init((void *)(& pl));
+ pl = (char *)(& l);
+ /*@ assert \base_addr(&l) ≡ \base_addr(pl); */
+ {
+ void *__e_acsl_base_addr_17;
+ void *__e_acsl_base_addr_18;
+ __e_acsl_base_addr_17 = __base_addr((void *)(& l));
+ __e_acsl_base_addr_18 = __base_addr((void *)pl);
+ __e_acsl_assert(__e_acsl_base_addr_17 == __e_acsl_base_addr_18,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(&l) == \\base_addr(pl)",33);
+ }
+ /*@ assert \base_addr(pl+2) ≡ \base_addr(&l); */
+ {
+ void *__e_acsl_base_addr_19;
+ void *__e_acsl_base_addr_20;
+ __e_acsl_base_addr_19 = __base_addr((void *)(pl + 2));
+ __e_acsl_base_addr_20 = __base_addr((void *)(& l));
+ __e_acsl_assert(__e_acsl_base_addr_19 == __e_acsl_base_addr_20,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(pl+2) == \\base_addr(&l)",34);
+ }
+ __full_init((void *)(& pi));
+ pi = (short *)(& l);
+ __full_init((void *)(& pi));
+ pi ++;
+ __full_init((void *)(& pl));
+ pl ++;
+ /*@ assert \base_addr(pi) ≡ \base_addr(pl); */
+ {
+ void *__e_acsl_base_addr_21;
+ void *__e_acsl_base_addr_22;
+ __e_acsl_base_addr_21 = __base_addr((void *)pi);
+ __e_acsl_base_addr_22 = __base_addr((void *)pl);
+ __e_acsl_assert(__e_acsl_base_addr_21 == __e_acsl_base_addr_22,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(pi) == \\base_addr(pl)",38);
+ }
+ /*@ assert \base_addr(pl) ≡ \base_addr(&l); */
+ {
+ void *__e_acsl_base_addr_23;
+ void *__e_acsl_base_addr_24;
+ __e_acsl_base_addr_23 = __base_addr((void *)pl);
+ __e_acsl_base_addr_24 = __base_addr((void *)(& l));
+ __e_acsl_assert(__e_acsl_base_addr_23 == __e_acsl_base_addr_24,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(pl) == \\base_addr(&l)",39);
+ }
+ __full_init((void *)(& p));
+ p = (char *)__e_acsl_malloc((unsigned long)12);
+ __full_init((void *)(& pd));
+ pd = p;
+ /*@ assert \base_addr(p) ≡ \base_addr(pd); */
+ {
+ void *__e_acsl_base_addr_25;
+ void *__e_acsl_base_addr_26;
+ __e_acsl_base_addr_25 = __base_addr((void *)p);
+ __e_acsl_base_addr_26 = __base_addr((void *)pd);
+ __e_acsl_assert(__e_acsl_base_addr_25 == __e_acsl_base_addr_26,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(p) == \\base_addr(pd)",44);
+ }
+ /*@ assert \base_addr(p+1) ≡ \base_addr(pd+5); */
+ {
+ void *__e_acsl_base_addr_27;
+ void *__e_acsl_base_addr_28;
+ __e_acsl_base_addr_27 = __base_addr((void *)(p + 1));
+ __e_acsl_base_addr_28 = __base_addr((void *)(pd + 5));
+ __e_acsl_assert(__e_acsl_base_addr_27 == __e_acsl_base_addr_28,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(p+1) == \\base_addr(pd+5)",45);
+ }
+ /*@ assert \base_addr(p+11) ≡ \base_addr(pd+1); */
+ {
+ void *__e_acsl_base_addr_29;
+ void *__e_acsl_base_addr_30;
+ __e_acsl_base_addr_29 = __base_addr((void *)(p + 11));
+ __e_acsl_base_addr_30 = __base_addr((void *)(pd + 1));
+ __e_acsl_assert(__e_acsl_base_addr_29 == __e_acsl_base_addr_30,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(p+11) == \\base_addr(pd+1)",46);
+ }
+ __full_init((void *)(& p));
+ p += 5;
+ /*@ assert \base_addr(p+5) ≡ \base_addr(p-5); */
+ {
+ void *__e_acsl_base_addr_31;
+ void *__e_acsl_base_addr_32;
+ __e_acsl_base_addr_31 = __base_addr((void *)(p + 5));
+ __e_acsl_base_addr_32 = __base_addr((void *)(p - 5));
+ __e_acsl_assert(__e_acsl_base_addr_31 == __e_acsl_base_addr_32,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(p+5) == \\base_addr(p-5)",48);
+ }
+ /*@ assert \base_addr(p-5) ≡ \base_addr(p+5); */
+ {
+ void *__e_acsl_base_addr_33;
+ void *__e_acsl_base_addr_34;
+ __e_acsl_base_addr_33 = __base_addr((void *)(p - 5));
+ __e_acsl_base_addr_34 = __base_addr((void *)(p + 5));
+ __e_acsl_assert(__e_acsl_base_addr_33 == __e_acsl_base_addr_34,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(p-5) == \\base_addr(p+5)",49);
+ }
+ __full_init((void *)(& q));
+ q = (long *)__e_acsl_malloc((unsigned long)30 * sizeof(long));
+ __full_init((void *)(& qd));
+ qd = q;
+ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ {
+ void *__e_acsl_base_addr_35;
+ void *__e_acsl_base_addr_36;
+ __e_acsl_base_addr_35 = __base_addr((void *)q);
+ __e_acsl_base_addr_36 = __base_addr((void *)qd);
+ __e_acsl_assert(__e_acsl_base_addr_35 == __e_acsl_base_addr_36,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(q) == \\base_addr(qd)",55);
+ }
+ __full_init((void *)(& q));
+ q ++;
+ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ {
+ void *__e_acsl_base_addr_37;
+ void *__e_acsl_base_addr_38;
+ __e_acsl_base_addr_37 = __base_addr((void *)q);
+ __e_acsl_base_addr_38 = __base_addr((void *)qd);
+ __e_acsl_assert(__e_acsl_base_addr_37 == __e_acsl_base_addr_38,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(q) == \\base_addr(qd)",57);
+ }
+ __full_init((void *)(& q));
+ q += 2;
+ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ {
+ void *__e_acsl_base_addr_39;
+ void *__e_acsl_base_addr_40;
+ __e_acsl_base_addr_39 = __base_addr((void *)q);
+ __e_acsl_base_addr_40 = __base_addr((void *)qd);
+ __e_acsl_assert(__e_acsl_base_addr_39 == __e_acsl_base_addr_40,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(q) == \\base_addr(qd)",59);
+ }
+ __full_init((void *)(& q));
+ q += 4;
+ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ {
+ void *__e_acsl_base_addr_41;
+ void *__e_acsl_base_addr_42;
+ __e_acsl_base_addr_41 = __base_addr((void *)q);
+ __e_acsl_base_addr_42 = __base_addr((void *)qd);
+ __e_acsl_assert(__e_acsl_base_addr_41 == __e_acsl_base_addr_42,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(q) == \\base_addr(qd)",61);
+ }
+ __retres = 0;
+ __delete_block((void *)(& PA));
+ __delete_block((void *)(A));
+ __delete_block((void *)(& qd));
+ __delete_block((void *)(& q));
+ __delete_block((void *)(& pd));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& pi));
+ __delete_block((void *)(& pl));
+ __delete_block((void *)(& l));
+ __delete_block((void *)(& pa));
+ __delete_block((void *)(a));
+ __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
index 3129aa3b85b7b2f6a32143ecd78edfa12c4e1b5a..76d2d7cdd2edf8e7a25f41fde8eca03a1cba64a0 100644
--- 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
@@ -1,113 +1,247 @@
/* Generated by Frama-C */
+int A[4] = {1, 2, 3, 4};
+int *PA;
+void __e_acsl_globals_init(void)
+{
+ __store_block((void *)(& PA),8UL);
+ __full_init((void *)(& PA));
+ __store_block((void *)(A),16UL);
+ __full_init((void *)(& A));
+ return;
+}
+
int main(void)
{
int __retres;
- char c;
- short slist[3];
- short *ps;
- int ilist[3];
+ int a[4];
+ long l;
+ char *pl;
int *pi;
- long *p;
+ char *p;
+ long *q;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_globals_init();
+ __store_block((void *)(& q),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; */
+ __store_block((void *)(& pl),8UL);
+ __store_block((void *)(& l),8UL);
+ __store_block((void *)(a),16UL);
+ PA = (int *)(& A);
+ /*@ assert \offset((int *)A) ≡ 0; */
{
int __e_acsl_offset;
- __e_acsl_offset = __offset((void *)(& c));
+ __e_acsl_offset = __offset((void *)(A));
__e_acsl_assert((unsigned long)__e_acsl_offset == (unsigned long)0,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(&c) == 0",10);
+ (char *)"\\offset((int *)A) == 0",13);
}
- __full_init((void *)(& ps));
- ps = slist;
- /*@ assert \offset(ps) ≡ 0; */
+ /*@ assert \offset(&A[3]) ≡ 12; */
{
int __e_acsl_offset_2;
- __e_acsl_offset_2 = __offset((void *)ps);
- __e_acsl_assert((unsigned long)__e_acsl_offset_2 == (unsigned long)0,
+ __e_acsl_offset_2 = __offset((void *)(& A[3]));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_2 == (unsigned long)12,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(ps) == 0",14);
+ (char *)"\\offset(&A[3]) == 12",14);
}
- /*@ assert \offset(ps+1) ≡ 2; */
+ /*@ assert \offset(PA) ≡ 0; */
{
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,
+ __e_acsl_offset_3 = __offset((void *)PA);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_3 == (unsigned long)0,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(ps+1) == 2",15);
+ (char *)"\\offset(PA) == 0",15);
}
- /*@ assert \offset(ps+2) ≡ 4; */
+ PA ++;
+ /*@ assert \offset(PA+1) ≡ 8; */
{
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,
+ __e_acsl_offset_4 = __offset((void *)(PA + 1));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_4 == (unsigned long)8,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(ps+2) == 4",16);
+ (char *)"\\offset(PA+1) == 8",17);
}
- __full_init((void *)(& pi));
- pi = ilist;
- /*@ assert \offset(pi) ≡ 0; */
+ __initialize((void *)(a),sizeof(int));
+ a[0] = 1;
+ __initialize((void *)(& a[1]),sizeof(int));
+ a[1] = 2;
+ __initialize((void *)(& a[2]),sizeof(int));
+ a[2] = 3;
+ __initialize((void *)(& a[3]),sizeof(int));
+ a[3] = 4;
+ /*@ assert \offset((int *)a) ≡ 0; */
{
int __e_acsl_offset_5;
- __e_acsl_offset_5 = __offset((void *)pi);
+ __e_acsl_offset_5 = __offset((void *)(a));
__e_acsl_assert((unsigned long)__e_acsl_offset_5 == (unsigned long)0,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(pi) == 0",20);
+ (char *)"\\offset((int *)a) == 0",21);
}
- /*@ assert \offset(pi+1) ≡ 4; */
+ /*@ assert \offset(&a[1]) ≡ 4; */
{
int __e_acsl_offset_6;
- __e_acsl_offset_6 = __offset((void *)(pi + 1));
+ __e_acsl_offset_6 = __offset((void *)(& a[1]));
__e_acsl_assert((unsigned long)__e_acsl_offset_6 == (unsigned long)4,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(pi+1) == 4",21);
+ (char *)"\\offset(&a[1]) == 4",22);
}
- /*@ assert \offset(pi+2) ≡ 8; */
+ /*@ assert \offset(&a[3]) ≡ 12; */
{
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,
+ __e_acsl_offset_7 = __offset((void *)(& a[3]));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_7 == (unsigned long)12,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(pi+2) == 8",22);
+ (char *)"\\offset(&a[3]) == 12",23);
}
- __full_init((void *)(& p));
- p = (long *)__e_acsl_malloc(sizeof(long) * (unsigned long)12);
- /*@ assert \offset(p) ≡ 0; */
+ __full_init((void *)(& l));
+ l = (long)4;
+ __full_init((void *)(& pl));
+ pl = (char *)(& l);
+ /*@ assert \offset(&l) ≡ 0; */
{
int __e_acsl_offset_8;
- __e_acsl_offset_8 = __offset((void *)p);
+ __e_acsl_offset_8 = __offset((void *)(& l));
__e_acsl_assert((unsigned long)__e_acsl_offset_8 == (unsigned long)0,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(p) == 0",26);
+ (char *)"\\offset(&l) == 0",28);
}
- /*@ assert \offset(p+1) ≡ 8; */
+ /*@ assert \offset(pl) ≡ 0; */
{
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,
+ __e_acsl_offset_9 = __offset((void *)pl);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_9 == (unsigned long)0,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(p+1) == 8",27);
+ (char *)"\\offset(pl) == 0",29);
}
- /*@ assert \offset(p+2) ≡ 16; */
+ /*@ assert \offset(pl+1) ≡ 1; */
{
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,
+ __e_acsl_offset_10 = __offset((void *)(pl + 1));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_10 == (unsigned long)1,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pl+1) == 1",30);
+ }
+ /*@ assert \offset(pl+7) ≡ 7; */
+ {
+ int __e_acsl_offset_11;
+ __e_acsl_offset_11 = __offset((void *)(pl + 7));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_11 == (unsigned long)7,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pl+7) == 7",31);
+ }
+ __full_init((void *)(& pi));
+ pi = (int *)(& l);
+ /*@ assert \offset(pi) ≡ 0; */
+ {
+ int __e_acsl_offset_12;
+ __e_acsl_offset_12 = __offset((void *)pi);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_12 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi) == 0",33);
+ }
+ __full_init((void *)(& pi));
+ pi ++;
+ /*@ assert \offset(pi) ≡ 4; */
+ {
+ int __e_acsl_offset_13;
+ __e_acsl_offset_13 = __offset((void *)pi);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_13 == (unsigned long)4,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(pi) == 4",35);
+ }
+ __full_init((void *)(& p));
+ p = (char *)__e_acsl_malloc((unsigned long)12);
+ /*@ assert \offset(p) ≡ 0; */
+ {
+ int __e_acsl_offset_14;
+ __e_acsl_offset_14 = __offset((void *)p);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_14 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p) == 0",39);
+ }
+ /*@ assert \offset(p+1) ≡ 1; */
+ {
+ int __e_acsl_offset_15;
+ __e_acsl_offset_15 = __offset((void *)(p + 1));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_15 == (unsigned long)1,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p+1) == 1",40);
+ }
+ /*@ assert \offset(p+11) ≡ 11; */
+ {
+ int __e_acsl_offset_16;
+ __e_acsl_offset_16 = __offset((void *)(p + 11));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_16 == (unsigned long)11,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p+11) == 11",41);
+ }
+ __full_init((void *)(& p));
+ p += 5;
+ /*@ assert \offset(p+5) ≡ 10; */
+ {
+ int __e_acsl_offset_17;
+ __e_acsl_offset_17 = __offset((void *)(p + 5));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_17 == (unsigned long)10,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p+5) == 10",43);
+ }
+ /*@ assert \offset(p-5) ≡ 0; */
+ {
+ int __e_acsl_offset_18;
+ __e_acsl_offset_18 = __offset((void *)(p - 5));
+ __e_acsl_assert((unsigned long)__e_acsl_offset_18 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(p-5) == 0",44);
+ }
+ __full_init((void *)(& q));
+ q = (long *)__e_acsl_malloc((unsigned long)30 * sizeof(long));
+ /*@ assert \offset(q) ≡ 0; */
+ {
+ int __e_acsl_offset_19;
+ __e_acsl_offset_19 = __offset((void *)q);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_19 == (unsigned long)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(q) == 0",49);
+ }
+ __full_init((void *)(& q));
+ q ++;
+ /*@ assert \offset(q) ≡ 8; */
+ {
+ int __e_acsl_offset_20;
+ __e_acsl_offset_20 = __offset((void *)q);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_20 == (unsigned long)8,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(q) == 8",51);
+ }
+ __full_init((void *)(& q));
+ q += 2;
+ /*@ assert \offset(q) ≡ 24; */
+ {
+ int __e_acsl_offset_21;
+ __e_acsl_offset_21 = __offset((void *)q);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_21 == (unsigned long)24,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\offset(q) == 24",53);
+ }
+ __full_init((void *)(& q));
+ q += 4;
+ /*@ assert \offset(q) ≡ 56; */
+ {
+ int __e_acsl_offset_22;
+ __e_acsl_offset_22 = __offset((void *)q);
+ __e_acsl_assert((unsigned long)__e_acsl_offset_22 == (unsigned long)56,
(char *)"Assertion",(char *)"main",
- (char *)"\\offset(p+2) == 16",28);
+ (char *)"\\offset(q) == 56",55);
}
__retres = 0;
+ __delete_block((void *)(& PA));
+ __delete_block((void *)(A));
+ __delete_block((void *)(& q));
__delete_block((void *)(& p));
__delete_block((void *)(& pi));
- __delete_block((void *)(ilist));
- __delete_block((void *)(& ps));
- __delete_block((void *)(slist));
- __delete_block((void *)(& c));
+ __delete_block((void *)(& pl));
+ __delete_block((void *)(& l));
+ __delete_block((void *)(a));
__e_acsl_memory_clean();
return __retres;
}
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
index 2a96bccb2378ab8a4b70d8911e0928dbfee9d2f0..b74c3bd68abfc70ceed37a1cd713666cb96a62ea 100644
--- 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
@@ -1,10 +1,10 @@
[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.
+tests/e-acsl-runtime/offset.c:10:[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.
+tests/e-acsl-runtime/offset.c:10:[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.
+tests/e-acsl-runtime/offset.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.
@@ -15,7 +15,13 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
[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.
+tests/e-acsl-runtime/offset.c:39:[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.
+tests/e-acsl-runtime/offset.c:40:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:41:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:43:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:44:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:49:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:51:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:53:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:55:[value] warning: assertion got status unknown.