Merge pull request #143 from viktormalik/freed-ptr-fix

peterschrammel · web-flow · commit 615a853923b1 · 2020-05-13T19:31:03.000+01:00
Handle comparison of freed pointers in assertions
diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp
@@ -804,7 +804,7 @@ void twols_parse_optionst::handle_freed_ptr_compare(goto_modelt &goto_model)
   {
     Forall_goto_program_instructions(i_it, f_it->second.body)
     {
-      if(i_it->is_goto())
+      if(i_it->is_goto() || i_it->is_assert())
       {
         auto &guard=i_it->guard;
         make_freed_ptr_comparison_nondet(

Original file line number	Diff line number	Diff line change
`@@ -804,7 +804,7 @@ void twols_parse_optionst::handle_freed_ptr_compare(goto_modelt &goto_model)`
`804`	`804`	`{`
`805`	`805`	`Forall_goto_program_instructions(i_it, f_it->second.body)`
`806`	`806`	`{`
`807`		`- if(i_it->is_goto())`
	`807`	`+ if(i_it->is_goto() \|\| i_it->is_assert())`
`808`	`808`	`{`
`809`	`809`	`auto &guard=i_it->guard;`
`810`	`810`	`make_freed_ptr_comparison_nondet(`