From acbfa65d77723a366d4bfcb930a00fbf4e39d09e Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 10 Jun 2020 12:45:08 +0200
Subject: [PATCH] [e-acsl] fix GMP's API

---
 src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

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 962a72dff8e..625d41ea3e4 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
@@ -144,6 +144,11 @@ extern void __gmpq_set(mpq_t q, const mpq_t q_orig)
 extern void __gmpq_set_d(mpq_t q, double d)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid(q);
+  @ assigns *q \from n,d; */
+extern void __gmpq_set_ui(mpq_t q, unsigned long int n, unsigned long int d)
+  __attribute__((FC_BUILTIN));
+
 /*@ requires \valid(q);
   @ assigns *q \from n,d; */
 extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
@@ -158,8 +163,8 @@ extern int __gmpq_set_str(mpq_t q, const char *str, int base)
   __attribute__((FC_BUILTIN));
 
 /*@ requires \valid(z);
-  @ assigns *z \from n,d; */
-extern void __gmpz_set_ui(mpz_t z, unsigned long int n, unsigned long int d)
+  @ assigns *z \from n; */
+extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
   __attribute__((FC_BUILTIN));
 
 /*@ requires \valid(z);
-- 
GitLab