diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
index 83baf0203e8ad739d0ffa94738214be88e13dab7..c7114754530d7e8738b0795e17ba7349466248bc 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
@@ -20,19 +20,23 @@
 /*                                                                        */
 /**************************************************************************/
 
-/* Bit-level manipulations and endianness checks.
- * Should be included after e_acsl_printf.h and e_acsl_string.h headers. */
+/*! ***********************************************************************
+ * \file  e_acsl_bits.h
+ * \brief Bit-level manipulations and endianness checks.
+ *
+ * Should be included after e_acsl_printf.h and e_acsl_string.h headers.
+ *
+ * FIXME: Present implementation is built for little-endian byte order.  That
+ * is, the implementation assumes that least significant bytes are stored at
+ * the highest memory addresses. In future support for big-endian/PDP byte
+ * orders should also be provided.
+***************************************************************************/
 
 #ifndef E_ACSL_BITS
 #define E_ACSL_BITS
 
 #include <stdint.h>
 
-/* FIXME: Present implementation is built for little-endian byte order.  That
- * is, the implementation assumes that least significant bytes are stored at
- * the highest memory addresses. In future support for big-endian/PDP byte
- * orders should also be provided. */
-
 /* Check if we have little-endian and abort the execution otherwise. */
 #if __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
 #  error "Big-endian byte order is unsupported"
@@ -44,58 +48,117 @@
 
 /* Bit-level manipulations {{{ */
 
-/* 64-bit type with all bits set to zeroes */
-const uint64_t ZERO = 0;
-
 /* 64-bit type with all bits set to ones */
-const uint64_t ONE  = ~0;
+#define ONE UINT64_MAX
 
-/* Set a given bit in a number to '1'.
- * Example: bitset(7, x) changes 7th lowest bit of x to 1 */
+/* 64-bit type with all bits set to zeroes */
+#define ZERO (~ONE)
+
+/* Set a given bit in a number to '1' (least-significant bit is at index zero). *
+ * Example:
+ *  int x = 0;
+ *    // x => 0000 0000 ...
+ *  bitset(0, x)
+ *    // x => 1000 0000 ...
+ *  bitset(7, x)
+ *    // x => 1000 0001 ... */
 #define setbit(_bit,_number) (_number |= 1 << _bit)
 
-/* Same as bitset but the bit is set of 0 */
+/* Same as bitset but the bit cleared (set of zer0) */
 #define clearbit(_bit, _number) (_number &= ~(1 << _bit))
 
-/* Evaluates to a true value if a given bit in a number is set to 1. */
+/* Evaluates to a true value if a given bit in a number is set to 1.
+ *  int x = 1;
+ *    // x => 1000 0000 ...
+ *  checkbit(0, x) // true
+ *  checkbit(1, x) // false */
 #define checkbit(_bit, _number) ((_number >> _bit) & 1)
 
-/* Toggle a given bit. */
+/* Toggle a given bit.
+ * Example:
+ *  int x = 4; (assume little-endian)
+ *    // x => 0010 0000 ...
+ *  togglebit(3, x);
+ *    // x => 0000 0000 ...
+ *  togglebit(3, x);
+ *    // x => 0010 0000 ... */
 #define togglebit(_bit, _number) (_number ^= 1 << _bit)
 
 /* Set a given bit to a specified value (e.g., 0 or 1). */
 #define changebit(_bit, _val, _number) \
   (_number ^= (-_val ^ _number) & (1 << _bit))
 
-/* Set up to 64-bit in given number (from the left)
- * Example: setbits64(x, 7) sets first 7 bits in x to ones */
-#define setbits64(_number, _bits)   (_number |= ~(ONE << _bits))
-
-/* Same as setbits64 but clears bits (sets to zeroes) */
-#define clearbits64(_number, _bits) (_number &= ONE << _bits)
-
-/* Assume _number is a 64-bit number and sets _bits from the right to ones
- * Example: let x is a 64-bit zero, then setbits64(x, 7) will yield:
- *   00000000 00000000 00000000 00000000 00000000 00000000 00000000 01111111 */
-#define setbits64_right(_number, _bits)   (_number |= ~(ONE >> _bits))
+/* Set up to 64 bits from left to right to ones.
+ * Example:
+ *  int x = 0;
+ *    // x => 00000000 00000000 00000000 00000000
+ *  setbits64(11, x)
+ *    // => 11111111 11100000 00000000 00000000
+ *  setbits64(65, x)
+ *    // => behaviour undefined */
+#define setbits64(_bits, _number)   (_number |= ~(ONE << _bits))
+
+/* Same as `setbits64' but clear the bits (set to zeroes). */
+#define clearbits64(_bits, _number) (_number &= ONE << _bits)
+
+/* Assume that `_number' is a 64-bit integral type.
+ * Set `_bits' bits from right to the left starting from a 64-bit boundary.
+ * Example:
+ *  long x = 0;
+ *    // x => ... 00000000 00000000 00000000 00000000
+ *  setbits64_right(10, x)
+ *    // x => ... 00000000 00000000 00000011 11111111 */
+#define setbits64_right(_bits, _number)   (_number |= ~(ONE >> _bits))
 
 /* Same as setbits64_right but clears bits (sets to zeroes) */
-#define clearbits64_right(_number, _bits) (_number &= ONE >> _bits)
-
+#define clearbits64_right(_bits, _number) (_number &= ONE >> _bits)
+
+/* Set `size' bits starting from an address given by `ptr' to ones.
+ * Example:
+ *  char a[4];
+ *  memset(a,0,4);
+ *    // => 00000000 00000000 00000000 00000000
+ *  setbits(&a, 11);
+ *    // => 11111111 11100000 00000000 00000000 */
 void setbits(void *ptr, size_t size) {
   size_t i;
   int64_t *lp = (int64_t*)ptr;
   for (i = 0; i < size/64; i++)
     *(lp+i) |= ONE;
-  setbits64(*(lp+i), size%64);
+  setbits64(size%64, *(lp+i));
 }
 
+/* Same as `setbits' but clear the bits (set to zeroes). */
 void clearbits(void *ptr, size_t size) {
   size_t i;
   int64_t *lp = (int64_t*)ptr;
   for (i = 0; i < size/64; i++)
     *(lp+i) &= ZERO;
-  clearbits64(*(lp+i), size%64);
+  clearbits64(size%64, *(lp+i));
+}
+
+/* Same as `setbits' but set the bits from right to left
+ * Example:
+ *  char a[4];
+ *  memset(a,0,4);
+ *    // => 00000000 00000000 00000000 00000000
+ *  setbits_right(&a, 11);
+ *    // => 00000000 00000000 00000111 11111111 */
+void setbits_right(void *ptr, size_t size) {
+  size_t i = 0;
+  int64_t *lp = (int64_t*)ptr - 1;
+  for (i = 0; i < size/64; i++)
+    *(lp-i) |= ONE;
+  setbits64_right(size%64, *(lp-i));
+}
+
+/* Same as `setbits_right' but clear the bits (set to zeroes). */
+void clearbits_right(void *ptr, size_t size) {
+  size_t i = 0;
+  int64_t *lp = (int64_t*)ptr - 1;
+  for (i = 0; i < size/64; i++)
+    *(lp-i) &= ZERO;
+  clearbits64_right(size%64, *(lp-i));
 }
 /* }}} */
 #endif
\ No newline at end of file