From 5e8cacaee55b98af7ef86a6a4504e803496b6164 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Tue, 31 Mar 2015 14:03:27 +0200
Subject: [PATCH] [mmodel] implementation of __freeable
---
.../share/e-acsl/memory_model/e_acsl_bittree.c | 16 +++++++---------
.../share/e-acsl/memory_model/e_acsl_mmodel.c | 18 ++++++++++++++++--
.../share/e-acsl/memory_model/e_acsl_mmodel.h | 4 ++++
.../e-acsl/memory_model/e_acsl_mmodel_api.h | 1 +
4 files changed, 28 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index e38e2dfb3f6..1ab256f0b66 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -312,11 +312,11 @@ void __add_element (struct _block * 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 */
+/* return the block B such as: begin addr of B == ptr if such a block exists,
+ return NULL otherwise */
/*@ assigns \nothing;
@ ensures \valid(\result);
- @ ensures \result->ptr == (size_t)ptr;
+ @ ensures \result == \null || \result->ptr == (size_t)ptr;
@*/
struct _block * __get_exact (void * ptr) {
struct bittree * tmp = __root;
@@ -326,8 +326,8 @@ struct _block * __get_exact (void * ptr) {
/*@ loop assigns tmp;
@*/
while(!tmp->is_leaf) {
- // prefix is consistent
- assert((tmp->addr & tmp->mask) == ((size_t)ptr & tmp->mask));
+ // if the ptr we are looking for does not share the prefix of tmp
+ if((tmp->addr & tmp->mask) != ((size_t)ptr & tmp->mask)) return NULL;
// two sons
assert(tmp->left != NULL && tmp->right != NULL);
// the prefix of one son is consistent
@@ -337,12 +337,10 @@ struct _block * __get_exact (void * ptr) {
else if((tmp->left->addr & tmp->left->mask)
== ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
- else
- assert(0);
+ else return NULL;
}
- assert(tmp->is_leaf);
- assert(tmp->leaf->ptr == (size_t)ptr);
+ if(tmp->leaf->ptr != (size_t)ptr) return NULL;
return tmp->leaf;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index 9f252b1a2e1..f8ea8707d41 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -56,6 +56,7 @@ void* __e_acsl_mmodel_memset (void* dest, int val, size_t len) {
size_t __memory_size = 0;
+struct _block * last_added_block = NULL; /* proceed with caution */
/*unsigned cpt_store_block = 0;*/
const int nbr_bits_to_1[256] = {
@@ -103,7 +104,9 @@ void* __store_block(void* ptr, size_t size) {
tmp->init_cpt = 0;
tmp->is_litteral_string = false;
tmp->is_out_of_bound = false;
+ tmp->freeable = false;
__add_element(tmp);
+ last_added_block = tmp;
/*cpt_store_block++;*/
return ptr;
}
@@ -128,7 +131,8 @@ void* __malloc(size_t size) {
if(tmp == NULL) return NULL;
tmp2 = __store_block(tmp, size);
__memory_size += size;
- assert(tmp2 != NULL);
+ assert(tmp2 != NULL && last_added_block != NULL);
+ last_added_block->freeable = true;
return tmp2;
}
@@ -146,6 +150,14 @@ void __free(void* ptr) {
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) {
@@ -197,6 +209,7 @@ void* __realloc(void* ptr, size_t size) {
}
}
tmp->size = size;
+ tmp->freeable = true;
__memory_size += size;
return (void*)tmp->ptr;
}
@@ -211,7 +224,8 @@ void* __calloc(size_t nbr_block, size_t size_block) {
if(tmp == NULL) return NULL;
tmp2 = __store_block(tmp, nbr_block * size_block);
__memory_size += nbr_block * size_block;
- assert(tmp2 != NULL);
+ assert(tmp2 != NULL && last_added_block != NULL);
+ last_added_block->freeable = true;
return tmp2;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 7dd28d91f6c..052bde62c82 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -38,6 +38,10 @@ void * __malloc(size_t size)
void __free(void * ptr)
__attribute__((FC_BUILTIN));
+/*@ assigns \result \from ptr; */
+int __freeable(void * ptr)
+ __attribute__((FC_BUILTIN));
+
/* resize the block starting at ptr to fit its new size,
* for further information, see realloc */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index d4cfb55ebf1..2805f60fb51 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -47,6 +47,7 @@ struct _block {
size_t init_cpt;
_Bool is_litteral_string;
_Bool is_out_of_bound;
+ _Bool freeable;
};
/* print the information about a block */
--
GitLab