From bc45b051e3f42833e17de68bbcca80d64e4e4760 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 18 May 2020 13:33:19 +0200
Subject: [PATCH] sync with frama-c master
---
frama-c | 2 +-
mini-gmp/mini-gmp.eva/warnings.log | 18 ++---
mini-gmp/mini-gmp.parse/framac.ast | 102 +++++++++++++++--------------
3 files changed, 62 insertions(+), 60 deletions(-)
diff --git a/frama-c b/frama-c
index 04fe04593..2b7c2f71f 160000
--- a/frama-c
+++ b/frama-c
@@ -1 +1 @@
-Subproject commit 04fe045939ae28f0f46844f8b84c80757fef361f
+Subproject commit 2b7c2f71f152b9e0758333f31d05bb9300e06ebd
diff --git a/mini-gmp/mini-gmp.eva/warnings.log b/mini-gmp/mini-gmp.eva/warnings.log
index ec08eac5d..97cb47335 100644
--- a/mini-gmp/mini-gmp.eva/warnings.log
+++ b/mini-gmp/mini-gmp.eva/warnings.log
@@ -1,15 +1,15 @@
-tests/hex-random.c:151:[eva:garbled-mix] warning: The specification of function __gmpz_neg has generated a garbled mix for assigns clause assigns clause *.
-tests/hex-random.c:153:[eva:garbled-mix] warning: The specification of function __gmpz_neg has generated a garbled mix for assigns clause assigns clause *.
-tests/hex-random.c:160:[eva:garbled-mix] warning: The specification of function __gmpz_add has generated a garbled mix for assigns clause assigns clause *.
+tests/hex-random.c:151:[eva:garbled-mix] warning: The specification of function __gmpz_neg has generated a garbled mix for assigns clause assigns clause *res.
+tests/hex-random.c:153:[eva:garbled-mix] warning: The specification of function __gmpz_neg has generated a garbled mix for assigns clause assigns clause *res.
+tests/hex-random.c:160:[eva:garbled-mix] warning: The specification of function __gmpz_add has generated a garbled mix for assigns clause assigns clause *res.
tests/hex-random.c:201:[eva] warning: ignoring unsupported \allocates clause
tests/hex-random.c:201:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause \result.
-tests/hex-random.c:201:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause *.
+tests/hex-random.c:201:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause *strp.
tests/hex-random.c:202:[eva] warning: ignoring unsupported \allocates clause
tests/hex-random.c:202:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause \result.
-tests/hex-random.c:202:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause *.
+tests/hex-random.c:202:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause *strp.
tests/hex-random.c:203:[eva] warning: ignoring unsupported \allocates clause
tests/hex-random.c:203:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause \result.
-tests/hex-random.c:203:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause *.
-tests/hex-random.c:205:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause assigns clause *.
-tests/hex-random.c:206:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause assigns clause *.
-tests/hex-random.c:207:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause assigns clause *.
+tests/hex-random.c:203:[eva:garbled-mix] warning: The specification of function __gmp_asprintf has generated a garbled mix for assigns clause assigns clause *strp.
+tests/hex-random.c:205:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause assigns clause *a.
+tests/hex-random.c:206:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause assigns clause *a.
+tests/hex-random.c:207:[eva:garbled-mix] warning: The specification of function __gmpz_clear has generated a garbled mix for assigns clause assigns clause *a.
diff --git a/mini-gmp/mini-gmp.parse/framac.ast b/mini-gmp/mini-gmp.parse/framac.ast
index e4fd25476..648cfb186 100644
--- a/mini-gmp/mini-gmp.parse/framac.ast
+++ b/mini-gmp/mini-gmp.parse/framac.ast
@@ -5553,32 +5553,33 @@ void __gmp_randinit_default(__gmp_randstate_struct *);
void __gmp_randseed_ui(__gmp_randstate_struct *, unsigned long);
-/*@ assigns \result, *, __fc_random_counter;
+/*@ assigns \result, *a, __fc_random_counter;
assigns \result \from __fc_random_counter;
- assigns * \from __fc_random_counter;
+ assigns *a \from __fc_random_counter;
assigns __fc_random_counter \from __fc_random_counter;
*/
-unsigned long __gmp_urandomb_ui(__gmp_randstate_struct *, unsigned long);
-
-/*@ requires \valid();
- ensures \initialized(\old());
- assigns \result, *;
- assigns \result \from ;
- assigns * \from ;
- allocates \old();
+unsigned long __gmp_urandomb_ui(__gmp_randstate_struct * /*[1]*/ a,
+ unsigned long b);
+
+/*@ requires \valid(strp);
+ ensures \initialized(\old(strp));
+ assigns \result, *strp;
+ assigns \result \from fmt;
+ assigns *strp \from fmt;
+ allocates \old(strp);
*/
-int __gmp_asprintf(char **, char const *, void * const *__va_params);
+int __gmp_asprintf(char **strp, char const *fmt, void * const *__va_params);
-/*@ requires \valid();
- ensures \initialized(\old());
- assigns *;
- assigns * \from , ;
+/*@ requires \valid(res);
+ ensures \initialized(\old(res));
+ assigns *res;
+ assigns *res \from a, b;
*/
-void __gmpz_add(mpz_ptr, mpz_srcptr, mpz_srcptr);
+void __gmpz_add(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_and(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_and(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
void __gmpz_cdiv_q_2exp(mpz_ptr, mpz_srcptr, mp_bitcnt_t);
@@ -5586,11 +5587,11 @@ void __gmpz_cdiv_qr(mpz_ptr, mpz_ptr, mpz_srcptr, mpz_srcptr);
void __gmpz_cdiv_r_2exp(mpz_ptr, mpz_srcptr, mp_bitcnt_t);
-/*@ assigns *, __fc_random_counter;
- assigns * \from __fc_random_counter;
+/*@ assigns *a, __fc_random_counter;
+ assigns *a \from __fc_random_counter;
assigns __fc_random_counter \from __fc_random_counter;
*/
-void __gmpz_clear(mpz_ptr);
+void __gmpz_clear(mpz_ptr a);
void __gmpz_clrbit(mpz_ptr, mp_bitcnt_t);
@@ -5608,42 +5609,43 @@ void __gmpz_fdiv_qr(mpz_ptr, mpz_ptr, mpz_srcptr, mpz_srcptr);
void __gmpz_fdiv_r_2exp(mpz_ptr, mpz_srcptr, mp_bitcnt_t);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_gcd(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_gcd(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
char *__gmpz_get_str(char *, int, mpz_srcptr);
-/*@ assigns *, __fc_random_counter;
- assigns * \from __fc_random_counter;
+/*@ assigns *a, __fc_random_counter;
+ assigns *a \from __fc_random_counter;
assigns __fc_random_counter \from __fc_random_counter;
*/
-void __gmpz_init(mpz_ptr);
+void __gmpz_init(mpz_ptr a);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_ior(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_ior(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_lcm(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_lcm(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_mul(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_mul(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
-/*@ assigns *;
- assigns * \from ; */
-void __gmpz_neg(mpz_ptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a; */
+void __gmpz_neg(mpz_ptr res, mpz_srcptr a);
void __gmpz_powm(mpz_ptr, mpz_srcptr, mpz_srcptr, mpz_srcptr);
-/*@ assigns *, *, __fc_random_counter;
- assigns * \from __fc_random_counter;
- assigns * \from __fc_random_counter;
+/*@ assigns *a, *b, __fc_random_counter;
+ assigns *a \from __fc_random_counter;
+ assigns *b \from __fc_random_counter;
assigns __fc_random_counter \from __fc_random_counter;
*/
-void __gmpz_rrandomb(mpz_ptr, __gmp_randstate_struct *, mp_bitcnt_t);
+void __gmpz_rrandomb(mpz_ptr a, __gmp_randstate_struct * /*[1]*/ b,
+ mp_bitcnt_t c);
mp_bitcnt_t __gmpz_scan0(mpz_srcptr, mp_bitcnt_t) __attribute__((__pure__));
@@ -5655,9 +5657,9 @@ void __gmpz_set_ui(mpz_ptr, unsigned long);
void __gmpz_setbit(mpz_ptr, mp_bitcnt_t);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_sub(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_sub(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
void __gmpz_tdiv_q_2exp(mpz_ptr, mpz_srcptr, mp_bitcnt_t);
@@ -5667,9 +5669,9 @@ void __gmpz_tdiv_r_2exp(mpz_ptr, mpz_srcptr, mp_bitcnt_t);
void __gmpz_urandomb(mpz_ptr, __gmp_randstate_struct *, mp_bitcnt_t);
-/*@ assigns *;
- assigns * \from , ; */
-void __gmpz_xor(mpz_ptr, mpz_srcptr, mpz_srcptr);
+/*@ assigns *res;
+ assigns *res \from a, b; */
+void __gmpz_xor(mpz_ptr res, mpz_srcptr a, mpz_srcptr b);
static gmp_randstate_t state;
/*@ requires valid_read_string(format);
--
GitLab