Add tests for properties of excluded methods

The tests from the previous commit show that the right methods are
excluded.
The tests from this commit show that an excluded method has the right
properties: meta-information such as parameter types and identifiers
should be preserved, while the real method should not be loaded and a
stub-like "return nondet" body should be used instead.
The tests from this commit would not have passed without the fixes from
this PR.

Author: antlechner

jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.class

@@ -0,0 +1,30 @@
+import org.cprover.other.MyOther;
+import org.cprover.other.Parent;
+import org.cprover.other.Child;
+
+public class ExcludedProperties {
+
+  public static void parameters() {
+    int i = MyOther.identity(21);
+    assert (i == 21);
+  }
+
+  public static void compileTimeReturnType() {
+    Parent p = MyOther.subclass();
+    assert (p == null || p instanceof Parent);
+    if (p == null) {
+      assert false; // reachable with "return nondet" body
+    } else {
+      if (p.num() == 1) {
+        assert false; // reachable with "return nondet" body
+      } else {
+        assert false; // reachable with "return nondet" body
+      }
+    }
+  }
+
+  public static void runtimeReturnType() {
+    Parent p = MyOther.subclass();
+    assert (p == null || p instanceof Child);
+  }
+}

jbmc/regression/jbmc/context-include-exclude/ExcludedProperties.java

@@ -0,0 +1,6 @@
+package org.cprover.other;
+
+public class Child extends Parent {
+
+  public int num() { return 2; }
+}

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.class

@@ -3,4 +3,6 @@
 public class MyOther {
 
   public static int identity(int x) { return x; }
+
+  public static Parent subclass() { return new Child(); }
 }

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Child.java

@@ -0,0 +1,8 @@
+package org.cprover.other;
+
+public class Parent {
+
+  int field = 1;
+
+  public int num() { return field; }
+}

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.class

@@ -0,0 +1,12 @@
+CORE
+ExcludedProperties.class
+--context-exclude org.cprover.other --function ExcludedProperties.runtimeReturnType
+^EXIT=10$
+^SIGNAL=0$
+.* line 28 assertion at file ExcludedProperties.java line 28.*: FAILURE
+--
+--
+Test that for an excluded method, we do not convert its "real" body from the
+bytecode.
+We instead assign it a "return nondet" body as for stubbed methods, which is
+tested by test_excluded_has_nondet_body.desc.

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/MyOther.java

@@ -0,0 +1,15 @@
+CORE
+ExcludedProperties.class
+--context-exclude org.cprover.other --function ExcludedProperties.compileTimeReturnType
+^EXIT=10$
+^SIGNAL=0$
+.* line 14 assertion at file ExcludedProperties.java line 14 .*: SUCCESS
+.* line 16 assertion at file ExcludedProperties.java line 16 .*: FAILURE
+.* line 19 assertion at file ExcludedProperties.java line 19 .*: FAILURE
+.* line 21 assertion at file ExcludedProperties.java line 21 .*: FAILURE
+--
+--
+Test that for an excluded method, we keep the information about the
+(compile-time) return type of the method and return a nondet object of that
+type, or null.
+Note that we do this in the same way as for stubbed methods.

jbmc/regression/jbmc/context-include-exclude/org/cprover/other/Parent.class

@@ -0,0 +1,13 @@
+CORE
+ExcludedProperties.class
+--context-exclude org.cprover.other --show-symbol-table --function ExcludedProperties.parameters
+^EXIT=0$
+^SIGNAL=0$
+java::org\.cprover\.other\.MyOther\.identity:\(I\)I::arg0i
+--
+java::org\.cprover\.other\.MyOther\.identity:\(I\)I::stub
+--
+Test that for an excluded method, we still create a symbol for its parameter(s)
+just like for non-excluded methods.
+Only the body of excluded methods should be missing, not their signature or
+other "meta-information".