Skip to content
Snippets Groups Projects
Commit e5d576cd authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Add debug guard to __e_acsl_store_block_duplicate of bittree model

parent 55314c7a
No related branches found
No related tags found
No related merge requests found
...@@ -316,13 +316,20 @@ static void delete_block(void* ptr) { ...@@ -316,13 +316,20 @@ static void delete_block(void* ptr) {
} }
static void* store_block_duplicate(void* ptr, size_t size) { static void* store_block_duplicate(void* ptr, size_t size) {
bt_block * tmp = NULL;
if (ptr != NULL) { if (ptr != NULL) {
bt_block * tmp = bt_lookup(ptr); bt_block * tmp = bt_lookup(ptr);
if (tmp) if (tmp) {
delete_block(tmp); #ifdef E_ACSL_DEBUG
/* Make sure that duplicate block, if so is of the same length */
if (tmp->size != size)
vabort("Attempt to store duplicate block of different length");
#endif
delete_block(ptr);
}
store_block(ptr, size); store_block(ptr, size);
} }
return ptr; return tmp;
} }
/* }}} */ /* }}} */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment