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 7518f1bf81df4b16eedd9af835020b8c80d7f9fb..ce0db01659d2b7348ea4ae986f51eb216efeb567 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 d84dfc7f4a5a300dba460b65cce3f483b01c8e89..8ed98de11a26916713e76bf64f9ba18856c40e5b 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 35705b2fbe99a41bb36200de18473273ae961c9e..662538e38aa62051af9c1ff20a545fa3f83769d4 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 5528763cc8e38fec6631bd155a1c487876cfb158..f427ed71dbdb6794359520bdb7607831881e06bb 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