diff --git a/src/plugins/e-acsl/INSTALL b/src/plugins/e-acsl/INSTALL
index a9889e86c57ab6f6aaf2fb1d7cae67c3c70a702e..2173ff442507777b09c6b173bf134f1179393aea 100644
--- a/src/plugins/e-acsl/INSTALL
+++ b/src/plugins/e-acsl/INSTALL
@@ -110,10 +110,9 @@ Shared files: (usually in `frama-c -print-share-path`/e-acsl)
- glibc/memmove.c
- glibc/memset.c
- glibc/strcmp.c
-- bittree_model/e_acsl_mmodel.c
-- bittree_model/e_acsl_mmodel_api.h
+- bittree_model/e_acsl_bittree_api.h
- bittree_model/e_acsl_bittree.h
-- bittree_model/e_acsl_bittree.c
+- bittree_model/e_acsl_bittree_mmodel.c
Manuals: (usually in `frama-c -print-share-path`/manuals)
--------
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9cfbdc6365004bf656a384aa218bdde641426b31..3ab581c387b8275934e63331723c42d9112817ee 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -128,6 +128,7 @@ clean::
$(PRINT_RM) generated test files
$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
$(RM) $(E_ACSL_DIR)/tests/test_config
+ $(RM) $(E_ACSL_DIR)/doc/doxygen/html/*
###########
# Install #
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_adt_mmodel.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_adt_mmodel.h
deleted file mode 100644
index 84d9125cbb00b824b33fd654cb3c1def54856ba6..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_adt_mmodel.h
+++ /dev/null
@@ -1,452 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of the Frama-C's E-ACSL plug-in. */
-/* */
-/* Copyright (C) 2012-2016 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file license/LGPLv2.1). */
-/* */
-/**************************************************************************/
-
-#ifndef E_ACSL_ADT_MMODEL
-#define E_ACSL_ADT_MMODEL
-
-#include "e_acsl_string.h"
-#include "e_acsl_printf.h"
-#include "e_acsl_bits.h"
-#include "e_acsl_assert.h"
-#include "e_acsl_debug.h"
-#include "e_acsl_malloc.h"
-#include "e_acsl_mmodel_api.h"
-#include "e_acsl_adt_api.h"
-
-size_t __heap_size = 0;
-
-static const int nbr_bits_to_1[256] = {
- 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,
- 3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,
- 3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,
- 4,5,4,5,5,6,4,5,5,6,5,6,6,7,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,
- 3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,
- 6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,
- 4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
-};
-
-/*@ assigns \nothing;
- @ ensures \result == __heap_size;
- @*/
-size_t __get_memory_size(void) {
- return __heap_size;
-}
-
-/* given the size of the memory block (_size) return (or rather evaluate to)
- * size in bytes requred to represent its partial initialization */
-#define needed_bytes(_size) \
- ((_size % 8) == 0 ? (_size/8) : (_size/8 + 1))
-
-/**************************/
-/* ALLOCATION */
-/**************************/
-
-/* erase information about initialization of a block */
-static void __clean_init (struct _block * ptr) {
- if(ptr->init_ptr != NULL) {
- native_free(ptr->init_ptr);
- ptr->init_ptr = NULL;
- }
- ptr->init_cpt = 0;
-}
-
-/* erase all information about a block */
-static void __clean_block (struct _block * ptr) {
- if(ptr) {
- __clean_init(ptr);
- native_free(ptr);
- }
-}
-
-/* store the block of size bytes starting at ptr, the new block is returned.
- * Warning: the return type is implicitly (struct _block*). */
-void* __store_block(void* ptr, size_t size) {
- struct _block * tmp;
- DASSERT(ptr != NULL);
- tmp = native_malloc(sizeof(struct _block));
- DASSERT(tmp != NULL);
- tmp->ptr = (size_t)ptr;
- tmp->size = size;
- tmp->init_ptr = NULL;
- tmp->init_cpt = 0;
- tmp->is_readonly = false;
- tmp->freeable = false;
- __add_element(tmp);
- return tmp;
-}
-
-/* remove the block starting at ptr */
-void __delete_block(void* ptr) {
- DASSERT(ptr != NULL);
- struct _block * tmp = __get_exact(ptr);
- DASSERT(tmp != NULL);
- __clean_init(tmp);
- __remove_element(tmp);
- native_free(tmp);
-}
-
-/* allocate size bytes and store the returned block
- * for further information, see malloc */
-void* __malloc(size_t size) {
- void * tmp;
- struct _block * new_block;
- if(size <= 0)
- return NULL;
- tmp = native_malloc(size);
- if(tmp == NULL)
- return NULL;
- new_block = __store_block(tmp, size);
- __heap_size += size;
- DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
- new_block->freeable = true;
- return (void*)new_block->ptr;
-}
-
-/* free the block starting at ptr,
- * for further information, see free */
-void __free(void* ptr) {
- struct _block * tmp;
- if(ptr == NULL)
- return;
- tmp = __get_exact(ptr);
- DASSERT(tmp != NULL);
- native_free(ptr);
- __clean_init(tmp);
- __heap_size -= tmp->size;
- __remove_element(tmp);
- native_free(tmp);
-}
-
-int __freeable(void* ptr) {
- struct _block * tmp;
- if(ptr == NULL)
- return false;
- tmp = __get_exact(ptr);
- if(tmp == NULL)
- return false;
- return tmp->freeable;
-}
-
-/* resize the block starting at ptr to fit its new size,
- * for further information, see realloc */
-void* __realloc(void* ptr, size_t size) {
- struct _block * tmp;
- void * new_ptr;
- /* ptr is NULL - malloc */
- if(ptr == NULL)
- return __malloc(size);
- /* size is zero - free */
- if(size == 0) {
- __free(ptr);
- return NULL;
- }
- tmp = __get_exact(ptr);
- DASSERT(tmp != NULL);
- new_ptr = native_realloc((void*)tmp->ptr, size);
- if(new_ptr == NULL)
- return NULL;
- __heap_size -= tmp->size;
- /* realloc changes start address -- re-enter the element into the ADT */
- if (tmp->ptr != (size_t)new_ptr) {
- __remove_element(tmp);
- tmp->ptr = (size_t)new_ptr;
- __add_element(tmp);
- }
- /* uninitialized, do nothing */
- if(tmp->init_cpt == 0) ;
- /* already fully initialized block */
- else if (tmp->init_cpt == tmp->size) {
- /* realloc smaller block */
- if(size <= tmp->size)
- /* adjust new size, allocation not necessary */
- tmp->init_cpt = size;
- /* realloc bigger larger block */
- else {
- /* size of tmp->init_ptr in the new block */
- int nb = needed_bytes(size);
- /* number of bits that need to be set in tmp->init_ptr */
- int nb_old = needed_bytes(tmp->size);
- /* allocate memory to store partial initialization */
- tmp->init_ptr = native_calloc(1, nb);
- /* carry out initialization of the old block */
- setbits(tmp->init_ptr, tmp->size);
- }
- }
- /* contains initialized and uninitialized parts */
- else {
- int nb = needed_bytes(size);
- int nb_old = needed_bytes(tmp->size);
- int i;
- tmp->init_ptr = native_realloc(tmp->init_ptr, nb);
- for(i = nb_old; i < nb; i++)
- tmp->init_ptr[i] = 0;
- tmp->init_cpt = 0;
- for(i = 0; i < nb; i++)
- tmp->init_cpt += nbr_bits_to_1[tmp->init_ptr[i]];
- if(tmp->init_cpt == size || tmp->init_cpt == 0) {
- native_free(tmp->init_ptr);
- tmp->init_ptr = NULL;
- }
- }
- tmp->size = size;
- tmp->freeable = true;
- __heap_size += size;
- return (void*)tmp->ptr;
-}
-
-/* allocate memory for an array of nbr_block elements of size_block size,
- * this memory is set to zero, the returned block is stored,
- * for further information, see calloc */
-void* __calloc(size_t nbr_block, size_t size_block) {
- void * tmp;
- size_t size = nbr_block * size_block;
- struct _block * new_block;
- if(size <= 0)
- return NULL;
- tmp = native_calloc(nbr_block, size_block);
- if(tmp == NULL)
- return NULL;
- new_block = __store_block(tmp, size);
- __heap_size += nbr_block * size_block;
- DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
- /* Mark allocated block as freeable and initialized */
- new_block->freeable = true;
- new_block->init_cpt = size;
- return (void*)new_block->ptr;
-}
-
-/**************************/
-/* INITIALIZATION */
-/**************************/
-
-/* mark the size bytes of ptr as initialized */
-void __initialize (void * ptr, size_t size) {
- struct _block * tmp;
- if(!ptr)
- return;
-
- tmp = __get_cont(ptr);
- if(tmp == NULL)
- return;
-
- /* already fully initialized, do nothing */
- if(tmp->init_cpt == tmp->size)
- return;
-
- /* fully uninitialized */
- if(tmp->init_cpt == 0) {
- int nb = needed_bytes(tmp->size);
- tmp->init_ptr = native_malloc(nb);
- memset(tmp->init_ptr, 0, nb);
- }
-
- /* partial initialization is kept via a character array accessible via the
- * tmp->init_ptr. This is such that a N-th bit of tmp->init_ptr tracks
- * initialization of the N-th byte of the memory block tracked by tmp.
- *
- * The following sets individual bits in tmp->init_ptr that track
- * initialization of `size' bytes starting from `ptr'. */
- unsigned i;
- for(i = 0; i < size; i++) {
- /* byte-offset within the block, i.e., mark `offset' byte as initialized */
- size_t offset = (uintptr_t)ptr - tmp->ptr + i;
- /* byte offset within tmp->init_ptr, i.e., a byte containing the bit to
- be toggled */
- int byte = offset/8;
- /* bit-offset within the above byte, i.e., bit to be toggled */
- int bit = offset%8;
-
- if (!checkbit(bit, tmp->init_ptr[byte])) { /* if bit is unset ... */
- setbit(bit, tmp->init_ptr[byte]); /* ... set the bit ... */
- tmp->init_cpt++; /* ... and increment initialized bytes count */
- }
- }
-
- /* now fully initialized */
- if(tmp->init_cpt == tmp->size) {
- native_free(tmp->init_ptr);
- tmp->init_ptr = NULL;
- }
-}
-
-/* mark all bytes of ptr as initialized */
-void __full_init (void * ptr) {
- struct _block * tmp;
- if (ptr == NULL)
- return;
-
- tmp = __get_exact(ptr);
- if (tmp == NULL)
- return;
-
- if (tmp->init_ptr != NULL) {
- native_free(tmp->init_ptr);
- tmp->init_ptr = NULL;
- }
-
- tmp->init_cpt = tmp->size;
-}
-
-/* mark a block as read-only */
-void __readonly (void * ptr) {
- struct _block * tmp;
- if (ptr == NULL)
- return;
- tmp = __get_exact(ptr);
- if (tmp == NULL)
- return;
- tmp->is_readonly = true;
-}
-
-/**************************/
-/* PREDICATES */
-/**************************/
-
-/* return whether the size bytes of ptr are initialized */
-int __initialized (void * ptr, size_t size) {
- unsigned i;
- struct _block * tmp = __get_cont(ptr);
- if(tmp == NULL)
- return false;
-
- /* fully uninitialized */
- if(tmp->init_cpt == 0)
- return false;
- /* fully initialized */
- if(tmp->init_cpt == tmp->size)
- return true;
-
- /* see implementation of function __initialize for details */
- for(i = 0; i < size; i++) {
- size_t offset = (uintptr_t)ptr - tmp->ptr + i;
- int byte = offset/8;
- int bit = offset%8;
- if (!checkbit(bit, tmp->init_ptr[byte]))
- return false;
- }
- return true;
-}
-
-/* return the length (in bytes) of the block containing ptr */
-size_t __block_length(void* ptr) {
- struct _block * tmp = __get_cont(ptr);
- /* Hard failure when un-allocated memory is used */
- vassert(tmp != NULL, "\\block_length of unallocated memory", NULL);
- return tmp->size;
-}
-
-/* return whether the size bytes of ptr are readable/writable */
-int __valid(void* ptr, size_t size) {
- struct _block * tmp;
- if(ptr == NULL)
- return false;
- tmp = __get_cont(ptr);
- return (tmp == NULL) ?
- false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
- && !tmp->is_readonly);
-}
-
-/* return whether the size bytes of ptr are readable */
-int __valid_read(void* ptr, size_t size) {
- struct _block * tmp;
- if(ptr == NULL)
- return false;
- tmp = __get_cont(ptr);
- return (tmp == NULL) ?
- false : (tmp->size - ((size_t)ptr - tmp->ptr) >= size);
-}
-
-/* return the base address of the block containing ptr */
-void* __base_addr(void* ptr) {
- struct _block * tmp = __get_cont(ptr);
- vassert(tmp != NULL, "\\base_addr of unallocated memory", NULL);
- return (void*)tmp->ptr;
-}
-
-/* return the offset of ptr within its block */
-int __offset(void* ptr) {
- struct _block * tmp = __get_cont(ptr);
- vassert(tmp != NULL, "\\offset of unallocated memory", NULL);
- return ((size_t)ptr - tmp->ptr);
-}
-
-/**************************/
-/* PROGRAM INITIALIZATION */
-/**************************/
-
-/* erase the content of the abstract structure */
-void __e_acsl_memory_clean() {
- __clean_struct();
-}
-
-/* adds argv to the memory model */
-static void __init_argv(int argc, char **argv) {
- int i;
-
- __store_block(argv, (argc+1)*sizeof(char*));
- __full_init(argv);
-
- for (i = 0; i < argc; i++) {
- __store_block(argv[i], strlen(argv[i])+1);
- __full_init(argv[i]);
- }
-}
-
-/* initialize contents of the abstract structure and record arguments
- * 'argc_ref` address the variable holding the argc parameter
- * 'argv_ref` address the variable holding the argv parameter
- * 'ptr_size` the size of the pointer computed during instrumentation. */
-void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
- arch_assert(ptr_size);
- if (argc_ref)
- __init_argv(*argc_ref, *argv_ref);
-}
-
-/**********************/
-/* DEBUG */
-/**********************/
-#ifdef E_ACSL_DEBUG
-
-/* print the information about a block */
-void __e_acsl_print_block (struct _block * ptr) {
- if (ptr != NULL) {
- DLOG("%a; %lu Bytes; %slitteral; [init] : %d ",
- (char*)ptr->ptr, ptr->size,
- ptr->is_readonly ? "" : "not ", ptr->init_cpt);
- if(ptr->init_ptr != NULL) {
- unsigned i;
- for(i = 0; i < ptr->size/8; i++)
- DLOG("%b ", ptr->init_ptr[i]);
- }
- DLOG("\n");
- }
-}
-
-static void debug_struct();
-
-/* print the content of the abstract structure */
-void __e_acsl_debug() {
- debug_struct();
-}
-
-#endif
-#endif
\ No newline at end of file
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
index 680006f7fb95b0118c607f57a15ab24150b2fa4a..989a640c1e938df2ff8644daff47db829b32da94 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
@@ -20,6 +20,11 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_bittree.h
+ * \brief Patricia Trie API Implementation
+***************************************************************************/
+
#ifndef E_ACSL_BITTREE
#define E_ACSL_BITTREE
@@ -29,7 +34,7 @@
#include "e_acsl_syscall.h"
#include "e_acsl_printf.h"
#include "e_acsl_assert.h"
-#include "e_acsl_adt_api.h"
+#include "e_acsl_bittree_api.h"
#define WORDBITS __WORDSIZE
@@ -140,7 +145,7 @@ static size_t mask(size_t a, size_t b) {
}
-/* called from __remove_element */
+/* called from remove_element */
/* the block we are looking for has to be in the tree */
/*@ requires \valid(ptr);
@ requires \valid(__root);
@@ -180,7 +185,7 @@ static struct bittree * __get_leaf_from_block (struct _block * ptr) {
/* the block we are looking for has to be in the tree */
/*@ requires \valid(ptr);
@*/
-static void __remove_element (struct _block * ptr) {
+static void remove_element (struct _block * ptr) {
struct bittree * leaf_to_delete = __get_leaf_from_block (ptr);
assert(leaf_to_delete->leaf == ptr);
@@ -217,7 +222,7 @@ static void __remove_element (struct _block * ptr) {
}
-/* called from __add_element */
+/* called from add_element */
/* the returned node will be the brother of the soon to be added node */
/*@ requires \valid(ptr);
@ requires \valid(__root);
@@ -248,7 +253,7 @@ static struct bittree * __most_similar_node (struct _block * ptr) {
/* add a block in the structure */
/*@ requires \valid(ptr);
@*/
-static void __add_element (struct _block * ptr) {
+static void add_element (struct _block * ptr) {
struct bittree * new_leaf;
assert(ptr != NULL);
@@ -317,7 +322,7 @@ static void __add_element (struct _block * ptr) {
@ ensures \valid(\result);
@ ensures \result == \null || \result->ptr == (size_t)ptr;
@*/
-static struct _block * __get_exact (void * ptr) {
+static struct _block * get_exact (void * ptr) {
struct bittree * tmp = __root;
assert(__root != NULL);
assert(ptr != NULL);
@@ -346,7 +351,7 @@ static struct _block * __get_exact (void * ptr) {
/* return the block B containing ptr, such as :
begin addr of B <= ptr < (begin addr + size) of B
or NULL if such a block does not exist */
-static struct _block * __get_cont (void * ptr) {
+static struct _block * get_cont (void * ptr) {
struct bittree * tmp = __root;
if(__root == NULL || ptr == NULL) return NULL;
@@ -406,13 +411,29 @@ static struct _block * __get_cont (void * ptr) {
/*******************/
/* CLEAN */
/*******************/
+/* erase information about initialization of a block */
+static void clean_init (struct _block * ptr) {
+ if(ptr->init_ptr != NULL) {
+ native_free(ptr->init_ptr);
+ ptr->init_ptr = NULL;
+ }
+ ptr->init_cpt = 0;
+}
+
+/* erase all information about a block */
+static void clean_block (struct _block * ptr) {
+ if(ptr) {
+ clean_init(ptr);
+ native_free(ptr);
+ }
+}
-/* called from __clean_struct */
+/* called from clean_struct */
/* recursively erase the content of the structure */
static void __clean_rec (struct bittree * ptr) {
if(ptr == NULL) return;
else if(ptr->is_leaf) {
- __clean_block(ptr->leaf);
+ clean_block(ptr->leaf);
ptr->leaf = NULL;
}
else {
@@ -424,7 +445,7 @@ static void __clean_rec (struct bittree * ptr) {
}
/* erase the content of the structure */
-static void __clean_struct () {
+static void clean_struct () {
__clean_rec(__root);
__root = NULL;
}
@@ -434,31 +455,43 @@ static void __clean_struct () {
/*********************/
#ifdef E_ACSL_DEBUG
-/* called from __debug_struct */
-/* recursively print the content of the structure */
-/*@ assigns \nothing;
- @*/
-static void debug_rec (struct bittree * ptr, int depth) {
+
+static void print_block(struct _block * ptr) {
+ if (ptr != NULL) {
+ DLOG("%a; %lu Bytes; %slitteral; [init] : %d ",
+ (char*)ptr->ptr, ptr->size,
+ ptr->is_readonly ? "" : "not ", ptr->init_cpt);
+ if(ptr->init_ptr != NULL) {
+ unsigned i;
+ for(i = 0; i < ptr->size/8; i++)
+ DLOG("%b ", ptr->init_ptr[i]);
+ }
+ DLOG("\n");
+ }
+}
+
+/* recursively print the content of the structure starting from a given node */
+/*@ assigns \nothing; */
+static void print_bittree_node(struct bittree * ptr, int depth) {
int i;
if(ptr == NULL)
return;
for(i = 0; i < depth; i++)
DLOG(" ");
if(ptr->is_leaf)
- __e_acsl_print_block(ptr->leaf);
+ print_block(ptr->leaf);
else {
DLOG("%p -- %p\n", (void*)ptr->mask, (void*)ptr->addr);
- debug_rec(ptr->left, depth+1);
- debug_rec(ptr->right, depth+1);
+ print_bittree_node(ptr->left, depth+1);
+ print_bittree_node(ptr->right, depth+1);
}
}
-/* print the content of the structure */
-/*@ assigns \nothing;
- @*/
-static void debug_struct () {
+/* print the contents of the entire bittree */
+/*@ assigns \nothing; */
+static void print_bittree() {
DLOG("------------DEBUG\n");
- debug_rec(__root, 0);
+ print_bittree_node(__root, 0);
DLOG("-----------------\n");
}
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_adt_api.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
similarity index 52%
rename from src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_adt_api.h
rename to src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
index 89fbdbc4445520032b7d7b1f483f3464a532a607..1297ccf38b8eade87fefe3fffbc8ae7886af5b35 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_adt_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
@@ -20,51 +20,51 @@
/* */
/**************************************************************************/
-#ifndef E_ACSL_MMODEL_API
-#define E_ACSL_MMODEL_API
+/*! ***********************************************************************
+ * \file e_acsl_bittree_api.h
+ * \brief Patricia Trie API
+***************************************************************************/
+
+#ifndef E_ACSL_BITTREE_API
+#define E_ACSL_BITTREE_API
#include "stdlib.h"
#include "stdbool.h"
-/* Memory block allocated and may be deallocated */
+/*! \brief Structure representing an allocated memory block */
struct _block {
- size_t ptr; /* begin address */
- size_t size; /* size in bytes */
-/* Keep trace of initialized sub-blocks within a memory block */
- unsigned char * init_ptr; /* dynamic array of booleans */
- size_t init_cpt;
- _Bool is_readonly;
- _Bool freeable;
+ size_t ptr; //!< Base address
+ size_t size; //!< Block length (in bytes)
+ unsigned char * init_ptr; //!< Per-bit initialization
+ size_t init_cpt; //!< Number of initialized bytes
+ _Bool is_readonly; //!< True if a block is marked read-only
+ _Bool freeable; //!< True if a block can be de-allocated using `free`
};
-/* print the information about a block */
-static void __print_block(struct _block * ptr );
-
-/* erase information about initialization of a block */
-static void __clean_init(struct _block * ptr );
-
-/* erase all information about a block */
-static void __clean_block(struct _block * ptr);
+/*! \brief Remove a block from the structure */
+static void remove_element(struct _block *b);
-/* remove the block from the structure */
-static void __remove_element(struct _block *);
+/*! \brief Add a block to the structure */
+static void add_element(struct _block *b);
-/* add a block in the structure */
-static void __add_element(struct _block *);
+/*! \brief Return block B such that: `\base_addr(B->ptr) == ptr`.
+NB: The function assumes that such a block exists. */
+static struct _block * get_exact(void *ptr);
-/* return the block B such as : begin addr of B == ptr
- we suppose that such a block exists, but we could return NULL if not */
-static struct _block * __get_exact(void *);
+/*! \brief Return block B such that:
+ `\base_addr(B->ptr) <= ptr < (\base_addr(B->ptr) + size)`
+ or NULL if such a block does not exist. */
+static struct _block * get_cont(void *ptr);
-/* return the block B containing ptr, such as :
- begin addr of B <= ptr < (begin addr + size) of B
- or NULL if such a block does not exist */
-static struct _block * __get_cont(void *);
+/*! \brief Erase the contents of the structure */
+static void clean_struct(void);
-/* erase the content of the structure */
-static void __clean_struct(void);
+/*! \brief Print information about a given block */
+static void print_block(struct _block *b);
-/* print the content of the structure */
-static void __debug_struct(void);
+/*! \brief Erase information about a block's initialization */
+static void clean_init(struct _block *b);
+/*! \brief Erase all information about a given block */
+static void clean_block(struct _block *b);
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 9494d8c5efd225acf06c3d2bd5cc299804b5ffc5..45bbbc15ff54129b788b97cdc25f3ea5b87157b2 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -3,7 +3,7 @@
/* This file is part of the Frama-C's E-ACSL plug-in. */
/* */
/* Copyright (C) 2012-2016 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
@@ -20,8 +20,401 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_bittree_mmodel.c
+ * \brief Implementation of E-ACSL public API using a memory model based
+ * on Patricia Trie. See e_acsl_mmodel_api.h for details.
+***************************************************************************/
+
#ifndef E_ACSL_BITTREE_MMODEL
#define E_ACSL_BITTREE_MMODEL
-# include "e_acsl_adt_mmodel.h"
-# include "e_acsl_bittree.h"
+
+#include "e_acsl_string.h"
+#include "e_acsl_printf.h"
+#include "e_acsl_bits.h"
+#include "e_acsl_assert.h"
+#include "e_acsl_debug.h"
+#include "e_acsl_malloc.h"
+#include "e_acsl_mmodel_api.h"
+#include "e_acsl_bittree.h"
+
+size_t __heap_size = 0;
+
+static const int nbr_bits_to_1[256] = {
+ 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,
+ 3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,
+ 3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,
+ 4,5,4,5,5,6,4,5,5,6,5,6,6,7,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,
+ 3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,
+ 6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,
+ 4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+
+size_t __get_memory_size(void) {
+ return __heap_size;
+}
+
+/* given the size of the memory block (_size) return (or rather evaluate to)
+ * size in bytes requred to represent its partial initialization */
+#define needed_bytes(_size) \
+ ((_size % 8) == 0 ? (_size/8) : (_size/8 + 1))
+
+/**************************/
+/* ALLOCATION */
+/**************************/
+
+/* store the block of size bytes starting at ptr, the new block is returned.
+ * Warning: the return type is implicitly (struct _block*). */
+void* __store_block(void* ptr, size_t size) {
+ struct _block * tmp;
+ DASSERT(ptr != NULL);
+ tmp = native_malloc(sizeof(struct _block));
+ DASSERT(tmp != NULL);
+ tmp->ptr = (size_t)ptr;
+ tmp->size = size;
+ tmp->init_ptr = NULL;
+ tmp->init_cpt = 0;
+ tmp->is_readonly = false;
+ tmp->freeable = false;
+ add_element(tmp);
+ return tmp;
+}
+
+/* remove the block starting at ptr */
+void __delete_block(void* ptr) {
+ DASSERT(ptr != NULL);
+ struct _block * tmp = get_exact(ptr);
+ DASSERT(tmp != NULL);
+ clean_init(tmp);
+ remove_element(tmp);
+ native_free(tmp);
+}
+
+/* allocate size bytes and store the returned block
+ * for further information, see malloc */
+void* __malloc(size_t size) {
+ void * tmp;
+ struct _block * new_block;
+ if(size <= 0)
+ return NULL;
+ tmp = native_malloc(size);
+ if(tmp == NULL)
+ return NULL;
+ new_block = __store_block(tmp, size);
+ __heap_size += size;
+ DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
+ new_block->freeable = true;
+ return (void*)new_block->ptr;
+}
+
+/* free the block starting at ptr,
+ * for further information, see free */
+void __free(void* ptr) {
+ struct _block * tmp;
+ if(ptr == NULL)
+ return;
+ tmp = get_exact(ptr);
+ DASSERT(tmp != NULL);
+ native_free(ptr);
+ clean_init(tmp);
+ __heap_size -= tmp->size;
+ remove_element(tmp);
+ native_free(tmp);
+}
+
+int __freeable(void* ptr) {
+ struct _block * tmp;
+ if(ptr == NULL)
+ return false;
+ tmp = get_exact(ptr);
+ if(tmp == NULL)
+ return false;
+ return tmp->freeable;
+}
+
+/* resize the block starting at ptr to fit its new size,
+ * for further information, see realloc */
+void* __realloc(void* ptr, size_t size) {
+ struct _block * tmp;
+ void * new_ptr;
+ /* ptr is NULL - malloc */
+ if(ptr == NULL)
+ return __malloc(size);
+ /* size is zero - free */
+ if(size == 0) {
+ __free(ptr);
+ return NULL;
+ }
+ tmp = get_exact(ptr);
+ DASSERT(tmp != NULL);
+ new_ptr = native_realloc((void*)tmp->ptr, size);
+ if(new_ptr == NULL)
+ return NULL;
+ __heap_size -= tmp->size;
+ /* realloc changes start address -- re-enter the element */
+ if (tmp->ptr != (size_t)new_ptr) {
+ remove_element(tmp);
+ tmp->ptr = (size_t)new_ptr;
+ add_element(tmp);
+ }
+ /* uninitialized, do nothing */
+ if(tmp->init_cpt == 0) ;
+ /* already fully initialized block */
+ else if (tmp->init_cpt == tmp->size) {
+ /* realloc smaller block */
+ if(size <= tmp->size)
+ /* adjust new size, allocation not necessary */
+ tmp->init_cpt = size;
+ /* realloc bigger larger block */
+ else {
+ /* size of tmp->init_ptr in the new block */
+ int nb = needed_bytes(size);
+ /* number of bits that need to be set in tmp->init_ptr */
+ int nb_old = needed_bytes(tmp->size);
+ /* allocate memory to store partial initialization */
+ tmp->init_ptr = native_calloc(1, nb);
+ /* carry out initialization of the old block */
+ setbits(tmp->init_ptr, tmp->size);
+ }
+ }
+ /* contains initialized and uninitialized parts */
+ else {
+ int nb = needed_bytes(size);
+ int nb_old = needed_bytes(tmp->size);
+ int i;
+ tmp->init_ptr = native_realloc(tmp->init_ptr, nb);
+ for(i = nb_old; i < nb; i++)
+ tmp->init_ptr[i] = 0;
+ tmp->init_cpt = 0;
+ for(i = 0; i < nb; i++)
+ tmp->init_cpt += nbr_bits_to_1[tmp->init_ptr[i]];
+ if(tmp->init_cpt == size || tmp->init_cpt == 0) {
+ native_free(tmp->init_ptr);
+ tmp->init_ptr = NULL;
+ }
+ }
+ tmp->size = size;
+ tmp->freeable = true;
+ __heap_size += size;
+ return (void*)tmp->ptr;
+}
+
+/* allocate memory for an array of nbr_block elements of size_block size,
+ * this memory is set to zero, the returned block is stored,
+ * for further information, see calloc */
+void* __calloc(size_t nbr_block, size_t size_block) {
+ void * tmp;
+ size_t size = nbr_block * size_block;
+ struct _block * new_block;
+ if(size <= 0)
+ return NULL;
+ tmp = native_calloc(nbr_block, size_block);
+ if(tmp == NULL)
+ return NULL;
+ new_block = __store_block(tmp, size);
+ __heap_size += nbr_block * size_block;
+ DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
+ /* Mark allocated block as freeable and initialized */
+ new_block->freeable = true;
+ new_block->init_cpt = size;
+ return (void*)new_block->ptr;
+}
+
+/**************************/
+/* INITIALIZATION */
+/**************************/
+
+/* mark the size bytes of ptr as initialized */
+void __initialize (void * ptr, size_t size) {
+ struct _block * tmp;
+ if(!ptr)
+ return;
+
+ tmp = get_cont(ptr);
+ if(tmp == NULL)
+ return;
+
+ /* already fully initialized, do nothing */
+ if(tmp->init_cpt == tmp->size)
+ return;
+
+ /* fully uninitialized */
+ if(tmp->init_cpt == 0) {
+ int nb = needed_bytes(tmp->size);
+ tmp->init_ptr = native_malloc(nb);
+ memset(tmp->init_ptr, 0, nb);
+ }
+
+ /* partial initialization is kept via a character array accessible via the
+ * tmp->init_ptr. This is such that a N-th bit of tmp->init_ptr tracks
+ * initialization of the N-th byte of the memory block tracked by tmp.
+ *
+ * The following sets individual bits in tmp->init_ptr that track
+ * initialization of `size' bytes starting from `ptr'. */
+ unsigned i;
+ for(i = 0; i < size; i++) {
+ /* byte-offset within the block, i.e., mark `offset' byte as initialized */
+ size_t offset = (uintptr_t)ptr - tmp->ptr + i;
+ /* byte offset within tmp->init_ptr, i.e., a byte containing the bit to
+ be toggled */
+ int byte = offset/8;
+ /* bit-offset within the above byte, i.e., bit to be toggled */
+ int bit = offset%8;
+
+ if (!checkbit(bit, tmp->init_ptr[byte])) { /* if bit is unset ... */
+ setbit(bit, tmp->init_ptr[byte]); /* ... set the bit ... */
+ tmp->init_cpt++; /* ... and increment initialized bytes count */
+ }
+ }
+
+ /* now fully initialized */
+ if(tmp->init_cpt == tmp->size) {
+ native_free(tmp->init_ptr);
+ tmp->init_ptr = NULL;
+ }
+}
+
+/* mark all bytes of ptr as initialized */
+void __full_init (void * ptr) {
+ struct _block * tmp;
+ if (ptr == NULL)
+ return;
+
+ tmp = get_exact(ptr);
+ if (tmp == NULL)
+ return;
+
+ if (tmp->init_ptr != NULL) {
+ native_free(tmp->init_ptr);
+ tmp->init_ptr = NULL;
+ }
+
+ tmp->init_cpt = tmp->size;
+}
+
+/* mark a block as read-only */
+void __readonly (void * ptr) {
+ struct _block * tmp;
+ if (ptr == NULL)
+ return;
+ tmp = get_exact(ptr);
+ if (tmp == NULL)
+ return;
+ tmp->is_readonly = true;
+}
+
+/**************************/
+/* PREDICATES */
+/**************************/
+
+/* return whether the size bytes of ptr are initialized */
+int __initialized (void * ptr, size_t size) {
+ unsigned i;
+ struct _block * tmp = get_cont(ptr);
+ if(tmp == NULL)
+ return false;
+
+ /* fully uninitialized */
+ if(tmp->init_cpt == 0)
+ return false;
+ /* fully initialized */
+ if(tmp->init_cpt == tmp->size)
+ return true;
+
+ /* see implementation of function __initialize for details */
+ for(i = 0; i < size; i++) {
+ size_t offset = (uintptr_t)ptr - tmp->ptr + i;
+ int byte = offset/8;
+ int bit = offset%8;
+ if (!checkbit(bit, tmp->init_ptr[byte]))
+ return false;
+ }
+ return true;
+}
+
+/* return the length (in bytes) of the block containing ptr */
+size_t __block_length(void* ptr) {
+ struct _block * tmp = get_cont(ptr);
+ /* Hard failure when un-allocated memory is used */
+ vassert(tmp != NULL, "\\block_length of unallocated memory", NULL);
+ return tmp->size;
+}
+
+/* return whether the size bytes of ptr are readable/writable */
+int __valid(void* ptr, size_t size) {
+ struct _block * tmp;
+ if(ptr == NULL)
+ return false;
+ tmp = get_cont(ptr);
+ return (tmp == NULL) ?
+ false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
+ && !tmp->is_readonly);
+}
+
+/* return whether the size bytes of ptr are readable */
+int __valid_read(void* ptr, size_t size) {
+ struct _block * tmp;
+ if(ptr == NULL)
+ return false;
+ tmp = get_cont(ptr);
+ return (tmp == NULL) ?
+ false : (tmp->size - ((size_t)ptr - tmp->ptr) >= size);
+}
+
+/* return the base address of the block containing ptr */
+void* __base_addr(void* ptr) {
+ struct _block * tmp = get_cont(ptr);
+ vassert(tmp != NULL, "\\base_addr of unallocated memory", NULL);
+ return (void*)tmp->ptr;
+}
+
+/* return the offset of `ptr` within its block */
+int __offset(void* ptr) {
+ struct _block * tmp = get_cont(ptr);
+ vassert(tmp != NULL, "\\offset of unallocated memory", NULL);
+ return ((size_t)ptr - tmp->ptr);
+}
+
+/**************************/
+/* PROGRAM INITIALIZATION */
+/**************************/
+
+/* erase the content of the abstract structure */
+void __e_acsl_memory_clean() {
+ clean_struct();
+}
+
+/* add `argv` to the memory model */
+static void __init_argv(int argc, char **argv) {
+ int i;
+
+ __store_block(argv, (argc+1)*sizeof(char*));
+ __full_init(argv);
+
+ for (i = 0; i < argc; i++) {
+ __store_block(argv[i], strlen(argv[i])+1);
+ __full_init(argv[i]);
+ }
+}
+
+void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+ arch_assert(ptr_size);
+ if (argc_ref)
+ __init_argv(*argc_ref, *argv_ref);
+}
+
+/**********************/
+/* DEBUG */
+/**********************/
+#ifdef E_ACSL_DEBUG
+/*! \brief print the information about a block */
+void __e_acsl_print_block (struct _block * ptr) {
+ print_block(ptr);
+}
+
+/*! \brief print the content of the abstract structure */
+void __e_acsl_print_bittree() {
+ print_bittree();
+}
+#endif
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.h b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
index cb580dc8e2867d46f30ad456ae30383b9e1a2738..1fb83eff4c987d8f4ead6f258ff7aa67bf86f6d6 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
@@ -20,17 +20,17 @@
/* */
/**************************************************************************/
-/************************/
-/* Standard C functions */
-/************************/
+/*! ***********************************************************************
+ * \file e_acsl.h
+ * \brief E-ACSL Public API independent of memory models
+ ***************************************************************************/
#ifndef E_ACSL
#define E_ACSL
-/*****************************/
-/* Dedicated E-ACSL function */
-/*****************************/
-
+/******************************/
+/* Dedicated E-ACSL assertion */
+/******************************/
/*@ requires predicate != 0;
@ assigns \nothing; */
void __e_acsl_assert(int predicate,
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h
index cce4df0709fd64fa3967871431acf8709b3aa31a..8d2de060598d325b8a9516c9d24801ddb6a2b8ce 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_debug.h
@@ -20,6 +20,11 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_debug.h
+ * \brief Debug-level functions and macros
+***************************************************************************/
+
/* Stringification macros {{{ */
#ifndef E_ACSL_STRINGIFICATION
#define E_ACSL_STRINGIFICATION
@@ -38,22 +43,22 @@
# define E_ACSL_DEBUG_LOG /tmp/e-acsl.log
#endif
-/* Name of the debug log file */
+/*! \brief Name of the debug log file */
static const char *dlog_name = TOSTRING(E_ACSL_DEBUG_LOG);
-/* File descriptior associated with the debug log file */
+/*! \brief File descriptor associated with the debug log file */
static int dlog_fd = -1;
-/* Output a message to a log file */
+/*! \brief Output a message to a log file */
#define DLOG(...) dprintf(dlog_fd, __VA_ARGS__)
-/* Debug-time assertion based on assert (see e_acsl.print.h) */
+/*! \brief Debug-time assertion based on assert (see e_acsl.print.h) */
#define DASSERT(_e) assert(_e)
-/* Debug-time assertion based on vassert (see e_acsl.print.h) */
+/*! \brief Debug-time assertion based on vassert (see e_acsl.print.h) */
#define DVASSERT(_expr, _fmt, ...) vassert(_expr, _fmt, __VA_ARGS__)
-/* Initialization of the debug report file:
+/*! \brief Initialize debug report file:
* - open file descriptor
* - add program arguments to the log */
static void initialize_report_file(int *argc, char ***argv) {
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
index 7518f1bf81df4b16eedd9af835020b8c80d7f9fb..ce0db01659d2b7348ea4ae986f51eb216efeb567 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
@@ -20,6 +20,12 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_gmp.h
+ * \brief Prototypes of functions belonging to GNU Multiple
+ * Precision Arithmetic Library (GMP) used within E-ACSL
+***************************************************************************/
+
/******************/
/* GMP prototypes */
/******************/
@@ -74,7 +80,7 @@ extern void __gmpz_init_set_si(mpz_t z, signed long int n)
@ allocates z;
@ ensures \valid(z);
@ ensures \initialized(z);
- @ assigns *z \from str[0..],base;
+ @ assigns *z \from str[0..],base;
@ assigns \result \from str[0..],base; */
extern int __gmpz_init_set_str(mpz_t z, const char *str, int base)
__attribute__((FC_BUILTIN));
@@ -181,7 +187,7 @@ extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3)
/*@ requires \valid(z1);
@ requires \valid_read(z2);
- @ assigns *z1 \from *z2;
+ @ assigns *z1 \from *z2;
@ assigns \result \from *z1,*z2; */
extern int __gmpz_com(mpz_t z1, const mpz_t z2)
__attribute__((FC_BUILTIN));
@@ -190,12 +196,12 @@ extern int __gmpz_com(mpz_t z1, const mpz_t z2)
/* Coercions to C types */
/************************/
-/*@ requires \valid_read(z);
+/*@ requires \valid_read(z);
@ assigns \result \from *z; */
extern long __gmpz_get_si(const mpz_t z)
__attribute__((FC_BUILTIN));
-/*@ requires \valid_read(z);
+/*@ requires \valid_read(z);
@ assigns \result \from *z; */
extern unsigned long __gmpz_get_ui(const mpz_t z)
__attribute__((FC_BUILTIN));
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
index d84dfc7f4a5a300dba460b65cce3f483b01c8e89..8ed98de11a26916713e76bf64f9ba18856c40e5b 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_types.h
@@ -23,6 +23,11 @@
#ifndef E_ACSL_GMP_TYPES
#define E_ACSL_GMP_TYPES
+/*! ***********************************************************************
+ * \file e_acsl_gmp_types.h
+ * \brief GMP types used within E-ACSL
+***************************************************************************/
+
/*************/
/* GMP types */
/*************/
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 05546aaf273bace1e17569e77e1641324e0738cc..b67a5ab011c6e260d952ca4c5e39e8fdaa96f7f9 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -99,7 +99,7 @@ void __initialize(void * ptr, size_t size)
void __full_init(void * ptr)
__attribute__((FC_BUILTIN));
-/*! \brief Mark a memory block which start address is given by \ptr as
+/*! \brief Mark a memory block which start address is given by \p ptr as
* read-only. */
/*@ assigns \nothing; */
void __readonly(void * ptr)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
index c4c5edec1f4df1fd14de2c0ee6de870a86f31c79..e417de91b8297907deca843419b47d999659aea6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
@@ -118,7 +118,7 @@ int main(void) {
}
/* Check duplicate initialization does not affect correct count of
- * initialized bits (relevant for ADT models only). */
+ * initialized bits (relevant for bittree model). */
int dup [2];
dup[0] = 1;
dup[0] = 1;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 35705b2fbe99a41bb36200de18473273ae961c9e..662538e38aa62051af9c1ff20a545fa3f83769d4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -21,7 +21,7 @@ tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 21
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
[value] using specification for function __gmpz_mul
[value] using specification for function __gmpz_add
[value] using specification for function __gmpz_cmp
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 5528763cc8e38fec6631bd155a1c487876cfb158..f427ed71dbdb6794359520bdb7607831881e06bb 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -21,7 +21,7 @@ tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 21
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: precondition got status unknown.
[value] using specification for function __gmpz_mul
[value] using specification for function __gmpz_add
[value] using specification for function __gmpz_cmp