From be25b4869cf736f77425014be1907b515889b555 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Fri, 1 Feb 2013 18:15:13 +0000
Subject: [PATCH] [e-acsl] algos are now correct
---
.../e-acsl/memory_model/e_acsl_bittree.c | 393 +++++++++++-------
.../e-acsl/memory_model/e_acsl_bittree.h | 2 +-
.../share/e-acsl/memory_model/e_acsl_mmodel.c | 25 +-
.../e-acsl/memory_model/e_acsl_mmodel_api.h | 2 +-
4 files changed, 266 insertions(+), 156 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 54aaedecd1b..c378f1bdfa8 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
@@ -3,10 +3,13 @@
#include <unistd.h>
#include "stdio.h"
#include "stdlib.h"
+#include "stdbool.h"
#include "e_acsl_mmodel_api.h"
#include "e_acsl_bittree.h"
#include "e_acsl_mmodel.h"
+#define WORDBITS 64
+
#if WORDBITS == 16
size_t Tmasks[] = {
@@ -159,193 +162,291 @@ int Tneq[] =
#endif
struct bittree {
- int is_leaf;
- char* addr;
- size_t mask;
- struct bittree * left;
- struct bittree * right;
- struct bittree * father;
+ _Bool is_leaf;
+ size_t addr, mask;
+ struct bittree * left, * right, * father;
struct _block * leaf;
} * __root = NULL;
-/* common bits of two addresses */
-size_t mask(void * a, void * b) {
- size_t nxor = ~((size_t)a ^ (size_t)b);
+
+/* common prefix of two addresses */
+/*@ assigns \nothing;
+ @ ensures \forall int i;
+ 0 <= i <= WORDBITS
+ ==> (Tmasks[i] & a) == (Tmasks[i] & b)
+ ==> \result >= Tmasks[i];
+ @ ensures (a & \result) == (b & \result);
+ @ ensures \exists int i; 0 <= i <= WORDBITS && \result == Tmasks[i];
+ @*/
+size_t mask(size_t a, size_t b) {
+ size_t nxor = ~(a ^ b), ret;
int i = WORDBITS/2; /* dichotomic search, starting in the middle */
/* if the current mask matches we use transition from Teq, else from Tneq
- we stop as soon as i is negative, meaning that we found the mask */
- while(i > 0)
- i = (nxor >= Tmasks[i]) ? Teq[i] : Tneq[i];
-
- assert(((size_t)a & Tmasks[-i]) == ((size_t)b & Tmasks[-i]));
+ we stop as soon as i is negative, meaning that we found the mask
+ a negative element i from Teq or Tneq means stop and return Tmasks[-i] */
+ /*@ loop invariant -WORDBITS <= i <= WORDBITS;
+ @ loop assigns i;
+ @*/
+ while(i > 0) {
+ //@ assert 0 < i <= WORDBITS;
+ //@ assert \valid(Tmasks+i);
+ if (nxor >= Tmasks[i])
+ //@ assert \valid(Teq+i);
+ i = Teq[i];
+ else
+ //@ assert \valid(Tneq+i);
+ i = Tneq[i];
+ }
- /* a negative element i from Teq or Tneq means stop and return Tmasks[-i] */
- return Tmasks[-i];
+ //@ assert -WORDBITS <= i <= 0;
+ ret = Tmasks[-i];
+ assert ((a & ret) == (b & ret));
+ return ret;
}
-/* remove the block from the structure */
-void __remove_element (struct _block * ptr) {
+/* called from __remove_element */
+/* the block we are looking for has to be in the tree */
+/*@ requires \valid(ptr);
+ @ requires \valid(__root);
+ @ assings \nothing;
+ @ ensures \valid(\result);
+ @ ensures \result->leaf == ptr;
+ @*/
+struct bittree * __get_leaf_from_block (struct _block * ptr) {
struct bittree * curr = __root;
assert(__root != NULL);
assert(ptr != NULL);
- if(__root->is_leaf) {
- assert(__root->addr == ptr->ptr);
- free(__root);
- __root = NULL;
- return;
+ /*@ loop assigns curr;
+ @*/
+ while(!curr->is_leaf) {
+ // the prefix is consistent
+ assert((curr->addr & curr->mask) == (ptr->ptr & curr->mask));
+ // two sons
+ assert(curr->left != NULL && curr->right != NULL);
+ // the prefix of one son is consistent
+ if((curr->right->addr & curr->right->mask)
+ == (ptr->ptr & curr->right->mask))
+ curr = curr->right;
+ else if((curr->left->addr & curr->left->mask)
+ == (ptr->ptr & curr->left->mask))
+ curr = curr->left;
+ else
+ assert(0);
}
+ assert(curr->is_leaf);
+ assert(curr->leaf == ptr);
+ return curr;
+}
+
+
+/* remove the block from the structure */
+/* the block we are looking for has to be in the tree */
+/*@ requires \valid(ptr);
+ @*/
+void __remove_element (struct _block * ptr) {
+ struct bittree * leaf_to_delete = __get_leaf_from_block (ptr);
+ assert(leaf_to_delete->leaf == ptr);
+ if(leaf_to_delete->father == NULL)
+ // the leaf is the root
+ __root = NULL;
+ else {
+ struct bittree * brother, * father;
+ father = leaf_to_delete->father;
+ brother = (leaf_to_delete == father->left) ? father->right : father->left;
+ assert(brother != NULL);
+ // copying all brother's fields into the father's
+ father->is_leaf = brother->is_leaf;
+ father->addr = brother->addr;
+ father->mask = brother->mask;
+ father->left = brother->left;
+ father->right = brother->right;
+ father->leaf = brother->leaf;
+ if(!brother->is_leaf) {
+ brother->left->father = father;
+ brother->right->father = father;
+ }
+ free(brother);
+ }
+ free(leaf_to_delete);
+}
+
+
+/* called from __add_element */
+/* the returned node will be the brother of the soon to be added node */
+/*@ requires \valid(ptr);
+ @ requires \valid(__root);
+ @ assigns \nothing;
+ @ ensures \valid(\result);
+ @*/
+struct bittree * __most_similar_node (struct _block * ptr) {
+ struct bittree * curr = __root;
+ size_t common_prefix, left_prefix, right_prefix;
+ assert(ptr != NULL);
+ assert(__root != NULL);
+
+ common_prefix = mask(curr->addr & curr->mask, ptr->ptr);
+ // no bits in common
+ if(common_prefix == Tmasks[0])
+ return curr;
+
while(1) {
- /* does not match the mask */
- assert(((size_t)curr->addr & curr->mask)
- == ((size_t)ptr->ptr & curr->mask));
-
- /* element to delete */
- if(curr->is_leaf) {
- struct bittree * brother, * cf;
- cf = curr->father;
- assert(cf != NULL);
- brother = (curr == cf->left) ? cf->right : cf->left;
- assert(brother != NULL);
-
- cf->is_leaf = brother->is_leaf;
- cf->addr = brother->addr;
- cf->mask = brother->mask;
- cf->left = brother->left;
- cf->right = brother->right;
- cf->leaf = brother->leaf;
-
- if(!brother->is_leaf) {
- brother->left->father = cf;
- brother->right->father = cf;
+ if(curr->is_leaf)
+ return curr;
+ assert(curr->left != NULL && curr->right != NULL);
+ /*printf("common_prefix = %p\n", common_prefix);*/
+ left_prefix = mask(curr->left->addr & curr->left->mask, ptr->ptr);
+ /*printf("left mask(%p, %p) = %p\n",
+ curr->left->addr & curr->left->mask, ptr->ptr, left_prefix);*/
+ if(left_prefix > curr->mask) {
+ curr = curr->left;
+ common_prefix = left_prefix;
+ }
+ else {
+ right_prefix = mask(curr->right->addr & curr->right->mask, ptr->ptr);
+ /*printf("right mask(%p, %p) = %p\n",
+ curr->right->addr & curr->right->mask, ptr->ptr, right_prefix);*/
+ if(right_prefix > curr->mask) {
+ curr = curr->right;
+ common_prefix = right_prefix;
}
-
- free(brother);
- free(curr);
- break;
+ else
+ return curr;
}
-
- assert(curr->left != NULL && curr->right != NULL);
-
- /* visit child with greatest common prefix,
- if the bit next to the mask is set to 1, go to right child,
- because its address is higher than the other */
- curr = ((curr->mask >> 1) & ( ~ curr->mask ) & (size_t)ptr->ptr) ?
- curr->right : curr->left;
}
}
+
+
/* add a block in the structure */
+/*@ requires \valid(ptr);
+ @*/
void __add_element (struct _block * ptr) {
struct bittree * new_leaf;
assert(ptr != NULL);
new_leaf = malloc(sizeof(struct bittree));
assert(new_leaf != NULL);
- new_leaf->is_leaf = 1;
+ new_leaf->is_leaf = true;
new_leaf->addr = ptr->ptr;
- new_leaf->mask = ~0ul;
- new_leaf->left = new_leaf->right = new_leaf->father = NULL;
+ new_leaf->mask = Tmasks[WORDBITS]; /* ~0ul */
+ new_leaf->left = NULL;
+ new_leaf->right = NULL;
+ new_leaf->father = NULL;
new_leaf->leaf = ptr;
-
- if(__root == NULL) __root = new_leaf;
+
+ if(__root == NULL)
+ __root = new_leaf;
else {
- struct bittree * curr = __root;
+ struct bittree * brother = __most_similar_node (ptr), * father, * aux;
- while(1) {
- /* matches the mask */
- if(((size_t)curr->addr & curr->mask)
- == ((size_t)ptr->ptr & curr->mask)) {
- /* is a leaf => already stored */
- if(curr->is_leaf)
- return;
-
- assert(!curr->is_leaf);
- assert(curr->left != NULL && curr->right != NULL);
-
- /* visit child with greatest common prefix */
- curr =
- ((curr->mask >> 1) & ( ~ curr->mask ) & (size_t)ptr->ptr) ?
- curr->right : curr->left;
- }
-
- /* does not match the mask : creating a new node */
- else {
- struct bittree * new_node;
- new_node = malloc(sizeof(struct bittree));
- assert(new_node != NULL);
-
- new_node->is_leaf = curr->is_leaf;
- new_node->addr = curr->addr;
- new_node->mask = curr->mask;
- new_node->left = curr->left;
- new_node->right = curr->right;
- new_node->father = curr;
- new_leaf->father = curr;
- new_node->leaf = curr->leaf;
-
- if(!new_node->is_leaf)
- new_node->left->father = new_node->right->father = new_node;
-
- curr->is_leaf = 0;
- curr->mask = mask(new_node->addr, ptr->ptr);
-
- /* smaller at left, higher at right */
- if(new_node->addr < ptr->ptr) {
- curr->left = new_node;
- curr->right = new_leaf;
- }
- else {
- curr->left = new_leaf;
- curr->right = new_node;
- }
- curr->leaf = NULL;
- break;
+ assert(brother != NULL);
+ father = malloc(sizeof(struct bittree));
+ assert(father != NULL);
+ father->is_leaf = false;
+ father->addr = brother->addr & new_leaf->addr;
+ /*father->mask = mask(brother->addr & brother->mask, ptr->ptr);*/
+ father->leaf = NULL;
+ if(new_leaf->addr <= brother->addr) {
+ father->left = new_leaf;
+ father->right = brother;
+ } else {
+ father->left = brother;
+ father->right = new_leaf;
+ }
+ new_leaf->father = father;
+
+ if(brother == __root) {
+ father->father = NULL;
+ father->mask = mask(brother->addr & brother->mask, ptr->ptr);
+ __root = father;
+ }
+ else {
+ if (brother->father->left == brother)
+ brother->father->left = father;
+ else
+ brother->father->right = father;
+ father->father = brother->father;
+
+ aux = father;
+ while(1) {
+ aux->mask = mask(aux->left->addr & aux->left->mask,
+ aux->right->addr & aux->right->mask);
+ if(aux == __root) break;
+ aux = aux->father;
}
}
+ brother->father = father;
+ if(!brother->is_leaf)
+ brother->mask = mask(brother->left->addr & brother->left->mask,
+ brother->right->addr & brother->right->mask);
+
+ assert((father->left == brother && father->right == new_leaf)
+ || (father->left == new_leaf && father->right == brother));
}
+ /*printf("%p added\n", (void*)ptr->ptr);
+ __debug();*/
}
+
/* 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 */
+/*@ assigns \nothing;
+ @ ensures \valid(\result);
+ @ ensures \result->ptr == (size_t)ptr;
+ @*/
struct _block * __get_exact (void * ptr) {
struct bittree * tmp = __root;
- if(__root == NULL || ptr == NULL) return NULL;
-
- while(1) {
- /* does not match the mask */
- if(((size_t)tmp->addr & tmp->mask)
- != ((size_t)ptr & tmp->mask))
- return NULL;
-
- /* the leaf we are looking for */
- if(tmp->is_leaf) {
- assert(tmp->leaf->ptr == ptr);
- return tmp->leaf;
- }
+ assert(__root != NULL);
+ assert(ptr != NULL);
+ /*@ loop assigns tmp;
+ @*/
+ while(!tmp->is_leaf) {
+ /*if(!((tmp->addr & tmp->mask) == ((size_t)ptr & tmp->mask))) {
+ printf("get_exact(%p)\n", ptr, (void*)tmp->addr);
+ printf("(tmp->addr & tmp->mask) = %p\n", (tmp->addr & tmp->mask));
+ printf("((size_t)ptr & tmp->mask) = %p\n", ((size_t)ptr & tmp->mask));
+ }*/
+
+ // prefix is consistent
+ assert((tmp->addr & tmp->mask) == ((size_t)ptr & tmp->mask));
+ // two sons
assert(tmp->left != NULL && tmp->right != NULL);
-
- /* visit child with greatest common prefix */
- if(((size_t)tmp->right->addr & (size_t)tmp->right->mask)
- == ((size_t)ptr & (size_t)tmp->right->mask))
+ // the prefix of one son is consistent
+ if((tmp->right->addr & tmp->right->mask)
+ == ((size_t)ptr & tmp->right->mask))
tmp = tmp->right;
- else if(((size_t)tmp->left->addr & (size_t)tmp->left->mask)
- == ((size_t)ptr & (size_t)tmp->left->mask))
+ else if((tmp->left->addr & tmp->left->mask)
+ == ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
- else
- return NULL;
+ else {
+ /*printf("get_exact(%p)\n", ptr);
+ __debug();*/
+ assert(0);
+ /*printf("get_exact(%p) at %p\n", ptr, (void*)tmp->addr);
+ printf("%p -- %p\n", tmp->left->mask, tmp->right->mask);
+ printf("%p\n", (tmp->right->addr & tmp->right->mask));
+ printf("%p\n", ((size_t)ptr & tmp->right->mask));
+ printf("%p\n", (tmp->left->addr & tmp->left->mask));
+ printf("%p\n", ((size_t)ptr & tmp->left->mask));
+ return NULL;*/
+ }
}
+
+ assert(tmp->is_leaf);
+ assert(tmp->leaf->ptr == (size_t)ptr);
+ return tmp->leaf;
}
+
+/* called from __get_cont */
/* return the block B containing ptr, starting from b and only exploring
- left children, or NULL if such block does not exist
- THIS METHOD IS INVOKED FROM __get_cont ONLY
- DO NOT CALL IT FROM ANYWHERE ELSE */
+ left children, or NULL if such block does not exist */
struct _block * __get_cont_by_left_child (void * ptr, struct bittree * b) {
struct bittree * tmp = b;
assert(((size_t)b->addr & b->mask) == ((size_t)ptr & b->mask));
@@ -360,7 +461,7 @@ struct _block * __get_cont_by_left_child (void * ptr, struct bittree * b) {
assert(tmp->is_leaf);
- return (tmp->addr == ptr) ? tmp->leaf : NULL;
+ return (tmp->addr == (size_t)ptr) ? tmp->leaf : NULL;
}
/* return the block B containing ptr, such as :
@@ -373,10 +474,10 @@ struct _block * __get_cont (void * ptr) {
while(1) {
if(tmp->is_leaf) {
/* tmp cannot contain ptr because its begin addr is higher */
- if(tmp->addr > (char*)ptr) return NULL;
+ if(tmp->addr > (size_t)ptr) return NULL;
/* tmp->addr <= ptr, tmp may contain ptr
ptr is contained if tmp is large enough (begin addr + size) */
- else if((char*)ptr < tmp->leaf->size + tmp->addr) return tmp->leaf;
+ else if((size_t)ptr < tmp->leaf->size + tmp->addr) return tmp->leaf;
/* tmp->addr <= ptr, but tmp->addr is not large enough */
return NULL;
}
@@ -407,8 +508,8 @@ struct _block * __get_cont (void * ptr) {
/* CLEAN */
/*******************/
-/* recursively erase the content of the structure,
- do not call directly */
+/* called from __clean_struct */
+/* recursively erase the content of the structure */
void __clean_rec (struct bittree * ptr) {
if(ptr == NULL) return;
else if(ptr->is_leaf) {
@@ -433,8 +534,10 @@ void __clean_struct () {
/* DEBUG */
/*********************/
-/* recursively print the content of the structure
- do not call directly */
+/* called from __debug_struct */
+/* recursively print the content of the structure */
+/*@ assigns \nothing;
+ @*/
void __debug_rec (struct bittree * ptr, int depth) {
int i;
if(ptr == NULL)
@@ -444,13 +547,15 @@ void __debug_rec (struct bittree * ptr, int depth) {
if(ptr->is_leaf)
__print_block(ptr->leaf);
else {
- printf("%p -- %p\n", (char*)ptr->mask, ptr->addr);
+ printf("%p -- %p\n", (void*)ptr->mask, (void*)ptr->addr);
__debug_rec(ptr->left, depth+1);
__debug_rec(ptr->right, depth+1);
}
}
/* print the content of the structure */
+/*@ assigns \nothing;
+ @*/
void __debug_struct () {
printf("\t\t\t------------DEBUG\n");
__debug_rec(__root, 0);
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
index 620a59d44be..81c724e589a 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
@@ -3,6 +3,6 @@
#include "stdlib.h"
-size_t mask(void*, void*);
+size_t mask(size_t, size_t);
#endif
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 f1be889f3b8..bf7226b46dc 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
@@ -6,6 +6,7 @@
#include <assert.h>
#include "e_acsl_bittree.h"
#include "e_acsl_mmodel_api.h"
+#include "e_acsl_mmodel.h"
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
@@ -21,7 +22,7 @@ void* __store_block(void* ptr, size_t size) {
assert(ptr != NULL);
tmp = malloc(sizeof(struct _block));
assert(tmp != NULL);
- tmp->ptr = ptr;
+ tmp->ptr = (size_t)ptr;
tmp->size = size;
tmp->init_ptr = NULL;
tmp->init_cpt = 0;
@@ -78,9 +79,9 @@ void* __realloc(void* ptr, size_t size) {
}
tmp = __get_exact(ptr);
assert(tmp != NULL);
- new_ptr = realloc(tmp->ptr, size);
+ new_ptr = realloc((void*)tmp->ptr, size);
if(new_ptr == NULL) return NULL;
- tmp->ptr = new_ptr;
+ tmp->ptr = (size_t)new_ptr;
/* uninitialized, do nothing */
if(tmp->init_cpt == 0) ;
/* already fully initialized block */
@@ -115,7 +116,7 @@ void* __realloc(void* ptr, size_t size) {
}
}
tmp->size = size;
- return tmp->ptr;
+ return (void*)tmp->ptr;
}
/* allocate memory for an array of nbr_block elements of size_block size,
@@ -151,7 +152,7 @@ void __initialize (void * ptr, size_t size) {
}
for(i = 0; i < size; i++) {
- int byte_offset =(char*)ptr - tmp->ptr + i;
+ int byte_offset = (size_t)ptr - tmp->ptr + i;
int ind = byte_offset / 8;
unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
if((tmp->init_ptr[ind] & mask_bit) == 0) tmp->init_cpt++;
@@ -170,6 +171,10 @@ void __full_init (void * ptr) {
struct _block * tmp;
assert(ptr != NULL);
tmp = __get_exact(ptr);
+ if(!tmp) {
+ printf("full_init(%p)\n", ptr);
+ __debug();
+ }
assert(tmp != NULL);
if (tmp->init_ptr != NULL) {
@@ -206,7 +211,7 @@ int __initialized (void * ptr, size_t size) {
for(i = 0; i < size; i++) {
/* if one byte is uninitialized */
- int byte_offset =(char*)ptr - tmp->ptr + i;
+ int byte_offset = (size_t)ptr - tmp->ptr + i;
int ind = byte_offset / 8;
unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
if((tmp->init_ptr[ind] & mask_bit) == 0) return false;
@@ -231,7 +236,7 @@ int __valid(void* ptr, size_t size) {
assert(size > 0);
tmp = __get_cont(ptr);
return (tmp == NULL) ?
- false : ( tmp->size - ( (char*)ptr - tmp->ptr ) >= size
+ false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
&& !tmp->is_litteral_string);
}
@@ -243,7 +248,7 @@ int __valid_read(void* ptr, size_t size) {
assert(size > 0);
tmp = __get_cont(ptr);
return (tmp == NULL) ?
- false : ( tmp->size - ( (char*)ptr - tmp->ptr ) >= size );
+ false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size );
}
/* return the base address of the block containing ptr */
@@ -252,7 +257,7 @@ void* __base_addr(void* ptr) {
assert(ptr != NULL);
tmp = __get_cont(ptr);
assert(tmp != NULL);
- return tmp->ptr;
+ return (void*)tmp->ptr;
}
/* return the offset of ptr within its block */
@@ -261,7 +266,7 @@ int _offset(void* ptr) {
assert(ptr != NULL);
tmp = __get_cont(ptr);
assert(tmp != NULL);
- return ((char*)ptr - tmp->ptr);
+ return ((size_t)ptr - tmp->ptr);
}
/*******************/
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 c99fd4285fa..6c3c77861ed 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
@@ -18,7 +18,7 @@
/* Memory block allocated and may be deallocated */
struct _block {
- char * ptr; /* begin address */
+ 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 */
--
GitLab