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 b35e8dc11f8e27f6766e3d738cd33c0d38b74749..e62516c2fa143a86ea7cc919724857bfa3c95a7b 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 @@ -316,13 +316,20 @@ static void delete_block(void* ptr) { } static void* store_block_duplicate(void* ptr, size_t size) { + bt_block * tmp = NULL; if (ptr != NULL) { bt_block * tmp = bt_lookup(ptr); - if (tmp) - delete_block(tmp); + if (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); } - return ptr; + return tmp; } /* }}} */