Commit 4afbcfd4 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:runtime] Register GMP bitwise and, or and xor API functions

parent e62d4444
......@@ -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;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment