diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index f26cb8fa5f1069e757cab8767ebfc5a128e5970f..b2f47a295b54b1d2d1d62a8871a4d47a2fa7afae 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -168,15 +168,22 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let ty2 = Typing.get_integer_ty t2 in
Typing.join ty1 ty2
in
- let t_plus_one t =
- Logic_const.term ~loc
- (TBinOp(PlusA, t, Logic_const.tinteger ~loc 1))
- Linteger
+ let t_plus_one ?ty t =
+ (* whenever provided, [ty] is known to be the type of the result *)
+ let tone = Logic_const.tinteger ~loc 1 in
+ let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
+ Extlib.may
+ (fun ty ->
+ Typing.unsafe_set tone ~ctx:ty ctx;
+ Typing.unsafe_set t ~ctx:ty ctx;
+ Typing.unsafe_set res ty)
+ ty;
+ res
in
let t1 = match rel1 with
| Rlt ->
let t = t_plus_one t1 in
- Typing.type_term ~force:true ~ctx t;
+ Typing.type_term ~use_gmp_opt:false ~ctx t;
t
| Rle -> t1
| Rgt | Rge | Req | Rneq -> assert false
@@ -190,7 +197,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
t_plus_one t2, Le
| Rgt | Rge | Req | Rneq -> assert false
in
- Typing.type_term ~force:true ~ctx t2_one;
+ Typing.type_term ~use_gmp_opt:false ~ctx t2_one;
let ctx_one =
let ty1 = Typing.get_integer_ty t1 in
let ty2 = Typing.get_integer_ty t2_one in
@@ -227,7 +234,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
Logic_const.term ~loc
(TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
in
- Typing.type_term ~force:true ~ctx:Typing.c_int guard;
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
let guard_blk, env =
@@ -242,10 +249,11 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
Env.Middle
in
let guard = stmts_block guard_blk in
- (* increment the loop counter [x++] *)
- let tlv_one = t_plus_one tlv in
- (* previous typing ensures that [x++] fits type [ty] *)
- Typing.type_term ~force:true ~ctx:ctx_one tlv_one;
+ (* increment the loop counter [x++];
+ previous typing ensures that [x++] fits type [ty] *)
+ (* TODO: should check that it does not overflow in the case of the type
+ of the loop variable is __declared__ too small. *)
+ let tlv_one = t_plus_one ~ty:ctx_one tlv in
let incr, env = term_to_exp kf (Env.push env) tlv_one in
let next_blk, env =
Env.pop_and_get
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 8a6f07863a3509b04d10f3086c74b4274174195b..008592aabeed2842471bb758a83c77769f90ccee 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -100,7 +100,7 @@ int __gen_e_acsl_sorted(int *t, int n)
goto e_acsl_end_loop1;
}
}
- __gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
+ __gen_e_acsl_i ++;
}
e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_forall;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index cd49f58f7fe5da25d10664226c2abb5e4368a0e0..a61c60c0e7edf9e6865995aa56fd410305a5d1d7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
@@ -3,6 +3,7 @@
int main(void)
{
int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
/*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
{
{
@@ -204,7 +205,157 @@ int main(void)
25);
}
}
+ {
+ int buf[10];
+ unsigned long len;
+ __e_acsl_store_block((void *)(buf),(size_t)40);
+ len = (unsigned long)9;
+ /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_7;
+ int __gen_e_acsl_i;
+ __gen_e_acsl_forall_7 = 1;
+ __gen_e_acsl_i = 0;
+ while (1) {
+ if (__gen_e_acsl_i < 10) ; else break;
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i]),
+ sizeof(int));
+ if (__gen_e_acsl_valid) ;
+ else {
+ __gen_e_acsl_forall_7 = 0;
+ goto e_acsl_end_loop9;
+ }
+ }
+ __gen_e_acsl_i ++;
+ }
+ e_acsl_end_loop9: ;
+ __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
+ 31);
+ }
+ }
+ /*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_8;
+ int __gen_e_acsl_i_2;
+ __gen_e_acsl_forall_8 = 1;
+ __gen_e_acsl_i_2 = (char)0;
+ while (1) {
+ if (__gen_e_acsl_i_2 < 10) ; else break;
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
+ sizeof(int));
+ if (__gen_e_acsl_valid_2) ;
+ else {
+ __gen_e_acsl_forall_8 = 0;
+ goto e_acsl_end_loop10;
+ }
+ }
+ __gen_e_acsl_i_2 ++;
+ }
+ e_acsl_end_loop10: ;
+ __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
+ 32);
+ }
+ }
+ /*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_9;
+ unsigned long __gen_e_acsl_i_3;
+ __gen_e_acsl_forall_9 = 1;
+ __gen_e_acsl_i_3 = 0UL;
+ while (1) {
+ if (__gen_e_acsl_i_3 < len) ; else break;
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_3]),
+ sizeof(int));
+ if (__gen_e_acsl_valid_3) ;
+ else {
+ __gen_e_acsl_forall_9 = 0;
+ goto e_acsl_end_loop11;
+ }
+ }
+ __gen_e_acsl_i_3 ++;
+ }
+ e_acsl_end_loop11: ;
+ __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
+ 33);
+ }
+ }
+ /*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_10;
+ __e_acsl_mpz_t __gen_e_acsl_i_4;
+ __gen_e_acsl_forall_10 = 1;
+ __gmpz_init(__gen_e_acsl_i_4);
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_set(__gen_e_acsl_i_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl_len;
+ int __gen_e_acsl_le;
+ __gmpz_init_set_ui(__gen_e_acsl_len,len);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_len));
+ if (__gen_e_acsl_le <= 0) ; else break;
+ __gmpz_clear(__gen_e_acsl_len);
+ }
+ {
+ long __gen_e_acsl_i_5;
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_i_5 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_5]),
+ sizeof(int));
+ if (__gen_e_acsl_valid_4) ;
+ else {
+ __gen_e_acsl_forall_10 = 0;
+ goto e_acsl_end_loop12;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gmpz_init_set_ui(__gen_e_acsl__2,1UL);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_set(__gen_e_acsl_i_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ }
+ e_acsl_end_loop12: ;
+ __e_acsl_assert(__gen_e_acsl_forall_10,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
+ 34);
+ __gmpz_clear(__gen_e_acsl_i_4);
+ __e_acsl_delete_block((void *)(buf));
+ }
+ }
+ }
__retres = 0;
+ __e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index 558fad0101c191e4585932d3e2b3a735b10dc670..1844eec87e0b99e77998499b3d0fdd1167959348 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -3,6 +3,7 @@
int main(void)
{
int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
/*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
{
{
@@ -54,7 +55,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__5;
__e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set_str(__gen_e_acsl__5,"1",10);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
@@ -121,7 +122,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__10;
__e_acsl_mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set_si(__gen_e_acsl__10,1L);
+ __gmpz_init_set_str(__gen_e_acsl__10,"1",10);
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
@@ -180,7 +181,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__14;
__e_acsl_mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set_si(__gen_e_acsl__14,1L);
+ __gmpz_init_set_str(__gen_e_acsl__14,"1",10);
__gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
@@ -238,7 +239,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__18;
__e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init_set_si(__gen_e_acsl__18,1L);
+ __gmpz_init_set_str(__gen_e_acsl__18,"1",10);
__gmpz_init(__gen_e_acsl_add_6);
__gmpz_add(__gen_e_acsl_add_6,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
@@ -346,7 +347,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__21;
__e_acsl_mpz_t __gen_e_acsl_add_9;
- __gmpz_init_set_si(__gen_e_acsl__21,1L);
+ __gmpz_init_set_str(__gen_e_acsl__21,"1",10);
__gmpz_init(__gen_e_acsl_add_9);
__gmpz_add(__gen_e_acsl_add_9,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_z),
@@ -360,7 +361,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__24;
__e_acsl_mpz_t __gen_e_acsl_add_10;
- __gmpz_init_set_si(__gen_e_acsl__24,1L);
+ __gmpz_init_set_str(__gen_e_acsl__24,"1",10);
__gmpz_init(__gen_e_acsl_add_10);
__gmpz_add(__gen_e_acsl_add_10,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y),
@@ -374,7 +375,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__27;
__e_acsl_mpz_t __gen_e_acsl_add_11;
- __gmpz_init_set_si(__gen_e_acsl__27,1L);
+ __gmpz_init_set_str(__gen_e_acsl__27,"1",10);
__gmpz_init(__gen_e_acsl_add_11);
__gmpz_add(__gen_e_acsl_add_11,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
@@ -402,16 +403,22 @@ int main(void)
__e_acsl_mpz_t __gen_e_acsl_x_6;
__gen_e_acsl_exists = 0;
__gmpz_init(__gen_e_acsl_x_6);
- __gmpz_set_si(__gen_e_acsl_x_6,0L);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__29;
+ __gmpz_init_set_si(__gen_e_acsl__29,0L);
+ __gmpz_set(__gen_e_acsl_x_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
+ __gmpz_clear(__gen_e_acsl__29);
+ }
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__29;
+ __e_acsl_mpz_t __gen_e_acsl__30;
int __gen_e_acsl_lt_5;
- __gmpz_init_set_si(__gen_e_acsl__29,10L);
+ __gmpz_init_set_si(__gen_e_acsl__30,10L);
__gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
if (__gen_e_acsl_lt_5 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__29);
+ __gmpz_clear(__gen_e_acsl__30);
}
{
__e_acsl_mpz_t __gen_e_acsl__28;
@@ -427,16 +434,16 @@ int main(void)
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__30;
+ __e_acsl_mpz_t __gen_e_acsl__31;
__e_acsl_mpz_t __gen_e_acsl_add_12;
- __gmpz_init_set_si(__gen_e_acsl__30,1L);
+ __gmpz_init_set_str(__gen_e_acsl__31,"1",10);
__gmpz_init(__gen_e_acsl_add_12);
__gmpz_add(__gen_e_acsl_add_12,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
__gmpz_set(__gen_e_acsl_x_6,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
- __gmpz_clear(__gen_e_acsl__30);
+ __gmpz_clear(__gen_e_acsl__31);
__gmpz_clear(__gen_e_acsl_add_12);
}
}
@@ -457,28 +464,34 @@ int main(void)
__e_acsl_mpz_t __gen_e_acsl_x_7;
__gen_e_acsl_forall_6 = 1;
__gmpz_init(__gen_e_acsl_x_7);
- __gmpz_set_si(__gen_e_acsl_x_7,0L);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__39;
+ __gmpz_init_set_si(__gen_e_acsl__39,0L);
+ __gmpz_set(__gen_e_acsl_x_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
+ __gmpz_clear(__gen_e_acsl__39);
+ }
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__38;
+ __e_acsl_mpz_t __gen_e_acsl__40;
int __gen_e_acsl_lt_6;
- __gmpz_init_set_si(__gen_e_acsl__38,10L);
+ __gmpz_init_set_si(__gen_e_acsl__40,10L);
__gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
if (__gen_e_acsl_lt_6 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__38);
+ __gmpz_clear(__gen_e_acsl__40);
}
{
- __e_acsl_mpz_t __gen_e_acsl__31;
__e_acsl_mpz_t __gen_e_acsl__32;
+ __e_acsl_mpz_t __gen_e_acsl__33;
int __gen_e_acsl_mod_guard;
__e_acsl_mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq_6;
int __gen_e_acsl_implies;
- __gmpz_init_set_si(__gen_e_acsl__31,2L);
- __gmpz_init_set_si(__gen_e_acsl__32,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__31),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ __gmpz_init_set_si(__gen_e_acsl__32,2L);
+ __gmpz_init_set_si(__gen_e_acsl__33,0L);
+ __gen_e_acsl_mod_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__32),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),
@@ -486,9 +499,9 @@ int main(void)
(char *)"2 == 0",26);
__gmpz_tdiv_r(__gen_e_acsl_mod,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mod),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
if (! (__gen_e_acsl_eq_6 == 0)) __gen_e_acsl_implies = 1;
else {
int __gen_e_acsl_exists_2;
@@ -496,23 +509,23 @@ int main(void)
__gen_e_acsl_exists_2 = 0;
__gmpz_init(__gen_e_acsl_y_2);
{
- __e_acsl_mpz_t __gen_e_acsl__34;
- __gmpz_init_set_si(__gen_e_acsl__34,0L);
+ __e_acsl_mpz_t __gen_e_acsl__35;
+ __gmpz_init_set_si(__gen_e_acsl__35,0L);
__gmpz_set(__gen_e_acsl_y_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
- __gmpz_clear(__gen_e_acsl__34);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__35));
+ __gmpz_clear(__gen_e_acsl__35);
}
while (1) {
{
- __e_acsl_mpz_t __gen_e_acsl__35;
__e_acsl_mpz_t __gen_e_acsl__36;
+ __e_acsl_mpz_t __gen_e_acsl__37;
int __gen_e_acsl_div_guard;
__e_acsl_mpz_t __gen_e_acsl_div;
int __gen_e_acsl_le_5;
- __gmpz_init_set_si(__gen_e_acsl__35,2L);
- __gmpz_init_set_si(__gen_e_acsl__36,0L);
- __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__35),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
+ __gmpz_init_set_si(__gen_e_acsl__36,2L);
+ __gmpz_init_set_si(__gen_e_acsl__37,0L);
+ __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__36),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard == 0),
@@ -520,26 +533,26 @@ int main(void)
(char *)"2 == 0",26);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__35));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
__gen_e_acsl_le_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
if (__gen_e_acsl_le_5 <= 0) ; else break;
- __gmpz_clear(__gen_e_acsl__35);
__gmpz_clear(__gen_e_acsl__36);
+ __gmpz_clear(__gen_e_acsl__37);
__gmpz_clear(__gen_e_acsl_div);
}
{
- __e_acsl_mpz_t __gen_e_acsl__33;
+ __e_acsl_mpz_t __gen_e_acsl__34;
__e_acsl_mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_eq_7;
- __gmpz_init_set_si(__gen_e_acsl__33,2L);
+ __gmpz_init_set_si(__gen_e_acsl__34,2L);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__34),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
__gen_e_acsl_eq_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __gmpz_clear(__gen_e_acsl__33);
+ __gmpz_clear(__gen_e_acsl__34);
__gmpz_clear(__gen_e_acsl_mul);
if (! (__gen_e_acsl_eq_7 == 0)) ;
else {
@@ -548,16 +561,16 @@ int main(void)
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__37;
+ __e_acsl_mpz_t __gen_e_acsl__38;
__e_acsl_mpz_t __gen_e_acsl_add_13;
- __gmpz_init_set_si(__gen_e_acsl__37,1L);
+ __gmpz_init_set_str(__gen_e_acsl__38,"1",10);
__gmpz_init(__gen_e_acsl_add_13);
__gmpz_add(__gen_e_acsl_add_13,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
__gmpz_set(__gen_e_acsl_y_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_13));
- __gmpz_clear(__gen_e_acsl__37);
+ __gmpz_clear(__gen_e_acsl__38);
__gmpz_clear(__gen_e_acsl_add_13);
}
}
@@ -565,8 +578,8 @@ int main(void)
__gen_e_acsl_implies = __gen_e_acsl_exists_2;
__gmpz_clear(__gen_e_acsl_y_2);
}
- __gmpz_clear(__gen_e_acsl__31);
__gmpz_clear(__gen_e_acsl__32);
+ __gmpz_clear(__gen_e_acsl__33);
__gmpz_clear(__gen_e_acsl_mod);
if (__gen_e_acsl_implies) ;
else {
@@ -575,16 +588,16 @@ int main(void)
}
}
{
- __e_acsl_mpz_t __gen_e_acsl__39;
+ __e_acsl_mpz_t __gen_e_acsl__41;
__e_acsl_mpz_t __gen_e_acsl_add_14;
- __gmpz_init_set_si(__gen_e_acsl__39,1L);
+ __gmpz_init_set_str(__gen_e_acsl__41,"1",10);
__gmpz_init(__gen_e_acsl_add_14);
__gmpz_add(__gen_e_acsl_add_14,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__41));
__gmpz_set(__gen_e_acsl_x_7,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_14));
- __gmpz_clear(__gen_e_acsl__39);
+ __gmpz_clear(__gen_e_acsl__41);
__gmpz_clear(__gen_e_acsl_add_14);
}
}
@@ -596,7 +609,247 @@ int main(void)
__gmpz_clear(__gen_e_acsl_x_7);
}
}
+ {
+ int buf[10];
+ unsigned long len;
+ __e_acsl_store_block((void *)(buf),(size_t)40);
+ len = (unsigned long)9;
+ /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_7;
+ __e_acsl_mpz_t __gen_e_acsl_i;
+ __gen_e_acsl_forall_7 = 1;
+ __gmpz_init(__gen_e_acsl_i);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__42;
+ __gmpz_init_set_si(__gen_e_acsl__42,0L);
+ __gmpz_set(__gen_e_acsl_i,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__42));
+ __gmpz_clear(__gen_e_acsl__42);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__43;
+ int __gen_e_acsl_lt_7;
+ __gmpz_init_set_si(__gen_e_acsl__43,10L);
+ __gen_e_acsl_lt_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__43));
+ if (__gen_e_acsl_lt_7 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__43);
+ }
+ {
+ long __gen_e_acsl_i_2;
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
+ sizeof(int));
+ if (__gen_e_acsl_valid) ;
+ else {
+ __gen_e_acsl_forall_7 = 0;
+ goto e_acsl_end_loop9;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl__44;
+ __e_acsl_mpz_t __gen_e_acsl_add_15;
+ __gmpz_init_set_str(__gen_e_acsl__44,"1",10);
+ __gmpz_init(__gen_e_acsl_add_15);
+ __gmpz_add(__gen_e_acsl_add_15,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__44));
+ __gmpz_set(__gen_e_acsl_i,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_15));
+ __gmpz_clear(__gen_e_acsl__44);
+ __gmpz_clear(__gen_e_acsl_add_15);
+ }
+ }
+ e_acsl_end_loop9: ;
+ __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
+ 31);
+ __gmpz_clear(__gen_e_acsl_i);
+ }
+ }
+ /*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_8;
+ __e_acsl_mpz_t __gen_e_acsl_i_3;
+ __gen_e_acsl_forall_8 = 1;
+ __gmpz_init(__gen_e_acsl_i_3);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__45;
+ __gmpz_init_set_si(__gen_e_acsl__45,0L);
+ __gmpz_set(__gen_e_acsl_i_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__45));
+ __gmpz_clear(__gen_e_acsl__45);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__46;
+ int __gen_e_acsl_lt_8;
+ __gmpz_init_set_si(__gen_e_acsl__46,10L);
+ __gen_e_acsl_lt_8 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__46));
+ if (__gen_e_acsl_lt_8 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__46);
+ }
+ {
+ long __gen_e_acsl_i_4;
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_i_4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3));
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_4]),
+ sizeof(int));
+ if (__gen_e_acsl_valid_2) ;
+ else {
+ __gen_e_acsl_forall_8 = 0;
+ goto e_acsl_end_loop10;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl__47;
+ __e_acsl_mpz_t __gen_e_acsl_add_16;
+ __gmpz_init_set_str(__gen_e_acsl__47,"1",10);
+ __gmpz_init(__gen_e_acsl_add_16);
+ __gmpz_add(__gen_e_acsl_add_16,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__47));
+ __gmpz_set(__gen_e_acsl_i_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_16));
+ __gmpz_clear(__gen_e_acsl__47);
+ __gmpz_clear(__gen_e_acsl_add_16);
+ }
+ }
+ e_acsl_end_loop10: ;
+ __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
+ 32);
+ __gmpz_clear(__gen_e_acsl_i_3);
+ }
+ }
+ /*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_9;
+ __e_acsl_mpz_t __gen_e_acsl_i_5;
+ __gen_e_acsl_forall_9 = 1;
+ __gmpz_init(__gen_e_acsl_i_5);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__48;
+ __gmpz_init_set_si(__gen_e_acsl__48,0L);
+ __gmpz_set(__gen_e_acsl_i_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__48));
+ __gmpz_clear(__gen_e_acsl__48);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl_len;
+ int __gen_e_acsl_lt_9;
+ __gmpz_init_set_ui(__gen_e_acsl_len,len);
+ __gen_e_acsl_lt_9 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_len));
+ if (__gen_e_acsl_lt_9 < 0) ; else break;
+ __gmpz_clear(__gen_e_acsl_len);
+ }
+ {
+ long __gen_e_acsl_i_6;
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_i_6 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5));
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_6]),
+ sizeof(int));
+ if (__gen_e_acsl_valid_3) ;
+ else {
+ __gen_e_acsl_forall_9 = 0;
+ goto e_acsl_end_loop11;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl__49;
+ __e_acsl_mpz_t __gen_e_acsl_add_17;
+ __gmpz_init_set_str(__gen_e_acsl__49,"1",10);
+ __gmpz_init(__gen_e_acsl_add_17);
+ __gmpz_add(__gen_e_acsl_add_17,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__49));
+ __gmpz_set(__gen_e_acsl_i_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_17));
+ __gmpz_clear(__gen_e_acsl__49);
+ __gmpz_clear(__gen_e_acsl_add_17);
+ }
+ }
+ e_acsl_end_loop11: ;
+ __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
+ 33);
+ __gmpz_clear(__gen_e_acsl_i_5);
+ }
+ }
+ /*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */
+ {
+ {
+ int __gen_e_acsl_forall_10;
+ __e_acsl_mpz_t __gen_e_acsl_i_7;
+ __gen_e_acsl_forall_10 = 1;
+ __gmpz_init(__gen_e_acsl_i_7);
+ {
+ __e_acsl_mpz_t __gen_e_acsl__50;
+ __gmpz_init_set_si(__gen_e_acsl__50,0L);
+ __gmpz_set(__gen_e_acsl_i_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__50));
+ __gmpz_clear(__gen_e_acsl__50);
+ }
+ while (1) {
+ {
+ __e_acsl_mpz_t __gen_e_acsl_len_2;
+ int __gen_e_acsl_le_6;
+ __gmpz_init_set_ui(__gen_e_acsl_len_2,len);
+ __gen_e_acsl_le_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_len_2));
+ if (__gen_e_acsl_le_6 <= 0) ; else break;
+ __gmpz_clear(__gen_e_acsl_len_2);
+ }
+ {
+ long __gen_e_acsl_i_8;
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_i_8 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7));
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_8]),
+ sizeof(int));
+ if (__gen_e_acsl_valid_4) ;
+ else {
+ __gen_e_acsl_forall_10 = 0;
+ goto e_acsl_end_loop12;
+ }
+ }
+ {
+ __e_acsl_mpz_t __gen_e_acsl__51;
+ __e_acsl_mpz_t __gen_e_acsl_add_18;
+ __gmpz_init_set_str(__gen_e_acsl__51,"1",10);
+ __gmpz_init(__gen_e_acsl_add_18);
+ __gmpz_add(__gen_e_acsl_add_18,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__51));
+ __gmpz_set(__gen_e_acsl_i_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_18));
+ __gmpz_clear(__gen_e_acsl__51);
+ __gmpz_clear(__gen_e_acsl_add_18);
+ }
+ }
+ e_acsl_end_loop12: ;
+ __e_acsl_assert(__gen_e_acsl_forall_10,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
+ 34);
+ __gmpz_clear(__gen_e_acsl_i_7);
+ __e_acsl_delete_block((void *)(buf));
+ }
+ }
+ }
__retres = 0;
+ __e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index ee86d9b6561cfff2f17d329fead0cbc47374e9c9..41b697aacc33ddd7e3ee3e2691b332c8debeebb9 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
@@ -14,6 +14,7 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns cl
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:9:[value] entering loop for the first time
[value] using specification for function __e_acsl_assert
@@ -31,4 +32,23 @@ tests/gmp/quantif.i:21:[value] entering loop for the first time
tests/gmp/quantif.i:25:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:25:[value] entering loop for the first time
tests/gmp/quantif.i:26:[value] entering loop for the first time
+[value] using specification for function __e_acsl_store_block
+tests/gmp/quantif.i:31:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:31:[value] entering loop for the first time
+[value] using specification for function __e_acsl_valid
+tests/gmp/quantif.i:32:[value] entering loop for the first time
+tests/gmp/quantif.i:33:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:33:[value] entering loop for the first time
+tests/gmp/quantif.i:34:[value] warning: assertion got status unknown.
+[value] using specification for function __gmpz_init
+[value] using specification for function __gmpz_init_set_si
+[value] using specification for function __gmpz_set
+[value] using specification for function __gmpz_clear
+tests/gmp/quantif.i:34:[value] entering loop for the first time
+[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_cmp
+[value] using specification for function __gmpz_get_si
+[value] using specification for function __gmpz_add
+[value] using specification for function __e_acsl_delete_block
+[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 5621b6492094bee92e8d32387de31f6ec5b785fa..fa5c3f60b290d2f10c3e019e0baf0e7a254a5cec 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -14,6 +14,7 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns cl
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_init_set_si
@@ -21,6 +22,7 @@ tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_clear
tests/gmp/quantif.i:9:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
+[value] using specification for function __gmpz_init_set_str
[value] using specification for function __gmpz_add
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
@@ -33,7 +35,6 @@ tests/gmp/quantif.i:12:[value] entering loop for the first time
tests/gmp/quantif.i:16:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:16:[value] entering loop for the first time
tests/gmp/quantif.i:21:[value] warning: assertion got status unknown.
-[value] using specification for function __gmpz_set_si
tests/gmp/quantif.i:21:[value] entering loop for the first time
tests/gmp/quantif.i:25:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:25:[value] entering loop for the first time
@@ -41,4 +42,17 @@ tests/gmp/quantif.i:25:[value] entering loop for the first time
tests/gmp/quantif.i:26:[value] entering loop for the first time
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_mul
+[value] using specification for function __e_acsl_store_block
+tests/gmp/quantif.i:31:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:31:[value] entering loop for the first time
+[value] using specification for function __gmpz_get_si
+[value] using specification for function __e_acsl_valid
+tests/gmp/quantif.i:32:[value] entering loop for the first time
+tests/gmp/quantif.i:33:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:33:[value] entering loop for the first time
+[value] using specification for function __gmpz_init_set_ui
+tests/gmp/quantif.i:34:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:34:[value] entering loop for the first time
+[value] using specification for function __e_acsl_delete_block
+[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/quantif.i b/src/plugins/e-acsl/tests/gmp/quantif.i
index 81531e338c23effc5ed53ecdcf3504258c150eb0..3a32e9a36b0a614127a7fce5585cecb41b64cfc6 100644
--- a/src/plugins/e-acsl/tests/gmp/quantif.i
+++ b/src/plugins/e-acsl/tests/gmp/quantif.i
@@ -25,5 +25,14 @@ int main(void) {
/*@ assert \forall int x; 0 <= x < 10
==> x % 2 == 0 ==> \exists integer y; 0 <= y <= x/2 && x == 2 * y; */
+ { // Gitlab issue #42
+ int buf[10];
+ unsigned long len = 9;
+ /*@ assert \forall integer i; 0 <= i < 10 ==> \valid(buf+i); */
+ /*@ assert \forall char i; 0 <= i < 10 ==> \valid(buf+i); */
+ /*@ assert \forall integer i; 0 <= i < len ==> \valid(buf+i); */
+ /*@ assert \forall integer i; 0 <= i <= len ==> \valid(buf+i); */
+ }
+
return 0;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 40d9186eb2fbdfc076b9b92e8abe4f44f43bfef1..f14c31ae5e7843325ad18b19b4f635b0e2363afc 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -46,7 +46,7 @@ int search(int elt)
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop1;
}
- __gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
+ __gen_e_acsl_i ++;
}
e_acsl_end_loop1: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",
@@ -93,7 +93,7 @@ int search(int elt)
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop2;
}
- __gen_e_acsl_i_2 = (int)(__gen_e_acsl_i_2 + 1L);
+ __gen_e_acsl_i_2 ++;
}
e_acsl_end_loop2: ;
__e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Invariant",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index 11048b4a56331b283cf2683c65fc5b836646bd3c..765047ff16e0e909eb56009920a832a684b0e1c1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -45,7 +45,7 @@ int main(int argc, char **argv)
goto e_acsl_end_loop1;
}
}
- __gen_e_acsl_k = (int)(__gen_e_acsl_k + 1L);
+ __gen_e_acsl_k ++;
}
e_acsl_end_loop1: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index b5229db0c78d4b229abf19aa1b8e9c8103d98280..d56b16f3667f0037ce4911fe0e6e254dd6fb1cf4 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -304,7 +304,7 @@ and context_insensitive_term_to_exp kf env t =
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
let ctx = Typing.get_integer_ty t in
- Typing.type_term ~force:false ~ctx zero;
+ Typing.type_term ~use_gmp_opt:true ~ctx zero;
let e, env =
comparison_to_exp kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
in
@@ -348,7 +348,7 @@ and context_insensitive_term_to_exp kf env t =
possible values of [t2] *)
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger 0 in
- Typing.type_term ~force:false ~ctx zero;
+ Typing.type_term ~use_gmp_opt:true ~ctx zero;
(* do not generate [e2] from [t2] twice *)
let guard, env =
let name = name_of_binop bop ^ "_guard" in
@@ -825,7 +825,7 @@ let term_to_exp typ t =
| _ -> Typing.other
in
let ctx = Extlib.opt_map ctx_of_typ typ in
- Typing.type_term ~force:false ?ctx t;
+ Typing.type_term ~use_gmp_opt:true ?ctx t;
let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
let env = Env.push env in
let env = Env.rte env false in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index d2b5849b6adb83a30c986172b19d0afd412c8efc..d71a6fb663415f330e304cff3731dff8d3a46e29 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -73,15 +73,14 @@ include Datatype.Make
(** Basic operations *)
(******************************************************************************)
-let join ty1 ty2 =
- if Options.Gmp_only.get () then Gmp
- else
- match ty1, ty2 with
- | Other, Other -> Other
- | Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
- Options.fatal "[typing] join failure: integer and non integer type"
- | Gmp, _ | _, Gmp -> Gmp
- | C_type i1, C_type i2 ->
+let join ty1 ty2 = match ty1, ty2 with
+ | Other, Other -> Other
+ | Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
+ Options.fatal "[typing] join failure: integer and non integer type"
+ | Gmp, _ | _, Gmp -> Gmp
+ | C_type i1, C_type i2 ->
+ if Options.Gmp_only.get () then Gmp
+ else
let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
match ty with
| TInt(i, _) -> C_type i
@@ -179,7 +178,9 @@ let ty_of_interv ?ctx i =
let ukind = Cil.intKindForValue u is_pos in
(* kind corresponding to the interval *)
if Cil.intTypeIncluded lkind ukind then ukind else lkind
- | _, _ -> Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+ | None, None -> raise Cil.Not_representable (* GMP *)
+ | None, Some _ | Some _, None ->
+ Kernel.fatal ~current:true "ival: %a" Ival.pretty i
in
(* convert the kind to [IInt] whenever smaller. *)
let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
@@ -224,18 +225,16 @@ let offset_ty t =
(** {2 Type system} *)
(******************************************************************************)
-(* generate a context [c]. Take --e-acsl-gmp-only into account iff not
- [force]. *)
-let mk_ctx ~force c =
- if force then c
- else match c with
- | Other -> Other
- | Gmp | C_type _ -> if Options.Gmp_only.get () then Gmp else c
-
-(* type the term [t] in a context [ctx]. Take --e-acsl-gmp-only into account iff
- not [force]. *)
-let rec type_term ~force ?(arith_operand=false) ?ctx t =
- let ctx = Extlib.opt_map (mk_ctx ~force) ctx in
+(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
+ is true. *)
+let mk_ctx ~use_gmp_opt = function
+ | Other | Gmp as c -> c
+ | C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmp else c
+
+(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
+ iff [use_gmp_opt] is true. *)
+let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
+ let ctx = Extlib.opt_map (mk_ctx ~use_gmp_opt) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
(* in order to get a minimal amount of generated casts for operators, the
@@ -244,10 +243,10 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
match ctx with
| None ->
(* no context: factorize *)
- dup (mk_ctx ~force:false (ty_of_interv i))
+ dup (mk_ctx ~use_gmp_opt:true (ty_of_interv i))
| Some ctx ->
- mk_ctx ~force:false (ty_of_interv ~ctx i),
- mk_ctx ~force:false (ty_of_interv i)
+ mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx i),
+ mk_ctx ~use_gmp_opt:true (ty_of_interv i)
in
let infer t =
Cil.CurrentLoc.set t.term_loc;
@@ -286,7 +285,7 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
try
let i = Interval.infer t in
(* [t'] must be typed, but it is a pointer *)
- ignore (type_term ~force:false ~ctx:Other t');
+ ignore (type_term ~use_gmp_opt:true ~ctx:Other t');
ty_of_interv ?ctx i
with Interval.Not_an_integer ->
assert false (* this term is an integer *)
@@ -298,8 +297,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
try
let i = Interval.infer t in
(* [t1] and [t2] must be typed, but they are pointers *)
- ignore (type_term ~force:false ~ctx:Other t1);
- ignore (type_term ~force:false ~ctx:Other t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Other t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Other t2);
ty_of_interv ?ctx i
with Interval.Not_an_integer ->
assert false (* this term is an integer *)
@@ -315,7 +314,7 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
- ignore (type_term ~force ~arith_operand:true ~ctx t');
+ ignore (type_term ~use_gmp_opt:true ~arith_operand:true ~ctx t');
(match unop with
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx_res)
@@ -340,8 +339,9 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
| _ -> true
in
let cast_first = cast_first t1 t2 in
- ignore (type_term ~force ~arith_operand:cast_first ~ctx t1);
- ignore (type_term ~force ~arith_operand:(not cast_first) ~ctx t2);
+ ignore (type_term ~use_gmp_opt:true ~arith_operand:cast_first ~ctx t1);
+ ignore
+ (type_term ~use_gmp_opt:true ~arith_operand:(not cast_first) ~ctx t2);
dup ctx_res
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
@@ -350,12 +350,12 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
try
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
- mk_ctx ~force:false (ty_of_interv ?ctx (Ival.join i1 i2))
+ mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Ival.join i1 i2))
with Interval.Not_an_integer ->
Other
in
- ignore (type_term ~force:false ~ctx t1);
- ignore (type_term ~force:false ~ctx t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx t2);
let ty = match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx
@@ -372,8 +372,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
Other
in
(* both operands fit in an int. *)
- ignore (type_term ~force:false ~ctx:c_int t1);
- ignore (type_term ~force:false ~ctx:c_int t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx:c_int t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:c_int t2);
dup ty
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
@@ -392,28 +392,31 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
Other
in
- ignore (type_term ~force:false ~ctx t');
+ ignore (type_term ~use_gmp_opt:true ~ctx t');
dup ctx
| Tif (t1, t2, t3) ->
- let ctx1 = mk_ctx ~force:true c_int (* an int must be generated *) in
- ignore (type_term ~force:true ~ctx:ctx1 t1);
+ let ctx1 =
+ mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
+ in
+ ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 t1);
let i = Interval.infer t in
let ctx =
try
let i2 = Interval.infer t2 in
let i3 = Interval.infer t3 in
let ctx = ty_of_interv ?ctx (Ival.join i (Ival.join i2 i3)) in
- mk_ctx ~force:false ctx
+ mk_ctx ~use_gmp_opt:true ctx
with Interval.Not_an_integer ->
Other
in
- ignore (type_term ~force:false ~ctx t2);
- ignore (type_term ~force:false ~ctx t3);
+ ignore (type_term ~use_gmp_opt:true ~ctx t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx t3);
dup ctx
| Tat (t, _)
- | TLogic_coerce (_, t) -> dup (type_term ~force ~arith_operand ?ctx t).ty
+ | TLogic_coerce (_, t) ->
+ dup (type_term ~use_gmp_opt ~arith_operand ?ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
@@ -425,8 +428,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
Other
in
- ignore (type_term ~force:false ~ctx t1);
- ignore (type_term ~force:false ~ctx t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx t2);
dup ctx
| TAddrOf tlv
@@ -437,20 +440,20 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
| Tbase_addr (_, t) ->
(* it is a pointer, but subterms must be typed. *)
- ignore (type_term ~force:false ~ctx:Other t);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Other t);
dup Other
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
- ignore (type_term ~force:false ~ctx:Other t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx:Other t1);
let ctx = offset_ty t2 in
- ignore (type_term ~force:true ~ctx t2);
+ ignore (type_term ~use_gmp_opt:false ~ctx t2);
dup Other
| Tapp(li, _, args) ->
let typ_arg lvi arg =
let ctx = ty_of_logic_ty lvi.lv_type in
- ignore (type_term ~force:true ~ctx arg)
+ ignore (type_term ~use_gmp_opt:false ~ctx arg)
in
List.iter2 typ_arg li.l_profile args;
(* [li.l_type is [None] for predicate only: not possible here.
@@ -487,7 +490,7 @@ and type_term_lval (host, offset) =
and type_term_lhost = function
| TVar _
| TResult _ -> ()
- | TMem t -> ignore (type_term ~force:false ~ctx:Other t)
+ | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:Other t)
and type_term_offset = function
| TNoOffset -> ()
@@ -495,7 +498,7 @@ and type_term_offset = function
| TModel(_, toff) -> type_term_offset toff
| TIndex(t, toff) ->
let ctx = offset_ty t in
- ignore (type_term ~force:true ~ctx t);
+ ignore (type_term ~use_gmp_opt:false ~ctx t);
type_term_offset toff
let rec type_predicate p =
@@ -512,12 +515,12 @@ let rec type_predicate p =
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let i = Ival.join i1 i2 in
- mk_ctx ~force:false (ty_of_interv ~ctx:c_int i)
+ mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
with Interval.Not_an_integer ->
Other
in
- ignore (type_term ~force:false ~ctx t1);
- ignore (type_term ~force:false ~ctx t2);
+ ignore (type_term ~use_gmp_opt:true ~ctx t1);
+ ignore (type_term ~use_gmp_opt:true ~ctx t2);
(match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx)
@@ -533,8 +536,8 @@ let rec type_predicate p =
ignore (type_predicate p);
c_int
| Pif(t, p1, p2) ->
- let ctx = mk_ctx ~force:true c_int in
- ignore (type_term ~force:true ~ctx t);
+ let ctx = mk_ctx ~use_gmp_opt:false c_int in
+ ignore (type_term ~use_gmp_opt:false ~ctx t);
ignore (type_predicate p1);
ignore (type_predicate p2);
c_int
@@ -552,8 +555,8 @@ let rec type_predicate p =
| _ -> assert false
in
let i2 = Interval.infer t2 in
- (* add one to [i2], since we increment the loop counter one more
- time before going outside the loop. *)
+ (* add one to [i2], since we increment the loop counter one more
+ time before going outside the loop. *)
let i2 = match r2 with
| Rlt -> i2
| Rle -> Ival.add_singleton_int Integer.one i2
@@ -561,10 +564,10 @@ let rec type_predicate p =
in
let i = Ival.join i1 i2 in
let ctx = match x.lv_type with
- | Linteger -> mk_ctx ~force:false (ty_of_interv ~ctx:Gmp i)
+ | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmp i)
| Ctype ty ->
(match Cil.unrollType ty with
- | TInt(ik, _) -> C_type ik
+ | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_type ik)
| ty ->
Options.fatal "unexpected type %a for quantified variable %a"
Printer.pp_typ ty
@@ -576,8 +579,15 @@ let rec type_predicate p =
in
(* forcing when typing bounds prevents to generate an extra useless
GMP variable when --e-acsl-gmp-only *)
- ignore (type_term ~force:true ~ctx t1);
- ignore (type_term ~force:true ~ctx t2);
+ ignore (type_term ~use_gmp_opt:false ~ctx t1);
+ ignore (type_term ~use_gmp_opt:false ~ctx t2);
+ (* if we must generate GMP code, degrade the interval in order to
+ guarantee that [x] will be a GMP when typing the goal *)
+ let i = match ctx with
+ | C_type _ -> i
+ | Gmp -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
+ | Other -> assert false
+ in
Interval.Env.add x i)
guards;
(type_predicate goal).ty
@@ -588,7 +598,7 @@ let rec type_predicate p =
| Pvalid(_, t)
| Pvalid_read(_, t)
| Pvalid_function t ->
- ignore (type_term ~force:false ~ctx:Other t);
+ ignore (type_term ~use_gmp_opt:false ~ctx:Other t);
c_int
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
@@ -599,10 +609,10 @@ let rec type_predicate p =
in
coerce ~arith_operand:false ~ctx:c_int ~op c_int
-let type_term ~force ?ctx t =
+let type_term ~use_gmp_opt ?ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
Printer.pp_term t (Pretty_utils.pp_opt pretty) ctx;
- ignore (type_term ~force ?ctx t)
+ ignore (type_term ~use_gmp_opt ?ctx t)
let type_named_predicate ?(must_clear=true) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
@@ -613,6 +623,11 @@ let type_named_predicate ?(must_clear=true) p =
end;
ignore (type_predicate p)
+let unsafe_set t ?ctx ty =
+ let ctx = match ctx with None -> ty | Some ctx -> ctx in
+ let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
+ ignore (Memo.memo mk t)
+
(******************************************************************************)
(** {2 Getters} *)
(******************************************************************************)
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 177e4f99acd6983fde71a8ce88124f73b24d5f27..59c489fd3fd1087e6a963aaf6fc5ab99e190535d 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -56,6 +56,8 @@ type integer_ty = private
| C_type of ikind
| Other (** Any non-integral type *)
+val pretty: Format.formatter -> integer_ty -> unit
+
(** {3 Smart constructors} *)
val gmp: integer_ty
@@ -81,9 +83,9 @@ val join: integer_ty -> integer_ty -> integer_ty
(** {2 Typing} *)
(******************************************************************************)
-val type_term: force:bool -> ?ctx:integer_ty -> term -> unit
+val type_term: use_gmp_opt:bool -> ?ctx:integer_ty -> term -> unit
(** Compute the type of each subterm of the given term in the given context. If
- [force] is true, then the conversion to the given context is done even if
+ [use_gmp_opt] is false, then the conversion to the given context is done even if
-e-acsl-gmp-only is set. *)
val type_named_predicate: ?must_clear:bool -> predicate -> unit
@@ -123,6 +125,10 @@ val get_cast: term -> typ option
val get_cast_of_predicate: predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
+val unsafe_set: term -> ?ctx:integer_ty -> integer_ty -> unit
+(** Register that the given term has the given type in the given context (if
+ any). No verification is done. *)
+
(******************************************************************************)
(** {2 Internal stuff} *)
(******************************************************************************)