[eacsl] Executing clang-format on C files

src/plugins/e-acsl/share/e-acsl/e_acsl.h

@@ -89,11 +89,11 @@
 /*** Generated code API {{{ ***/
 /************************************************************************/
 
-#include "observation_model/e_acsl_observation_model.h"
 #include "instrumentation_model/e_acsl_contract.h"
 #include "instrumentation_model/e_acsl_temporal.h"
 #include "numerical_model/e_acsl_floating_point.h"
 #include "numerical_model/e_acsl_gmp_api.h"
+#include "observation_model/e_acsl_observation_model.h"
 
 /* }}} */
 

src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c

@@ -22,7 +22,7 @@
 
 /* Get default definitions and macros e.g., PATH_MAX */
 #ifndef _DEFAULT_SOURCE
-# define _DEFAULT_SOURCE 1
+#  define _DEFAULT_SOURCE 1
 #endif
 
 /* On Windows, setup minimum version to Windows 8 (or Server 2012) to be able to
@@ -30,7 +30,7 @@
    Check directly for windows instead of using E_ACSL_OS_IS_WINDOWS so that it
    can be done without including anything. */
 #if defined(WIN32) || defined(_WIN32) || defined(__WIN32)
-# define _WIN32_WINNT 0x0602
+#  define _WIN32_WINNT 0x0602
 #endif
 
 // Internals

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c

@@ -37,22 +37,23 @@ int eacsl_runtime_sound_verdict = 1;
 #ifndef E_ACSL_EXTERNAL_ASSERT
 /*! \brief Default implementation of E-ACSL runtime assertions */
 void eacsl_runtime_assert(int predicate, int blocking, const char *kind,
-    const char *fct, const char *pred_txt, const char * file, int line) {
+                          const char *fct, const char *pred_txt,
+                          const char *file, int line) {
   if (eacsl_runtime_sound_verdict) {
-    if (! predicate) {
+    if (!predicate) {
       STDERR("%s: In function '%s'\n"
              "%s:%d: Error: %s failed:\n"
              "\tThe failing predicate is:\n"
              "\t%s.\n",
              file, fct, file, line, kind, pred_txt);
       if (blocking) {
-#ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
-#ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
+#  ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
+#    ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
         exit(E_ACSL_FAIL_EXITCODE);
-#else
+#    else
         raise_abort(file, line); /* Raise abort signal */
-#endif
-#endif
+#    endif
+#  endif
       }
     }
   } else
@@ -60,6 +61,6 @@ void eacsl_runtime_assert(int predicate, int blocking, const char *kind,
            "%s:%d: Warning: no sound verdict for %s (guess: %s).\n"
            "\tthe considered predicate is:\n"
            "\t%s\n",
-           file, fct, file, line, kind, predicate ? "ok": "FAIL", pred_txt);
+           file, fct, file, line, kind, predicate ? "ok" : "FAIL", pred_txt);
 }
 #endif

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h

@@ -57,7 +57,8 @@ extern int __attribute__((FC_BUILTIN)) eacsl_runtime_sound_verdict;
   @ complete behaviors;
   @ disjoint behaviors; */
 void eacsl_runtime_assert(int pred, int blocking, const char *kind,
-    const char *fct, const char *pred_txt, const char * file, int line)
-  __attribute__((FC_BUILTIN));
+                          const char *fct, const char *pred_txt,
+                          const char *file, int line)
+    __attribute__((FC_BUILTIN));
 
 #endif // E_ACSL_ASSERT_H

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c

@@ -35,124 +35,124 @@
 /*! \brief Return the index of the `char` where the bit number
     `global_bit_index` is located. */
 static inline size_t find_char_index(size_t global_bit_index) {
-    return global_bit_index / CHAR_BIT;
+  return global_bit_index / CHAR_BIT;
 }
 
 /*! \brief Return the index of the bit in the `char` given by
     \ref find_char_index for the bit number `global_bit_index`. */
 static inline size_t find_bit_index(size_t global_bit_index) {
-    return global_bit_index % CHAR_BIT;
+  return global_bit_index % CHAR_BIT;
 }
 
 /*! \brief Return the number of `char` to allocate to store `bit_count` bits. */
 static inline size_t find_char_count(size_t bit_count) {
-    size_t char_count = bit_count / CHAR_BIT;
-    if (bit_count % CHAR_BIT > 0) {
-        ++char_count;
-    }
-    return char_count;
+  size_t char_count = bit_count / CHAR_BIT;
+  if (bit_count % CHAR_BIT > 0) {
+    ++char_count;
+  }
+  return char_count;
 }
 
 /*! \brief Normalize the boolean parameter `value` to 0 or 1 */
 static inline int normalize_to_boolean(int value) {
-    return value ? 1 : 0;
+  return value ? 1 : 0;
 }
 
 /* Documented in e_acsl.h */
 struct contract_t {
-    /*! \brief Number of cells in the char array used to store the results of
+  /*! \brief Number of cells in the char array used to store the results of
      * the assumes clauses.
      */
-    size_t char_count;
+  size_t char_count;
 
-    /*! \brief Char array to store the results of the assumes clauses. One bit
+  /*! \brief Char array to store the results of the assumes clauses. One bit
      * per behavior.
      *
      * The functions \ref find_char_index() and \ref find_bit_index() can be
      * used to find the location of the bit for a specific behavior. */
-    char * assumes;
+  char *assumes;
 };
 
 /* Documented in e_acsl.h */
