Add test of constant propagation through function returns

Author: thomasspriggs

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,16 @@
+CORE
+main.c
+--constant-propagator
+^EXIT=10$
+^SIGNAL=0$
+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`.