From 015317004fee8cb5584097e26dd6d8db411915a1 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Thu, 31 Jan 2013 10:19:52 +0000
Subject: [PATCH] [e-acsl] fix _get_exact
---
.../share/e-acsl/memory_model/e_acsl_bittree.c | 13 +++++++++----
1 file changed, 9 insertions(+), 4 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 df1d159cc30..6d78a7cfc94 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
@@ -296,7 +296,7 @@ void __add_element (struct _block * ptr) {
curr->is_leaf = 0;
curr->mask = mask(new_node->addr, ptr->ptr);
- curr->addr = (void*)((unsigned long)and(new_node, ptr) & curr->mask);
+ /*curr->addr = (void*)((unsigned long)and(new_node, ptr) & curr->mask);*/
/* smaller at left, higher at right */
if(new_node->addr < ptr->ptr) {
@@ -330,9 +330,14 @@ struct _block * __get_exact (void * ptr) {
assert(tmp->left != NULL && tmp->right != NULL);
/* visit child with greatest common prefix */
- tmp = /*((tmp->mask >> 1) & ( ~ tmp->mask ) & (unsigned long)ptr)*/
- ((unsigned long)ptr >= (unsigned long)tmp->right->addr) ?
- tmp->right : tmp->left;
+ if(((unsigned long)tmp->right->addr & (unsigned long)tmp->right->mask)
+ == ((unsigned long)ptr & (unsigned long)tmp->right->mask))
+ tmp = tmp->right;
+ else if(((unsigned long)tmp->left->addr & (unsigned long)tmp->left->mask)
+ == ((unsigned long)ptr & (unsigned long)tmp->left->mask))
+ tmp = tmp->left;
+ else
+ return NULL;
}
}
--
GitLab