Merge pull request #6340 from NlightNFotis/6168_workaround

Add workaround for issue described in #6168.

Author: NlightNFotis

regression/contracts/github_6168_infinite_unwinding_bug/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+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
+    }
+}

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.

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))