diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index efc72c375b0559a68b2db7706a817f0444aaf640..38608a2fddc9289e35c1a72413c5ddc0f3e8b591 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -106,40 +106,6 @@ let generic_affect ~loc fname lv ev e =
end else
Smart_stmt.assigns ~loc:e.eloc ~result:lv e
-let init_set ~loc lv ev e =
- let fname =
- let ty = Cil.typeOf ev in
- if Gmp_types.Z.is_t ty then
- "__gmpz_init_set"
- else if Gmp_types.Q.is_t ty then
- Options.fatal "no __gmpq_init_set: init then set separately"
- else
- ""
- in
- try generic_affect ~loc fname lv ev e
- with
- | Longlong IULongLong ->
- (match e.enode with
- | Lval elv ->
- assert (Gmp_types.Z.is_t (Cil.typeOf ev));
- let call =
- Smart_stmt.rtl_call ~loc
- ~prefix:""
- "__gmpz_import"
- [ ev;
- Cil.one ~loc;
- Cil.one ~loc;
- Cil.sizeOf ~loc (TInt(IULongLong, []));
- Cil.zero ~loc;
- Cil.zero ~loc;
- Cil.mkAddrOf ~loc elv ]
- in
- Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
- | _ ->
- Error.not_yet "unsigned long long expression requiring GMP")
- | Longlong ILongLong ->
- Error.not_yet "long long requiring GMP"
-
let affect ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
@@ -151,6 +117,43 @@ let affect ~loc lv ev e =
with Longlong _ ->
Error.not_yet "quantification over long long and requiring GMP"
+let init_set ~loc lv ev e =
+ let mpz_init_set fname =
+ try generic_affect ~loc fname lv ev e
+ with
+ | Longlong IULongLong ->
+ (match e.enode with
+ | Lval elv ->
+ assert (Gmp_types.Z.is_t (Cil.typeOf ev));
+ let call =
+ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ "__gmpz_import"
+ [ ev;
+ Cil.one ~loc;
+ Cil.one ~loc;
+ Cil.sizeOf ~loc (TInt(IULongLong, []));
+ Cil.zero ~loc;
+ Cil.zero ~loc;
+ Cil.mkAddrOf ~loc elv ]
+ in
+ Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
+ | _ ->
+ Error.not_yet "unsigned long long expression requiring GMP")
+ | Longlong ILongLong ->
+ Error.not_yet "long long requiring GMP"
+ in
+ let ty = Cil.typeOf ev in
+ if Gmp_types.Z.is_t ty then
+ mpz_init_set "__gmpz_init_set"
+ else if Gmp_types.Q.is_t ty then
+ Smart_stmt.block_stmt
+ (Cil.mkBlock
+ [ init ~loc ev ;
+ affect ~loc lv ev e ])
+ else
+ mpz_init_set ""
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 791fcf4ee83b89aa508ceffb48c13272cf13cb4f..861672fca4f8924e8b715a2947c25673ab164c1d 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -62,7 +62,7 @@ let result_as_extra_argument typ =
| TInt _ | TVoid _ | TFloat _ | TFun _ | TNamed _ | TEnum _
| TBuiltin_va_list _ -> false
in
- Gmp_types.Z.is_t typ || Gmp_types.Q.is_t typ || is_composite typ
+ Gmp_types.is_t typ || is_composite typ
(*****************************************************************************)
(****************** Generation of function bodies ****************************)
@@ -105,7 +105,7 @@ let pred_to_block ~loc kf env ret_vi p =
generate_return_block ~loc env ret_vi e
(* Generate the function's body for terms. *)
-let term_to_block ~loc ~is_mpq kf env ret_ty ret_vi t =
+let term_to_block ~loc kf env ret_ty ret_vi t =
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
if Cil.isVoidType ret_ty then
(* if the function's result is a GMP, it is the first parameter of the
@@ -113,9 +113,7 @@ let term_to_block ~loc ~is_mpq kf env ret_ty ret_vi t =
let set =
let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
let star_ret = Smart_exp.lval ~loc lv_star_ret in
- if is_mpq
- then Rational.init_set ~loc lv_star_ret star_ret e
- else Gmp.init_set ~loc lv_star_ret star_ret e
+ Gmp.init_set ~loc lv_star_ret star_ret e
in
let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
let b, env = Env.pop_and_get env set ~global_clear:false Env.Middle in
@@ -125,8 +123,8 @@ let term_to_block ~loc ~is_mpq kf env ret_ty ret_vi t =
else
generate_return_block ~loc env ret_vi e
-let generate_body ~loc ~is_mpq kf env ret_ty ret_vi = function
- | LBterm t -> term_to_block ~loc ~is_mpq kf env ret_ty ret_vi t
+let generate_body ~loc kf env ret_ty ret_vi = function
+ | LBterm t -> term_to_block ~loc kf env ret_ty ret_vi t
| LBpred p -> pred_to_block ~loc kf env ret_vi p
| LBnone |LBreads _ | LBinductive _ -> assert false
@@ -158,8 +156,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
in
(* build the varinfo storing the result *)
let res_as_extra_arg = result_as_extra_argument ret_ty in
- let is_mpz = Gmp_types.Z.is_t ret_ty in
- let is_mpq = Gmp_types.Q.is_t ret_ty in
+ let is_gmp = Gmp_types.is_t ret_ty in
let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
let vname = "__retres" in
if res_as_extra_arg then
@@ -218,7 +215,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
let assigned_var =
Logic_const.new_identified_term
(if res_as_extra_arg then
- Assigns.get_assigned_var ~loc ~is_gmp:(is_mpz || is_mpq) ret_vi
+ Assigns.get_assigned_var ~loc ~is_gmp ret_vi
else
Logic_const.tresult fundec.svar.vtype)
in
@@ -240,7 +237,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
kf
(Writes [ assigned_var , From assigns_from]);
end;
- let b, env = generate_body ~loc ~is_mpq kf env ret_ty ret_vi li.l_body in
+ let b, env = generate_body ~loc kf env ret_ty ret_vi li.l_body in
fundec.sbody <- b;
(* add the generated variables in the necessary lists *)
(* TODO: factorized the code below that add the generated vars with method
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 904f1c9fb591cb72f64869f322dd1d5f438134fd..102ac515432819a2f174fadaff5cb929c186b07a 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -412,11 +412,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let ty = Typing.get_typ ~logic_env t in
let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
let e, _, env = term_to_exp kf env t in
- let ty = Cil.typeOf e in
- let init_set =
- if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
- in
- let let_stmt = init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
+ let let_stmt = Gmp.init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
let stmts, env =
mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 4e11ce0f4e4a79c512b78f656aec5700dd1cce3a..4f385a6ff5df6ed5010a860c2cda9c12f3e08730 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -22,13 +22,6 @@
open Cil_types
-(* No init_set for GMPQ: init then set separately *)
-let init_set ~loc lval vi_e e =
- Smart_stmt.block_stmt
- (Cil.mkBlock
- [ Gmp.init ~loc vi_e ;
- Gmp.affect ~loc lval vi_e e ])
-
let create ~loc ?name e env kf t_opt =
let ty = Cil.typeOf e in
if Gmp_types.Q.is_t ty then
diff --git a/src/plugins/e-acsl/src/code_generator/rational.mli b/src/plugins/e-acsl/src/code_generator/rational.mli
index 84f197cab38f15517f4b84fb2dc11ed975dfab9d..72e4a5a2b555da0634d08adc0df440aeca31f995 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.mli
+++ b/src/plugins/e-acsl/src/code_generator/rational.mli
@@ -33,11 +33,6 @@ val create:
exp * Env.t
(** Create a real *)
-(* TODO: change the call convention *)
-val init_set: loc:location -> lval -> exp -> exp -> stmt
-(** [init_set lval lval_as_exp exp] sets [lval] to [exp] while guranteeing that
- [lval] is properly initialized wrt the underlying real library. *)
-
val normalize_str: string -> string
(** Normalize the string so that it fits the representation used by the
underlying real library. For example, "0.1" is a real number in ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index cf14ab17aa83a48331f6ebf86548c3b230534d5f..654ff848a0f0518204f319e010983f731fda1728 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -282,10 +282,7 @@ let pretranslate_to_exp ~loc kf env pot =
t_opt
ty
(fun var_vi var_e ->
- let init_set =
- if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
- in
- [ init_set ~loc (Cil.var var_vi) var_e e ])
+ [ Gmp.init_set ~loc (Cil.var var_vi) var_e e ])
in
var_vi, env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 5b6f157fc6c94f5b8c41fc08f5624e2c122cea64..665dd752c4410b6b117afb4504cd20b7581668f4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -284,8 +284,7 @@ let env_of_li ~adata ~loc kf env li =
let stmt = match Typing.get_number_ty ~logic_env t with
| C_integer _ | C_float _ | Nan ->
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
- | Gmpz -> Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Rational -> Rational.init_set ~loc (Cil.var vi) vi_e e
+ | Gmpz | Rational -> Gmp.init_set ~loc (Cil.var vi) vi_e e
| Real -> Error.not_yet "real number"
in
adata, Env.add_stmt env stmt