From bd6473341f1db2059cfe66e1842de3e43a12b75f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 4 May 2020 09:48:03 +0200
Subject: [PATCH] [eacsl:codegen] Add support for bitwise AND, OR and XOR when
using GMP parameters
---
.../e-acsl/src/code_generator/translate.ml | 17 ++++++++++++++---
1 file changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 33ca70c7a8d..ad1b39718cb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -57,8 +57,11 @@ let name_of_mpz_arith_bop = function
| Mult -> "__gmpz_mul"
| Div -> "__gmpz_tdiv_q"
| Mod -> "__gmpz_tdiv_r"
- | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
- | Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
+ | BAnd -> "__gmpz_and"
+ | BOr -> "__gmpz_ior"
+ | BXor -> "__gmpz_xor"
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | Shiftlt | Shiftrt | PlusPI
+ | IndexPI | MinusPI | MinusPP -> assert false
(* Type of a string that represents a number.
Used when a string is required to encode a constant number because it is not
@@ -426,7 +429,15 @@ and context_insensitive_term_to_exp kf env t =
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
- not_yet env "bitwise operator on arbitrary precision"
+ let mk_stmts _v e =
+ let name = name_of_mpz_arith_bop bop in
+ let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
+ [ instr ]
+ in
+ let name = Misc.name_of_binop bop in
+ let t = Some t in
+ let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
+ e, env, C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
--
GitLab