From 2ee422c3cdfd3a39fa87f217296326d1c46d5655 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 6 Dec 2017 09:04:16 +0100
Subject: [PATCH] [tests] improved tests for base_addr
---
src/plugins/e-acsl/tests/runtime/base_addr.c | 2 +
.../tests/runtime/oracle/base_addr.res.oracle | 10 +-
.../tests/runtime/oracle/gen_base_addr.c | 244 ++++++++++--------
3 files changed, 139 insertions(+), 117 deletions(-)
diff --git a/src/plugins/e-acsl/tests/runtime/base_addr.c b/src/plugins/e-acsl/tests/runtime/base_addr.c
index c4f54ceddae..ad6c77d4a2e 100644
--- a/src/plugins/e-acsl/tests/runtime/base_addr.c
+++ b/src/plugins/e-acsl/tests/runtime/base_addr.c
@@ -10,6 +10,7 @@ int *PA;
int main(void) {
/* Global memory */
PA = (int*)&A;
+ /*@ assert \base_addr(&A[0]) == \base_addr(&A); */
/*@ assert \base_addr(&A[0]) == \base_addr(PA); */
/*@ assert \base_addr(A+3) == \base_addr(PA); */
PA++;
@@ -21,6 +22,7 @@ int main(void) {
int *pa;
pa = (int*)&a;
+ /*@ assert \base_addr(&a[0]) == \base_addr(&a); */
/*@ assert \base_addr(&a[0]) == \base_addr(pa); */
/*@ assert \base_addr(a+3) == \base_addr(pa); */
pa++;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
index 6bc437e615c..5b338e13b22 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
@@ -1,12 +1,12 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-tests/runtime/base_addr.c:44:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/base_addr.c:45:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:46:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/runtime/base_addr.c:47:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:48:[value] warning: assertion got status unknown.
-tests/runtime/base_addr.c:49:[value] warning: assertion got status unknown.
-tests/runtime/base_addr.c:55:[value] warning: assertion got status unknown.
+tests/runtime/base_addr.c:50:[value] warning: assertion got status unknown.
+tests/runtime/base_addr.c:51:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:57:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:59:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:61:[value] warning: assertion got status unknown.
+tests/runtime/base_addr.c:63:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
index d616deab77b..253dc7142cf 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
@@ -19,236 +19,232 @@ int main(void)
__e_acsl_globals_init();
__e_acsl_store_block((void *)(& pa),(size_t)8);
PA = (int *)(& A);
- /*@ assert \base_addr((int *)A) ≡ \base_addr(PA); */
+ /*@ assert \base_addr((int *)A) ≡ \base_addr(&A); */
{
void *__gen_e_acsl_base_addr;
void *__gen_e_acsl_base_addr_2;
__gen_e_acsl_base_addr = __e_acsl_base_addr((void *)(A));
- __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)PA);
+ __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)(& A));
__e_acsl_assert(__gen_e_acsl_base_addr == __gen_e_acsl_base_addr_2,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr((int *)A) == \\base_addr(PA)",13);
+ (char *)"\\base_addr((int *)A) == \\base_addr(&A)",13);
}
- /*@ assert \base_addr(&A[3]) ≡ \base_addr(PA); */
+ /*@ assert \base_addr((int *)A) ≡ \base_addr(PA); */
{
void *__gen_e_acsl_base_addr_3;
void *__gen_e_acsl_base_addr_4;
- __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(A));
__gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)PA);
__e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(&A[3]) == \\base_addr(PA)",14);
+ (char *)"\\base_addr((int *)A) == \\base_addr(PA)",14);
}
- PA ++;
- /*@ assert \base_addr(PA) ≡ \base_addr((int *)A); */
+ /*@ assert \base_addr(&A[3]) ≡ \base_addr(PA); */
{
void *__gen_e_acsl_base_addr_5;
void *__gen_e_acsl_base_addr_6;
- __gen_e_acsl_base_addr_5 = __e_acsl_base_addr((void *)PA);
- __gen_e_acsl_base_addr_6 = __e_acsl_base_addr((void *)(A));
+ __gen_e_acsl_base_addr_5 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_6 = __e_acsl_base_addr((void *)PA);
__e_acsl_assert(__gen_e_acsl_base_addr_5 == __gen_e_acsl_base_addr_6,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(PA) == \\base_addr((int *)A)",16);
+ (char *)"\\base_addr(&A[3]) == \\base_addr(PA)",15);
}
- /*@ assert \base_addr(PA + 2) ≡ \base_addr(&A[3]); */
+ PA ++;
+ /*@ assert \base_addr(PA) ≡ \base_addr((int *)A); */
{
void *__gen_e_acsl_base_addr_7;
void *__gen_e_acsl_base_addr_8;
- __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2));
- __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)PA);
+ __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(A));
__e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(PA + 2) == \\base_addr(&A[3])",17);
+ (char *)"\\base_addr(PA) == \\base_addr((int *)A)",17);
}
- int a[4] = {1, 2, 3, 4};
- __e_acsl_store_block((void *)(a),(size_t)16);
- __e_acsl_full_init((void *)(& a));
- __e_acsl_full_init((void *)(& pa));
- pa = (int *)(& a);
- /*@ assert \base_addr((int *)a) ≡ \base_addr(pa); */
+ /*@ assert \base_addr(PA + 2) ≡ \base_addr(&A[3]); */
{
void *__gen_e_acsl_base_addr_9;
void *__gen_e_acsl_base_addr_10;
- __gen_e_acsl_base_addr_9 = __e_acsl_base_addr((void *)(a));
- __gen_e_acsl_base_addr_10 = __e_acsl_base_addr((void *)pa);
+ __gen_e_acsl_base_addr_9 = __e_acsl_base_addr((void *)(PA + 2));
+ __gen_e_acsl_base_addr_10 = __e_acsl_base_addr((void *)(& A[3]));
__e_acsl_assert(__gen_e_acsl_base_addr_9 == __gen_e_acsl_base_addr_10,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr((int *)a) == \\base_addr(pa)",24);
+ (char *)"\\base_addr(PA + 2) == \\base_addr(&A[3])",18);
}
- /*@ assert \base_addr(&a[3]) ≡ \base_addr(pa); */
+ int a[4] = {1, 2, 3, 4};
+ __e_acsl_store_block((void *)(a),(size_t)16);
+ __e_acsl_full_init((void *)(& a));
+ __e_acsl_full_init((void *)(& pa));
+ pa = (int *)(& a);
+ /*@ assert \base_addr((int *)a) ≡ \base_addr(&a); */
{
void *__gen_e_acsl_base_addr_11;
void *__gen_e_acsl_base_addr_12;
- __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3]));
- __gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa);
+ __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(a));
+ __gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)(& a));
__e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(&a[3]) == \\base_addr(pa)",25);
+ (char *)"\\base_addr((int *)a) == \\base_addr(&a)",25);
}
- __e_acsl_full_init((void *)(& pa));
- pa ++;
- /*@ assert \base_addr(pa) ≡ \base_addr((int *)a); */
+ /*@ assert \base_addr((int *)a) ≡ \base_addr(pa); */
{
void *__gen_e_acsl_base_addr_13;
void *__gen_e_acsl_base_addr_14;
- __gen_e_acsl_base_addr_13 = __e_acsl_base_addr((void *)pa);
- __gen_e_acsl_base_addr_14 = __e_acsl_base_addr((void *)(a));
+ __gen_e_acsl_base_addr_13 = __e_acsl_base_addr((void *)(a));
+ __gen_e_acsl_base_addr_14 = __e_acsl_base_addr((void *)pa);
__e_acsl_assert(__gen_e_acsl_base_addr_13 == __gen_e_acsl_base_addr_14,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(pa) == \\base_addr((int *)a)",27);
+ (char *)"\\base_addr((int *)a) == \\base_addr(pa)",26);
}
- /*@ assert \base_addr(pa + 2) ≡ \base_addr((int *)a); */
+ /*@ assert \base_addr(&a[3]) ≡ \base_addr(pa); */
{
void *__gen_e_acsl_base_addr_15;
void *__gen_e_acsl_base_addr_16;
- __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2));
- __gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a));
+ __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(& a[3]));
+ __gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)pa);
__e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(pa + 2) == \\base_addr((int *)a)",
- 28);
+ (char *)"\\base_addr(&a[3]) == \\base_addr(pa)",27);
}
- long l = (long)4;
- __e_acsl_store_block((void *)(& l),(size_t)8);
- __e_acsl_full_init((void *)(& l));
- char *pl = (char *)(& l);
- __e_acsl_store_block((void *)(& pl),(size_t)8);
- __e_acsl_full_init((void *)(& pl));
- /*@ assert \base_addr(&l) ≡ \base_addr(pl); */
+ __e_acsl_full_init((void *)(& pa));
+ pa ++;
+ /*@ assert \base_addr(pa) ≡ \base_addr((int *)a); */
{
void *__gen_e_acsl_base_addr_17;
void *__gen_e_acsl_base_addr_18;
- __gen_e_acsl_base_addr_17 = __e_acsl_base_addr((void *)(& l));
- __gen_e_acsl_base_addr_18 = __e_acsl_base_addr((void *)pl);
+ __gen_e_acsl_base_addr_17 = __e_acsl_base_addr((void *)pa);
+ __gen_e_acsl_base_addr_18 = __e_acsl_base_addr((void *)(a));
__e_acsl_assert(__gen_e_acsl_base_addr_17 == __gen_e_acsl_base_addr_18,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(&l) == \\base_addr(pl)",33);
+ (char *)"\\base_addr(pa) == \\base_addr((int *)a)",29);
}
- /*@ assert \base_addr(pl + 2) ≡ \base_addr(&l); */
+ /*@ assert \base_addr(pa + 2) ≡ \base_addr((int *)a); */
{
void *__gen_e_acsl_base_addr_19;
void *__gen_e_acsl_base_addr_20;
- __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2));
- __gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l));
+ __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pa + 2));
+ __gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(a));
__e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(pl + 2) == \\base_addr(&l)",34);
+ (char *)"\\base_addr(pa + 2) == \\base_addr((int *)a)",
+ 30);
}
- short *pi = (short *)(& l);
- __e_acsl_store_block((void *)(& pi),(size_t)8);
- __e_acsl_full_init((void *)(& pi));
- __e_acsl_full_init((void *)(& pi));
- pi ++;
+ long l = (long)4;
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_full_init((void *)(& l));
+ char *pl = (char *)(& l);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
__e_acsl_full_init((void *)(& pl));
- pl ++;
- /*@ assert \base_addr(pi) ≡ \base_addr(pl); */
+ /*@ assert \base_addr(&l) ≡ \base_addr(pl); */
{
void *__gen_e_acsl_base_addr_21;
void *__gen_e_acsl_base_addr_22;
- __gen_e_acsl_base_addr_21 = __e_acsl_base_addr((void *)pi);
+ __gen_e_acsl_base_addr_21 = __e_acsl_base_addr((void *)(& l));
__gen_e_acsl_base_addr_22 = __e_acsl_base_addr((void *)pl);
__e_acsl_assert(__gen_e_acsl_base_addr_21 == __gen_e_acsl_base_addr_22,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(pi) == \\base_addr(pl)",38);
+ (char *)"\\base_addr(&l) == \\base_addr(pl)",35);
}
- /*@ assert \base_addr(pl) ≡ \base_addr(&l); */
+ /*@ assert \base_addr(pl + 2) ≡ \base_addr(&l); */
{
void *__gen_e_acsl_base_addr_23;
void *__gen_e_acsl_base_addr_24;
- __gen_e_acsl_base_addr_23 = __e_acsl_base_addr((void *)pl);
+ __gen_e_acsl_base_addr_23 = __e_acsl_base_addr((void *)(pl + 2));
__gen_e_acsl_base_addr_24 = __e_acsl_base_addr((void *)(& l));
__e_acsl_assert(__gen_e_acsl_base_addr_23 == __gen_e_acsl_base_addr_24,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(pl) == \\base_addr(&l)",39);
+ (char *)"\\base_addr(pl + 2) == \\base_addr(&l)",36);
}
- char *p = malloc((unsigned long)12);
- __e_acsl_store_block((void *)(& p),(size_t)8);
- __e_acsl_full_init((void *)(& p));
- char *pd = p;
- __e_acsl_store_block((void *)(& pd),(size_t)8);
- __e_acsl_full_init((void *)(& pd));
- /*@ assert \base_addr(p) ≡ \base_addr(pd); */
+ short *pi = (short *)(& l);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_full_init((void *)(& pi));
+ __e_acsl_full_init((void *)(& pi));
+ pi ++;
+ __e_acsl_full_init((void *)(& pl));
+ pl ++;
+ /*@ assert \base_addr(pi) ≡ \base_addr(pl); */
{
void *__gen_e_acsl_base_addr_25;
void *__gen_e_acsl_base_addr_26;
- __gen_e_acsl_base_addr_25 = __e_acsl_base_addr((void *)p);
- __gen_e_acsl_base_addr_26 = __e_acsl_base_addr((void *)pd);
+ __gen_e_acsl_base_addr_25 = __e_acsl_base_addr((void *)pi);
+ __gen_e_acsl_base_addr_26 = __e_acsl_base_addr((void *)pl);
__e_acsl_assert(__gen_e_acsl_base_addr_25 == __gen_e_acsl_base_addr_26,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(p) == \\base_addr(pd)",44);
+ (char *)"\\base_addr(pi) == \\base_addr(pl)",40);
}
- /*@ assert \base_addr(p + 1) ≡ \base_addr(pd + 5); */
+ /*@ assert \base_addr(pl) ≡ \base_addr(&l); */
{
void *__gen_e_acsl_base_addr_27;
void *__gen_e_acsl_base_addr_28;
- __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1));
- __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5));
+ __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)pl);
+ __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(& l));
__e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(p + 1) == \\base_addr(pd + 5)",45);
+ (char *)"\\base_addr(pl) == \\base_addr(&l)",41);
}
- /*@ assert \base_addr(p + 11) ≡ \base_addr(pd + 1); */
+ char *p = malloc((unsigned long)12);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_full_init((void *)(& p));
+ char *pd = p;
+ __e_acsl_store_block((void *)(& pd),(size_t)8);
+ __e_acsl_full_init((void *)(& pd));
+ /*@ assert \base_addr(p) ≡ \base_addr(pd); */
{
void *__gen_e_acsl_base_addr_29;
void *__gen_e_acsl_base_addr_30;
- __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11));
- __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1));
+ __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)p);
+ __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(p + 11) == \\base_addr(pd + 1)",46);
+ (char *)"\\base_addr(p) == \\base_addr(pd)",46);
}
- __e_acsl_full_init((void *)(& p));
- p += 5;
- /*@ assert \base_addr(p + 5) ≡ \base_addr(pd); */
+ /*@ assert \base_addr(p + 1) ≡ \base_addr(pd + 5); */
{
void *__gen_e_acsl_base_addr_31;
void *__gen_e_acsl_base_addr_32;
- __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5));
- __gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd);
+ __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 1));
+ __gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)(pd + 5));
__e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(p + 5) == \\base_addr(pd)",48);
+ (char *)"\\base_addr(p + 1) == \\base_addr(pd + 5)",47);
}
- /*@ assert \base_addr(p - 5) ≡ \base_addr(pd); */
+ /*@ assert \base_addr(p + 11) ≡ \base_addr(pd + 1); */
{
void *__gen_e_acsl_base_addr_33;
void *__gen_e_acsl_base_addr_34;
- __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5));
- __gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd);
+ __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p + 11));
+ __gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)(pd + 1));
__e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(p - 5) == \\base_addr(pd)",49);
+ (char *)"\\base_addr(p + 11) == \\base_addr(pd + 1)",48);
}
- long *q = malloc((unsigned long)30 * sizeof(long));
- __e_acsl_store_block((void *)(& q),(size_t)8);
- __e_acsl_full_init((void *)(& q));
- long *qd = q;
- __e_acsl_store_block((void *)(& qd),(size_t)8);
- __e_acsl_full_init((void *)(& qd));
- /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ __e_acsl_full_init((void *)(& p));
+ p += 5;
+ /*@ assert \base_addr(p + 5) ≡ \base_addr(pd); */
{
void *__gen_e_acsl_base_addr_35;
void *__gen_e_acsl_base_addr_36;
- __gen_e_acsl_base_addr_35 = __e_acsl_base_addr((void *)q);
- __gen_e_acsl_base_addr_36 = __e_acsl_base_addr((void *)qd);
+ __gen_e_acsl_base_addr_35 = __e_acsl_base_addr((void *)(p + 5));
+ __gen_e_acsl_base_addr_36 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_35 == __gen_e_acsl_base_addr_36,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(q) == \\base_addr(qd)",55);
+ (char *)"\\base_addr(p + 5) == \\base_addr(pd)",50);
}
- __e_acsl_full_init((void *)(& q));
- q ++;
- /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ /*@ assert \base_addr(p - 5) ≡ \base_addr(pd); */
{
void *__gen_e_acsl_base_addr_37;
void *__gen_e_acsl_base_addr_38;
- __gen_e_acsl_base_addr_37 = __e_acsl_base_addr((void *)q);
- __gen_e_acsl_base_addr_38 = __e_acsl_base_addr((void *)qd);
+ __gen_e_acsl_base_addr_37 = __e_acsl_base_addr((void *)(p - 5));
+ __gen_e_acsl_base_addr_38 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_37 == __gen_e_acsl_base_addr_38,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(q) == \\base_addr(qd)",57);
+ (char *)"\\base_addr(p - 5) == \\base_addr(pd)",51);
}
+ long *q = malloc((unsigned long)30 * sizeof(long));
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_full_init((void *)(& q));
- q += 2;
+ long *qd = q;
+ __e_acsl_store_block((void *)(& qd),(size_t)8);
+ __e_acsl_full_init((void *)(& qd));
/*@ assert \base_addr(q) ≡ \base_addr(qd); */
{
void *__gen_e_acsl_base_addr_39;
@@ -257,10 +253,10 @@ int main(void)
__gen_e_acsl_base_addr_40 = __e_acsl_base_addr((void *)qd);
__e_acsl_assert(__gen_e_acsl_base_addr_39 == __gen_e_acsl_base_addr_40,
(char *)"Assertion",(char *)"main",
- (char *)"\\base_addr(q) == \\base_addr(qd)",59);
+ (char *)"\\base_addr(q) == \\base_addr(qd)",57);
}
__e_acsl_full_init((void *)(& q));
- q += 4;
+ q ++;
/*@ assert \base_addr(q) ≡ \base_addr(qd); */
{
void *__gen_e_acsl_base_addr_41;
@@ -268,9 +264,33 @@ int main(void)
__gen_e_acsl_base_addr_41 = __e_acsl_base_addr((void *)q);
__gen_e_acsl_base_addr_42 = __e_acsl_base_addr((void *)qd);
__e_acsl_assert(__gen_e_acsl_base_addr_41 == __gen_e_acsl_base_addr_42,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(q) == \\base_addr(qd)",59);
+ }
+ __e_acsl_full_init((void *)(& q));
+ q += 2;
+ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ {
+ void *__gen_e_acsl_base_addr_43;
+ void *__gen_e_acsl_base_addr_44;
+ __gen_e_acsl_base_addr_43 = __e_acsl_base_addr((void *)q);
+ __gen_e_acsl_base_addr_44 = __e_acsl_base_addr((void *)qd);
+ __e_acsl_assert(__gen_e_acsl_base_addr_43 == __gen_e_acsl_base_addr_44,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(q) == \\base_addr(qd)",61);
}
+ __e_acsl_full_init((void *)(& q));
+ q += 4;
+ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
+ {
+ void *__gen_e_acsl_base_addr_45;
+ void *__gen_e_acsl_base_addr_46;
+ __gen_e_acsl_base_addr_45 = __e_acsl_base_addr((void *)q);
+ __gen_e_acsl_base_addr_46 = __e_acsl_base_addr((void *)qd);
+ __e_acsl_assert(__gen_e_acsl_base_addr_45 == __gen_e_acsl_base_addr_46,
+ (char *)"Assertion",(char *)"main",
+ (char *)"\\base_addr(q) == \\base_addr(qd)",63);
+ }
__retres = 0;
__e_acsl_delete_block((void *)(& PA));
__e_acsl_delete_block((void *)(A));
--
GitLab