Commit 3ea203e6 authored by Julien Signoles's avatar Julien Signoles Committed by Kostyantyn Vorobyov
Browse files

[typing] fix another bug in typing of quantifiers

parent 1bb8f7bc
......@@ -168,10 +168,17 @@ 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 ->
......@@ -242,12 +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++] *)
(* 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 tlv in
(* previous typing ensures that [x++] fits type [ty] *)
Typing.type_term ~use_gmp_opt:false ~ctx:ctx_one tlv_one;
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
......
......@@ -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;
......
......@@ -207,7 +207,9 @@ int main(void)
}
{
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]); */
{
{
......@@ -233,7 +235,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
30);
31);
}
}
/*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
......@@ -261,7 +263,93 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
(char *)"main",
(char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
31);
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));
}
}
......
......@@ -55,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),
......@@ -122,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),
......@@ -181,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),
......@@ -239,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),
......@@ -347,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),
......@@ -361,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),
......@@ -375,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),
......@@ -436,7 +436,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__31;
__e_acsl_mpz_t __gen_e_acsl_add_12;
__gmpz_init_set_si(__gen_e_acsl__31,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),
......@@ -563,7 +563,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__38;
__e_acsl_mpz_t __gen_e_acsl_add_13;
__gmpz_init_set_si(__gen_e_acsl__38,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),
......@@ -590,7 +590,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__41;
__e_acsl_mpz_t __gen_e_acsl_add_14;
__gmpz_init_set_si(__gen_e_acsl__41,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),
......@@ -611,7 +611,9 @@ int main(void)
}
{
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]); */
{
{
......@@ -651,7 +653,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__44;
__e_acsl_mpz_t __gen_e_acsl_add_15;
__gmpz_init_set_si(__gen_e_acsl__44,1L);
__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),
......@@ -666,7 +668,7 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
(char *)"main",
(char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
30);
31);
__gmpz_clear(__gen_e_acsl_i);
}
}
......@@ -709,7 +711,7 @@ int main(void)
{
__e_acsl_mpz_t __gen_e_acsl__47;
__e_acsl_mpz_t __gen_e_acsl_add_16;
__gmpz_init_set_si(__gen_e_acsl__47,1L);
__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),
......@@ -724,8 +726,124 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
(char *)"main",
(char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
31);
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));
}
}
......
......@@ -33,10 +33,22 @@ 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:30:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:30:[value] entering loop for the first time
[value] using specification for function __e_acsl_valid
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
......@@ -22,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.
......@@ -42,11 +43,16 @@ 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:30:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:30:[value] entering loop for the first time
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:31:[value] entering loop for the first time
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
......@@ -27,8 +27,11 @@ int main(void) {
{ // 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;
......
......@@ -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",
......
......@@ -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",
......
......@@ -623,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} *)
(******************************************************************************)
......
......@@ -125,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} *)
(******************************************************************************)
......
Markdown is supported
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