From 4afbcfd4f8bed181883ef47578859bf808b213a9 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 4 May 2020 09:45:17 +0200
Subject: [PATCH] [eacsl:runtime] Register GMP bitwise and, or and xor API
 functions

---
 .../e-acsl/share/e-acsl/e_acsl_gmp_api.h      | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
index 39946e50b14..302d9979e34 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
@@ -294,6 +294,27 @@ extern void __gmpq_div(mpq_t q1, const mpq_t q2, const mpq_t q3)
 /* Bitwise operators */
 /*********************/
 
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_and(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_ior(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_xor(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
 /*@ requires \valid(z1);
   @ requires \valid_read(z2);
   @ assigns *z1 \from *z2;
-- 
GitLab