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 962a72dff8ef756177a10cc06c1835959d6d451f..625d41ea3e4a89d66a369913c8b75db81ec1c4bd 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);