-contract_t * contract_init(size_t size) {
-    // Allocate memory for the structure
-    contract_t * c = malloc(sizeof(contract_t));
-    DVASSERT(c != NULL,
-        "Unable to allocate %d bytes of memory for contract_t",
-        sizeof(contract_t));
-
-    // Compute the number of char needed to store `size` behaviors, assuming
-    // that one behavior is stored in one bit.
-    c->char_count = find_char_count(size);
-
-    // Allocate an array of char of the computed count
-    if (c->char_count > 0) {
-        c->assumes = calloc(c->char_count, sizeof(char));
-        DVASSERT(c->assumes != NULL,
-            "Unable to allocate %d cells of %d bytes of memory for contract_t::assumes",
-            c->char_count, sizeof(char));
-    } else {
-        c->assumes = NULL;
-    }
-
-    return c;
+contract_t *contract_init(size_t size) {
+  // Allocate memory for the structure
+  contract_t *c = malloc(sizeof(contract_t));
+  DVASSERT(c != NULL, "Unable to allocate %d bytes of memory for contract_t",
+           sizeof(contract_t));
+
+  // Compute the number of char needed to store `size` behaviors, assuming
+  // that one behavior is stored in one bit.
+  c->char_count = find_char_count(size);
+
+  // Allocate an array of char of the computed count
+  if (c->char_count > 0) {
+    c->assumes = calloc(c->char_count, sizeof(char));
+    DVASSERT(c->assumes != NULL,
+             "Unable to allocate %d cells of %d bytes of memory for "
+             "contract_t::assumes",
+             c->char_count, sizeof(char));
+  } else {
+    c->assumes = NULL;
+  }
+
+  return c;
 }
 
 /* Documented in e_acsl.h */
-void contract_clean(contract_t * c) {
-    // Free array of char
-    free(c->assumes);
-    // Free structure
-    free(c);
+void contract_clean(contract_t *c) {
+  // Free array of char
+  free(c->assumes);
+  // Free structure
+  free(c);
 }
 
 /* Documented in e_acsl.h */
-void contract_set_behavior_assumes(contract_t * c, size_t i, int assumes) {
-    size_t char_idx = find_char_index(i);
-    DVASSERT(char_idx < c->char_count,
-        "Out of bound char index %d (char_count: %d)",
-        char_idx, c->char_count);
-    size_t bit_idx = find_bit_index(i);
-    assumes = normalize_to_boolean(assumes);
-    c->assumes[char_idx] |= (assumes<<bit_idx);
+void contract_set_behavior_assumes(contract_t *c, size_t i, int assumes) {
+  size_t char_idx = find_char_index(i);
+  DVASSERT(char_idx < c->char_count,
+           "Out of bound char index %d (char_count: %d)", char_idx,
+           c->char_count);
+  size_t bit_idx = find_bit_index(i);
+  assumes = normalize_to_boolean(assumes);
+  c->assumes[char_idx] |= (assumes << bit_idx);
 }
 
 /* Documented in e_acsl.h */
-int contract_get_behavior_assumes(const contract_t * c, size_t i) {
-    size_t char_idx = find_char_index(i);
-    DVASSERT(char_idx < c->char_count,
-        "Out of bound char index %d (char_count: %d)",
-        char_idx, c->char_count);
-    size_t bit_idx = find_bit_index(i);
-    int result = c->assumes[char_idx] & (1<<bit_idx);
-    return normalize_to_boolean(result);
+int contract_get_behavior_assumes(const contract_t *c, size_t i) {
+  size_t char_idx = find_char_index(i);
+  DVASSERT(char_idx < c->char_count,
+           "Out of bound char index %d (char_count: %d)", char_idx,
+           c->char_count);
+  size_t bit_idx = find_bit_index(i);
+  int result = c->assumes[char_idx] & (1 << bit_idx);
+  return normalize_to_boolean(result);
 }
 
 /* Documented in e_acsl.h */
-int contract_partial_count_behaviors(const contract_t * c, size_t count, ...) {
-    va_list args;
-    va_start(args, count);
+int contract_partial_count_behaviors(const contract_t *c, size_t count, ...) {
+  va_list args;
+  va_start(args, count);
 
-    int result = 0;
-    for (size_t i = 0 ; i < 2 && i < count ; ++i) {
-        result += contract_get_behavior_assumes(c, va_arg(args, int));
-    }
+  int result = 0;
+  for (size_t i = 0; i < 2 && i < count; ++i) {
+    result += contract_get_behavior_assumes(c, va_arg(args, int));
+  }
 
-    va_end(args);
-    return result;
+  va_end(args);
+  return result;
 }
 
 /* Documented in e_acsl.h */
-int contract_partial_count_all_behaviors(const contract_t * c) {
-    int result = 0;
-    for (int i = 0 ; i < c->char_count && result < 2 ; ++i) {
-        // Counting bits set with Kernighan's algorithm, but stopping at two
-        // bits set.
-        // cf. <https://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetKernighan>
-        unsigned char assumes_cell = c->assumes[i];
-        for (; assumes_cell && result < 2 ; ++result) {
-            assumes_cell &= assumes_cell - 1;
-        }
+int contract_partial_count_all_behaviors(const contract_t *c) {
+  int result = 0;
+  for (int i = 0; i < c->char_count && result < 2; ++i) {
+    // Counting bits set with Kernighan's algorithm, but stopping at two
+    // bits set.
+    // cf. <https://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetKernighan>
+    unsigned char assumes_cell = c->assumes[i];
+    for (; assumes_cell && result < 2; ++result) {
+      assumes_cell &= assumes_cell - 1;
     }
-    return result;
+  }
+  return result;
 }

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h

@@ -33,18 +33,22 @@
 #include "../internals/e_acsl_alias.h"
 
 #ifdef __FC_STDLIB
-#include <__fc_alloc_axiomatic.h>
+#  include <__fc_alloc_axiomatic.h>
 #else
 /*@ ghost extern int __fc_heap_status; */
 #endif
 
-#define contract_t                            export_alias(contract_t)
-#define contract_init                         export_alias(contract_init)
-#define contract_clean                        export_alias(contract_clean)
-#define contract_set_behavior_assumes         export_alias(contract_set_behavior_assumes)
-#define contract_get_behavior_assumes         export_alias(contract_get_behavior_assumes)
-#define contract_partial_count_behaviors      export_alias(contract_partial_count_behaviors)
-#define contract_partial_count_all_behaviors  export_alias(contract_partial_count_all_behaviors)
+#define contract_t     export_alias(contract_t)
+#define contract_init  export_alias(contract_init)
+#define contract_clean export_alias(contract_clean)
+#define contract_set_behavior_assumes                                          \
+  export_alias(contract_set_behavior_assumes)
+#define contract_get_behavior_assumes                                          \
+  export_alias(contract_get_behavior_assumes)
+#define contract_partial_count_behaviors                                       \
+  export_alias(contract_partial_count_behaviors)
+#define contract_partial_count_all_behaviors                                   \
+  export_alias(contract_partial_count_all_behaviors)
 
 /*! \brief Structure to hold pieces of information about function and statement
  * contracts at runtime. */
@@ -58,7 +62,7 @@ typedef struct contract_t __attribute__((__FC_BUILTIN__)) contract_t;
  */
 /*@ assigns \result \from indirect:__fc_heap_status, indirect:size;
   @ admit ensures \valid(\result); */
-contract_t * contract_init(size_t size) __attribute__((FC_BUILTIN));
+contract_t *contract_init(size_t size) __attribute__((FC_BUILTIN));
 
 /*! \brief Cleanup the structure `c` previously allocated by
  * \ref contract_init.
@@ -67,7 +71,7 @@ contract_t * contract_init(size_t size) __attribute__((FC_BUILTIN));
  */
 /*@ requires \valid(c);
   @ assigns \nothing; */
-void contract_clean(contract_t * c) __attribute__((FC_BUILTIN));
+void contract_clean(contract_t *c) __attribute__((FC_BUILTIN));
 
 /*! \brief Set the result of the assumes clauses for the behavior `i` in the
  * structure.
@@ -79,8 +83,8 @@ void contract_clean(contract_t * c) __attribute__((FC_BUILTIN));
  */
 /*@ requires \valid(c);
   @ assigns *c \from indirect:c, indirect:i, assumes; */
-void contract_set_behavior_assumes(contract_t * c, size_t i, int assumes)
-  __attribute__((FC_BUILTIN));
+void contract_set_behavior_assumes(contract_t *c, size_t i, int assumes)
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Retrieve the result of the assumes clauses for the behavior `i` from
  * the structure.
@@ -94,8 +98,8 @@ void contract_set_behavior_assumes(contract_t * c, size_t i, int assumes)
 /*@ requires \valid_read(c);
   @ assigns \result \from indirect:c, indirect:i;
   @ ensures \result == 0 || \result == 1; */
-int contract_get_behavior_assumes(const contract_t * c, size_t i)
-  __attribute__((FC_BUILTIN));
+int contract_get_behavior_assumes(const contract_t *c, size_t i)
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Count the number of active behaviors among the `count` given
  * behaviors.
@@ -108,8 +112,8 @@ int contract_get_behavior_assumes(const contract_t * c, size_t i)
  * \return 0 if no behaviors are active, 1 if exactly one behavior is active,
  *         and 2 if more than one behavior is active.
  */
-int contract_partial_count_behaviors(const contract_t * c, size_t count, ...)
-  __attribute__((FC_BUILTIN));
+int contract_partial_count_behaviors(const contract_t *c, size_t count, ...)
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Count the number of active behaviors among all the behaviors of the
  * contract.
@@ -118,7 +122,7 @@ int contract_partial_count_behaviors(const contract_t * c, size_t count, ...)
  * \return 0 if no behaviors are active, 1 if exactly one behavior is active,
  *         and 2 if more than one behavior is active.
  */
-int contract_partial_count_all_behaviors(const contract_t * c)
-  __attribute__((FC_BUILTIN));
+int contract_partial_count_all_behaviors(const contract_t *c)
+    __attribute__((FC_BUILTIN));
 
 #endif

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c

@@ -22,14 +22,14 @@
 
 #ifdef E_ACSL_TEMPORAL
 
-#include <stddef.h>
+#  include <stddef.h>
 
-#include "../internals/e_acsl_private_assert.h"
-#include "../observation_model/internals/e_acsl_omodel_debug.h"
-#include "../observation_model/internals/e_acsl_timestamp_retrieval.h"
-#include "e_acsl_temporal_timestamp.h"
+#  include "../internals/e_acsl_private_assert.h"
+#  include "../observation_model/internals/e_acsl_omodel_debug.h"
+#  include "../observation_model/internals/e_acsl_timestamp_retrieval.h"
+#  include "e_acsl_temporal_timestamp.h"
 
-#include "e_acsl_temporal.h"
+#  include "e_acsl_temporal.h"
 
 /* Temporal store {{{ */
 void eacsl_temporal_store_nblock(void *lhs, void *rhs) {
@@ -45,7 +45,7 @@ void eacsl_temporal_store_nreferent(void *lhs, void *rhs) {
 void eacsl_temporal_memcpy(void *dest, void *src, size_t size) {
   /* Memcpy is only relevant for pointers here, so if there is a
    * copy under a pointer's size then there no point in copying memory*/
-  if (size >= sizeof(void*)) {
+  if (size >= sizeof(void *)) {
     DVALIDATE_ALLOCATED(src, size, src);
     DVALIDATE_WRITEABLE(dest, size, dest);
     void *dest_shadow = (void *)temporal_referent_shadow(dest);
@@ -79,18 +79,18 @@ void eacsl_temporal_save_copy_parameter(void *ptr, unsigned int param) {
 
 void eacsl_temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
   struct temporal_parameter *tpar = &parameter_referents[param];
-  switch(tpar->temporal_flow) {
-    case TBlockN:
-      store_temporal_referent(ptr, origin_timestamp(tpar->ptr));
-      break;
-    case TReferentN:
-      store_temporal_referent(ptr, referent_timestamp(tpar->ptr));
-      break;
-    case TCopy:
-      eacsl_temporal_memcpy(ptr, tpar->ptr, size);
-      break;
-    default:
-      private_assert(0, "Unreachable", NULL);
+  switch (tpar->temporal_flow) {
+  case TBlockN:
+    store_temporal_referent(ptr, origin_timestamp(tpar->ptr));
+    break;
+  case TReferentN:
+    store_temporal_referent(ptr, referent_timestamp(tpar->ptr));
+    break;
+  case TCopy:
+    eacsl_temporal_memcpy(ptr, tpar->ptr, size);
+    break;
+  default:
+    private_assert(0, "Unreachable", NULL);
   }
 }
 
@@ -101,7 +101,7 @@ void eacsl_temporal_reset_parameters() {
 
 /* Return values {{{ */
 void eacsl_temporal_save_return(void *ptr) {
-  return_referent = (ptr, sizeof(void*)) ? referent_timestamp(ptr) : 0;
+  return_referent = (ptr, sizeof(void *)) ? referent_timestamp(ptr) : 0;
 }
 
 void eacsl_temporal_pull_return(void *ptr) {

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h

@@ -54,13 +54,13 @@
  * store it as a referent number of a pointer given by `ptr_addr`. */
 /*@ assigns \nothing; */
 void eacsl_temporal_store_nblock(void *lhs, void *rhs)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Same as `eacsl_temporal_store_nblock` but take a referent
  * number of `block_addr` instead */
 /*@ assigns \nothing; */
 void eacsl_temporal_store_nreferent(void *lhs, void *rhs)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /* }}} */
 
@@ -70,13 +70,13 @@ void eacsl_temporal_store_nreferent(void *lhs, void *rhs)
  * [dest, dest + size]. Counterpart of the memcpy function */
 /*@ assigns \nothing; */
 void eacsl_temporal_memcpy(void *dest, void *src, size_t size)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Set temporal shadow data from [src, src + size] to 0.
  * Counterpart of memset the function */
 /*@ assigns \nothing; */
 void eacsl_temporal_memset(void *dest, int c, size_t size)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 /* }}} */
 
 /* Function parameters {{{ */
@@ -85,30 +85,29 @@ void eacsl_temporal_memset(void *dest, int c, size_t size)
  *  in the global parameter array. */
 /*@ assigns \nothing; */
 void eacsl_temporal_save_nblock_parameter(void *ptr, unsigned int param)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /*! \brief store struct { .ptr = ptr, .temporal_flow = TReferentN }
  *  in the global parameter array. */
 /*@ assigns \nothing; */
 void eacsl_temporal_save_nreferent_parameter(void *ptr, unsigned int param)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /*! \brief store struct { .ptr = ptr, .temporal_flow = TCopy } in the global
  *  parameter array. */
 /*@ assigns \nothing; */
 void eacsl_temporal_save_copy_parameter(void *ptr, unsigned int param)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Assign a referent number of `ptr` based on the record in the global
  * parameter array at index `param`. */
 /*@ assigns \nothing; */
 void eacsl_temporal_pull_parameter(void *ptr, unsigned int param, size_t size)
-  __attribute__((FC_BUILTIN));
+    __attribute__((FC_BUILTIN));
 
 /*! \brief Nullify global parameter array  */
 /*@ assigns \nothing; */
-void eacsl_temporal_reset_parameters()
-  __attribute__((FC_BUILTIN));
+void eacsl_temporal_reset_parameters() __attribute__((FC_BUILTIN));
 /* }}} */
 
 /* Return values {{{ */
@@ -116,20 +115,17 @@ void eacsl_temporal_reset_parameters()
 /*! \brief Save temporal referent number of `ptr` in a placeholder variable
  * tracking the referent number of a function's return. */
 /*@ assigns \nothing; */
-void eacsl_temporal_save_return(void *ptr)
-  __attribute__((FC_BUILTIN));
+void eacsl_temporal_save_return(void *ptr) __attribute__((FC_BUILTIN));
 
 /*! \brief Take a temporal referent stored in the placeholder tracking return
  * values  as a temporal referent number of `ptr`. */
 /*@ assigns \nothing; */
-void eacsl_temporal_pull_return(void *ptr)
-  __attribute__((FC_BUILTIN));
+void eacsl_temporal_pull_return(void *ptr) __attribute__((FC_BUILTIN));
 
 /*! \brief Nullify a placeholder variable tracking the referent number of a
  * function's return. */
 /*@ assigns \nothing; */
-void eacsl_temporal_reset_return()
-  __attribute__((FC_BUILTIN));
+void eacsl_temporal_reset_return() __attribute__((FC_BUILTIN));
 /* }}} */
 
 /* Temporal valid {{{ */

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h

@@ -30,8 +30,8 @@
 
 #ifdef E_ACSL_TEMPORAL /*{{{*/
 
-#include "../internals/e_acsl_rtl_string.h"
-#include <stdint.h>
+#  include "../internals/e_acsl_rtl_string.h"
+#  include <stdint.h>
 
 /*! Temporal time stamp generator variable
  * Time stamp is generated by incrementing `temporal_timestamp` variable.
@@ -43,23 +43,19 @@
  *  `>1` - heap or stack blocks allocated during a program's execution */
 static uint32_t temporal_timestamp = 2;
 
-#define INVALID_TEMPORAL_TIMESTAMP 0
-#define GLOBAL_TEMPORAL_TIMESTAMP 1
-#define NEW_TEMPORAL_TIMESTAMP() (++temporal_timestamp)
+#  define INVALID_TEMPORAL_TIMESTAMP 0
+#  define GLOBAL_TEMPORAL_TIMESTAMP  1
+#  define NEW_TEMPORAL_TIMESTAMP()   (++temporal_timestamp)
 
 /*! Maximal number of parameters a function can accept
  * [ C99, 5.2.4.1 Translation Limits ] */
-#define MAX_PARAMETERS 127
+#  define MAX_PARAMETERS 127
 
 struct temporal_parameter {
   void *ptr;
   /* Number all members such that there is no `0` which potentially
      corresponds to an invalid number */
-  enum {
-    TBlockN = 10,
-    TReferentN  = 20,
-    TCopy = 30
-  } temporal_flow;
+  enum { TBlockN = 10, TReferentN = 20, TCopy = 30 } temporal_flow;
 };
 
 typedef struct temporal_parameter temporal_parameter;
@@ -72,8 +68,8 @@ typedef struct temporal_parameter temporal_parameter;
 static temporal_parameter parameter_referents[MAX_PARAMETERS];
 static uint32_t return_referent;
 
-#define reset_parameter_referents() \
-  memset(parameter_referents, 0, sizeof(parameter_referents))
+#  define reset_parameter_referents()                                          \
+    memset(parameter_referents, 0, sizeof(parameter_referents))
 
 #endif /*}}} E_ACSL_TEMPORAL */
 #endif /*}}} E_ACSL_TEMPORAL_TIMESTAMP */

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_alias.h

@@ -29,11 +29,11 @@
 #define E_ACSL_ALIAS_H
 
 /* Concatenation of 2 tokens */
-# define preconcat(x,y) x ## y
-# define concat(x,y) preconcat(x,y)
+#define preconcat(x, y) x##y
+#define concat(x, y)    preconcat(x, y)
 /** Prefix of public functions */
-# define export_prefix __e_acsl_
+#define export_prefix __e_acsl_
 /** Add public prefix to an identifier */
-# define export_alias(_n) concat(export_prefix, _n)
+#define export_alias(_n) concat(export_prefix, _n)
 
 #endif

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h

@@ -38,8 +38,8 @@
 #ifndef E_ACSL_BITS_H
 #define E_ACSL_BITS_H
 
-#include <stdint.h>
 #include <stddef.h>
+#include <stdint.h>
 
 /* Bit-level manipulations {{{ */
 
@@ -54,7 +54,7 @@
  *  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)
+#define setbit(_bit, _number) (_number |= 1 << _bit)
 
 /** Same as bitset but the `_bit` bit is cleared (i.e., set of zero) */
 #define clearbit(_bit, _number) (_number &= ~(1 << _bit))
@@ -73,7 +73,7 @@
 #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) \
+#define changebit(_bit, _val, _number)                                         \
   (_number ^= (-_val ^ _number) & (1 << _bit))
 
 /** Set up to 64 bits from left to right to ones.
@@ -81,14 +81,14 @@
  *  int x = 0;        // x => 00000000 00000000 ...
  *  setbits64(11, x)  //   => 11111111 11100000 ...
  *  setbits64(64, x)  //   => behaviour undefined */
-#define setbits64(_bits, _number)   (_number |= ~(ONE << _bits))
+#define setbits64(_bits, _number) (_number |= ~(ONE << _bits))
 
 /** Set up to 64 bits from left to right to ones skiping `_skip` leftmost bits
  * Example:
  *  int x = 0;          // x => 00000000 00000000 ...
  *  setbits64(11, x, 2) //   => 00111111 11111000 ...
  *  setbits64(64, x, 2) //   => behaviour undefined */
-#define setbits64_skip(_bits, _number, _skip) \
+#define setbits64_skip(_bits, _number, _skip)                                  \
   (_number |= ~(ONE << _bits) << _skip)
 
 /** Evaluate to 1 if up to 64 bits from left to right in `_number` are set:
@@ -98,8 +98,8 @@
  *  checkbits64(5, x)   //   => 1
  *  checkbits64(6, x)   //   => 0
  *  checkbits64(64, x)  //   => behaviour undefined */
-#define checkbits64(_bits, _number) \
-  ((_number & ~(ONE << _bits)) ==  (~(ONE << _bits)))
+#define checkbits64(_bits, _number)                                            \
+  ((_number & ~(ONE << _bits)) == (~(ONE << _bits)))
 
 /** Same as checkbits64 but with skipping `_skip` leftmost bits
  * Example:
@@ -109,7 +109,7 @@
  *  checkbits64_skip(5,  x, 2) // => 0
  *  checkbits64_skip(3,  x, 1) // => 0
  *  checkbits64_skip(64, x, 0) // => behaviour undefined */
-#define checkbits64_skip(_bits, _number, _skip) \
+#define checkbits64_skip(_bits, _number, _skip)                                \
   ((_number & ~(ONE << _bits) << _skip) == (~(ONE << _bits) << _skip))
 
 /** Same as `setbits64' but clear the bits (set to zeroes). */
@@ -119,7 +119,7 @@
  * 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))
+#define setbits64_right(_bits, _number) (_number |= ~(ONE >> _bits))
 
 /** Same as setbits64_right but clears bits (sets to zeroes) */
 #define clearbits64_right(_bits, _number) (_number &= ONE >> _bits)
@@ -131,30 +131,30 @@
  *  setbits(&a, 11);  // => 11111111 11100000 00000000 00000000 */
 static inline void setbits(size_t size, void *ptr) {
   size_t i;
-  int64_t *lp = (int64_t*)ptr;
-  for (i = 0; i < size/64; i++)
-    *(lp+i) |= ONE;
-  setbits64(size%64, *(lp+i));
+  int64_t *lp = (int64_t *)ptr;
+  for (i = 0; i < size / 64; i++)
+    *(lp + i) |= ONE;
+  setbits64(size % 64, *(lp + i));
 }
 
 /** Same as `setbits' but clear the bits (set to zeroes). */
 static inline void clearbits(size_t size, void *ptr) {
   size_t i;
-  int64_t *lp = (int64_t*)ptr;
-  for (i = 0; i < size/64; i++)
-    *(lp+i) &= ZERO;
-  clearbits64(size%64, *(lp+i));
+  int64_t *lp = (int64_t *)ptr;
+  for (i = 0; i < size / 64; i++)
+    *(lp + i) &= ZERO;
+  clearbits64(size % 64, *(lp + i));
 }
 
 /** Same as `setbits' but clear the bits (set to zeroes). */
 static inline int checkbits(size_t size, void *ptr) {
   size_t i;
-  int64_t *lp = (int64_t*)ptr;
-  for (i = 0; i < size/64; i++) {
-    if (*(lp+i) != ONE)
+  int64_t *lp = (int64_t *)ptr;
+  for (i = 0; i < size / 64; i++) {
+    if (*(lp + i) != ONE)
       return 0;
   }
-  return checkbits64(size%64, *(lp+i));
+  return checkbits64(size % 64, *(lp + i));
 }
 
 /** Same as `setbits' but set the bits from right to left
@@ -164,19 +164,19 @@ static inline int checkbits(size_t size, void *ptr) {
  *  setbits_right(&a, 11); // => 00000000 00000000 00000111 11111111 */
 static inline void setbits_right(size_t size, void *ptr) {
   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));
+  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). */
 static inline void clearbits_right(size_t size, void *ptr) {
   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));
+  int64_t *lp = (int64_t *)ptr - 1;
+  for (i = 0; i < size / 64; i++)
+    *(lp - i) &= ZERO;
+  clearbits64_right(size % 64, *(lp - i));
 }
 
 #endif // E_ACSL_BITS_H

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h

@@ -34,9 +34,9 @@
 
 // OS detection
 //  - Assign values to specific OSes
-#define E_ACSL_OS_LINUX_VALUE 1
+#define E_ACSL_OS_LINUX_VALUE   1
 #define E_ACSL_OS_WINDOWS_VALUE 2
-#define E_ACSL_OS_OTHER_VALUE 999
+#define E_ACSL_OS_OTHER_VALUE   999
 //  - Declare defines to test for a specific OS
 /*!
  * \brief True if the target OS is linux, false otherwise
@@ -53,14 +53,14 @@
 //  - Check current OS
 #ifdef __linux__
 // Linux compilation
-# define E_ACSL_OS E_ACSL_OS_LINUX_VALUE
+#  define E_ACSL_OS E_ACSL_OS_LINUX_VALUE
 #elif defined(WIN32) || defined(_WIN32) || defined(__WIN32)
 // Windows compilation
-# define E_ACSL_OS E_ACSL_OS_WINDOWS_VALUE
+#  define E_ACSL_OS E_ACSL_OS_WINDOWS_VALUE
 #else
 // Other
-# define E_ACSL_OS E_ACSL_OS_OTHER_VALUE
-# error "Unsupported OS for E-ACSL RTL"
+#  define E_ACSL_OS E_ACSL_OS_OTHER_VALUE
+#  error "Unsupported OS for E-ACSL RTL"
 #endif
 
 #endif // E_ACSL_CONFIG_H

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c

@@ -20,8 +20,8 @@
 /*                                                                        */
 /**************************************************************************/
 
-#include <sys/stat.h>
 #include <fcntl.h>
+#include <sys/stat.h>
 
 #include "../observation_model/internals/e_acsl_omodel_debug.h"
 #include "e_acsl_config.h"
@@ -46,13 +46,14 @@ void initialize_report_file(int *argc, char ***argv) {
   if (!strcmp(dlog_name, "-") || !strcmp(dlog_name, "1")) {
     dlog_fd = 2;
   } else {
-#if E_ACSL_OS_IS_LINUX
-    dlog_fd = open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC | O_NONBLOCK
-      | O_NOCTTY, S_IRUSR | S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH | S_IWOTH);
-#elif E_ACSL_OS_IS_WINDOWS
-    dlog_fd = _open(dlog_name, _O_WRONLY | _O_CREAT | _O_TRUNC,
-      _S_IREAD | _S_IWRITE);
-#endif
+#  if E_ACSL_OS_IS_LINUX
+    dlog_fd =
+        open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC | O_NONBLOCK | O_NOCTTY,
+             S_IRUSR | S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH | S_IWOTH);
+#  elif E_ACSL_OS_IS_WINDOWS
+    dlog_fd =
+        _open(dlog_name, _O_WRONLY | _O_CREAT | _O_TRUNC, _S_IREAD | _S_IWRITE);
+#  endif
   }
   if (dlog_fd == -1)
     private_abort("Cannot open file descriptor for %s\n", dlog_name);
@@ -62,39 +63,41 @@ void initialize_report_file(int *argc, char ***argv) {
 // }}}
 
 #ifdef E_ACSL_WEAK_VALIDITY
-# define E_ACSL_VALIDITY_DESC "weak"
+#  define E_ACSL_VALIDITY_DESC "weak"
 #else
-# define E_ACSL_VALIDITY_DESC "strong"
+#  define E_ACSL_VALIDITY_DESC "strong"
 #endif
 
 #ifdef E_ACSL_NO_ASSERT_FAIL
-# define E_ACSL_ASSERT_NO_FAIL_DESC "pass through"
+#  define E_ACSL_ASSERT_NO_FAIL_DESC "pass through"
 #else
-# define E_ACSL_ASSERT_NO_FAIL_DESC "abort"
+#  define E_ACSL_ASSERT_NO_FAIL_DESC "abort"
 #endif
 
 #ifdef E_ACSL_TEMPORAL
-#define E_ACSL_TEMPORAL_DESC "enabled"
+#  define E_ACSL_TEMPORAL_DESC "enabled"
 #else
-# define E_ACSL_TEMPORAL_DESC "disabled"
+#  define E_ACSL_TEMPORAL_DESC "disabled"
 #endif // E_ACSL_TEMPORAL
 
 #ifndef E_ACSL_VALIDATE_FORMAT_STRINGS
-# define E_ACSL_FORMAT_VALIDITY_DESC "disabled"
+#  define E_ACSL_FORMAT_VALIDITY_DESC "disabled"
 #else
-# define E_ACSL_FORMAT_VALIDITY_DESC "enabled"
+#  define E_ACSL_FORMAT_VALIDITY_DESC "enabled"
 #endif // E_ACSL_VALIDATE_FORMAT_STRINGS
 
 void describe_run() {
 #if defined(E_ACSL_VERBOSE)
-  rtl_printf("/* ========================================================= */\n");
-  rtl_printf(" * E-ACSL instrumented run\n" );
+  rtl_printf(
+      "/* ========================================================= */\n");
+  rtl_printf(" * E-ACSL instrumented run\n");
   rtl_printf(" * Execution mode:  %s\n", E_ACSL_DEBUG_DESC);
   describe_observation_model();
   rtl_printf(" * Assertions mode: %s\n", E_ACSL_ASSERT_NO_FAIL_DESC);
   rtl_printf(" * Validity notion: %s\n", E_ACSL_VALIDITY_DESC);
   rtl_printf(" * Temporal checks: %s\n", E_ACSL_TEMPORAL_DESC);
   rtl_printf(" * Format Checks:   %s\n", E_ACSL_FORMAT_VALIDITY_DESC);
-  rtl_printf("/* ========================================================= */\n");
+  rtl_printf(
+      "/* ========================================================= */\n");
 #endif
 }

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h

@@ -43,35 +43,35 @@
  * Enabled in the presence of the E_ACSL_DEBUG macro */
 #ifdef E_ACSL_DEBUG
 
-#define E_ACSL_DEBUG_DESC "debug"
+#  define E_ACSL_DEBUG_DESC "debug"
 
-#include "e_acsl_private_assert.h"
-#include "e_acsl_rtl_io.h"
+#  include "e_acsl_private_assert.h"
+#  include "e_acsl_rtl_io.h"
 
-#include <stdio.h>
+#  include <stdio.h>
 
 /* Default location of the E_ACSL log file */
-#ifndef E_ACSL_DEBUG_LOG
-#  define E_ACSL_DEBUG_LOG -
-#endif
+#  ifndef E_ACSL_DEBUG_LOG
+#    define E_ACSL_DEBUG_LOG -
+#  endif
 
 /*! \brief File descriptor associated with the debug log file */
 int dlog_fd;
 
 /*! \brief Output a message to a log file */
-#define DLOG(...) rtl_dprintf(dlog_fd, __VA_ARGS__)
+#  define DLOG(...) rtl_dprintf(dlog_fd, __VA_ARGS__)
 
-#ifdef E_ACSL_DEBUG_VERBOSE
-# define DVLOG(...) rtl_dprintf(dlog_fd, __VA_ARGS__)
-#else
-# define DVLOG(...)
-#endif
+#  ifdef E_ACSL_DEBUG_VERBOSE
+#    define DVLOG(...) rtl_dprintf(dlog_fd, __VA_ARGS__)
+#  else
+#    define DVLOG(...)
+#  endif
 
 /*! \brief Debug-time assertion based on assert (see e_acsl_assert.h) */
-#define DASSERT(_e) private_assert(_e,TOSTRING(_e),NULL)
+#  define DASSERT(_e) private_assert(_e, TOSTRING(_e), NULL)
 
 /*! \brief Debug-time assertion based on vassert (see e_acsl_assert.h) */
-#define DVASSERT(_expr, _fmt, ...) private_assert(_expr, _fmt, __VA_ARGS__)
+#  define DVASSERT(_expr, _fmt, ...) private_assert(_expr, _fmt, __VA_ARGS__)
 
 /*! \brief Initialize debug report file:
  *  - open file descriptor
@@ -79,11 +79,14 @@ int dlog_fd;
 void initialize_report_file(int *argc, char ***argv);
 
 int debug_stop_number;
-#define DSTOP { \
-  DLOG(" << ***** " "Debug Stop %d in '%s' at %s:%d" " ***** >> ", \
-    ++debug_stop_number, __func__, __FILE__, __LINE__); \
-  getchar(); \
-}
+#  define DSTOP                                                                \
+    {                                                                          \
+      DLOG(" << ***** "                                                        \
+           "Debug Stop %d in '%s' at %s:%d"                                    \
+           " ***** >> ",                                                       \
+           ++debug_stop_number, __func__, __FILE__, __LINE__);                 \
+      getchar();                                                               \
+    }
 
 #else
 #  define E_ACSL_DEBUG_DESC "production"

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c

@@ -23,11 +23,11 @@
 #include "e_acsl_malloc.h"
 
 struct memory_spaces mem_spaces = {
-  .rtl_mspace = NULL,
-  .heap_mspace = NULL,
-  .heap_start = 0,
-  .heap_end = 0,
-  .heap_mspace_least = 0,
+    .rtl_mspace = NULL,
+    .heap_mspace = NULL,
+    .heap_start = 0,
+    .heap_end = 0,
+    .heap_mspace_least = 0,
 };
 
 /* \brief Create two memory spaces, one for RTL and the other for application
@@ -38,11 +38,13 @@ void eacsl_make_memory_spaces(size_t rtl_size, size_t heap_size) {
   mem_spaces.heap_mspace = eacsl_create_mspace(heap_size, 0);
   /* Do not use `eacsl_mspace_least_addr` here, as it returns the address of the
      mspace header. */
-  mem_spaces.heap_start = (uintptr_t)eacsl_mspace_malloc(mem_spaces.heap_mspace,1);
+  mem_spaces.heap_start =
+      (uintptr_t)eacsl_mspace_malloc(mem_spaces.heap_mspace, 1);
   mem_spaces.heap_end = mem_spaces.heap_start + heap_size;
   /* Save initial least address of heap memspace. This address is used later
      to check whether memspace has been moved. */
-  mem_spaces.heap_mspace_least = (uintptr_t)eacsl_mspace_least_addr(mem_spaces.heap_mspace);
+  mem_spaces.heap_mspace_least =
+      (uintptr_t)eacsl_mspace_least_addr(mem_spaces.heap_mspace);
 }
 
 void eacsl_destroy_memory_spaces() {

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h

@@ -35,18 +35,18 @@
 #ifndef E_ACSL_MALLOC_H
 #define E_ACSL_MALLOC_H
 
-#include <stdint.h>
 #include <stddef.h>
+#include <stdint.h>
 
 #include "e_acsl_alias.h"
 
 /* Block size units in bytes */
-#define KB (1024)         //!< Bytes in a kilobyte
-#define MB (1024*KB)      //!< Bytes in a megabyte
-#define GB (1024*MB)      //!< Bytes in a gigabyte
-#define KB_SZ(_s) (_s/KB) //!< Convert bytes to kilobytes
-#define MB_SZ(_s) (_s/MB) //!< Convert bytes to megabytes
-#define GB_SZ(_s) (_s/GB) //!< Convert bytes to gigabytes
+#define KB        (1024)      //!< Bytes in a kilobyte
+#define MB        (1024 * KB) //!< Bytes in a megabyte
+#define GB        (1024 * MB) //!< Bytes in a gigabyte
+#define KB_SZ(_s) (_s / KB)   //!< Convert bytes to kilobytes
+#define MB_SZ(_s) (_s / MB)   //!< Convert bytes to megabytes
+#define GB_SZ(_s) (_s / GB)   //!< Convert bytes to gigabytes
 
 /************************************************************************/
 /*** Mspace initialization {{{ ***/
@@ -66,7 +66,6 @@ void eacsl_destroy_memory_spaces();
 
 /* }}} */
 
-
 /************************************************************************/
 /*** Mspace allocators (from dlmalloc) {{{ ***/
 /************************************************************************/
@@ -81,26 +80,26 @@ void eacsl_destroy_memory_spaces();
 #define eacsl_mspace_posix_memalign export_alias(mspace_posix_memalign)
 #define eacsl_mspace_aligned_alloc  export_alias(mspace_aligned_alloc)
 
-typedef void* mspace;
+typedef void *mspace;
 
 struct memory_spaces {
-  mspace rtl_mspace; /* `private` (RTL) mspace */
-  mspace heap_mspace;  /* `public` (application) mspace */
-  uintptr_t heap_start; /* least address in application mspace */
-  uintptr_t heap_end; /* greatest address in application mspace */
+  mspace rtl_mspace;           /* `private` (RTL) mspace */
+  mspace heap_mspace;          /* `public` (application) mspace */
+  uintptr_t heap_start;        /* least address in application mspace */
+  uintptr_t heap_end;          /* greatest address in application mspace */
   uintptr_t heap_mspace_least; /* Initial least address in heap mspace */
 };
 extern struct memory_spaces mem_spaces;
 
 extern mspace eacsl_create_mspace(size_t, int);
 extern size_t eacsl_destroy_mspace(mspace);
-extern void*  eacsl_mspace_malloc(mspace, size_t);
-extern void   eacsl_mspace_free(mspace, void*);
-extern void*  eacsl_mspace_calloc(mspace msp, size_t, size_t);
-extern void*  eacsl_mspace_realloc(mspace msp, void*, size_t);
-extern void*  eacsl_mspace_aligned_alloc(mspace, size_t, size_t);
-extern int    eacsl_mspace_posix_memalign(mspace, void **, size_t, size_t);
-extern void*  eacsl_mspace_least_addr(mspace);
+extern void *eacsl_mspace_malloc(mspace, size_t);
+extern void eacsl_mspace_free(mspace, void *);
+extern void *eacsl_mspace_calloc(mspace msp, size_t, size_t);
+extern void *eacsl_mspace_realloc(mspace msp, void *, size_t);
+extern void *eacsl_mspace_aligned_alloc(mspace, size_t, size_t);
+extern int eacsl_mspace_posix_memalign(mspace, void **, size_t, size_t);
+extern void *eacsl_mspace_least_addr(mspace);
 
 /* }}} */
 
@@ -111,12 +110,17 @@ extern void*  eacsl_mspace_least_addr(mspace);
 /* Used within RTL to override standard allocation */
 /* Shortcuts for public allocation functions */
 
-#define public_malloc(...)         eacsl_mspace_malloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_realloc(...)        eacsl_mspace_realloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_calloc(...)         eacsl_mspace_calloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_free(...)           eacsl_mspace_free(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_aligned_alloc(...)  eacsl_mspace_aligned_alloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_posix_memalign(...) eacsl_mspace_posix_memalign(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_malloc(...)                                                     \
+  eacsl_mspace_malloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_realloc(...)                                                    \
+  eacsl_mspace_realloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_calloc(...)                                                     \
+  eacsl_mspace_calloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_free(...) eacsl_mspace_free(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_aligned_alloc(...)                                              \
+  eacsl_mspace_aligned_alloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_posix_memalign(...)                                             \
+  eacsl_mspace_posix_memalign(mem_spaces.heap_mspace, __VA_ARGS__)
 
 /* }}} */
 
@@ -124,10 +128,13 @@ extern void*  eacsl_mspace_least_addr(mspace);
 /*** Private allocators usable within RTL and GMP {{{ ***/
 /************************************************************************/
 
-#define private_malloc(...)  eacsl_mspace_malloc(mem_spaces.rtl_mspace, __VA_ARGS__)
-#define private_calloc(...)  eacsl_mspace_calloc(mem_spaces.rtl_mspace, __VA_ARGS__)
-#define private_realloc(...) eacsl_mspace_realloc(mem_spaces.rtl_mspace, __VA_ARGS__)
-#define private_free(...)    eacsl_mspace_free(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_malloc(...)                                                    \
+  eacsl_mspace_malloc(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_calloc(...)                                                    \
+  eacsl_mspace_calloc(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_realloc(...)                                                   \
+  eacsl_mspace_realloc(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_free(...) eacsl_mspace_free(mem_spaces.rtl_mspace, __VA_ARGS__)
 
 /* }}} */
 

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c

@@ -31,49 +31,49 @@
 
 #include "e_acsl_private_assert.h"
 
-#define prepend_file_line(file, line, fmt) \
-  do { \
-    char * afmt = "%s:%d: %s\n"; \
-    char buf[strlen(fmt) + strlen(afmt) + PATH_MAX + 11]; \
-    rtl_sprintf(buf, afmt, file, line, fmt); \
-    fmt = buf; \
+#define prepend_file_line(file, line, fmt)                                     \
+  do {                                                                         \
+    char *afmt = "%s:%d: %s\n";                                                \
+    char buf[strlen(fmt) + strlen(afmt) + PATH_MAX + 11];                      \
+    rtl_sprintf(buf, afmt, file, line, fmt);                                   \
+    fmt = buf;                                                                 \
   } while (0)
 
 void raise_abort(const char *file, int line) {
 #ifdef E_ACSL_DEBUG
-#ifndef E_ACSL_NO_TRACE
+#  ifndef E_ACSL_NO_TRACE
   trace();
-#endif
+#  endif
 #endif
   raise(SIGABRT);
 }
 
-void private_abort_fail(const char * file, int line, char *fmt, ...) {
+void private_abort_fail(const char *file, int line, char *fmt, ...) {
   va_list va;
 #if E_ACSL_OS_IS_LINUX
   sigset_t defer_abrt;
   sigemptyset(&defer_abrt);
-  sigaddset(&defer_abrt,SIGABRT);
-  sigprocmask(SIG_BLOCK,&defer_abrt,NULL);
+  sigaddset(&defer_abrt, SIGABRT);
+  sigprocmask(SIG_BLOCK, &defer_abrt, NULL);
 #endif // E_ACSL_OS_IS_LINUX
-  va_start(va,fmt);
+  va_start(va, fmt);
   rtl_veprintf(fmt, va);
   va_end(va);
 #if E_ACSL_OS_IS_LINUX
-  sigprocmask(SIG_UNBLOCK,&defer_abrt,NULL);
+  sigprocmask(SIG_UNBLOCK, &defer_abrt, NULL);
 #endif // E_ACSL_OS_IS_LINUX
   raise_abort(file, line);
 }
 
-void private_assert_fail(int expr, const char *file, int line, char *fmt,  ...) {
+void private_assert_fail(int expr, const char *file, int line, char *fmt, ...) {
   if (!expr) {
-    char * afmt = "%s:%d: %s";
+    char *afmt = "%s:%d: %s";
     char buf[strlen(fmt) + strlen(afmt) + PATH_MAX + 11];
     rtl_sprintf(buf, afmt, file, line, fmt);
     fmt = buf;
 
     va_list va;
-    va_start(va,fmt);
+    va_start(va, fmt);
     rtl_veprintf(fmt, va);
     va_end(va);
     raise_abort(file, line);

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.h

@@ -29,29 +29,30 @@
 #define E_ACSL_PRIVATE_ASSERT
 
 /*! \brief Assert with printf-like error message support */
-#define private_assert(expr, fmt_and_args...) \
+#define private_assert(expr, fmt_and_args...)                                  \
   private_assert_fail(expr, __FILE__, __LINE__, fmt_and_args)
 
 /*! \brief Output a message to error stream using printf-like format string
  * and abort the execution.
  *
  * This is a wrapper for \p eprintf combined with \p abort */
-#define private_abort(fmt_and_args...) \
+#define private_abort(fmt_and_args...)                                         \
   private_abort_fail(__FILE__, __LINE__, fmt_and_args)
 
-
-void private_assert_fail(int expr, const char *file, int line, char *fmt,  ...);
-void private_abort_fail(const char * file, int line, char *fmt, ...);
-void raise_abort(const char * file, int line);
+void private_assert_fail(int expr, const char *file, int line, char *fmt, ...);
+void private_abort_fail(const char *file, int line, char *fmt, ...);
+void raise_abort(const char *file, int line);
 
 /* Instances of assertions shared accross different memory models */
 
 /*! \brief Abort the execution if the size of the pointer computed during
  * instrumentation (\p _ptr_sz) does not match the size of the pointer used
  * by a compiler (\p void*) */
-#define arch_assert(_ptr_sz) \
-  private_assert(_ptr_sz == sizeof(void*), \
-    "Mismatch of instrumentation- and compile-time pointer sizes: " \
-    "%lu vs %lu\n", _ptr_sz, sizeof(void*))
+#define arch_assert(_ptr_sz)                                                   \
+  private_assert(                                                              \
+      _ptr_sz == sizeof(void *),                                               \
+      "Mismatch of instrumentation- and compile-time pointer sizes: "          \
+      "%lu vs %lu\n",                                                          \
+      _ptr_sz, sizeof(void *))
 
 #endif // E_ACSL_PRIVATE_ASSERT

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c

@@ -47,314 +47,322 @@
 
 #include "e_acsl_rtl_io.h"
 
-typedef void (*putcf) (void*,char);
+typedef void (*putcf)(void *, char);
 
 /* Unsigned long integers to string conversion (%u) */
-static void uli2a(unsigned long int num, unsigned int base, int uc,char * bf) {
-  int n=0;
-  unsigned long int d=1;
-  while (num/d >= base)
-    d*=base;
-  while (d!=0) {
+static void uli2a(unsigned long int num, unsigned int base, int uc, char *bf) {
+  int n = 0;
+  unsigned long int d = 1;
+  while (num / d >= base)
+    d *= base;
+  while (d != 0) {
     int dgt = num / d;
-    num%=d;
-    d/=base;
-    if (n || dgt>0|| d==0) {
-      *bf++ = dgt+(dgt<10 ? '0' : (uc ? 'A' : 'a')-10);
+    num %= d;
+    d /= base;
+    if (n || dgt > 0 || d == 0) {
+      *bf++ = dgt + (dgt < 10 ? '0' : (uc ? 'A' : 'a') - 10);
       ++n;
     }
   }
-  *bf=0;
+  *bf = 0;
 }
 
 /* Unsigned pointer-wide integers to memory address conversion (%a) */
-static void addr2a(uintptr_t addr, char * bf) {
+static void addr2a(uintptr_t addr, char *bf) {
   *bf++ = '0';
   *bf++ = 'x';
 
   unsigned int digits = 1;
-  int n=0;
-  unsigned long int d=1;
-  while (addr/d >= 10) {
-    d*=10;
+  int n = 0;
+  unsigned long int d = 1;
+  while (addr / d >= 10) {
+    d *= 10;
     digits++;
   }
 
   unsigned int ctr = 0;
-  while (d!=0) {
+  while (d != 0) {
     ctr++;
     int dgt = addr / d;
-    addr%=d;
-    d/=10;
-    if (n || dgt>0|| d==0) {
-      *bf++ = dgt+(dgt<10 ? '0' : 'a' - 10);
+    addr %= d;
+    d /= 10;
+    if (n || dgt > 0 || d == 0) {
+      *bf++ = dgt + (dgt < 10 ? '0' : 'a' - 10);
       ++n;
     }
-    if (--digits%5 == 0 && d != 0)
-        *bf++ = '-';
+    if (--digits % 5 == 0 && d != 0)
+      *bf++ = '-';
   }
-  *bf=0;
+  *bf = 0;
 }
 
 /* Pointer to string conversion (%p) */
 static void ptr2a(void *p, char *bf) {
-    *bf++ = '0';
-    *bf++ = 'x';
-    uli2a((intptr_t)p,16,0,bf);
+  *bf++ = '0';
+  *bf++ = 'x';
+  uli2a((intptr_t)p, 16, 0, bf);
 }
 
 /* Signed long integer to string conversion (%ld) */
-static void li2a (long num, char * bf) {
-  if (num<0) {
-    num=-num;
+static void li2a(long num, char *bf) {
+  if (num < 0) {
+    num = -num;
     *bf++ = '-';
   }
-  uli2a(num,10,0,bf);
+  uli2a(num, 10, 0, bf);
 }
 
 /* Signed integer to string conversion (%d) */
-static void ui2a(unsigned int num, unsigned int base, int uc,char * bf) {
-  int n=0;
-  unsigned int d=1;
-  while (num/d >= base)
-    d*=base;
-  while (d!=0) {
+static void ui2a(unsigned int num, unsigned int base, int uc, char *bf) {
+  int n = 0;
+  unsigned int d = 1;
+  while (num / d >= base)
+    d *= base;
+  while (d != 0) {
     int dgt = num / d;
-    num%= d;
-    d/=base;
-    if (n || dgt>0 || d==0) {
-      *bf++ = dgt+(dgt<10 ? '0' : (uc ? 'A' : 'a')-10);
+    num %= d;
+    d /= base;
+    if (n || dgt > 0 || d == 0) {
+      *bf++ = dgt + (dgt < 10 ? '0' : (uc ? 'A' : 'a') - 10);
       ++n;
     }
   }
-  *bf=0;
+  *bf = 0;
 }
 
 /* Integer bit-fields to string conversion (%b, %B) */
 static void bits2a(long int v, int size, char *bf, int l2r) {
   int i;
   if (l2r) {
-    for(i = 0; i < size; i++) {
+    for (i = 0; i < size; i++) {
       *bf++ = '0' + ((v >> i) & 1);
-      if (i && i+1 < size && (i+1)%8 == 0)
-        *bf++  = ' ';
+      if (i && i + 1 < size && (i + 1) % 8 == 0)
+        *bf++ = ' ';
     }
   } else {
-    for(i = size - 1; i >= 0; i--) {
+    for (i = size - 1; i >= 0; i--) {
       *bf++ = '0' + ((v >> i) & 1);
-      if (i && i+1 < size && i%4 == 0)
-        *bf++  = ' ';
+      if (i && i + 1 < size && i % 4 == 0)
+        *bf++ = ' ';
     }
   }
-  *bf=0;
+  *bf = 0;
 }
 
 /* Pointer bit-fields to string conversion (%v, %V) */
 static void pbits2a(void *p, int size, char *bf, int l2r) {
-  char *v = (char*)p;
+  char *v = (char *)p;
   int i;
   if (l2r) {
-    for(i = 0; i < size; i++) {
-      *bf++ = '0' + ((v[i/8] >> i%8) & 1);
-      if (i && i+1 < size && (i+1)%4 == 0)
-        *bf++  = ' ';
+    for (i = 0; i < size; i++) {
+      *bf++ = '0' + ((v[i / 8] >> i % 8) & 1);
+      if (i && i + 1 < size && (i + 1) % 4 == 0)
+        *bf++ = ' ';
     }
   } else {
-    for(i = size - 1; i >= 0; i--) {
-      *bf++ = '0' + ((v[i/8] >> i%8) & 1);
-      if (i && i+1 < size && i%4 == 0)
-        *bf++  = ' ';
+    for (i = size - 1; i >= 0; i--) {
+      *bf++ = '0' + ((v[i / 8] >> i % 8) & 1);
+      if (i && i + 1 < size && i % 4 == 0)
+        *bf++ = ' ';
     }
   }
-  *bf=0;
+  *bf = 0;
 }
 
 /* Signed integer to string (%d) */
-static void i2a (int num, char * bf) {
-  if (num<0) {
-    num=-num;
+static void i2a(int num, char *bf) {
+  if (num < 0) {
+    num = -num;
     *bf++ = '-';
   }
-  ui2a(num,10,0,bf);
+  ui2a(num, 10, 0, bf);
 }
 
 /* Char to int conversion  */
 static int a2d(char ch) {
-  if (ch>='0' && ch<='9')
-    return ch-'0';
-  else if (ch>='a' && ch<='f')
-    return ch-'a'+10;
-  else if (ch>='A' && ch<='F')
-    return ch-'A'+10;
-  else return -1;
+  if (ch >= '0' && ch <= '9')
+    return ch - '0';
+  else if (ch >= 'a' && ch <= 'f')
+    return ch - 'a' + 10;
+  else if (ch >= 'A' && ch <= 'F')
+    return ch - 'A' + 10;
+  else
+    return -1;
 }
 
-static char a2i(char ch, char** src, int base, int* nump) {
-  char* p= *src;
-  int num=0;
+static char a2i(char ch, char **src, int base, int *nump) {
+  char *p = *src;
+  int num = 0;
   int digit;
-  while ((digit=a2d(ch))>=0) {
-    if (digit>base) break;
-    num=num*base+digit;
-    ch=*p++;
+  while ((digit = a2d(ch)) >= 0) {
+    if (digit > base)
+      break;
+    num = num * base + digit;
+    ch = *p++;
   }
-  *src=p;
-  *nump=num;
+  *src = p;
+  *nump = num;
   return ch;
 }
 
-static void putchw(void* putp, putcf putf, int n, char z, char* bf) {
-  char fc=z? '0' : ' ';
+static void putchw(void *putp, putcf putf, int n, char z, char *bf) {
+  char fc = z ? '0' : ' ';
   char ch;
-  char* p=bf;
+  char *p = bf;
   while (*p++ && n > 0)
     n--;
   while (n-- > 0)
-    putf(putp,fc);
-  while ((ch= *bf++))
-    putf(putp,ch);
+    putf(putp, fc);
+  while ((ch = *bf++))
+    putf(putp, ch);
 }
 
-static void putcp(void* p,char c) {
-  *(*((char**)p))++ = c;
+static void putcp(void *p, char c) {
+  *(*((char **)p))++ = c;
 }
 
-static void _format(void* putp, putcf putf, char *fmt, va_list va) {
+static void _format(void *putp, putcf putf, char *fmt, va_list va) {
   char bf[256];
   char ch;
-  while ((ch=*(fmt++))) {
-    if (ch!='%') // if not '%' print character as is
-      putf(putp,ch);
+  while ((ch = *(fmt++))) {
+    if (ch != '%') // if not '%' print character as is
+      putf(putp, ch);
     else { // otherwise do the print based on the format following '%'
-      char lz=0;
-      char lng=0; // long (i.e., 'l' specifier)
-      int w=0;
-      ch=*(fmt++);
-      if (ch=='0') { // '0' specifier - padding with zeroes
-        ch=*(fmt++);
-        lz=1;
+      char lz = 0;
+      char lng = 0; // long (i.e., 'l' specifier)
+      int w = 0;
+      ch = *(fmt++);
+      if (ch == '0') { // '0' specifier - padding with zeroes
+        ch = *(fmt++);
+        lz = 1;
       }
-      if (ch>='0' && ch<='9') {
-        ch=a2i(ch,&fmt,10,&w);
+      if (ch >= '0' && ch <= '9') {
+        ch = a2i(ch, &fmt, 10, &w);
       }
-      if (ch=='l') {
-        ch=*(fmt++);
-        lng=1;
+      if (ch == 'l') {
+        ch = *(fmt++);
+        lng = 1;
       }
       switch (ch) {
-        case 0:
-          break;
-        case 'u': {
-          if (lng)
-            uli2a(va_arg(va, unsigned long int),10,0,bf);
-          else
-            ui2a(va_arg(va, unsigned int),10,0,bf);
-          putchw(putp,putf,w,lz,bf);
-          break;
-        }
-        case 'd': {
-          if (lng)
-            li2a(va_arg(va, unsigned long int),bf);
-          else
-            i2a(va_arg(va, int),bf);
-          putchw(putp,putf,w,lz,bf);
-          break;
-        }
-        case 'p':
-          ptr2a(va_arg(va, void*), bf);
-          putchw(putp,putf,w,lz,bf);
-          break;
-        case 'a':
-          addr2a(va_arg(va, uintptr_t), bf);
-          putchw(putp,putf,w,lz,bf);
-          break;
-        case 'b':
-          bits2a(va_arg(va, long), w > 64 ? 64 : w ? w : 8, bf, 1);
-          putchw(putp,putf,0,0,bf);
-          break;
-        case 'B':
-          bits2a(va_arg(va, long), w > 64 ? 64 : w ? w : 8, bf, 0);
-          putchw(putp,putf,0,0,bf);
-          break;
-        case 'v':
-          pbits2a(va_arg(va, void*), w ? w : 8, bf, 1);
-          putchw(putp,putf,0,0,bf);
-          break;
-        case 'V':
-          pbits2a(va_arg(va, void*), w ? w : 8, bf, 0);
-          putchw(putp,putf,0,0,bf);
-          break;
-        case 'x':
-        case 'X':
-          if (lng)
-            uli2a(va_arg(va, unsigned long int),16,(ch=='X'),bf);
-          else
-            ui2a(va_arg(va, unsigned int),16,(ch=='X'),bf);
-          putchw(putp,putf,w,lz,bf);
-          break;
-        case 'f' : {
-          double num = va_arg(va, double);
-          int ord = (int)num;
-          i2a(ord,bf);
-          putchw(putp,putf,w,lz,bf);
-          putf(putp,'.');
-          num = num - ord;
-          num *= 1000;
-          ord = (int)num;
-          i2a(ord,bf);
-          putchw(putp,putf,w,lz,bf);
-          break;
-        }
-        case 'c' :
-          putf(putp,(char)(va_arg(va, int)));
-          break;
-        case 's' :
-          putchw(putp,putf,w,0,va_arg(va, char*));
-          break;
-        case '%' :
-          putf(putp,ch);
-        default:
-          break;
+      case 0:
+        break;
+      case 'u': {
+        if (lng)
+          uli2a(va_arg(va, unsigned long int), 10, 0, bf);
+        else
+          ui2a(va_arg(va, unsigned int), 10, 0, bf);
+        putchw(putp, putf, w, lz, bf);
+        break;
+      }
+      case 'd': {
+        if (lng)
+          li2a(va_arg(va, unsigned long int), bf);
+        else
+          i2a(va_arg(va, int), bf);
+        putchw(putp, putf, w, lz, bf);
+        break;
+      }
+      case 'p':
+        ptr2a(va_arg(va, void *), bf);
+        putchw(putp, putf, w, lz, bf);
+        break;
+      case 'a':
+        addr2a(va_arg(va, uintptr_t), bf);
+        putchw(putp, putf, w, lz, bf);
+        break;
+      case 'b':
+        bits2a(va_arg(va, long), w > 64 ? 64 : w ? w : 8, bf, 1);
+        putchw(putp, putf, 0, 0, bf);
+        break;
+      case 'B':
+        bits2a(va_arg(va, long), w > 64 ? 64 : w ? w : 8, bf, 0);
+        putchw(putp, putf, 0, 0, bf);
+        break;
+      case 'v':
+        pbits2a(va_arg(va, void *), w ? w : 8, bf, 1);
+        putchw(putp, putf, 0, 0, bf);
+        break;
+      case 'V':
+        pbits2a(va_arg(va, void *), w ? w : 8, bf, 0);
+        putchw(putp, putf, 0, 0, bf);
+        break;
+      case 'x':
+      case 'X':
+        if (lng)
+          uli2a(va_arg(va, unsigned long int), 16, (ch == 'X'), bf);
+        else
+          ui2a(va_arg(va, unsigned int), 16, (ch == 'X'), bf);
+        putchw(putp, putf, w, lz, bf);
+        break;
+      case 'f': {
+        double num = va_arg(va, double);
+        int ord = (int)num;
+        i2a(ord, bf);
+        putchw(putp, putf, w, lz, bf);
+        putf(putp, '.');
+        num = num - ord;
+        num *= 1000;
+        ord = (int)num;
+        i2a(ord, bf);
+        putchw(putp, putf, w, lz, bf);
+        break;
+      }
+      case 'c':
+        putf(putp, (char)(va_arg(va, int)));
+        break;
+      case 's':
+        putchw(putp, putf, w, 0, va_arg(va, char *));
+        break;
+      case '%':
+        putf(putp, ch);
+      default:
+        break;
       }
     }
   }
 }
 
-static void _charc_stdout (void* p, char c) { write(STDOUT_FILENO,&c,1); }
-static void _charc_stderr (void* p, char c) { write(STDERR_FILENO,&c,1); }
-static void _charc_file (void* p, char c) { write((size_t)p,&c,1); }
+static void _charc_stdout(void *p, char c) {
+  write(STDOUT_FILENO, &c, 1);
+}
+static void _charc_stderr(void *p, char c) {
+  write(STDERR_FILENO, &c, 1);
+}
+static void _charc_file(void *p, char c) {
+  write((size_t)p, &c, 1);
+}
 
-static void _charc_literal  (void* p, char c) {
-  switch(c) {
-    case '\r':
-      write((size_t)p,"\\r",2);
-      break;
-    case '\f':
-      write((size_t)p,"\\f",2);
-      break;
-    case '\b':
-      write((size_t)p,"\\b",2);
-      break;
-    case '\a':
-      write((size_t)p,"\\a",2);
-      break;
-    case '\n':
-      write((size_t)p,"\\n",2);
-      break;
-    case '\t':
-      write((size_t)p,"\\t",2);
-      break;
-    case '\0':
-      write((size_t)p,"\\0",2);
-      break;
-    default:
-      write((size_t)p,&c,1);
+static void _charc_literal(void *p, char c) {
+  switch (c) {
+  case '\r':
+    write((size_t)p, "\\r", 2);
+    break;
+  case '\f':
+    write((size_t)p, "\\f", 2);
+    break;
+  case '\b':
+    write((size_t)p, "\\b", 2);
+    break;
+  case '\a':
+    write((size_t)p, "\\a", 2);
+    break;
+  case '\n':
+    write((size_t)p, "\\n", 2);
+    break;
+  case '\t':
+    write((size_t)p, "\\t", 2);
+    break;
+  case '\0':
+    write((size_t)p, "\\0", 2);
+    break;
+  default:
+    write((size_t)p, &c, 1);
   }
 }
 
 int rtl_printf(char *fmt, ...) {
   va_list va;
-  va_start(va,fmt);
+  va_start(va, fmt);
   int result = rtl_vprintf(fmt, va);
   va_end(va);
   return result;
@@ -367,7 +375,7 @@ int rtl_vprintf(char *fmt, va_list vlist) {
 
 int rtl_eprintf(char *fmt, ...) {
   va_list va;
-  va_start(va,fmt);
+  va_start(va, fmt);
   int result = rtl_veprintf(fmt, va);
   va_end(va);
   return result;
@@ -380,7 +388,7 @@ int rtl_veprintf(char *fmt, va_list vlist) {
 
 int rtl_dprintf(int fd, char *fmt, ...) {
   va_list va;
-  va_start(va,fmt);
+  va_start(va, fmt);
   int result = rtl_vdprintf(fd, fmt, va);
   va_end(va);
   return result;
@@ -388,13 +396,13 @@ int rtl_dprintf(int fd, char *fmt, ...) {
 
 int rtl_vdprintf(int fd, char *fmt, va_list vlist) {
   intptr_t fd_long = fd;
-  _format((void*)fd_long, _charc_file, fmt, vlist);
+  _format((void *)fd_long, _charc_file, fmt, vlist);
   return 1;
 }
 
-int rtl_sprintf(char* s, char *fmt, ...) {
+int rtl_sprintf(char *s, char *fmt, ...) {
   va_list va;
-  va_start(va,fmt);
+  va_start(va, fmt);
   int result = rtl_vsprintf(s, fmt, va);
   va_end(va);
   return result;
@@ -402,6 +410,6 @@ int rtl_sprintf(char* s, char *fmt, ...) {
 
 int rtl_vsprintf(char *s, char *fmt, va_list vlist) {
   _format(&s, putcp, fmt, vlist);
-  putcp(&s,0);
+  putcp(&s, 0);
   return 1;
 }

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h

@@ -82,7 +82,7 @@ int rtl_printf(char *fmt, ...);
 int rtl_vprintf(char *fmt, va_list vlist);
 
 /* Same as printf but write to a string buffer */
-int rtl_sprintf(char* s, char *fmt, ...);
+int rtl_sprintf(char *s, char *fmt, ...);
 int rtl_vsprintf(char *s, char *fmt, va_list vlist);
 
 /* Same as printf but write to the error stream. */