diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
index 96b37ea579d10fb9ea0959581868b8470c0230a7..4acc2f23cf50d7be0abb7034d5ff566ceec296ae 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
@@ -79,156 +79,156 @@ int main(void)
/*@ assert (\let u = 1; u) + 1 ≡ 2; */
{
int __gen_e_acsl_u_3;
+ __e_acsl_mpz_t __gen_e_acsl_u_4;
__e_acsl_mpz_t __gen_e_acsl__4;
- __e_acsl_mpz_t __gen_e_acsl__5;
__e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__5;
int __gen_e_acsl_eq;
__gen_e_acsl_u_3 = 1;
- __gmpz_init_set_si(__gen_e_acsl__4,(long)__gen_e_acsl_u_3);
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set_si(__gen_e_acsl_u_4,(long)__gen_e_acsl_u_3);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gmpz_init_set_si(__gen_e_acsl__6,2L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gmpz_init_set_si(__gen_e_acsl__5,2L);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"(\\let u = 1; u) + 1 == 2",12);
+ __gmpz_clear(__gen_e_acsl_u_4);
__gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl__5);
__gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__5);
}
/*@ assert \let u = 1; (\let v = u + 1; v) ≡ 2; */
{
- int __gen_e_acsl_u_4;
+ int __gen_e_acsl_u_5;
__e_acsl_mpz_t __gen_e_acsl_v_2;
- __e_acsl_mpz_t __gen_e_acsl_u_5;
- __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_u_6;
+ __e_acsl_mpz_t __gen_e_acsl__6;
__e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl__7;
int __gen_e_acsl_eq_2;
- __gen_e_acsl_u_4 = 1;
- __gmpz_init_set_si(__gen_e_acsl_u_5,(long)__gen_e_acsl_u_4);
- __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gen_e_acsl_u_5 = 1;
+ __gmpz_init_set_si(__gen_e_acsl_u_6,(long)__gen_e_acsl_u_5);
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init_set(__gen_e_acsl_v_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_init_set_si(__gen_e_acsl__8,2L);
+ __gmpz_init_set_si(__gen_e_acsl__7,2L);
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_v_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
(char *)"main",
(char *)"\\let u = 1; (\\let v = u + 1; v) == 2",14);
__gmpz_clear(__gen_e_acsl_v_2);
- __gmpz_clear(__gen_e_acsl_u_5);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_u_6);
+ __gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl__7);
}
/*@ assert \let u = 1; (\let u = u + 1; u) ≡ 2; */
{
- int __gen_e_acsl_u_6;
- __e_acsl_mpz_t __gen_e_acsl_u_7;
+ int __gen_e_acsl_u_7;
__e_acsl_mpz_t __gen_e_acsl_u_8;
- __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_u_9;
+ __e_acsl_mpz_t __gen_e_acsl__8;
__e_acsl_mpz_t __gen_e_acsl_add_4;
- __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__9;
int __gen_e_acsl_eq_3;
- __gen_e_acsl_u_6 = 1;
- __gmpz_init_set_si(__gen_e_acsl_u_8,(long)__gen_e_acsl_u_6);
- __gmpz_init_set_si(__gen_e_acsl__9,1L);
+ __gen_e_acsl_u_7 = 1;
+ __gmpz_init_set_si(__gen_e_acsl_u_9,(long)__gen_e_acsl_u_7);
+ __gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_add_4);
__gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __gmpz_init_set(__gen_e_acsl_u_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init_set(__gen_e_acsl_u_8,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_init_set_si(__gen_e_acsl__10,2L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_u_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_init_set_si(__gen_e_acsl__9,2L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_u_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",
(char *)"\\let u = 1; (\\let u = u + 1; u) == 2",17);
- __gmpz_clear(__gen_e_acsl_u_7);
__gmpz_clear(__gen_e_acsl_u_8);
- __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_u_9);
+ __gmpz_clear(__gen_e_acsl__8);
__gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__9);
}
long m = 0x7fffffffffffffffL;
/*@ assert (\let u = m; u * u) > m; */
{
- long __gen_e_acsl_u_9;
- __e_acsl_mpz_t __gen_e_acsl_u_10;
+ long __gen_e_acsl_u_10;
+ __e_acsl_mpz_t __gen_e_acsl_u_11;
__e_acsl_mpz_t __gen_e_acsl_mul_3;
__e_acsl_mpz_t __gen_e_acsl_m;
int __gen_e_acsl_gt_2;
- __gen_e_acsl_u_9 = m;
- __gmpz_init_set_si(__gen_e_acsl_u_10,__gen_e_acsl_u_9);
+ __gen_e_acsl_u_10 = m;
+ __gmpz_init_set_si(__gen_e_acsl_u_11,__gen_e_acsl_u_10);
__gmpz_init(__gen_e_acsl_mul_3);
__gmpz_mul(__gen_e_acsl_mul_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_10));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_11));
__gmpz_init_set_si(__gen_e_acsl_m,m);
__gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_m));
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
(char *)"(\\let u = m; u * u) > m",21);
- __gmpz_clear(__gen_e_acsl_u_10);
+ __gmpz_clear(__gen_e_acsl_u_11);
__gmpz_clear(__gen_e_acsl_mul_3);
__gmpz_clear(__gen_e_acsl_m);
}
char c = (char)'a';
/*@ assert \let u = 'b'; c < u; */
{
- int __gen_e_acsl_u_11;
+ int __gen_e_acsl_u_12;
__e_acsl_mpz_t __gen_e_acsl_c;
- __e_acsl_mpz_t __gen_e_acsl_u_12;
+ __e_acsl_mpz_t __gen_e_acsl_u_13;
int __gen_e_acsl_lt;
- __gen_e_acsl_u_11 = 'b';
+ __gen_e_acsl_u_12 = 'b';
__gmpz_init_set_si(__gen_e_acsl_c,(long)c);
- __gmpz_init_set_si(__gen_e_acsl_u_12,(long)__gen_e_acsl_u_11);
+ __gmpz_init_set_si(__gen_e_acsl_u_13,(long)__gen_e_acsl_u_12);
__gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_12));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_13));
__e_acsl_assert(__gen_e_acsl_lt < 0,(char *)"Assertion",(char *)"main",
(char *)"\\let u = \'b\'; c < u",24);
__gmpz_clear(__gen_e_acsl_c);
- __gmpz_clear(__gen_e_acsl_u_12);
+ __gmpz_clear(__gen_e_acsl_u_13);
}
float f = 1.0f;
__e_acsl_store_block((void *)(& f),(size_t)4);
__e_acsl_full_init((void *)(& f));
/*@ assert \let u = f; u ≡ f; */
{
- float __gen_e_acsl_u_13;
- __gen_e_acsl_u_13 = f;
- __e_acsl_assert(__gen_e_acsl_u_13 == f,(char *)"Assertion",
+ float __gen_e_acsl_u_14;
+ __gen_e_acsl_u_14 = f;
+ __e_acsl_assert(__gen_e_acsl_u_14 == f,(char *)"Assertion",
(char *)"main",(char *)"\\let u = f; u == f",27);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
{
- int * /*[4]*/ __gen_e_acsl_u_14;
- __e_acsl_mpz_t __gen_e_acsl__11;
+ int * /*[4]*/ __gen_e_acsl_u_15;
+ __e_acsl_mpz_t __gen_e_acsl__10;
int __gen_e_acsl_eq_4;
- __gen_e_acsl_u_14 = & t[1];
- __gmpz_init_set_si(__gen_e_acsl__11,1L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gen_e_acsl_u_15 = & t[1];
+ __gmpz_init_set_si(__gen_e_acsl__10,1L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let u = &t[1]; 1 == 1",30);
- __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl__10);
}
/*@ assert (\let u = &t[1]; 1) ≡ 1; */
{
- int * /*[4]*/ __gen_e_acsl_u_15;
- __gen_e_acsl_u_15 = & t[1];
+ int * /*[4]*/ __gen_e_acsl_u_16;
+ __gen_e_acsl_u_16 = & t[1];
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(\\let u = &t[1]; 1) == 1",32);
}
@@ -237,35 +237,35 @@ int main(void)
__e_acsl_full_init((void *)(& r));
/*@ assert \let u = r; u.x + u.y ≡ 3; */
{
- struct __anonstruct_r_1 __gen_e_acsl_u_16;
+ struct __anonstruct_r_1 __gen_e_acsl_u_17;
+ __e_acsl_mpz_t __gen_e_acsl__11;
__e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl__13;
__e_acsl_mpz_t __gen_e_acsl_add_5;
- __e_acsl_mpz_t __gen_e_acsl__14;
+ __e_acsl_mpz_t __gen_e_acsl__13;
int __gen_e_acsl_eq_5;
- __gen_e_acsl_u_16 = r;
- __gmpz_init_set_si(__gen_e_acsl__12,(long)__gen_e_acsl_u_16.x);
- __gmpz_init_set_si(__gen_e_acsl__13,(long)__gen_e_acsl_u_16.y);
+ __gen_e_acsl_u_17 = r;
+ __gmpz_init_set_si(__gen_e_acsl__11,(long)__gen_e_acsl_u_17.x);
+ __gmpz_init_set_si(__gen_e_acsl__12,(long)__gen_e_acsl_u_17.y);
__gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
- __gmpz_init_set_si(__gen_e_acsl__14,3L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_init_set_si(__gen_e_acsl__13,3L);
__gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let u = r; u.x + u.y == 3",35);
+ __gmpz_clear(__gen_e_acsl__11);
__gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl__13);
__gmpz_clear(__gen_e_acsl_add_5);
- __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl__13);
}
s.x = 5;
/*@ assert (\let u = s; u.x) > 0; */
{
- union __anonunion_s_2 __gen_e_acsl_u_17;
- __gen_e_acsl_u_17 = s;
- __e_acsl_assert(__gen_e_acsl_u_17.x > 0,(char *)"Assertion",
+ union __anonunion_s_2 __gen_e_acsl_u_18;
+ __gen_e_acsl_u_18 = s;
+ __e_acsl_assert(__gen_e_acsl_u_18.x > 0,(char *)"Assertion",
(char *)"main",(char *)"(\\let u = s; u.x) > 0",39);
}
__retres = 0;
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index e1115ea839a39602c767ea1ade28fa445a9f4e70..67c14e38f65f239a8c54deb7f040c960c7689447 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -477,7 +477,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
infer_if_integer li;
let li_t = Misc.term_of_li li in
ignore (type_term ~use_gmp_opt:true li_t);
- dup (type_term ~use_gmp_opt:true t).ty
+ dup (type_term ~use_gmp_opt:true ?ctx t).ty
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"