Replace GNU-style aliases with macro definitions in temporal analysis

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

@@ -99,8 +99,8 @@ static void describe_run();
 #  error "No E-ACSL memory model defined. Aborting compilation"
 #endif
 
-/* This header contains temporal analysis shared by both models.
-   It should be here as it uses macros differently defined macros */
+/* Temporal analysis shared by both models.
+ * Uses macros differently defined macros */
 #include "e_acsl_temporal.h"
 
 #ifdef E_ACSL_WEAK_VALIDITY

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

@@ -58,6 +58,21 @@
 /* Heap size */
 #define heap_allocation_size      export_alias(heap_allocation_size)
 #define get_heap_allocation_size  export_alias(get_heap_allocation_size)
+/* Temporal analysis */
+/* No need to encapsulate using macro: using these extra definitions does
+ * not hurt, otherwise need to pass additional parameters to frama-c */
+#define temporal_store_nblock             export_alias(temporal_store_nblock)
+#define temporal_store_nreferent          export_alias(temporal_store_nreferent)
+#define temporal_save_nblock_parameter    export_alias(temporal_save_nblock_parameter)
+#define temporal_save_nreferent_parameter export_alias(temporal_save_nreferent_parameter)
+#define temporal_save_copy_parameter      export_alias(temporal_save_copy_parameter)
+#define temporal_pull_parameter           export_alias(temporal_pull_parameter)
+#define temporal_save_return              export_alias(temporal_save_return)
+#define temporal_reset_parameters         export_alias(temporal_reset_parameters)
+#define temporal_pull_return              export_alias(temporal_pull_return)
+#define temporal_reset_return             export_alias(temporal_reset_return)
+#define temporal_memcpy                   export_alias(temporal_memcpy)
+#define temporal_memset                   export_alias(temporal_memset)
 
 /***********************************************/
 /************ Basic API ************************/
@@ -269,71 +284,71 @@ extern size_t heap_allocation_size;
 /*! \brief Take origin number of a memory block containing `block_addr` and
  * store it as a referent number of a pointer given by `ptr_addr`. */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_store_nblock(void *ptr_addr, void *block_addr)
+void temporal_store_nblock(void *ptr_addr, void *block_addr)
   __attribute__((FC_BUILTIN));
 
-/*! \brief Same as `__e_acsl_temporal_store_nblock` but take a referent
+/*! \brief Same as `temporal_store_nblock` but take a referent
  * number of `block_addr` instead */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_store_nreferent(void *ptr_addr, void *block_addr)
+void temporal_store_nreferent(void *ptr_addr, void *block_addr)
   __attribute__((FC_BUILTIN));
 
 /*! \brief store struct { .ptr = ptr, .temporal_flow = TReferentN }
  *  in the global parameter array. */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_save_nreferent_parameter(void *ptr, unsigned int param)
+void temporal_save_nreferent_parameter(void *ptr, unsigned int param)
   __attribute__((FC_BUILTIN));
 
 /*! \brief store struct { .ptr = ptr, .temporal_flow = TBlockN }
  *  in the global parameter array. */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_save_nblock_parameter(void *ptr, unsigned int param)
+void temporal_save_nblock_parameter(void *ptr, unsigned int param)
   __attribute__((FC_BUILTIN));
 
 /*! \brief store struct { .ptr = ptr, .temporal_flow = TCopy } in the global
  *  parameter array. */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_save_copy_parameter(void *ptr, unsigned int param)
+void temporal_save_copy_parameter(void *ptr, unsigned int param)
   __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 __e_acsl_temporal_pull_parameter(void *ptr, unsigned int param, size_t size)
+void temporal_pull_parameter(void *ptr, unsigned int param, size_t size)
   __attribute__((FC_BUILTIN));
 
 /*! \brief Nullify global parameter array  */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_reset_parameters()
+void temporal_reset_parameters()
   __attribute__((FC_BUILTIN));
 
 /*! \brief Save temporal referent number of `ptr` in a placeholder variable
  * tracking the referent number of a function's return. */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_save_return(void *ptr)
+void 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 __e_acsl_temporal_pull_return(void *ptr)
+void 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 __e_acsl_temporal_reset_return()
+void temporal_reset_return()
   __attribute__((FC_BUILTIN));
 
 /*! \brief Copy temporal shadow data from [src, src + size] to
  * [dest, dest + size]. Counterpart of the memcpy function */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_memcpy(void *dest, void *src, size_t size)
+void temporal_memcpy(void *dest, void *src, size_t size)
   __attribute__((FC_BUILTIN));
 
 /*! \brief Set temporal shadow data from [src, src + size] to 0.
  * Counterpart of memset the function */
 /*@ assigns \nothing; */
-void __e_acsl_temporal_memset(void *dest, int n, size_t size)
+void temporal_memset(void *dest, int n, size_t size)
   __attribute__((FC_BUILTIN));
 #endif

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

@@ -42,25 +42,25 @@ static uintptr_t temporal_referent_shadow(void *addr);
 /*! \brief Return referent time stamp associated with a pointer which address
  * is given by `ptr`. This function expects that `ptr` is allocated and at
  * least `sizeof(uintptr_t)` bytes long */
