Merge pull request #7305 from tautschnig/bugfixes/dfcc-segv

Contracts/DFCC: do not access invalidated references

Author: tautschnig

src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp

@@ -55,8 +55,7 @@ void dfcc_is_freeablet::rewrite_calls(
             .set_identifier(library.get_dfcc_fun_name(dfcc_funt::IS_FREEABLE));
           target->call_arguments().push_back(write_set);
         }
-
-        if(fun_name == CPROVER_PREFIX "was_freed")
+        else if(fun_name == CPROVER_PREFIX "was_freed")
         {
           // insert call to precondition for vacuity checking
           auto inst = goto_programt::make_function_call(

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -454,8 +454,7 @@ void dfcc_libraryt::fix_malloc_free_calls()
 
           if(fun_name == (CONTRACTS_PREFIX "malloc"))
             to_symbol_expr(ins->call_function()).set_identifier("malloc");
-
-          if(fun_name == (CONTRACTS_PREFIX "free"))
+          else if(fun_name == (CONTRACTS_PREFIX "free"))
             to_symbol_expr(ins->call_function()).set_identifier("free");
         }
       }