Skip to content
Snippets Groups Projects
Commit 2ee422c3 authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] improved tests for base_addr

parent dc4995f7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/runtime/base_addr.c
+ 2
− 0
View file @ 2ee422c3
...@@ -10,6 +10,7 @@ int *PA; ...@@ -10,6 +10,7 @@ int *PA;
int main(void) { int main(void) {
/* Global memory */ /* Global memory */
PA = (int*)&A; PA = (int*)&A;
/*@ assert \base_addr(&A[0]) == \base_addr(&A); */
/*@ assert \base_addr(&A[0]) == \base_addr(PA); */ /*@ assert \base_addr(&A[0]) == \base_addr(PA); */
/*@ assert \base_addr(A+3) == \base_addr(PA); */ /*@ assert \base_addr(A+3) == \base_addr(PA); */
PA++; PA++;
...@@ -21,6 +22,7 @@ int main(void) { ...@@ -21,6 +22,7 @@ int main(void) {
int *pa; int *pa;
pa = (int*)&a; pa = (int*)&a;
/*@ assert \base_addr(&a[0]) == \base_addr(&a); */
/*@ assert \base_addr(&a[0]) == \base_addr(pa); */ /*@ assert \base_addr(&a[0]) == \base_addr(pa); */
/*@ assert \base_addr(a+3) == \base_addr(pa); */ /*@ assert \base_addr(a+3) == \base_addr(pa); */
pa++; pa++;
......
src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
+ 5
− 5
View file @ 2ee422c3
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl". [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. 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:48:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:49:[value] warning: assertion got status unknown. tests/runtime/base_addr.c:50:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:55:[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:57:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:59:[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:61:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:63:[value] warning: assertion got status unknown.
src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
+ 132
− 112
View file @ 2ee422c3
...@@ -19,236 +19,232 @@ int main(void) ...@@ -19,236 +19,232 @@ int main(void)
__e_acsl_globals_init(); __e_acsl_globals_init();
__e_acsl_store_block((void *)(& pa),(size_t)8); __e_acsl_store_block((void *)(& pa),(size_t)8);
PA = (int *)(& A); 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;
void *__gen_e_acsl_base_addr_2; void *__gen_e_acsl_base_addr_2;
__gen_e_acsl_base_addr = __e_acsl_base_addr((void *)(A)); __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, __e_acsl_assert(__gen_e_acsl_base_addr == __gen_e_acsl_base_addr_2,
(char *)"Assertion",(char *)"main", (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_3;
void *__gen_e_acsl_base_addr_4; 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); __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, __e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
(char *)"Assertion",(char *)"main", (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(&A[3]) ≡ \base_addr(PA); */
/*@ assert \base_addr(PA) ≡ \base_addr((int *)A); */
{ {
void *__gen_e_acsl_base_addr_5; void *__gen_e_acsl_base_addr_5;
void *__gen_e_acsl_base_addr_6; void *__gen_e_acsl_base_addr_6;
__gen_e_acsl_base_addr_5 = __e_acsl_base_addr((void *)PA); __gen_e_acsl_base_addr_5 = __e_acsl_base_addr((void *)(& A[3]));
__gen_e_acsl_base_addr_6 = __e_acsl_base_addr((void *)(A)); __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, __e_acsl_assert(__gen_e_acsl_base_addr_5 == __gen_e_acsl_base_addr_6,
(char *)"Assertion",(char *)"main", (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_7;
void *__gen_e_acsl_base_addr_8; 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_7 = __e_acsl_base_addr((void *)PA);
__gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3])); __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, __e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
(char *)"Assertion",(char *)"main", (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}; /*@ assert \base_addr(PA + 2) ≡ \base_addr(&A[3]); */
__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); */
{ {
void *__gen_e_acsl_base_addr_9; void *__gen_e_acsl_base_addr_9;
void *__gen_e_acsl_base_addr_10; void *__gen_e_acsl_base_addr_10;
__gen_e_acsl_base_addr_9 = __e_acsl_base_addr((void *)(a)); __gen_e_acsl_base_addr_9 = __e_acsl_base_addr((void *)(PA + 2));
__gen_e_acsl_base_addr_10 = __e_acsl_base_addr((void *)pa); __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, __e_acsl_assert(__gen_e_acsl_base_addr_9 == __gen_e_acsl_base_addr_10,
(char *)"Assertion",(char *)"main", (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_11;
void *__gen_e_acsl_base_addr_12; 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_11 = __e_acsl_base_addr((void *)(a));
__gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa); __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, __e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
(char *)"Assertion",(char *)"main", (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)); /*@ assert \base_addr((int *)a) ≡ \base_addr(pa); */
pa ++;
/*@ assert \base_addr(pa) ≡ \base_addr((int *)a); */
{ {
void *__gen_e_acsl_base_addr_13; void *__gen_e_acsl_base_addr_13;
void *__gen_e_acsl_base_addr_14; void *__gen_e_acsl_base_addr_14;
__gen_e_acsl_base_addr_13 = __e_acsl_base_addr((void *)pa); __gen_e_acsl_base_addr_13 = __e_acsl_base_addr((void *)(a));
__gen_e_acsl_base_addr_14 = __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, __e_acsl_assert(__gen_e_acsl_base_addr_13 == __gen_e_acsl_base_addr_14,
(char *)"Assertion",(char *)"main", (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_15;
void *__gen_e_acsl_base_addr_16; 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_15 = __e_acsl_base_addr((void *)(& a[3]));
__gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a)); __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, __e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
(char *)"Assertion",(char *)"main", (char *)"Assertion",(char *)"main",
(char *)"\\base_addr(pa + 2) == \\base_addr((int *)a)", (char *)"\\base_addr(&a[3]) == \\base_addr(pa)",27);
28);
} }
long l = (long)4; __e_acsl_full_init((void *)(& pa));
__e_acsl_store_block((void *)(& l),(size_t)8); pa ++;
__e_acsl_full_init((void *)(& l)); /*@ assert \base_addr(pa) ≡ \base_addr((int *)a); */
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); */
{ {
void *__gen_e_acsl_base_addr_17; void *__gen_e_acsl_base_addr_17;
void *__gen_e_acsl_base_addr_18; void *__gen_e_acsl_base_addr_18;
__gen_e_acsl_base_addr_17 = __e_acsl_base_addr((void *)(& l)); __gen_e_acsl_base_addr_17 = __e_acsl_base_addr((void *)pa);
__gen_e_acsl_base_addr_18 = __e_acsl_base_addr((void *)pl); __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, __e_acsl_assert(__gen_e_acsl_base_addr_17 == __gen_e_acsl_base_addr_18,
(char *)"Assertion",(char *)"main", (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_19;
void *__gen_e_acsl_base_addr_20; 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_19 = __e_acsl_base_addr((void *)(pa + 2));
__gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l)); __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, __e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
(char *)"Assertion",(char *)"main", (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); long l = (long)4;
__e_acsl_store_block((void *)(& pi),(size_t)8); __e_acsl_store_block((void *)(& l),(size_t)8);
__e_acsl_full_init((void *)(& pi)); __e_acsl_full_init((void *)(& l));
__e_acsl_full_init((void *)(& pi)); char *pl = (char *)(& l);
pi ++; __e_acsl_store_block((void *)(& pl),(size_t)8);
__e_acsl_full_init((void *)(& pl)); __e_acsl_full_init((void *)(& pl));
pl ++; /*@ assert \base_addr(&l) ≡ \base_addr(pl); */
/*@ assert \base_addr(pi) ≡ \base_addr(pl); */
{ {
void *__gen_e_acsl_base_addr_21; void *__gen_e_acsl_base_addr_21;
void *__gen_e_acsl_base_addr_22; 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); __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, __e_acsl_assert(__gen_e_acsl_base_addr_21 == __gen_e_acsl_base_addr_22,
(char *)"Assertion",(char *)"main", (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_23;
void *__gen_e_acsl_base_addr_24; 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)); __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, __e_acsl_assert(__gen_e_acsl_base_addr_23 == __gen_e_acsl_base_addr_24,
(char *)"Assertion",(char *)"main", (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); short *pi = (short *)(& l);
__e_acsl_store_block((void *)(& p),(size_t)8); __e_acsl_store_block((void *)(& pi),(size_t)8);
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& pi));
char *pd = p; __e_acsl_full_init((void *)(& pi));
__e_acsl_store_block((void *)(& pd),(size_t)8); pi ++;
__e_acsl_full_init((void *)(& pd)); __e_acsl_full_init((void *)(& pl));
/*@ assert \base_addr(p) ≡ \base_addr(pd); */ pl ++;
/*@ assert \base_addr(pi) ≡ \base_addr(pl); */
{ {
void *__gen_e_acsl_base_addr_25; void *__gen_e_acsl_base_addr_25;
void *__gen_e_acsl_base_addr_26; void *__gen_e_acsl_base_addr_26;
__gen_e_acsl_base_addr_25 = __e_acsl_base_addr((void *)p); __gen_e_acsl_base_addr_25 = __e_acsl_base_addr((void *)pi);
__gen_e_acsl_base_addr_26 = __e_acsl_base_addr((void *)pd); __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, __e_acsl_assert(__gen_e_acsl_base_addr_25 == __gen_e_acsl_base_addr_26,
(char *)"Assertion",(char *)"main", (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_27;
void *__gen_e_acsl_base_addr_28; 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_27 = __e_acsl_base_addr((void *)pl);
__gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5)); __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, __e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
(char *)"Assertion",(char *)"main", (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_29;
void *__gen_e_acsl_base_addr_30; 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_29 = __e_acsl_base_addr((void *)p);
__gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1)); __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, __e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
(char *)"Assertion",(char *)"main", (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)); /*@ assert \base_addr(p + 1) ≡ \base_addr(pd + 5); */
p += 5;
/*@ assert \base_addr(p + 5) ≡ \base_addr(pd); */
{ {
void *__gen_e_acsl_base_addr_31; void *__gen_e_acsl_base_addr_31;
void *__gen_e_acsl_base_addr_32; 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_31 = __e_acsl_base_addr((void *)(p + 1));
__gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd); __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, __e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
(char *)"Assertion",(char *)"main", (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_33;
void *__gen_e_acsl_base_addr_34; 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_33 = __e_acsl_base_addr((void *)(p + 11));
__gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd); __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, __e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
(char *)"Assertion",(char *)"main", (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_full_init((void *)(& p));
__e_acsl_store_block((void *)(& q),(size_t)8); p += 5;
__e_acsl_full_init((void *)(& q)); /*@ assert \base_addr(p + 5) ≡ \base_addr(pd); */
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_35; void *__gen_e_acsl_base_addr_35;
void *__gen_e_acsl_base_addr_36; void *__gen_e_acsl_base_addr_36;
__gen_e_acsl_base_addr_35 = __e_acsl_base_addr((void *)q); __gen_e_acsl_base_addr_35 = __e_acsl_base_addr((void *)(p + 5));
__gen_e_acsl_base_addr_36 = __e_acsl_base_addr((void *)qd); __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, __e_acsl_assert(__gen_e_acsl_base_addr_35 == __gen_e_acsl_base_addr_36,
(char *)"Assertion",(char *)"main", (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)); /*@ assert \base_addr(p - 5) ≡ \base_addr(pd); */
q ++;
/*@ assert \base_addr(q) ≡ \base_addr(qd); */
{ {
void *__gen_e_acsl_base_addr_37; void *__gen_e_acsl_base_addr_37;
void *__gen_e_acsl_base_addr_38; void *__gen_e_acsl_base_addr_38;
__gen_e_acsl_base_addr_37 = __e_acsl_base_addr((void *)q); __gen_e_acsl_base_addr_37 = __e_acsl_base_addr((void *)(p - 5));
__gen_e_acsl_base_addr_38 = __e_acsl_base_addr((void *)qd); __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, __e_acsl_assert(__gen_e_acsl_base_addr_37 == __gen_e_acsl_base_addr_38,
(char *)"Assertion",(char *)"main", (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)); __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); */ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
{ {
void *__gen_e_acsl_base_addr_39; void *__gen_e_acsl_base_addr_39;
...@@ -257,10 +253,10 @@ int main(void) ...@@ -257,10 +253,10 @@ int main(void)
__gen_e_acsl_base_addr_40 = __e_acsl_base_addr((void *)qd); __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, __e_acsl_assert(__gen_e_acsl_base_addr_39 == __gen_e_acsl_base_addr_40,
(char *)"Assertion",(char *)"main", (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)); __e_acsl_full_init((void *)(& q));
q += 4; q ++;
/*@ assert \base_addr(q) ≡ \base_addr(qd); */ /*@ assert \base_addr(q) ≡ \base_addr(qd); */
{ {
void *__gen_e_acsl_base_addr_41; void *__gen_e_acsl_base_addr_41;
...@@ -268,9 +264,33 @@ int main(void) ...@@ -268,9 +264,33 @@ int main(void)
__gen_e_acsl_base_addr_41 = __e_acsl_base_addr((void *)q); __gen_e_acsl_base_addr_41 = __e_acsl_base_addr((void *)q);
__gen_e_acsl_base_addr_42 = __e_acsl_base_addr((void *)qd); __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, __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 *)"Assertion",(char *)"main",
(char *)"\\base_addr(q) == \\base_addr(qd)",61); (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; __retres = 0;
__e_acsl_delete_block((void *)(& PA)); __e_acsl_delete_block((void *)(& PA));
__e_acsl_delete_block((void *)(A)); __e_acsl_delete_block((void *)(A));
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment