From 964091d1539e25130bf7ad7a0f2510d28ded8c7f Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Mon, 10 Oct 2022 16:49:44 +0200
Subject: [PATCH] [e-acsl] refactor Gmp: add Z.cmp
---
.../e-acsl/src/code_generator/gmp_gen.ml | 16 ++++++++++++++++
.../e-acsl/src/code_generator/gmp_gen.mli | 9 +++++++--
.../src/code_generator/translate_utils.ml | 17 +----------------
3 files changed, 24 insertions(+), 18 deletions(-)
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 0d5e839e776..288922dcd1e 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 2357bd68f0c..b1412502e9b 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 bbf09e0809c..38630b93ac0 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
--
GitLab