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

[tests] fix additional oracles

parent 90590234
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/bts/oracle/gen_bts1324.c
+ 22
− 0
View file @ 3cf2b60e
...@@ -78,6 +78,7 @@ int __gen_e_acsl_sorted(int *t, int n) ...@@ -78,6 +78,7 @@ int __gen_e_acsl_sorted(int *t, int n)
while (1) { while (1) {
if (__gen_e_acsl_i < n) ; else break; if (__gen_e_acsl_i < n) ; else break;
{ {
<<<<<<< HEAD
int __gen_e_acsl_valid_read; int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2; int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (unsigned long)((unsigned int)__gen_e_acsl_i)), __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (unsigned long)((unsigned int)__gen_e_acsl_i)),
...@@ -85,6 +86,21 @@ int __gen_e_acsl_sorted(int *t, int n) ...@@ -85,6 +86,21 @@ int __gen_e_acsl_sorted(int *t, int n)
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE", __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"sorted", (char *)"sorted",
(char *)"mem_access: \\valid_read(t+(unsigned long)__gen_e_acsl_i)", (char *)"mem_access: \\valid_read(t+(unsigned long)__gen_e_acsl_i)",
||||||| merged common ancestors
int __e_acsl_valid_read;
int __e_acsl_valid_read_2;
__e_acsl_valid_read = __valid_read((void *)(t + (unsigned long)((unsigned int)__e_acsl_i)),
sizeof(int));
__e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"sorted",
(char *)"mem_access: \\valid_read(t+(unsigned long)__e_acsl_i)",
=======
int __e_acsl_valid_read;
int __e_acsl_valid_read_2;
__e_acsl_valid_read = __valid_read((void *)(t + (unsigned long)__e_acsl_i),
sizeof(int));
__e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"sorted",
(char *)"mem_access: \\valid_read(t+(unsigned long)__e_acsl_i)",
>>>>>>> [tests] fix additional oracles
6); 6);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (unsigned long)( __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (unsigned long)(
__gen_e_acsl_i - 1)), __gen_e_acsl_i - 1)),
...@@ -100,7 +116,13 @@ int __gen_e_acsl_sorted(int *t, int n) ...@@ -100,7 +116,13 @@ int __gen_e_acsl_sorted(int *t, int n)
goto e_acsl_end_loop1; goto e_acsl_end_loop1;
} }
} }
<<<<<<< HEAD
__gen_e_acsl_i ++; __gen_e_acsl_i ++;
||||||| merged common ancestors
__e_acsl_i ++;
=======
__e_acsl_i = (int)(__e_acsl_i + 1L);
>>>>>>> [tests] fix additional oracles
} }
e_acsl_end_loop1: ; e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_forall; __gen_e_acsl_at = __gen_e_acsl_forall;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_offset.c
+ 46
− 66
View file @ 3cf2b60e
...@@ -32,34 +32,30 @@ int main(void) ...@@ -32,34 +32,30 @@ int main(void)
{ {
int __gen_e_acsl_offset; int __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset((void *)(A)); __gen_e_acsl_offset = __e_acsl_offset((void *)(A));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset((int *)A) == 0",13);
(char *)"\\offset((int *)A) == 0",13);
} }
/*@ assert \offset(&A[3]) ≡ 12; */ /*@ assert \offset(&A[3]) ≡ 12; */
{ {
int __gen_e_acsl_offset_2; int __gen_e_acsl_offset_2;
__gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3])); __gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3]));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_2 == (unsigned long)12, __e_acsl_assert(__gen_e_acsl_offset_2 == 12,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(&A[3]) == 12",14);
(char *)"\\offset(&A[3]) == 12",14);
} }
/*@ assert \offset(PA) ≡ 0; */ /*@ assert \offset(PA) ≡ 0; */
{ {
int __gen_e_acsl_offset_3; int __gen_e_acsl_offset_3;
__gen_e_acsl_offset_3 = __e_acsl_offset((void *)PA); __gen_e_acsl_offset_3 = __e_acsl_offset((void *)PA);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_3 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_3 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(PA) == 0",15);
(char *)"\\offset(PA) == 0",15);
} }
PA ++; PA ++;
/*@ assert \offset(PA+1) ≡ 8; */ /*@ assert \offset(PA+1) ≡ 8; */
{ {
int __gen_e_acsl_offset_4; int __gen_e_acsl_offset_4;
__gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1)); __gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_4 == (unsigned long)8, __e_acsl_assert(__gen_e_acsl_offset_4 == 8,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(PA+1) == 8",17);
(char *)"\\offset(PA+1) == 8",17);
} }
__e_acsl_initialize((void *)(a),sizeof(int)); __e_acsl_initialize((void *)(a),sizeof(int));
a[0] = 1; a[0] = 1;
...@@ -73,25 +69,22 @@ int main(void) ...@@ -73,25 +69,22 @@ int main(void)
{ {
int __gen_e_acsl_offset_5; int __gen_e_acsl_offset_5;
__gen_e_acsl_offset_5 = __e_acsl_offset((void *)(a)); __gen_e_acsl_offset_5 = __e_acsl_offset((void *)(a));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_5 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_5 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset((int *)a) == 0",21);
(char *)"\\offset((int *)a) == 0",21);
} }
/*@ assert \offset(&a[1]) ≡ 4; */ /*@ assert \offset(&a[1]) ≡ 4; */
{ {
int __gen_e_acsl_offset_6; int __gen_e_acsl_offset_6;
__gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1])); __gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1]));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_6 == (unsigned long)4, __e_acsl_assert(__gen_e_acsl_offset_6 == 4,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(&a[1]) == 4",22);
(char *)"\\offset(&a[1]) == 4",22);
} }
/*@ assert \offset(&a[3]) ≡ 12; */ /*@ assert \offset(&a[3]) ≡ 12; */
{ {
int __gen_e_acsl_offset_7; int __gen_e_acsl_offset_7;
__gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3])); __gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3]));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_7 == (unsigned long)12, __e_acsl_assert(__gen_e_acsl_offset_7 == 12,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(&a[3]) == 12",23);
(char *)"\\offset(&a[3]) == 12",23);
} }
__e_acsl_full_init((void *)(& l)); __e_acsl_full_init((void *)(& l));
l = (long)4; l = (long)4;
...@@ -101,33 +94,29 @@ int main(void) ...@@ -101,33 +94,29 @@ int main(void)
{ {
int __gen_e_acsl_offset_8; int __gen_e_acsl_offset_8;
__gen_e_acsl_offset_8 = __e_acsl_offset((void *)(& l)); __gen_e_acsl_offset_8 = __e_acsl_offset((void *)(& l));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_8 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_8 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(&l) == 0",28);
(char *)"\\offset(&l) == 0",28);
} }
/*@ assert \offset(pl) ≡ 0; */ /*@ assert \offset(pl) ≡ 0; */
{ {
int __gen_e_acsl_offset_9; int __gen_e_acsl_offset_9;
__gen_e_acsl_offset_9 = __e_acsl_offset((void *)pl); __gen_e_acsl_offset_9 = __e_acsl_offset((void *)pl);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_9 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_9 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(pl) == 0",29);
(char *)"\\offset(pl) == 0",29);
} }
/*@ assert \offset(pl+1) ≡ 1; */ /*@ assert \offset(pl+1) ≡ 1; */
{ {
int __gen_e_acsl_offset_10; int __gen_e_acsl_offset_10;
__gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1)); __gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_10 == (unsigned long)1, __e_acsl_assert(__gen_e_acsl_offset_10 == 1,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(pl+1) == 1",30);
(char *)"\\offset(pl+1) == 1",30);
} }
/*@ assert \offset(pl+7) ≡ 7; */ /*@ assert \offset(pl+7) ≡ 7; */
{ {
int __gen_e_acsl_offset_11; int __gen_e_acsl_offset_11;
__gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7)); __gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_11 == (unsigned long)7, __e_acsl_assert(__gen_e_acsl_offset_11 == 7,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(pl+7) == 7",31);
(char *)"\\offset(pl+7) == 7",31);
} }
__e_acsl_full_init((void *)(& pi)); __e_acsl_full_init((void *)(& pi));
pi = (int *)(& l); pi = (int *)(& l);
...@@ -135,9 +124,8 @@ int main(void) ...@@ -135,9 +124,8 @@ int main(void)
{ {
int __gen_e_acsl_offset_12; int __gen_e_acsl_offset_12;
__gen_e_acsl_offset_12 = __e_acsl_offset((void *)pi); __gen_e_acsl_offset_12 = __e_acsl_offset((void *)pi);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_12 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_12 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(pi) == 0",33);
(char *)"\\offset(pi) == 0",33);
} }
__e_acsl_full_init((void *)(& pi)); __e_acsl_full_init((void *)(& pi));
pi ++; pi ++;
...@@ -145,9 +133,8 @@ int main(void) ...@@ -145,9 +133,8 @@ int main(void)
{ {
int __gen_e_acsl_offset_13; int __gen_e_acsl_offset_13;
__gen_e_acsl_offset_13 = __e_acsl_offset((void *)pi); __gen_e_acsl_offset_13 = __e_acsl_offset((void *)pi);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_13 == (unsigned long)4, __e_acsl_assert(__gen_e_acsl_offset_13 == 4,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(pi) == 4",35);
(char *)"\\offset(pi) == 4",35);
} }
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
p = (char *)__gen_e_acsl_malloc((unsigned long)12); p = (char *)__gen_e_acsl_malloc((unsigned long)12);
...@@ -155,25 +142,22 @@ int main(void) ...@@ -155,25 +142,22 @@ int main(void)
{ {
int __gen_e_acsl_offset_14; int __gen_e_acsl_offset_14;
__gen_e_acsl_offset_14 = __e_acsl_offset((void *)p); __gen_e_acsl_offset_14 = __e_acsl_offset((void *)p);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_14 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_14 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(p) == 0",39);
(char *)"\\offset(p) == 0",39);
} }
/*@ assert \offset(p+1) ≡ 1; */ /*@ assert \offset(p+1) ≡ 1; */
{ {
int __gen_e_acsl_offset_15; int __gen_e_acsl_offset_15;
__gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1)); __gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_15 == (unsigned long)1, __e_acsl_assert(__gen_e_acsl_offset_15 == 1,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(p+1) == 1",40);
(char *)"\\offset(p+1) == 1",40);
} }
/*@ assert \offset(p+11) ≡ 11; */ /*@ assert \offset(p+11) ≡ 11; */
{ {
int __gen_e_acsl_offset_16; int __gen_e_acsl_offset_16;
__gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11)); __gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_16 == (unsigned long)11, __e_acsl_assert(__gen_e_acsl_offset_16 == 11,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(p+11) == 11",41);
(char *)"\\offset(p+11) == 11",41);
} }
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
p += 5; p += 5;
...@@ -181,17 +165,15 @@ int main(void) ...@@ -181,17 +165,15 @@ int main(void)
{ {
int __gen_e_acsl_offset_17; int __gen_e_acsl_offset_17;
__gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5)); __gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_17 == (unsigned long)10, __e_acsl_assert(__gen_e_acsl_offset_17 == 10,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(p+5) == 10",43);
(char *)"\\offset(p+5) == 10",43);
} }
/*@ assert \offset(p-5) ≡ 0; */ /*@ assert \offset(p-5) ≡ 0; */
{ {
int __gen_e_acsl_offset_18; int __gen_e_acsl_offset_18;
__gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5)); __gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5));
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_18 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_18 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(p-5) == 0",44);
(char *)"\\offset(p-5) == 0",44);
} }
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
q = (long *)__gen_e_acsl_malloc((unsigned long)30 * sizeof(long)); q = (long *)__gen_e_acsl_malloc((unsigned long)30 * sizeof(long));
...@@ -199,9 +181,8 @@ int main(void) ...@@ -199,9 +181,8 @@ int main(void)
{ {
int __gen_e_acsl_offset_19; int __gen_e_acsl_offset_19;
__gen_e_acsl_offset_19 = __e_acsl_offset((void *)q); __gen_e_acsl_offset_19 = __e_acsl_offset((void *)q);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_19 == (unsigned long)0, __e_acsl_assert(__gen_e_acsl_offset_19 == 0,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(q) == 0",49);
(char *)"\\offset(q) == 0",49);
} }
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
q ++; q ++;
...@@ -209,9 +190,8 @@ int main(void) ...@@ -209,9 +190,8 @@ int main(void)
{ {
int __gen_e_acsl_offset_20; int __gen_e_acsl_offset_20;
__gen_e_acsl_offset_20 = __e_acsl_offset((void *)q); __gen_e_acsl_offset_20 = __e_acsl_offset((void *)q);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_20 == 8UL, __e_acsl_assert(__gen_e_acsl_offset_20 == 8,(char *)"Assertion",
(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(q) == sizeof(long)",51);
(char *)"\\offset(q) == sizeof(long)",51);
} }
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
q += 2; q += 2;
...@@ -219,9 +199,9 @@ int main(void) ...@@ -219,9 +199,9 @@ int main(void)
{ {
int __gen_e_acsl_offset_21; int __gen_e_acsl_offset_21;
__gen_e_acsl_offset_21 = __e_acsl_offset((void *)q); __gen_e_acsl_offset_21 = __e_acsl_offset((void *)q);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_21 == (unsigned long)( __e_acsl_assert(__gen_e_acsl_offset_21 == 8 * 3,(char *)"Assertion",
8 * 3),(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(q) == sizeof(long)*3",
(char *)"\\offset(q) == sizeof(long)*3",53); 53);
} }
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
q += 4; q += 4;
...@@ -229,9 +209,9 @@ int main(void) ...@@ -229,9 +209,9 @@ int main(void)
{ {
int __gen_e_acsl_offset_22; int __gen_e_acsl_offset_22;
__gen_e_acsl_offset_22 = __e_acsl_offset((void *)q); __gen_e_acsl_offset_22 = __e_acsl_offset((void *)q);
__e_acsl_assert((unsigned long)__gen_e_acsl_offset_22 == (unsigned long)( __e_acsl_assert(__gen_e_acsl_offset_22 == 8 * 7,(char *)"Assertion",
8 * 7),(char *)"Assertion",(char *)"main", (char *)"main",(char *)"\\offset(q) == sizeof(long)*7",
(char *)"\\offset(q) == sizeof(long)*7",55); 55);
} }
__retres = 0; __retres = 0;
__e_acsl_delete_block((void *)(& PA)); __e_acsl_delete_block((void *)(& PA));
......
src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
+ 1
− 2
View file @ 3cf2b60e
...@@ -16,8 +16,7 @@ int main(void) ...@@ -16,8 +16,7 @@ int main(void)
__e_acsl_assert(y == 0,(char *)"Assertion",(char *)"main", __e_acsl_assert(y == 0,(char *)"Assertion",(char *)"main",
(char *)"y == (int)0",13); (char *)"y == (int)0",13);
/*@ assert (unsigned int)y ≡ (unsigned int)0; */ /*@ assert (unsigned int)y ≡ (unsigned int)0; */
__e_acsl_assert((unsigned int)y == (unsigned int)0,(char *)"Assertion", __e_acsl_assert((unsigned int)y == 0,(char *)"Assertion",(char *)"main",
(char *)"main",
(char *)"(unsigned int)y == (unsigned int)0",14); (char *)"(unsigned int)y == (unsigned int)0",14);
/*@ assert y ≢ (int)0xfffffffffffffff; */ /*@ assert y ≢ (int)0xfffffffffffffff; */
__e_acsl_assert(y != (int)0xfffffffffffffff,(char *)"Assertion", __e_acsl_assert(y != (int)0xfffffffffffffff,(char *)"Assertion",
......
src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
+ 2
− 2
View file @ 3cf2b60e
...@@ -52,7 +52,7 @@ int main(void) ...@@ -52,7 +52,7 @@ int main(void)
mpz_t __gen_e_acsl__4; mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_3; int __gen_e_acsl_eq_3;
__gmpz_init_set_si(__gen_e_acsl_y_3,(long)y); __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
__gmpz_init_set_si(__gen_e_acsl__3,(long)0); __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)0);
__gen_e_acsl_cast_3 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__3)); __gen_e_acsl_cast_3 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init_set_ui(__gen_e_acsl__4,__gen_e_acsl_cast_3); __gmpz_init_set_ui(__gen_e_acsl__4,__gen_e_acsl_cast_3);
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_3), __gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_3),
...@@ -75,7 +75,7 @@ int main(void) ...@@ -75,7 +75,7 @@ int main(void)
__gmpz_init_set_si(__gen_e_acsl_y_4,(long)y); __gmpz_init_set_si(__gen_e_acsl_y_4,(long)y);
__gen_e_acsl_cast_4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_y_4)); __gen_e_acsl_cast_4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_y_4));
__gmpz_init_set_ui(__gen_e_acsl__5,__gen_e_acsl_cast_4); __gmpz_init_set_ui(__gen_e_acsl__5,__gen_e_acsl_cast_4);
__gmpz_init_set_si(__gen_e_acsl__6,(long)0); __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)0);
__gen_e_acsl_cast_5 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__6)); __gen_e_acsl_cast_5 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init_set_ui(__gen_e_acsl__7,__gen_e_acsl_cast_5); __gmpz_init_set_ui(__gen_e_acsl__7,__gen_e_acsl_cast_5);
__gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5), __gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
......
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