Merge branch 'bugfix/basile/eacsl-bittree-compilation' into 'master'

[eacsl] Fix bittree compilation

See merge request frama-c/frama-c!2899

src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c

@@ -26,6 +26,7 @@
 ***************************************************************************/
 
 #include "../../internals/e_acsl_malloc.h"
+#include "../../internals/e_acsl_private_assert.h"
 
 #include "e_acsl_bittree.h"
 
@@ -160,7 +161,7 @@ static bt_node * bt_get_leaf_from_block (bt_block * ptr) {
 	    == (ptr->ptr & curr->left->mask))
       curr = curr->left;
     else
-      vassert(0, "Unreachable", NULL);
+      private_assert(0, "Unreachable", NULL);
   }
   DASSERT(curr->is_leaf);
   DASSERT(curr->leaf == ptr);

src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c

@@ -31,7 +31,7 @@
 #include "../../internals/e_acsl_private_assert.h"
 #include "../../instrumentation_model/e_acsl_temporal.h"
 #include "../../numerical_model/e_acsl_floating_point.h"
-#include "../internals/e_acsl_safe_locations.h""
+#include "../internals/e_acsl_safe_locations.h"
 #include "e_acsl_bittree.h"
 
 #include "../e_acsl_observation_model.h"
@@ -231,12 +231,12 @@ int eacsl_valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
   bt_block * blk = lookup_allocated(ptr, size, ptr_base);
   return
     size == 0
-    ||
+    || (
     blk != NULL && !blk->is_readonly
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
 #endif
-  ;
+    );
 }
 
 /* return whether the size bytes of ptr are readable */
@@ -244,12 +244,12 @@ int eacsl_valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base)
   bt_block * blk = lookup_allocated(ptr, size, ptr_base);
   return
     size == 0
-    ||
+    || (
     blk != NULL
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
 #endif
-  ;
+    );
 }
 
 /* return the base address of the block containing ptr */
@@ -260,7 +260,7 @@ void* eacsl_base_addr(void* ptr) {
 }
 
 /* return the offset of `ptr` within its block */
-size_t offset(void* ptr) {
+size_t eacsl_offset(void* ptr) {
   bt_block * tmp = bt_find(ptr);
   private_assert(tmp != NULL, "\\offset of unallocated memory", NULL);
   return ((uintptr_t)ptr - tmp->ptr);
@@ -585,7 +585,7 @@ void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   /* Tracking safe locations */
   collect_safe_locations();
   int i;
-  for (i = 0; i < get_safe_location_count(); i++) {
+  for (i = 0; i < get_safe_locations_count(); i++) {
     memory_location * loc = get_safe_location(i);
     void *addr = (void*)loc->address;
     uintptr_t len = loc->length;

src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c

+/* run.config_ci, run.config_dev
+  COMMENT: Compile RTL with bittree memory model
+  STDOPT:#"-e-acsl-full-mtracking"
+  MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model bittree
+ */
+int main() {
+  return 0;
+}

src/plugins/e-acsl/tests/special/e-acsl-segment-model.c

+/* run.config_ci, run.config_dev
+  COMMENT: Compile RTL with segment memory model
+  STDOPT:#"-e-acsl-full-mtracking"
+  MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model segment
+ */
+int main() {
+  return 0;
+}

src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(& __retres),(size_t)4);
+  __e_acsl_full_init((void *)(& __retres));
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(& __retres),(size_t)4);
+  __e_acsl_full_init((void *)(& __retres));
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+