diff --git a/regression/contracts/github_6168_infinite_unwinding_bug/main.c b/regression/contracts/github_6168_infinite_unwinding_bug/main.c new file mode 100644 index 00000000000..c24c4aff133 --- /dev/null +++ b/regression/contracts/github_6168_infinite_unwinding_bug/main.c @@ -0,0 +1,21 @@ +#include +#include + +static int adder(const int *a, const int *b) +{ + return (*a + *b); +} + +int main() +{ + int x = 1024; + + int (*local_adder)(const int *, const int *) = adder; + + while(x > 0) + __CPROVER_loop_invariant(1 == 1) + { + x += local_adder(&x, &x); // loop detection fails + //x += adder(&x, &x); // works fine + } +} diff --git a/regression/contracts/github_6168_infinite_unwinding_bug/test.desc b/regression/contracts/github_6168_infinite_unwinding_bug/test.desc new file mode 100644 index 00000000000..b8c6488def9 --- /dev/null +++ b/regression/contracts/github_6168_infinite_unwinding_bug/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +^\[main.1\] line \d+ Check loop invariant before entry: SUCCESS$ +^\[main.2\] line \d+ Check that loop invariant is preserved: SUCCESS$ +-- +-- +This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168. diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index ad6881ed206..69b2dd3c13d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1154,6 +1154,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.isset(FLAG_ENFORCE_CONTRACT) || cmdline.isset(FLAG_ENFORCE_ALL_CONTRACTS)) { + do_indirect_call_and_rtti_removal(); code_contractst cont(goto_model, log); if(cmdline.isset(FLAG_REPLACE_CALL))