-static uint32_t referent_timestamp(void *ptr);
+uint32_t referent_timestamp(void *ptr);
 
 /*! \brief Store a referent number `ref` in the shadow of `ptr` */
-static void store_temporal_referent(void *ptr, uint32_t ref);
+void store_temporal_referent(void *ptr, uint32_t ref);
 /* }}} */
 
 /* Temporal store {{{ */
-static void temporal_store_nblock(void *lhs, void *rhs) {
+void temporal_store_nblock(void *lhs, void *rhs) {
   store_temporal_referent(lhs, origin_timestamp(rhs));
 }
 
-static void temporal_store_nreferent(void *lhs, void *rhs) {
+void temporal_store_nreferent(void *lhs, void *rhs) {
   store_temporal_referent(lhs, referent_timestamp(rhs));
 }
 
 /* }}} */
 
 /* Memcpy/memset {{{ */
-static void temporal_memcpy(void *dest, void *src, size_t size) {
+void 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*)) {
@@ -72,7 +72,7 @@ static void temporal_memcpy(void *dest, void *src, size_t size) {
   }
 }
 
-static void temporal_memset(void *dest, int c, size_t size) {
+void temporal_memset(void *dest, int c, size_t size) {
   DVALIDATE_RW_ACCESS(dest, size);
   void *dest_shadow = (void *)temporal_referent_shadow(dest);
   memset(dest_shadow, 0, size);
@@ -80,22 +80,22 @@ static void temporal_memset(void *dest, int c, size_t size) {
 /* }}} */
 
 /* Function parameters {{{ */
-static void temporal_save_nblock_parameter(void *ptr, unsigned int param) {
+void temporal_save_nblock_parameter(void *ptr, unsigned int param) {
   parameter_referents[param].ptr = ptr;
   parameter_referents[param].temporal_flow = TBlockN;
 }
 
-static void temporal_save_nreferent_parameter(void *ptr, unsigned int param) {
+void temporal_save_nreferent_parameter(void *ptr, unsigned int param) {
   parameter_referents[param].ptr = ptr;
   parameter_referents[param].temporal_flow = TReferentN;
 }
 
-static void temporal_save_copy_parameter(void *ptr, unsigned int param) {
+void temporal_save_copy_parameter(void *ptr, unsigned int param) {
   parameter_referents[param].ptr = ptr;
   parameter_referents[param].temporal_flow = TCopy;
 }
 
-static void temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
+void temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
   struct temporal_parameter *tpar = &parameter_referents[param];
   switch(tpar->temporal_flow) {
     case TBlockN:
@@ -112,27 +112,27 @@ static void temporal_pull_parameter(void *ptr, unsigned int param, size_t size)
   }
 }
 
-static void temporal_reset_parameters() {
+void temporal_reset_parameters() {
   reset_parameter_referents();
 }
 /* }}} */
 
 /* Return values {{{ */
-static void temporal_save_return(void *ptr) {
+void temporal_save_return(void *ptr) {
   return_referent = (ptr, sizeof(void*)) ? referent_timestamp(ptr) : 0;
 }
 
-static void temporal_pull_return(void *ptr) {
+void temporal_pull_return(void *ptr) {
   store_temporal_referent(ptr, return_referent);
 }
 
-static void temporal_reset_return() {
+void temporal_reset_return() {
   return_referent = 0;
 }
 /* }}} */
 
 /* Temporal valid {{{ */
-static int temporal_valid(void *ptr, void *addr_of_ptr) {
+int temporal_valid(void *ptr, void *addr_of_ptr) {
   /* Could check for NULL, but since temporal_valid if ran by `valid`, this
    * has been already checked.
    * FIXME: If the address of pointer and the pointer itself reference the same
@@ -155,21 +155,6 @@ static int temporal_valid(void *ptr, void *addr_of_ptr) {
   return 1;
 }
 /* }}} */
-
-/* Public API Bindings {{{*/
-public_alias(temporal_store_nblock)
-public_alias(temporal_store_nreferent)
-public_alias(temporal_save_nblock_parameter)
-public_alias(temporal_save_nreferent_parameter)
-public_alias(temporal_save_copy_parameter)
-public_alias(temporal_pull_parameter)
-public_alias(temporal_save_return)
-public_alias(temporal_reset_parameters)
-public_alias(temporal_pull_return)
-public_alias(temporal_reset_return)
-public_alias(temporal_memcpy)
-public_alias(temporal_memset)
-/*}}}*/
 #else
 #  define E_ACSL_TEMPORAL_DESC "disabled"
 #endif

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

@@ -69,11 +69,5 @@ static uint32_t return_referent;
 #define reset_parameter_referents() \
   memset(parameter_referents, 0, sizeof(parameter_referents))
 
-/* Forward declarations used by all models */
-static int temporal_valid(void*, void*);
-static void temporal_store_nblock(void *lhs, void *rhs);
-static void temporal_store_nreferent(void *lhs, void *rhs);
-static uint32_t origin_timestamp(void *ptr);
-static uint32_t referent_timestamp(void *ptr);
 #endif /*}}} E_ACSL_TEMPORAL */
 #endif /*}}} E_ACSL_TEMPORAL_TIMESTAMP */