Add test for constant- and value-set propagation out of a may-throw function

This is possible now that #return_value variables are not subject to special rules
in phi_function, and the value-set is cleared when variables are marked dead, meaning
that there is no chance a second function call which only sometimes defines #return_value
might witness the previous call's results.

Author: smowton

jbmc/regression/jbmc/throwing-function-return-value/Sub.class

@@ -0,0 +1,49 @@
+public class Test {
+
+  public static Test f(boolean unknown) throws Exception {
+
+    if(unknown)
+      throw new Exception();
+    else
+      return new Test();
+
+  }
+
+  public static void main(boolean unknown) {
+
+    Sub s = new Sub(); // Make sure Sub is loaded
+    int x = 0;
+
+    // The routine below is repeated twice because historically symex could
+    // behave differently the first and second times a may-throw function was
+    // called.
+
+    try {
+      Test t1 = f(unknown);
+      t1.f();
+      x += t1.g();
+    }
+    catch(Exception e) { }
+
+    try {
+      Test t2 = f(unknown);
+      t2.f();
+      x += t2.g();
+    }
+    catch(Exception e) { }
+
+    assert x == 10;
+
+  }
+
+  public void f() { }
+  public int g() { return 5; }
+
+}
+
+class Sub extends Test {
+
+  public void f() { }
+  public int g() { return 0; }
+
+}

jbmc/regression/jbmc/throwing-function-return-value/Test.class

@@ -0,0 +1,18 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
+java::Test\.main:\(Z\)V::9::x!0@1#\d+ = 5 \+ java::Test\.main:\(Z\)V::9::x!0@1#\d+
+^EXIT=0$
+^SIGNAL=0$
+--
+return_value!0#0
+java::Sub\.g:\(\)
+--
+This checks that when a function may throw, we can nontheless constant-propagate
+and populate the value-set for the normal-return path. In particular we don't
+expect to see any reference to a zero-generation return value (indicating
+reading the return-value when not defined), nor do we expect to see any code
+from the Sub class, which is not accessible and can only be reached when
+constant propagation has lost information to the point we're not sure which type
+virtual calls against Test may find.