Commit 632573a2 authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] infer type of intervals wrt context: reduce the number of generated casts

parent 11874835
......@@ -41,6 +41,10 @@ type integer_ty =
| C_type of ikind
| Other
let gmp = Gmp
let c_int = C_type IInt
let ikind ik = C_type ik
let join ty1 ty2 = match ty1, ty2 with
| Other, Other -> Other
| Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
......@@ -59,8 +63,6 @@ let typ_of_integer_ty = function
| C_type ik -> TInt(ik, [])
| Other -> Options.fatal "[typing] not an integer type"
let c_int = C_type IInt
let size_t () = match Cil.theMachine.Cil.typeOfSizeOf with
| TInt(kind, _) -> C_type kind
| _ -> assert false
......@@ -132,16 +134,18 @@ end
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv i =
let ty_of_interv ~ctx i =
let open Interval in
let is_pos = Integer.ge i.lower Integer.zero in
try
let lkind = Cil.intKindForValue i.lower is_pos in
let ukind = Cil.intKindForValue i.upper is_pos in
let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
(* int whenever possible to prevent superfluous casts in the generated
(* ctx type whenever possible to prevent superfluous casts in the generated
code *)
if Cil.intTypeIncluded kind IInt then c_int else C_type kind
(match ctx with
| Gmp | Other -> C_type kind
| C_type ik -> if Cil.intTypeIncluded kind ik then ctx else C_type kind)
with Cil.Not_representable ->
Gmp
......@@ -174,7 +178,7 @@ let rec type_term env ~ctx t =
| TAlignOf _ ->
(try
let i = Interval.infer env t in
ty_of_interv i
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
......@@ -182,7 +186,7 @@ let rec type_term env ~ctx t =
(try
let i = Interval.infer env t in
type_term_lval env tlv;
ty_of_interv i
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
......@@ -193,7 +197,7 @@ let rec type_term env ~ctx t =
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 i
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other)
......@@ -203,14 +207,14 @@ let rec type_term env ~ctx t =
(* [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 i
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 (Interval.join i i')) in
let ctx = mk_ctx (ty_of_interv ~ctx (Interval.join i i')) in
ignore (type_term env ~ctx t');
ctx
......@@ -218,7 +222,9 @@ let rec type_term env ~ctx t =
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 (Interval.join i (Interval.join i1 i2))) 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
......@@ -228,7 +234,7 @@ let rec type_term env ~ctx t =
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv (Interval.join i1 i2))
mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
......@@ -244,7 +250,7 @@ let rec type_term env ~ctx t =
(* both operands fit in an int. *)
ignore (type_term env ~ctx:c_int t1);
ignore (type_term env ~ctx:c_int t2);
ty_of_interv (Interval.join i1 i2)
ty_of_interv ~ctx (Interval.join i1 i2)
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
| TBinOp (BXor, _, _) -> Error.not_yet "bitwise xor"
......@@ -258,7 +264,7 @@ let rec type_term env ~ctx t =
(* nothing to do more: [i] is already more precise than what we could
infer from the arguments of the cast. Also, do not type the internal
term: possibly it is not even an integer *)
let ty = ty_of_interv i in
let ty = ty_of_interv ~ctx i in
ignore (type_term env ~ctx:ty t');
ty
with Interval.Not_an_integer ->
......@@ -273,7 +279,7 @@ let rec type_term env ~ctx t =
try
let i2 = Interval.infer env t2 in
let i3 = Interval.infer env t3 in
mk_ctx (ty_of_interv (Interval.join i (Interval.join i2 i3)))
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
with Interval.Not_an_integer ->
Other
in
......@@ -288,7 +294,7 @@ let rec type_term env ~ctx t =
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let ty = ty_of_interv (Interval.join i (Interval.join i1 i2)) in
let ty = ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)) in
ignore (type_term env ~ctx:ty t1);
ignore (type_term env ~ctx:ty t2);
ty
......@@ -361,7 +367,7 @@ let rec type_predicate_named env p =
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let i = Interval.join i1 i2 in
mk_ctx (ty_of_interv i)
mk_ctx (ty_of_interv ~ctx:c_int i)
with Interval.Not_an_integer ->
Other
in
......@@ -409,7 +415,21 @@ let rec type_predicate_named env p =
| _ -> assert false
in
let i = Interval.join i1 i2 in
let ctx = mk_ctx (ty_of_interv i) in
let ctx = match x.lv_type with
| Linteger -> Gmp
| Ctype ty ->
(match Cil.unrollType ty with
| TInt(ik, _) -> C_type ik
| ty ->
Options.fatal "unexpected type %a for quantified variable %a"
Printer.pp_typ ty
Printer.pp_logic_var x)
| lty ->
Options.fatal "unexpected type %a for quantified variable %a"
Printer.pp_logic_type lty
Printer.pp_logic_var x
in
let ctx = mk_ctx (ty_of_interv ~ctx i) in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
Interval.Env.add x i env)
......
......@@ -30,11 +30,15 @@ open Cil_types
(** {2 Datatypes} *)
(******************************************************************************)
type integer_ty =
type integer_ty = private
| Gmp
| C_type of ikind
| Other
val gmp: integer_ty
val c_int: integer_ty
val ikind: ikind -> integer_ty
val typ_of_integer_ty: integer_ty -> typ
val join: integer_ty -> integer_ty -> integer_ty
......
......@@ -214,7 +214,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
let tlv = Logic_const.tvar ~loc llv in
let guard = Logic_const.term ~loc (TBinOp(bop2, tlv, t2)) Linteger in
New_typing.type_term ~ctx:(New_typing.C_type IInt) guard;
New_typing.type_term ~ctx:New_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 =
......
......@@ -13,10 +13,10 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/block_length.c:45:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/block_length.c:46:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/block_length.c:48:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/block_length.c:54:[value] warning: assertion got status unknown.
......
......@@ -48,7 +48,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_3;
void *__gen_e_acsl_base_addr_4;
__gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[(unsigned long)3]));
__gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3]));
__gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)PA);
__e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
(char *)"Assertion",(char *)"main",
......@@ -69,8 +69,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_7;
void *__gen_e_acsl_base_addr_8;
__gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + (unsigned long)2));
__gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[(unsigned long)3]));
__gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2));
__gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3]));
__e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(PA+2) == \\base_addr(&A[3])",17);
......@@ -99,7 +99,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_11;
void *__gen_e_acsl_base_addr_12;
__gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[(unsigned long)3]));
__gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3]));
__gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa);
__e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
(char *)"Assertion",(char *)"main",
......@@ -121,7 +121,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_15;
void *__gen_e_acsl_base_addr_16;
__gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + (unsigned long)2));
__gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2));
__gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a));
__e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
(char *)"Assertion",(char *)"main",
......@@ -145,7 +145,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_19;
void *__gen_e_acsl_base_addr_20;
__gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + (unsigned long)2));
__gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2));
__gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l));
__e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
(char *)"Assertion",(char *)"main",
......@@ -195,8 +195,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_27;
void *__gen_e_acsl_base_addr_28;
__gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + (unsigned long)1));
__gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + (unsigned long)5));
__gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1));
__gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5));
__e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+1) == \\base_addr(pd+5)",45);
......@@ -205,8 +205,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_29;
void *__gen_e_acsl_base_addr_30;
__gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + (unsigned long)11));
__gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + (unsigned long)1));
__gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11));
__gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1));
__e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+11) == \\base_addr(pd+1)",46);
......@@ -217,7 +217,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_31;
void *__gen_e_acsl_base_addr_32;
__gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + (unsigned long)5));
__gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5));
__gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
(char *)"Assertion",(char *)"main",
......@@ -227,7 +227,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_33;
void *__gen_e_acsl_base_addr_34;
__gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - (unsigned long)5));
__gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5));
__gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
(char *)"Assertion",(char *)"main",
......
......@@ -26,13 +26,15 @@ FRAMAC_SHARE/libc/stdlib.h:213:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:213:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
......@@ -5,13 +5,15 @@ tests/e-acsl-runtime/vector.c:28:[e-acsl] warning: E-ACSL construct `complete be
Ignoring annotation.
tests/e-acsl-runtime/vector.c:28:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
......@@ -15,6 +15,7 @@
[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.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_neg
[value] done for function main
......@@ -41,7 +41,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_le;
__gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
__gmpz_init_set_si(__gen_e_acsl_,(long)0);
__gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_le <= 0,(char *)"Assertion",(char *)"main",
......@@ -55,7 +55,7 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_ge;
__gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
__gmpz_init_set_si(__gen_e_acsl__2,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gen_e_acsl_ge = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_3),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ge >= 0,(char *)"Assertion",(char *)"main",
......@@ -72,8 +72,8 @@ int main(void)
mpz_t __gen_e_acsl__3;
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_lt_2;
__gmpz_init_set_si(__gen_e_acsl__3,(long)5);
__gmpz_init_set_si(__gen_e_acsl__4,(long)18);
__gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)5);
__gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)18);
__gen_e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__3),
(__mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_lt_2 < 0,(char *)"Assertion",(char *)"main",
......@@ -86,8 +86,8 @@ int main(void)
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl__6;
int __gen_e_acsl_gt_2;
__gmpz_init_set_si(__gen_e_acsl__5,(long)32);
__gmpz_init_set_si(__gen_e_acsl__6,(long)3);
__gmpz_init_set_ui(__gen_e_acsl__5,(unsigned long)32);
__gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)3);
__gen_e_acsl_gt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__5),
(__mpz_struct const *)(__gen_e_acsl__6));
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
......@@ -100,8 +100,8 @@ int main(void)
mpz_t __gen_e_acsl__7;
mpz_t __gen_e_acsl__8;
int __gen_e_acsl_le_2;
__gmpz_init_set_si(__gen_e_acsl__7,(long)12);
__gmpz_init_set_si(__gen_e_acsl__8,(long)13);
__gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)12);
__gmpz_init_set_ui(__gen_e_acsl__8,(unsigned long)13);
__gen_e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__7),
(__mpz_struct const *)(__gen_e_acsl__8));
__e_acsl_assert(__gen_e_acsl_le_2 <= 0,(char *)"Assertion",
......@@ -114,8 +114,8 @@ int main(void)
mpz_t __gen_e_acsl__9;
mpz_t __gen_e_acsl__10;
int __gen_e_acsl_ge_2;
__gmpz_init_set_si(__gen_e_acsl__9,(long)123);
__gmpz_init_set_si(__gen_e_acsl__10,(long)12);
__gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)123);
__gmpz_init_set_ui(__gen_e_acsl__10,(unsigned long)12);
__gen_e_acsl_ge_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__9),
(__mpz_struct const *)(__gen_e_acsl__10));
__e_acsl_assert(__gen_e_acsl_ge_2 >= 0,(char *)"Assertion",
......@@ -127,7 +127,7 @@ int main(void)
{
mpz_t __gen_e_acsl__11;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl__11,(long)0xff);
__gmpz_init_set_ui(__gen_e_acsl__11,(unsigned long)0xff);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__11),
(__mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
......@@ -139,8 +139,8 @@ int main(void)
mpz_t __gen_e_acsl__12;
mpz_t __gen_e_acsl__13;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl__12,(long)1);
__gmpz_init_set_si(__gen_e_acsl__13,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__12,(unsigned long)1);
__gmpz_init_set_ui(__gen_e_acsl__13,(unsigned long)2);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__12),
(__mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
......@@ -154,10 +154,10 @@ int main(void)
mpz_t __gen_e_acsl_neg;
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_lt_3;
__gmpz_init_set_si(__gen_e_acsl__14,(long)5);
__gmpz_init_set_ui(__gen_e_acsl__14,(unsigned long)5);
__gmpz_init(__gen_e_acsl_neg);
__gmpz_neg(__gen_e_acsl_neg,(__mpz_struct const *)(__gen_e_acsl__14));
__gmpz_init_set_si(__gen_e_acsl__15,(long)18);
__gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)18);
__gen_e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg),
(__mpz_struct const *)(__gen_e_acsl__15));
__e_acsl_assert(__gen_e_acsl_lt_3 < 0,(char *)"Assertion",(char *)"main",
......@@ -172,8 +172,8 @@ int main(void)
mpz_t __gen_e_acsl__17;
mpz_t __gen_e_acsl_neg_2;
int __gen_e_acsl_gt_3;
__gmpz_init_set_si(__gen_e_acsl__16,(long)32);
__gmpz_init_set_si(__gen_e_acsl__17,(long)3);
__gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)32);
__gmpz_init_set_ui(__gen_e_acsl__17,(unsigned long)3);
__gmpz_init(__gen_e_acsl_neg_2);
__gmpz_neg(__gen_e_acsl_neg_2,(__mpz_struct const *)(__gen_e_acsl__17));
__gen_e_acsl_gt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__16),
......@@ -190,10 +190,10 @@ int main(void)
mpz_t __gen_e_acsl_neg_3;
mpz_t __gen_e_acsl__19;
int __gen_e_acsl_le_3;
__gmpz_init_set_si(__gen_e_acsl__18,(long)12);
__gmpz_init_set_ui(__gen_e_acsl__18,(unsigned long)12);
__gmpz_init(__gen_e_acsl_neg_3);
__gmpz_neg(__gen_e_acsl_neg_3,(__mpz_struct const *)(__gen_e_acsl__18));
__gmpz_init_set_si(__gen_e_acsl__19,(long)13);
__gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)13);
__gen_e_acsl_le_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_3),
(__mpz_struct const *)(__gen_e_acsl__19));
__e_acsl_assert(__gen_e_acsl_le_3 <= 0,(char *)"Assertion",
......@@ -208,8 +208,8 @@ int main(void)
mpz_t __gen_e_acsl__21;
mpz_t __gen_e_acsl_neg_4;
int __gen_e_acsl_ge_3;
__gmpz_init_set_si(__gen_e_acsl__20,(long)123);
__gmpz_init_set_si(__gen_e_acsl__21,(long)12);
__gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)123);
__gmpz_init_set_ui(__gen_e_acsl__21,(unsigned long)12);
__gmpz_init(__gen_e_acsl_neg_4);
__gmpz_neg(__gen_e_acsl_neg_4,(__mpz_struct const *)(__gen_e_acsl__21));
__gen_e_acsl_ge_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__20),
......@@ -225,7 +225,7 @@ int main(void)
mpz_t __gen_e_acsl__22;
mpz_t __gen_e_acsl_neg_5;
int __gen_e_acsl_eq_2;
__gmpz_init_set_si(__gen_e_acsl__22,(long)0xff);
__gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)0xff);
__gmpz_init(__gen_e_acsl_neg_5);
__gmpz_neg(__gen_e_acsl_neg_5,(__mpz_struct const *)(__gen_e_acsl__22));
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_neg_5),
......@@ -241,8 +241,8 @@ int main(void)
mpz_t __gen_e_acsl__24;
mpz_t __gen_e_acsl_neg_6;
int __gen_e_acsl_ne_2;
__gmpz_init_set_si(__gen_e_acsl__23,(long)1);
__gmpz_init_set_si(__gen_e_acsl__24,(long)2);
__gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)1);
__gmpz_init_set_ui(__gen_e_acsl__24,(unsigned long)2);
__gmpz_init(__gen_e_acsl_neg_6);
__gmpz_neg(__gen_e_acsl_neg_6,(__mpz_struct const *)(__gen_e_acsl__24));
__gen_e_acsl_ne_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__23),
......
......@@ -7,7 +7,7 @@ int main(void)
{
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_,(long)0);
__gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
......@@ -21,8 +21,8 @@ int main(void)
mpz_t __gen_e_acsl__2;
mpz_t __gen_e_acsl__3;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl__2,(long)0);
__gmpz_init_set_si(__gen_e_acsl__3,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)0);
__gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)1);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__2),
(__mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
......
......@@ -39,17 +39,17 @@ int main(void)
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
unsigned long __gen_e_acsl__4;
__gmpz_init_set_si(__gen_e_acsl_,(long)2);
__gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)2);
__gmpz_init(__gen_e_acsl_x);
__gmpz_import(__gen_e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_x));
__gmpz_init_set_si(__gen_e_acsl__2,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_mul),
(__mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init_set_si(__gen_e_acsl__3,0L);
__gmpz_init_set_ui(__gen_e_acsl__3,0UL);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
......
......@@ -39,17 +39,17 @@ int main(void)
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_,(long)2);
__gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)2);
__gmpz_init(__gen_e_acsl_x);
__gmpz_import(__gen_e_acsl_x,1UL,1,8UL,0,0UL,(void const *)(& x));
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,(__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl_x));
__gmpz_init_set_si(__gen_e_acsl__2,(long)1);
__gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_mul),
(__mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init_set_si(__gen_e_acsl__3,0L);
__gmpz_init_set_ui(__gen_e_acsl__3,0UL);
__gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
(__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
......
......@@ -10,7 +10,7 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
__gmpz_init_set_si(__gen_e_acsl_,0L);
__gmpz_init_set_ui(__gen_e_acsl_,0UL);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
......@@ -25,7 +25,7 @@ int main(void)
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_ne;
__gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gmpz_init_set_ui(__gen_e_acsl__2,0UL);
__gen_e_acsl_ne = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",
......
......@@ -10,11 +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_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.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init_set_str
[value] done for function main
......@@ -16,9 +16,9 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
[value] using specification for function my_pow
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
[value] using specification for function __gmpz_init_set_si