Merge pull request #7105 from thomasspriggs/tas/const-prop-returns

Perform remove_returns pass before constant_propagator

Author: tautschnig

regression/goto-instrument/constant-propagation-function-call/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+int ab, bc;
+int f(int x)
+{
+  ab = 1 + 1 + 1 + 1;
+  bc = ab + x;
+  return ab + bc;
+}
+int main()
+{
+  int a;
+  a = -4;
+  int b;
+  b = nondet();
+  a = f(a);
+  assert(!(0 <= a && a < 5 && 0 <= b && b < 5));
+}

regression/goto-instrument/constant-propagation-function-call/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--constant-propagator
+^EXIT=10$
+^SIGNAL=0$
+Removing returns
+VERIFICATION FAILED
+ASSIGN main\:\:1\:\:a \:\= 4
+ASSERT ¬\(main::1::b ≥ 0\) ∨ main::1::b ≥ 5
+--
+^warning: ignoring
+ASSERT true
+--
+This tests that constants are propagated through function calls, correctly
+taking into account the return value. Constant propagation should result in
+simplifying away the conditions in the assertion on `a` but not the conditions
+on `b`.

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1285,6 +1285,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("constant-propagator"))
   {
     do_indirect_call_and_rtti_removal();
+    do_remove_returns();
 
     log.status() << "Propagating Constants" << messaget::eom;