Skip to content

Commit cdffe05

Browse files
committed
Add workaround for issue described in #6168.
This fixes the infinite unwinding by adding calls to `do_indirect_call_and_rtti_removal()` before the contracts code invocation in `goto-instrument/`.
1 parent 14d35cc commit cdffe05

File tree

2 files changed

+4
-0
lines changed

2 files changed

+4
-0
lines changed

src/goto-instrument/contracts/contracts.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1268,5 +1268,8 @@ bool code_contractst::enforce_contracts(const std::set<std::string> &functions)
12681268
if(!fail)
12691269
fail = enforce_contract(function);
12701270
}
1271+
1272+
apply_loop_contracts();
1273+
12711274
return fail;
12721275
}

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1154,6 +1154,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11541154
cmdline.isset(FLAG_ENFORCE_CONTRACT) ||
11551155
cmdline.isset(FLAG_ENFORCE_ALL_CONTRACTS))
11561156
{
1157+
do_indirect_call_and_rtti_removal();
11571158
code_contractst cont(goto_model, log);
11581159

11591160
if(cmdline.isset(FLAG_REPLACE_CALL))

0 commit comments

Comments
 (0)