From 7ab09585fd3333a66e119102ffa8efeee9ef038c Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Mon, 10 Oct 2022 16:03:20 +0200
Subject: [PATCH] [e-acsl] refactor Gmp: remove Rational.name_arith_bop
---
src/plugins/e-acsl/src/code_generator/gmp.ml | 8 ++++++++
src/plugins/e-acsl/src/code_generator/gmp.mli | 8 ++++++++
src/plugins/e-acsl/src/code_generator/rational.ml | 10 +---------
3 files changed, 17 insertions(+), 9 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 9ab2527d36b..1048b8a9d3f 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -159,6 +159,14 @@ module Z = struct
end
module Q = struct
+ let name_arith_bop = function
+ | PlusA -> "__gmpq_add"
+ | MinusA -> "__gmpq_sub"
+ | Mult -> "__gmpq_mul"
+ | Div -> "__gmpq_div"
+ | Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
+ | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP -> assert false
+
exception Not_a_decimal of string
exception Is_a_float
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.mli b/src/plugins/e-acsl/src/code_generator/gmp.mli
index e8756f44515..219cb2a108a 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.mli
+++ b/src/plugins/e-acsl/src/code_generator/gmp.mli
@@ -48,6 +48,14 @@ module Z : sig
end
+module Q : sig
+
+ val name_arith_bop: binop -> string
+ (** [name_of_mpz_arith_bop bop] returns the name of the GMP function on integer
+ corresponding to the [bop] arithmetic operation. *)
+
+end
+
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/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index b53f8d76ad0..14bb46e1067 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -111,16 +111,8 @@ let new_var_and_init ~loc ?scope ?name env kf t_opt mk_stmts =
(Gmp_types.Q.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
-let name_arith_bop = function
- | PlusA -> "__gmpq_add"
- | MinusA -> "__gmpq_sub"
- | Mult -> "__gmpq_mul"
- | Div -> "__gmpq_div"
- | Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
- | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP -> assert false
-
let binop ~loc bop e1 e2 env kf t_opt =
- let name = name_arith_bop bop in
+ let name = Gmp.Q.name_arith_bop bop in
(* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
[e2] *)
let e1, env = Gmp_gen.Q.create ~loc None env kf e1 in
--
GitLab