Skip to content

Commit 44c7297

Browse files
committed
Handle comparison of freed pointers in assertions
Until now, we only handled correct comparison of freed pointers in normal conditions, not in assersions. Note: --pointer-check must be used to handle freed pointers properly.
1 parent 477e225 commit 44c7297

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/2ls/preprocessing_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -804,7 +804,7 @@ void twols_parse_optionst::handle_freed_ptr_compare(goto_modelt &goto_model)
804804
{
805805
Forall_goto_program_instructions(i_it, f_it->second.body)
806806
{
807-
if(i_it->is_goto())
807+
if(i_it->is_goto() || i_it->is_assert())
808808
{
809809
auto &guard=i_it->guard;
810810
make_freed_ptr_comparison_nondet(

0 commit comments

Comments
 (0)