Commit 4ded561b authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] fix bug with logical operators: do always follow the theory, guy

parent 0ad2bd7a
......@@ -12,10 +12,11 @@
__e_acsl_heap_size ∈ [--..--]
[value] using specification for function __e_acsl_assert
[value] using specification for function __gmpz_init_set_str
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_cmp
[value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_clear
[value] done for function main
......@@ -10,9 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_neg
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[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.
......
......@@ -16,14 +16,14 @@ int main(void)
__e_acsl_assert(0 != ~ 0,(char *)"Assertion",(char *)"main",
(char *)"0 != ~0",12);
/*@ assert x+1 ≡ -2; */
__e_acsl_assert((long)x + (long)1 == (long)(-2),(char *)"Assertion",
(char *)"main",(char *)"x+1 == -2",14);
__e_acsl_assert(x + 1 == -2,(char *)"Assertion",(char *)"main",
(char *)"x+1 == -2",14);
/*@ assert x-1 ≡ -4; */
__e_acsl_assert((long)x - (long)1 == (long)(-4),(char *)"Assertion",
(char *)"main",(char *)"x-1 == -4",15);
__e_acsl_assert(x - 1 == -4,(char *)"Assertion",(char *)"main",
(char *)"x-1 == -4",15);
/*@ assert x*3 ≡ -9; */
__e_acsl_assert((long)x * (long)3 == (long)(-9),(char *)"Assertion",
(char *)"main",(char *)"x*3 == -9",16);
__e_acsl_assert(x * 3 == -9,(char *)"Assertion",(char *)"main",
(char *)"x*3 == -9",16);
/*@ assert x/3 ≡ -1; */
__e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
(char *)"x/3 == -1",17);
......@@ -33,10 +33,9 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_div_guard;
mpz_t __gen_e_acsl_div;
mpz_t __gen_e_acsl__3;
int __gen_e_acsl_eq;
unsigned long __gen_e_acsl__3;
__gmpz_init_set_str(__gen_e_acsl_,"309485009821345068724781055",10);
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gmpz_init_set_ui(__gen_e_acsl__2,0UL);
__gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init(__gen_e_acsl_div);
......@@ -46,16 +45,13 @@ int main(void)
18);
__gmpz_tdiv_q(__gen_e_acsl_div,(__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_));
__gmpz_init_set_si(__gen_e_acsl__3,(long)1);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div),
(__mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
__gen_e_acsl__3 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_div));
__e_acsl_assert(__gen_e_acsl__3 == 1,(char *)"Assertion",(char *)"main",
(char *)"0xffffffffffffffffffffff/0xffffffffffffffffffffff == 1",
18);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_div);
__gmpz_clear(__gen_e_acsl__3);
}
/*@ assert x%2 ≡ -1; */
__e_acsl_assert(x % 2 == -1,(char *)"Assertion",(char *)"main",
......@@ -67,9 +63,9 @@ int main(void)
__e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
(char *)"3%-2 == 1",21);
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */
__e_acsl_assert((((long)x * (long)2 + ((long)3 + (long)y)) - (long)4) + (
(long)x - (long)y) == (long)(-10),(char *)"Assertion",
(char *)"main",(char *)"((x*2+(3+y))-4)+(x-y) == -10",23);
__e_acsl_assert(((x * 2 + (3 + y)) - 4) + (x - y) == -10,
(char *)"Assertion",(char *)"main",
(char *)"((x*2+(3+y))-4)+(x-y) == -10",23);
/*@ assert (0≡1) ≡ !(0≡0); */
__e_acsl_assert((0 == 1) == ! (0 == 0),(char *)"Assertion",(char *)"main",
(char *)"(0==1) == !(0==0)",25);
......
......@@ -12,7 +12,7 @@ int main(void)
mpz_t __gen_e_acsl_neg;
mpz_t __gen_e_acsl_x;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_,(long)3);
__gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)3);
__gmpz_init(__gen_e_acsl_neg);
__gmpz_neg(__gen_e_acsl_neg,(__mpz_struct const *)(__gen_e_acsl_));
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
......@@ -31,7 +31,7 @@ int main(void)
mpz_t __gen_e_acsl_neg_2;
int __gen_e_acsl_eq_2;
__gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
__gmpz_init_set_si(__gen_e_acsl__2,(long)3);
__gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)3);
__gmpz_init(__gen_e_acsl_neg_2);
__gmpz_neg(__gen_e_acsl_neg_2,(__mpz_struct const *)(__gen_e_acsl__2));
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
......@@ -47,7 +47,7 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl_bnot;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl__3,(long)0);
__gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)0);
__gmpz_init(__gen_e_acsl_bnot);
__gmpz_com(__gen_e_acsl_bnot,(__mpz_struct const *)(__gen_e_acsl__3));
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
......@@ -66,11 +66,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_3;
int __gen_e_acsl_eq_3;
__gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
__gmpz_init_set_si(__gen_e_acsl__4,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl__4));
__gmpz_init_set_si(__gen_e_acsl__5,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__5,(unsigned long)2);
__gmpz_init(__gen_e_acsl_neg_3);
__gmpz_neg(__gen_e_acsl_neg_3,(__mpz_struct const *)(__gen_e_acsl__5));
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_add),
......@@ -92,11 +92,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_4;
int __gen_e_acsl_eq_4;
__gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
__gmpz_init_set_si(__gen_e_acsl__6,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)1);
__gmpz_init(__gen_e_acsl_sub);
__gmpz_sub(__gen_e_acsl_sub,(__mpz_struct const *)(__gen_e_acsl_x_4),
(__mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init_set_si(__gen_e_acsl__7,(long)4);
__gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)4);
__gmpz_init(__gen_e_acsl_neg_4);
__gmpz_neg(__gen_e_acsl_neg_4,(__mpz_struct const *)(__gen_e_acsl__7));
__gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_sub),
......@@ -118,11 +118,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_5;
int __gen_e_acsl_eq_5;
__gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
__gmpz_init_set_si(__gen_e_acsl__8,(long)3);
__gmpz_init_set_ui(__gen_e_acsl__8,(unsigned long)3);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_x_5),
(__mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,(long)9);
__gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)9);
__gmpz_init(__gen_e_acsl_neg_5);
__gmpz_neg(__gen_e_acsl_neg_5,(__mpz_struct const *)(__gen_e_acsl__9));
__gen_e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mul),
......@@ -146,8 +146,8 @@ int main(void)
mpz_t __gen_e_acsl_neg_6;
int __gen_e_acsl_eq_6;
__gmpz_init_set_si(__gen_e_acsl_x_6,(long)x);
__gmpz_init_set_si(__gen_e_acsl__10,(long)3);
__gmpz_init_set_si(__gen_e_acsl__11,0L);
__gmpz_init_set_ui(__gen_e_acsl__10,(unsigned long)3);
__gmpz_init_set_ui(__gen_e_acsl__11,0UL);
__gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__10),
(__mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init(__gen_e_acsl_div);
......@@ -156,7 +156,7 @@ int main(void)
(char *)"main",(char *)"3 == 0",17);
__gmpz_tdiv_q(__gen_e_acsl_div,(__mpz_struct const *)(__gen_e_acsl_x_6),
(__mpz_struct const *)(__gen_e_acsl__10));
__gmpz_init_set_si(__gen_e_acsl__12,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__12,(unsigned long)1);
__gmpz_init(__gen_e_acsl_neg_6);
__gmpz_neg(__gen_e_acsl_neg_6,(__mpz_struct const *)(__gen_e_acsl__12));
__gen_e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div),
......@@ -179,7 +179,7 @@ int main(void)
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_eq_7;
__gmpz_init_set_str(__gen_e_acsl__13,"309485009821345068724781055",10);
__gmpz_init_set_si(__gen_e_acsl__14,0L);
__gmpz_init_set_ui(__gen_e_acsl__14,0UL);
__gen_e_acsl_div_guard_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__13),
(__mpz_struct const *)(__gen_e_acsl__14));
__gmpz_init(__gen_e_acsl_div_2);
......@@ -190,7 +190,7 @@ int main(void)
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__mpz_struct const *)(__gen_e_acsl__13),
(__mpz_struct const *)(__gen_e_acsl__13));
__gmpz_init_set_si(__gen_e_acsl__15,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)1);
__gen_e_acsl_eq_7 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div_2),
(__mpz_struct const *)(__gen_e_acsl__15));
__e_acsl_assert(__gen_e_acsl_eq_7 == 0,(char *)"Assertion",
......@@ -213,8 +213,8 @@ int main(void)
mpz_t __gen_e_acsl_neg_7;
int __gen_e_acsl_eq_8;
__gmpz_init_set_si(__gen_e_acsl_x_7,(long)x);
__gmpz_init_set_si(__gen_e_acsl__16,(long)2);
__gmpz_init_set_si(__gen_e_acsl__17,0L);
__gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)2);
__gmpz_init_set_ui(__gen_e_acsl__17,0UL);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__16),
(__mpz_struct const *)(__gen_e_acsl__17));
__gmpz_init(__gen_e_acsl_mod);
......@@ -223,7 +223,7 @@ int main(void)
(char *)"main",(char *)"2 == 0",19);
__gmpz_tdiv_r(__gen_e_acsl_mod,(__mpz_struct const *)(__gen_e_acsl_x_7),
(__mpz_struct const *)(__gen_e_acsl__16));
__gmpz_init_set_si(__gen_e_acsl__18,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__18,(unsigned long)1);
__gmpz_init(__gen_e_acsl_neg_7);
__gmpz_neg(__gen_e_acsl_neg_7,(__mpz_struct const *)(__gen_e_acsl__18));
__gen_e_acsl_eq_8 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod),
......@@ -249,13 +249,13 @@ int main(void)
mpz_t __gen_e_acsl__22;
mpz_t __gen_e_acsl_neg_10;
int __gen_e_acsl_eq_9;
__gmpz_init_set_si(__gen_e_acsl__19,(long)3);
__gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)3);
__gmpz_init(__gen_e_acsl_neg_8);
__gmpz_neg(__gen_e_acsl_neg_8,(__mpz_struct const *)(__gen_e_acsl__19));
__gmpz_init_set_si(__gen_e_acsl__20,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)2);
__gmpz_init(__gen_e_acsl_neg_9);
__gmpz_neg(__gen_e_acsl_neg_9,(__mpz_struct const *)(__gen_e_acsl__20));
__gmpz_init_set_si(__gen_e_acsl__21,0L);
__gmpz_init_set_ui(__gen_e_acsl__21,0UL);
__gen_e_acsl_mod_guard_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_9),
(__mpz_struct const *)(__gen_e_acsl__21));
__gmpz_init(__gen_e_acsl_mod_2);
......@@ -265,7 +265,7 @@ int main(void)
__gmpz_tdiv_r(__gen_e_acsl_mod_2,
(__mpz_struct const *)(__gen_e_acsl_neg_8),
(__mpz_struct const *)(__gen_e_acsl_neg_9));
__gmpz_init_set_si(__gen_e_acsl__22,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)1);
__gmpz_init(__gen_e_acsl_neg_10);
__gmpz_neg(__gen_e_acsl_neg_10,(__mpz_struct const *)(__gen_e_acsl__22));
__gen_e_acsl_eq_9 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod_2),
......@@ -291,11 +291,11 @@ int main(void)
mpz_t __gen_e_acsl_mod_3;
mpz_t __gen_e_acsl__26;
int __gen_e_acsl_eq_10;
__gmpz_init_set_si(__gen_e_acsl__23,(long)3);
__gmpz_init_set_si(__gen_e_acsl__24,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)3);
__gmpz_init_set_ui(__gen_e_acsl__24,(unsigned long)2);
__gmpz_init(__gen_e_acsl_neg_11);
__gmpz_neg(__gen_e_acsl_neg_11,(__mpz_struct const *)(__gen_e_acsl__24));
__gmpz_init_set_si(__gen_e_acsl__25,0L);
__gmpz_init_set_ui(__gen_e_acsl__25,0UL);
__gen_e_acsl_mod_guard_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_11),
(__mpz_struct const *)(__gen_e_acsl__25));
__gmpz_init(__gen_e_acsl_mod_3);
......@@ -305,7 +305,7 @@ int main(void)
__gmpz_tdiv_r(__gen_e_acsl_mod_3,
(__mpz_struct const *)(__gen_e_acsl__23),
(__mpz_struct const *)(__gen_e_acsl_neg_11));
__gmpz_init_set_si(__gen_e_acsl__26,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__26,(unsigned long)1);
__gen_e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod_3),
(__mpz_struct const *)(__gen_e_acsl__26));
__e_acsl_assert(__gen_e_acsl_eq_10 == 0,(char *)"Assertion",
......@@ -334,11 +334,11 @@ int main(void)
mpz_t __gen_e_acsl_neg_12;
int __gen_e_acsl_eq_11;
__gmpz_init_set_si(__gen_e_acsl_x_8,(long)x);
__gmpz_init_set_si(__gen_e_acsl__27,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__27,(unsigned long)2);
__gmpz_init(__gen_e_acsl_mul_2);
__gmpz_mul(__gen_e_acsl_mul_2,(__mpz_struct const *)(__gen_e_acsl_x_8),
(__mpz_struct const *)(__gen_e_acsl__27));
__gmpz_init_set_si(__gen_e_acsl__28,(long)3);
__gmpz_init_set_ui(__gen_e_acsl__28,(unsigned long)3);
__gmpz_init_set_si(__gen_e_acsl_y,(long)y);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)(__gen_e_acsl__28),
......@@ -346,7 +346,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,(__mpz_struct const *)(__gen_e_acsl_mul_2),
(__mpz_struct const *)(__gen_e_acsl_add_2));
__gmpz_init_set_si(__gen_e_acsl__29,(long)4);
__gmpz_init_set_ui(__gen_e_acsl__29,(unsigned long)4);
__gmpz_init(__gen_e_acsl_sub_2);
__gmpz_sub(__gen_e_acsl_sub_2,(__mpz_struct const *)(__gen_e_acsl_add_3),
(__mpz_struct const *)(__gen_e_acsl__29));
......@@ -356,7 +356,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_add_4);
__gmpz_add(__gen_e_acsl_add_4,(__mpz_struct const *)(__gen_e_acsl_sub_2),
(__mpz_struct const *)(__gen_e_acsl_sub_3));
__gmpz_init_set_si(__gen_e_acsl__30,(long)10);
__gmpz_init_set_ui(__gen_e_acsl__30,(unsigned long)10);
__gmpz_init(__gen_e_acsl_neg_12);
__gmpz_neg(__gen_e_acsl_neg_12,(__mpz_struct const *)(__gen_e_acsl__30));
__gen_e_acsl_eq_11 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_add_4),
......@@ -388,8 +388,8 @@ int main(void)
int __gen_e_acsl_not;
mpz_t __gen_e_acsl__35;
int __gen_e_acsl_eq_14;
__gmpz_init_set_si(__gen_e_acsl__31,(long)0);
__gmpz_init_set_si(__gen_e_acsl__32,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__31,(unsigned long)0);
__gmpz_init_set_ui(__gen_e_acsl__32,(unsigned long)1);
__gen_e_acsl_eq_12 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__31),
(__mpz_struct const *)(__gen_e_acsl__32));
__gmpz_init_set_si(__gen_e_acsl__33,(long)(__gen_e_acsl_eq_12 == 0));
......@@ -419,8 +419,8 @@ int main(void)
int __gen_e_acsl_gt;
mpz_t __gen_e_acsl__39;
int __gen_e_acsl_eq_15;
__gmpz_init_set_si(__gen_e_acsl__36,(long)0);
__gmpz_init_set_si(__gen_e_acsl__37,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__36,(unsigned long)0);
__gmpz_init_set_ui(__gen_e_acsl__37,(unsigned long)1);
__gmpz_init(__gen_e_acsl_neg_13);
__gmpz_neg(__gen_e_acsl_neg_13,(__mpz_struct const *)(__gen_e_acsl__37));
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__36),
......@@ -449,8 +449,8 @@ int main(void)
int __gen_e_acsl_le_2;
mpz_t __gen_e_acsl__43;
int __gen_e_acsl_eq_16;
__gmpz_init_set_si(__gen_e_acsl__40,(long)0);
__gmpz_init_set_si(__gen_e_acsl__41,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__40,(unsigned long)0);
__gmpz_init_set_ui(__gen_e_acsl__41,(unsigned long)1);
__gmpz_init(__gen_e_acsl_neg_14);
__gmpz_neg(__gen_e_acsl_neg_14,(__mpz_struct const *)(__gen_e_acsl__41));
__gen_e_acsl_ge = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__40),
......@@ -480,8 +480,8 @@ int main(void)
int __gen_e_acsl_not_2;
mpz_t __gen_e_acsl__48;
int __gen_e_acsl_eq_17;
__gmpz_init_set_si(__gen_e_acsl__44,(long)0);
__gmpz_init_set_si(__gen_e_acsl__45,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__44,(unsigned long)0);
__gmpz_init_set_ui(__gen_e_acsl__45,(unsigned long)1);
__gen_e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__44),
(__mpz_struct const *)(__gen_e_acsl__45));
__gmpz_init_set_si(__gen_e_acsl__46,(long)(__gen_e_acsl_ne_2 != 0));
......@@ -512,11 +512,11 @@ int main(void)
int __gen_e_acsl_not_3;
mpz_t __gen_e_acsl__53;
int __gen_e_acsl_eq_18;
__gmpz_init_set_si(__gen_e_acsl__49,(long)0);
__gmpz_init_set_ui(__gen_e_acsl__49,(unsigned long)0);
__gen_e_acsl_ne_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__49),
(__mpz_struct const *)(__gen_e_acsl__49));
__gmpz_init_set_si(__gen_e_acsl__50,(long)(__gen_e_acsl_ne_4 != 0));
__gmpz_init_set_si(__gen_e_acsl__51,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__51,(unsigned long)1);
__gen_e_acsl_ne_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__51),
(__mpz_struct const *)(__gen_e_acsl__49));
__gmpz_init_set_si(__gen_e_acsl__52,(long)(__gen_e_acsl_ne_5 != 0));
......@@ -542,9 +542,9 @@ int main(void)
mpz_t __gen_e_acsl_div_3;
mpz_t __gen_e_acsl__56;
int __gen_e_acsl_eq_19;
__gmpz_init_set_si(__gen_e_acsl__54,(long)4);
__gmpz_init_set_ui(__gen_e_acsl__54,(unsigned long)4);
__gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
__gmpz_init_set_si(__gen_e_acsl__55,0L);
__gmpz_init_set_ui(__gen_e_acsl__55,0UL);
__gen_e_acsl_div_guard_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_2),
(__mpz_struct const *)(__gen_e_acsl__55));
__gmpz_init(__gen_e_acsl_div_3);
......@@ -554,7 +554,7 @@ int main(void)
__gmpz_tdiv_q(__gen_e_acsl_div_3,
(__mpz_struct const *)(__gen_e_acsl__54),
(__mpz_struct const *)(__gen_e_acsl_y_2));
__gmpz_init_set_si(__gen_e_acsl__56,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__56,(unsigned long)2);
__gen_e_acsl_eq_19 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_div_3),
(__mpz_struct const *)(__gen_e_acsl__56));
__e_acsl_assert(__gen_e_acsl_eq_19 == 0,(char *)"Assertion",
......
......@@ -100,8 +100,6 @@ let add_cast ~loc ?name env ctx is_mpz_string t_opt e =
| None -> e, env
| Some ctx ->
let ty = Cil.typeOf e in
(* Options.feedback "exp %a of type %a in context %a"
Printer.pp_exp e Printer.pp_typ ty Printer.pp_typ ctx;*)
if Gmpz.is_t ctx then
if Gmpz.is_t ty then
e, env
......@@ -294,7 +292,7 @@ and context_insensitive_term_to_exp kf env t =
else
Cil.new_exp ~loc (UnOp(op, e, ty)), env, false, ""
| TUnOp(LNot, t) ->
let ty = Typing.get_typ t in
let ty = Typing.get_op t in
if Gmpz.is_t ty then
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
......@@ -378,7 +376,7 @@ and context_insensitive_term_to_exp kf env t =
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
let ity = Typing.get_integer_ty t in
let ity = Typing.get_integer_op t in
let e, env = comparison_to_exp ~loc kf env ity bop t1 t2 (Some t) in
e, env, false, ""
| TBinOp((Shiftlt | Shiftrt), _, _) ->
......@@ -627,7 +625,7 @@ and named_predicate_content_to_exp ?name kf env p =
| Pdangling _ -> not_yet env "\\dangling"
| Pvalid_function _ -> not_yet env "\\valid_function"
| Prel(rel, t1, t2) ->
let ity = Typing.get_integer_ty_of_predicate p in
let ity = Typing.get_integer_op_of_predicate p in
comparison_to_exp ~loc kf env ity (relation_to_binop rel) t1 t2 None
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
......
......@@ -93,6 +93,7 @@ include Datatype.Make
type computed_info =
{ ty: t; (* type required for the term *)
op: t; (* type required for the operation *)
cast: t option; (* if not [None], type of the context which the term
must be casted to. If [None], no cast needed. *)
}
......@@ -150,15 +151,15 @@ let ty_of_interv ~ctx i =
with Cil.Not_representable ->
Gmp
let coerce ~ctx ty =
let coerce ~ctx ~op ty =
if compare ty ctx = 1 then begin
(* type larger than the expected context,
so we must introduce an explicit cast *)
{ ty = ty; cast = Some ctx }
{ ty; op; cast = Some ctx }
end else
(* only add an explicit cast if the context is [Gmp] and [ty] is not *)
if ctx = Gmp && ty <> Gmp then { ty = ty; cast = Some Gmp }
else { ty = ty; cast = None }
if ctx = Gmp && ty <> Gmp then { ty; op; cast = Some Gmp }
else { ty; op; cast = None }
(******************************************************************************)
(** {2 Type system} *)
......@@ -170,6 +171,7 @@ let mk_ctx c = match c with
let rec type_term env ~ctx t =
let ctx = mk_ctx ctx in
let dup ty = ty, ty in
let infer t =
Cil.CurrentLoc.set t.term_loc;
match t.term_node with
......@@ -177,82 +179,110 @@ let rec type_term env ~ctx t =
| TSizeOf _
| TSizeOfStr _
| TAlignOf _ ->
(try
let i = Interval.infer env t in
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
let ty =
try
let i = Interval.infer env t in
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
dup ty
| TLval tlv ->
(try
let i = Interval.infer env t in
type_term_lval env tlv;
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
let ty =
try
let i = Interval.infer env t in
type_term_lval env tlv;
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
dup ty
| Toffset(_, t')
| Tblock_length(_, t')
| TSizeOfE t'
| TAlignOfE t' ->
(try
let i = Interval.infer env t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term env ~ctx:Other t');
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
let ty =
try
let i = Interval.infer env t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term env ~ctx:Other t');
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
dup ty
| TBinOp (MinusPP, t1, t2) ->
(try
let i = Interval.infer env t in
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term env ~ctx:Other t1);
ignore (type_term env ~ctx:Other t2);
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
| TUnOp (_, t') ->
let i = Interval.infer env t in
let i' = Interval.infer env t' in
let ctx = mk_ctx (ty_of_interv ~ctx (Interval.join i i')) in
ignore (type_term env ~ctx t');
ctx
let ty =
try
let i = Interval.infer env t in
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term env ~ctx:Other t1);
ignore (type_term env ~ctx:Other t2);
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
dup ty
| TUnOp (unop, t') ->
let ty =
let i = Interval.infer env t in
let i' = Interval.infer env t' in
let ctx = mk_ctx (ty_of_interv ~ctx (Interval.join i i')) in
ignore (type_term env ~ctx t');
ctx
in
(match unop with
| LNot -> c_int, ty (* converted into [t == 0] in casse of GMP *)
| Neg | BNot -> dup ty)
| TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let ctx =
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)))
let ty =
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let ctx =
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)))
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
ctx
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
ctx
dup ty
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (compare ctx c_int >= 0);
let ctx =
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
let ty =
let ctx =
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
(match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx)
c_int, ty