diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml index ae396de6e1fca30290cdab3e7a31a4428fe933cb..9ab2527d36b0e264d329a301232111659060dda0 100644 --- a/src/plugins/e-acsl/src/code_generator/gmp.ml +++ b/src/plugins/e-acsl/src/code_generator/gmp.ml @@ -37,23 +37,6 @@ let apply_on_var ~loc funname e = in Smart_stmt.rtl_call ~loc ~prefix funname [ e ] -let name_of_mpz_arith_bop = function - | PlusA -> "__gmpz_add" - | MinusA -> "__gmpz_sub" - | Mult -> "__gmpz_mul" - | Div -> "__gmpz_tdiv_q" - | Mod -> "__gmpz_tdiv_r" - | BAnd -> "__gmpz_and" - | BOr -> "__gmpz_ior" - | BXor -> "__gmpz_xor" - | Shiftlt -> "__gmpz_mul_2exp" - | Shiftrt -> "__gmpz_tdiv_q_2exp" - | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | MinusPI - | MinusPP as bop -> - Options.fatal - "Operation '%a' either not arithmetic or not supported on GMP integers" - Printer.pp_binop bop - let init ~loc e = apply_on_var "init" ~loc e let clear ~loc e = apply_on_var "clear" ~loc e @@ -154,6 +137,26 @@ let init_set ~loc lv ev e = else mpz_init_set "" +module Z = struct + + let name_arith_bop = function + | PlusA -> "__gmpz_add" + | MinusA -> "__gmpz_sub" + | Mult -> "__gmpz_mul" + | Div -> "__gmpz_tdiv_q" + | Mod -> "__gmpz_tdiv_r" + | BAnd -> "__gmpz_and" + | BOr -> "__gmpz_ior" + | BXor -> "__gmpz_xor" + | Shiftlt -> "__gmpz_mul_2exp" + | Shiftrt -> "__gmpz_tdiv_q_2exp" + | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | MinusPI + | MinusPP as bop -> + Options.fatal + "Operation '%a' either not arithmetic or not supported on GMP integers" + Printer.pp_binop bop + +end module Q = struct exception Not_a_decimal of string diff --git a/src/plugins/e-acsl/src/code_generator/gmp.mli b/src/plugins/e-acsl/src/code_generator/gmp.mli index 99d6d8ad453c34adba828d1669c9633e8463b4fc..e8756f445154230bef12e807356e18a9a486a8de 100644 --- a/src/plugins/e-acsl/src/code_generator/gmp.mli +++ b/src/plugins/e-acsl/src/code_generator/gmp.mli @@ -24,10 +24,6 @@ open Cil_types -val name_of_mpz_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. *) - val init: loc:location -> exp -> stmt (** build stmt [mpz_init(v)] or [mpq_init(v)] depending on typ of [v] *) @@ -44,6 +40,14 @@ val affect: loc:location -> lval -> exp -> exp -> stmt or [mpq_set*(e)] with the good function 'set' according to the type of [e] *) +module Z : 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/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml index 140ab022cb22ff35af3919db2b2c91f1ffe1ef09..a41f4de4fa07ff770e66583dae8639807555a7a6 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml @@ -115,7 +115,7 @@ let affect_binop ~loc var_as_varinfo var_as_exp binop exp_type exp1 exp2 = "__gmpz_cmp" [exp1; exp2] | Some e -> - let name = Gmp.name_of_mpz_arith_bop binop in + let name = Gmp.Z.name_arith_bop binop in Smart_stmt.rtl_call ~loc ~prefix:"" name [e; exp1; exp2]) else if Gmp_types.Q.is_t exp_type then @@ -350,7 +350,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t = let e1, adata, env = to_exp ~adata kf env t1 in let e2, adata, env = to_exp ~adata kf env t2 in if Gmp_types.Z.is_t ty then - let name = Gmp.name_of_mpz_arith_bop bop in + let name = Gmp.Z.name_arith_bop bop in let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc ~prefix:"" name @@ -384,7 +384,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t = RTE should do this automatically. *) let ctx = Typing.get_number_ty ~logic_env t in let t = Some t in - let name = Gmp.name_of_mpz_arith_bop bop in + let name = Gmp.Z.name_arith_bop bop in (* [TODO] can now do better since the type system got some info about possible values of [t2] *) (* guarding divisions and modulos *) @@ -560,7 +560,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t = (* Create the shift instruction *) let mk_shift_instr result_e = - let name = Gmp.name_of_mpz_arith_bop bop in + let name = Gmp.Z.name_arith_bop bop in Smart_stmt.rtl_call ~loc ~prefix:"" name @@ -691,7 +691,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t = let e2, adata, env = to_exp ~adata kf env t2 in if Gmp_types.Z.is_t ty then let mk_stmts _v e = - let name = Gmp.name_of_mpz_arith_bop bop in + let name = Gmp.Z.name_arith_bop bop in let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in [ instr ] in