diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index c68e2919feb196332ea6c2ca4d33b2ec9703e5ca..3bdd79d845b6973fbf97efd4643a65dc3af471f9 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -565,8 +565,26 @@ let rec type_term
(* possible to have an [LBpred] here because we transformed
[Papp] into [Tapp] *)
List.iter
- (fun x -> ignore
- (type_term ~use_gmp_opt ~under_lambda ~arith_operand ~profile x))
+ (fun x ->
+ let ctx = match x.term_type with
+ | Linteger ->
+ (* If the function parameter is an integer,
+ the kernel introduces a coercion to integer, so we will
+ always see integer here.*)
+ begin match x.term_node with
+ |TLogic_coerce _ -> None
+ |_ -> if Options.Gmp_only.get() then Some Gmpz else None
+ end
+ | Lreal -> Some Real
+ | Ctype _| Ltype _| Larrow _ | Lvar _ -> None
+ in
+ ignore
+ (type_term
+ ~use_gmp_opt:true
+ ~under_lambda:true
+ ~arith_operand
+ ?ctx
+ ~profile x))
args;
let new_profile = List.map (Interval.get_p ~profile) args in
Stack.push
@@ -576,21 +594,48 @@ let rec type_term
dup c_int
| LBterm t_body ->
List.iter
- (fun x -> ignore
- (type_term ~use_gmp_opt ~under_lambda ~arith_operand ~profile x))
+ (fun x ->
+ let ctx = match x.term_type with
+ | Linteger ->
+ (* If the function parameter is an integer,
+ the kernel introduces a coercion to integer, so we will
+ always see integer here.*)
+ begin match x.term_node with
+ | TLogic_coerce _ -> None
+ |_ -> if Options.Gmp_only.get() then Some Gmpz else None
+ end
+ | Lreal -> Some Real
+ | Ctype _| Ltype _| Larrow _ | Lvar _ -> None
+ in
+ ignore
+ (type_term
+ ~use_gmp_opt:true
+ ~under_lambda:true
+ ~arith_operand
+ ?ctx
+ ~profile x))
args;
let new_profile = List.map (Interval.get_p ~profile) args in
+ let gmp,ctx_body = match li.l_type with
+ | Some (Ctype typ) ->
+ false, Some (number_ty_of_typ ~post:false typ)
+ | _ ->
+ true, if Options.Gmp_only.get() then Some Gmpz else ctx
+ in
Stack.push
(fun () ->
ignore (type_term
- ~use_gmp_opt
+ ~use_gmp_opt:false
~under_lambda:true
~arith_operand
- ?ctx
+ ?ctx:ctx_body
~profile:new_profile
t_body))
pending_typing;
- dup (ty_of_interv ?ctx ~use_gmp_opt (Interval.get_p ~profile t))
+ dup (ty_of_interv
+ ?ctx:ctx_body
+ ~use_gmp_opt:(gmp && use_gmp_opt)
+ (Interval.get_p ~profile t))
| LBnone ->
(match args with
| [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ] ->
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index f9d204856addaf0e4034ccedba76f46e529ae22d..8f49596fcb03a4d4220f9ab066c861986ea91b82 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -514,14 +514,16 @@ long __gen_e_acsl_f1(int x, int y)
assigns \result \from c; */
int __gen_e_acsl_h_char(int c)
{
- return c;
+ int __retres = (char)c;
+ return __retres;
}
/*@ assigns \result;
assigns \result \from s; */
int __gen_e_acsl_h_short(int s)
{
- return s;
+ int __retres = (short)s;
+ return __retres;
}
/*@ assigns \result;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index 898a5189079e6808563ad2fd90b98668537e85a7..96769bd85897cb0c48ed5e981e1df7c304173738 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -24,17 +24,22 @@ int __gen_e_acsl_p2(int x, int y);
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+int __gen_e_acsl_p2_5(int x, __e_acsl_mpz_struct * y);
+
/*@ logic integer f1(integer x, integer y) = x + y;
*/
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
+void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y);
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y);
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y);
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
+
/*@ logic char h_char(char c) = c;
*/
int __gen_e_acsl_h_char(int c);
@@ -175,16 +180,22 @@ int main(void)
}
/*@ assert f1(x, y) == 3; */ ;
{
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__7;
__e_acsl_mpz_t __gen_e_acsl_f1_4;
int __gen_e_acsl_p2_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl_f1(& __gen_e_acsl_f1_4,3,4);
+ __gmpz_init_set_str(__gen_e_acsl__6,"4",10);
+ __gmpz_init_set_str(__gen_e_acsl__7,"3",10);
+ __gen_e_acsl_f1_3(& __gen_e_acsl_f1_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__7,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__6);
/*@ assert
Eva: initialization:
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
*/
- __gen_e_acsl_p2_6 = __gen_e_acsl_p2_3(x,
+ __gen_e_acsl_p2_6 = __gen_e_acsl_p2_5(x,
(__e_acsl_mpz_struct *)__gen_e_acsl_f1_4);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_5,"f1(3, 4)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4));
@@ -199,22 +210,27 @@ int main(void)
__gen_e_acsl_assert_data_5.line = 49;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__7);
__gmpz_clear(__gen_e_acsl_f1_4);
}
/*@ assert p2(x, f1(3, 4)); */ ;
{
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl__10;
__e_acsl_mpz_t __gen_e_acsl_f1_6;
- __e_acsl_mpz_t __gen_e_acsl__7;
- int __gen_e_acsl_gt_4;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_gt_5;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
- __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
- __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,9,
- (__e_acsl_mpz_struct *)__gen_e_acsl__6);
- __gmpz_init_set_si(__gen_e_acsl__7,0L);
- __gen_e_acsl_gt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init_set_str(__gen_e_acsl__9,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__10,"9",10);
+ __gen_e_acsl_f1_5(& __gen_e_acsl_f1_6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__10,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__9);
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_gt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,
"f1(9, 99999999999999999999999999999)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6));
@@ -224,27 +240,28 @@ int main(void)
__gen_e_acsl_assert_data_6.file = "functions.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 50;
- __e_acsl_assert(__gen_e_acsl_gt_4 > 0,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__gen_e_acsl_gt_5 > 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl__10);
__gmpz_clear(__gen_e_acsl_f1_6);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl__11);
}
/*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
{
- __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl__12;
__e_acsl_mpz_t __gen_e_acsl_f1_8;
- __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl__13;
int __gen_e_acsl_eq_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gmpz_init_set_str(__gen_e_acsl__8,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__12,"99999999999999999999999999999",10);
__gen_e_acsl_f1_7(& __gen_e_acsl_f1_8,
- (__e_acsl_mpz_struct *)__gen_e_acsl__8,
- (__e_acsl_mpz_struct *)__gen_e_acsl__8);
- __gmpz_init_set_str(__gen_e_acsl__9,"199999999999999999999999999998",10);
+ (__e_acsl_mpz_struct *)__gen_e_acsl__12,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__12);
+ __gmpz_init_set_str(__gen_e_acsl__13,"199999999999999999999999999998",10);
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,
"f1(99999999999999999999999999999, 99999999999999999999999999999)",
0,
@@ -257,9 +274,9 @@ int main(void)
__gen_e_acsl_assert_data_7.line = 51;
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl__12);
__gmpz_clear(__gen_e_acsl_f1_8);
- __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl__13);
}
/*@
assert
@@ -357,15 +374,15 @@ int main(void)
{
mystruct __gen_e_acsl_t1_2;
__e_acsl_mpz_t __gen_e_acsl_t2_2;
- __e_acsl_mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl__16;
int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
__gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
- __gmpz_init_set_si(__gen_e_acsl__12,17L);
+ __gmpz_init_set_si(__gen_e_acsl__16,17L);
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"m");
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"t1(m)");
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_11,"t2(t1(m))",0,
@@ -379,25 +396,25 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_eq_6 == 0,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
__gmpz_clear(__gen_e_acsl_t2_2);
- __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl__16);
}
/*@ assert t2(t1(m)) == 17; */ ;
__gen_e_acsl_k(9);
double d = 2.0;
{
double __gen_e_acsl_f2_2;
- __e_acsl_mpq_t __gen_e_acsl__15;
- __e_acsl_mpq_t __gen_e_acsl__16;
- int __gen_e_acsl_gt_5;
+ __e_acsl_mpq_t __gen_e_acsl__19;
+ __e_acsl_mpq_t __gen_e_acsl__20;
+ int __gen_e_acsl_gt_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
__gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
- __gmpq_init(__gen_e_acsl__15);
- __gmpq_set_str(__gen_e_acsl__15,"0",10);
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_d(__gen_e_acsl__16,__gen_e_acsl_f2_2);
- __gen_e_acsl_gt_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__15));
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_str(__gen_e_acsl__19,"0",10);
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_d(__gen_e_acsl__20,__gen_e_acsl_f2_2);
+ __gen_e_acsl_gt_6 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
__e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"d",d);
__e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"f2(d)",
__gen_e_acsl_f2_2);
@@ -407,10 +424,10 @@ int main(void)
__gen_e_acsl_assert_data_12.file = "functions.c";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 71;
- __e_acsl_assert(__gen_e_acsl_gt_5 > 0,& __gen_e_acsl_assert_data_12);
+ __e_acsl_assert(__gen_e_acsl_gt_6 > 0,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
- __gmpq_clear(__gen_e_acsl__15);
- __gmpq_clear(__gen_e_acsl__16);
+ __gmpq_clear(__gen_e_acsl__19);
+ __gmpq_clear(__gen_e_acsl__20);
}
/*@ assert f2(d) > 0; */ ;
__retres = 0;
@@ -515,47 +532,63 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from x, y; */
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+/*@ assigns \result;
+ assigns \result \from x, *((__e_acsl_mpz_struct *)y); */
+int __gen_e_acsl_p2_5(int x, __e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y_3;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- __gmpz_clear(__gen_e_acsl_y_3);
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ int __gen_e_acsl_gt_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gen_e_acsl_gt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ int __retres = __gen_e_acsl_gt_4 > 0;
+ __gmpz_clear(__gen_e_acsl_x_5);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ __gmpz_clear(__gen_e_acsl__8);
+ return __retres;
}
/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from x, *((__e_acsl_mpz_struct *)y);
+ assigns (*__retres_arg)[0]
+ \from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
*/
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_x_5;
__e_acsl_mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
__gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+ __gmpz_add(__gen_e_acsl_add_5,(__e_acsl_mpz_struct const *)(x),
(__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
- __gmpz_clear(__gen_e_acsl_x_5);
__gmpz_clear(__gen_e_acsl_add_5);
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0]
+ \from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
+ */
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl_add_7);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0]
\from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
@@ -563,13 +596,34 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
+ __e_acsl_mpz_t __gen_e_acsl_add_8;
+ __gmpz_init(__gen_e_acsl_add_8);
+ __gmpz_add(__gen_e_acsl_add_8,(__e_acsl_mpz_struct const *)(x),
(__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl_add_6);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_8));
+ __gmpz_clear(__gen_e_acsl_add_8);
+ return;
+}
+
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from x, y; */
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl_add_4);
return;
}
@@ -577,14 +631,16 @@ void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
assigns \result \from c; */
int __gen_e_acsl_h_char(int c)
{
- return c;
+ int __retres = (char)c;
+ return __retres;
}
/*@ assigns \result;
assigns \result \from s; */
int __gen_e_acsl_h_short(int s)
{
- return s;
+ int __retres = (short)s;
+ return __retres;
}
/*@ assigns \result;
@@ -614,20 +670,20 @@ mystruct __gen_e_acsl_t1(mystruct m)
assigns (*__retres_arg)[0] \from m; */
void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
{
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
- __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_add_9;
+ __gmpz_init_set_si(__gen_e_acsl__14,(long)m.k);
+ __gmpz_init_set_si(__gen_e_acsl__15,(long)m.l);
+ __gmpz_init(__gen_e_acsl_add_9);
+ __gmpz_add(__gen_e_acsl_add_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_add_7);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_9));
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_add_9);
return;
}
@@ -652,21 +708,21 @@ int __gen_e_acsl_k_pred(int x)
assigns \result \from x; */
double __gen_e_acsl_f2(double x)
{
- __e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl__17;
+ __e_acsl_mpq_t __gen_e_acsl__18;
__e_acsl_mpq_t __gen_e_acsl_div;
double __gen_e_acsl_cast;
- __gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"1",10);
- __gmpq_init(__gen_e_acsl__14);
- __gmpq_set_d(__gen_e_acsl__14,x);
+ __gmpq_init(__gen_e_acsl__17);
+ __gmpq_set_str(__gen_e_acsl__17,"1",10);
+ __gmpq_init(__gen_e_acsl__18);
+ __gmpq_set_d(__gen_e_acsl__18,x);
__gmpq_init(__gen_e_acsl_div);
__gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__18));
__gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl__17);
+ __gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl_div);
/*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
return __gen_e_acsl_cast;