[RTL] Doxygen documentation for GMP headers

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));

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 */
 /*************/

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

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