diff --git a/src/plugins/e-acsl/src/code_generator/gmp_gen.ml b/src/plugins/e-acsl/src/code_generator/gmp_gen.ml index 0d5e839e776b4fae7e43e3e339eae1cc618dacfc..288922dcd1e37a72ed32d5045d23d9bfe77de01d 100644 --- a/src/plugins/e-acsl/src/code_generator/gmp_gen.ml +++ b/src/plugins/e-acsl/src/code_generator/gmp_gen.ml @@ -46,6 +46,22 @@ module Z = struct in e,env + let cmp ~loc name t_opt bop env kf e1 e2 = + let _, e, env = Env.new_var + ~loc + env + kf + t_opt + ~name + Cil.intType + (fun v _ -> + [ Smart_stmt.rtl_call ~loc + ~result:(Cil.var v) + ~prefix:"" + "__gmpz_cmp" + [ e1; e2 ] ]) + in + Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env end module Q = struct diff --git a/src/plugins/e-acsl/src/code_generator/gmp_gen.mli b/src/plugins/e-acsl/src/code_generator/gmp_gen.mli index 2357bd68f0cecbca0fe7aeaef63969ed70da5cd6..b1412502e9b3566e5cf7d48187c0ff3f39985b44 100644 --- a/src/plugins/e-acsl/src/code_generator/gmp_gen.mli +++ b/src/plugins/e-acsl/src/code_generator/gmp_gen.mli @@ -15,9 +15,14 @@ module Z : sig val binop: loc:location -> term option -> binop -> Env.t -> kernel_function -> exp -> exp -> exp * Env.t - (** Applies [binop] to the given expressions. The optional term - indicates whether the comparison has a correspondance in the logic. *) + (** Applies [binop] to the given expressions. The optional term + indicates whether the comparison has a correspondance in the logic. *) + val cmp: + loc:location -> string -> term option -> binop -> Env.t -> + kernel_function -> exp -> exp -> exp * Env.t + (** Compares two expressions according to the given [binop]. The optional term + indicates whether the comparison has a correspondance in the logic. *) end 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 bbf09e0809cd7c353d321f37f6b42f770db4ad2e..38630b93ac05c66cd289c905667865dce8c8c81e 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml @@ -205,22 +205,7 @@ let comparison_to_exp match ity with | C_integer _ | C_float _ | Nan -> Cil.mkBinOp ~loc bop e1 e2, env - | Gmpz -> - let _, e, env = Env.new_var - ~loc - env - kf - t_opt - ~name - Cil.intType - (fun v _ -> - [ Smart_stmt.rtl_call ~loc - ~result:(Cil.var v) - ~prefix:"" - "__gmpz_cmp" - [ e1; e2 ] ]) - in - Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env + | Gmpz -> Gmp_gen.Z.cmp ~loc name t_opt bop env kf e1 e2 | Rational -> Gmp_gen.Q.cmp ~loc t_opt bop env kf e1 e2 | Real -> Error.not_yet "comparison involving real numbers" end