[eacsl:runtime] Add a C function for the `separated` predicate

src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c

@@ -20,6 +20,78 @@
 /*                                                                        */
 /**************************************************************************/
 
+/************************************************************************/
+/*** Common functions between all memory models {{{ ***/
+/************************************************************************/
+
+#include <stdarg.h>
+#include <stddef.h>
+
+#include "../internals/e_acsl_debug.h"
+
+#include "e_acsl_observation_model.h"
+
+/**
+ * Check if the memory location represented by `ptr1..ptr1+size1` is separated
+ * with the memory locatin represented by `ptr2..ptr2+size2`.
+ *
+ * \return A non-zero value if the two memory locations are separated, zero
+ * otherwise.
+ */
+int separated2(void * ptr1, size_t size1, void * ptr2, size_t size2) {
+  DASSERT(valid_read(ptr1, size1, base_addr(ptr1), NULL) && valid_read(ptr2, size2, base_addr(ptr2), NULL));
+
+  // Cast pointers to char* to be able to do pointer arithmetic without
+  // triggering undefined behavior
+  char * cptr1 = ptr1;
+  char * cptr2 = ptr2;
+
+  // If at least one of the memory location is an empty set (size == 0), then
+  // the memory is separated.
+  // Otherwise the memory is separated if `cptr1 + size1 <= cptr2` or
+  // `cptr2 + size2 <= cptr1`
+  int sep = size1 == 0 || size2 == 0 ||
+    (cptr1 + size1) <= cptr2 || (cptr2 + size2) <= cptr1;
+
+  return sep;
+}
+
+int separated(size_t count, ...) {
+  void * ptrs[count];
+  size_t sizes[count];
+
+  // Extract arguments in an array to be able to iterate over them several times
+  va_list args;
+  va_start(args, count);
+  for (size_t i = 0 ; i < count ; ++i) {
+    ptrs[i] = va_arg(args, void*);
+    sizes[i] = va_arg(args, size_t);
+  }
+  va_end(args);
+
+  int result = 1;
+
+  // Check that every pointer is separated with any other pointer
+  void * ptr1;
+  size_t size1;
+  for (size_t i = 0 ; result && i < count - 1 ; ++i) {
+    ptr1 = ptrs[i];
+    size1 = sizes[i];
+    for (size_t j = i + 1 ; result && j < count ; ++j) {
+        result = separated2(ptr1, size1, ptrs[j], sizes[j]);
+    }
+  }
+
+  return result;
+}
+
+/* }}} */
+
+
+/************************************************************************/
+/*** Implementation of the memory model {{{ ***/
+/************************************************************************/
+
 #include "internals/e_acsl_heap_tracking.c"
 #include "internals/e_acsl_safe_locations.c"
 
@@ -39,3 +111,5 @@
 #else
 # error "No E-ACSL memory model defined. Aborting compilation"
 #endif
+
+/* }}} */

src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h

@@ -57,6 +57,7 @@
 #define valid                 export_alias(valid)
 #define initialized           export_alias(initialized)
 #define freeable              export_alias(freeable)
+#define separated             export_alias(separated)
 
 /* Block initialization  */
 #define mark_readonly         export_alias(mark_readonly)
@@ -325,6 +326,27 @@ size_t offset(void * ptr)
 int initialized(void * ptr, size_t size)
   __attribute__((FC_BUILTIN));
 
+/*! \brief Implementation of the \b \\separated predicate of E-ACSL.
+ *
+ * The function should be called with `count` being the number of pointers to
+ * check, and the variadic arguments filled with `count` successions of pointers
+ * and sizes of the memory location.
+ *
+ * For instance, the ACSL notation `\separated(a[0..3], b[0..4])` could
+ * correspond to the following call: `separated(2, a, 4, b, 5)`.
+ *
+ * \param count Number of couple (ptr, size) that are to be checked for
+ * separation.
+ * \param ... Pointer and size in succession that are to be checked for
+ * separation.
+ * \return A non-zero value if the memory locations given as parameters are
+ * separated.
+ */
+/*@ assigns \result \from indirect:count;
+  @ ensures \result == 0 || \result == 1; */
+int separated(size_t count, ...)
+  __attribute__((FC_BUILTIN));
+
 /* }}} */
 
-#endif // E_ACSL_OBSERVATION_MODEL_H
\ No newline at end of file
+#endif // E_ACSL_OBSERVATION_MODEL_H