From 47335f25d8c42f2a6fb69ef0a956b0d4dbd66dd1 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 22 Mar 2016 12:53:07 +0100
Subject: [PATCH] [RTL] Doxygen documentation for GMP headers

---
 src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h       | 14 ++++++++++----
 src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h |  5 +++++
 .../e-acsl/tests/gmp/oracle/longlong.0.res.oracle  |  2 +-
 .../e-acsl/tests/gmp/oracle/longlong.1.res.oracle  |  2 +-
 4 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
index 7518f1bf81d..ce0db01659d 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
@@ -20,6 +20,12 @@
 /*                                                                        */
 /**************************************************************************/
 
+/*! ***********************************************************************
+ * \file  e_acsl_gmp.h
+ * \brief Prototypes of functions belonging to GNU Multiple
+ * Precision Arithmetic Library (GMP) used within E-ACSL
+***************************************************************************/
+
 /******************/
 /* GMP prototypes */
 /******************/
@@ -74,7 +80,7 @@ extern void __gmpz_init_set_si(mpz_t z, signed long int n)
   @ allocates z;
   @ ensures \valid(z);
   @ ensures \initialized(z);
-  @ assigns *z \from str[0..],base; 
+  @ assigns *z \from str[0..],base;
   @ assigns \result \from str[0..],base; */
 extern int __gmpz_init_set_str(mpz_t z, const char *str, int base)
   __attribute__((FC_BUILTIN));
@@ -181,7 +187,7 @@ extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3)
 
 /*@ requires \valid(z1);
   @ requires \valid_read(z2);
-  @ assigns *z1 \from *z2; 
+  @ assigns *z1 \from *z2;
   @ assigns \result \from *z1,*z2; */
 extern int __gmpz_com(mpz_t z1, const mpz_t z2)
   __attribute__((FC_BUILTIN));
@@ -190,12 +196,12 @@ extern int __gmpz_com(mpz_t z1, const mpz_t z2)
 /* Coercions to C types */
 /************************/
 
-/*@ requires \valid_read(z); 
+/*@ requires \valid_read(z);
   @ assigns \result \from *z; */
 extern long __gmpz_get_si(const mpz_t z)
   __attribute__((FC_BUILTIN));
 
-/*@ requires \valid_read(z); 
+/*@ requires \valid_read(z);
   @ assigns \result \from *z; */
 extern unsigned long __gmpz_get_ui(const mpz_t z)
   __attribute__((FC_BUILTIN));
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
index d84dfc7f4a5..8ed98de11a2 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
@@ -23,6 +23,11 @@
 #ifndef E_ACSL_GMP_TYPES
 #define E_ACSL_GMP_TYPES
 
+/*! ***********************************************************************
+ * \file  e_acsl_gmp_types.h
+ * \brief GMP types used within E-ACSL
+***************************************************************************/
+
 /*************/
 /* GMP types */
 /*************/
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 35705b2fbe9..662538e38aa 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -21,7 +21,7 @@ tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 21
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_import
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
 [value] using specification for function __gmpz_mul
 [value] using specification for function __gmpz_add
 [value] using specification for function __gmpz_cmp
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 5528763cc8e..f427ed71dbd 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -21,7 +21,7 @@ tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 21
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_import
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
 [value] using specification for function __gmpz_mul
 [value] using specification for function __gmpz_add
 [value] using specification for function __gmpz_cmp
-- 
GitLab