Add tests for value-set filtering for virtual method calls

The test without a deref in the this argument works with
value-set filtering on its own. The test with a deref in the
this argument also requires the use temporary variable for
the this argument of virtual method calls (though we only
need to do this when a dispatch table is made and when the
this argument contains a dereference).

Author: Owen

jbmc/regression/jbmc/virtual_filter_value_sets/A.class

@@ -0,0 +1,18 @@
+CORE
+virtual_filter_value_sets.class
+--show-vcc --function virtual_filter_value_sets.test_with_deref
+^EXIT=0$
+^SIGNAL=0$
+java::B\.f:\(\)I#return_value!0#.* = 9$
+--
+java::B\.f:\(\)I#return_value!0#.* = .*byte_extract_.*_endian
+^warning: ignoring
+--
+When B.f is called on `c.a_field`, it is guarded by a conditional which implies
+that `c.a_field` must be a B. Symex should filter the value set for `c.a_field`
+to remove anything which doesn't satisfy that condition. It will then be able
+to determine that the return value of B.f is 9. If it thinks that `c.a_field`
+might contain an A then it will create a more complicated expression for the
+return value of B.f, which will include byte_extract_little_endian or
+byte_extract_big_endian, as this is what it will produce when trying to read
+the field `int flag` from a class that doesn't have any fields.

jbmc/regression/jbmc/virtual_filter_value_sets/B.class

@@ -0,0 +1,18 @@
+CORE
+virtual_filter_value_sets.class
+--show-vcc --function virtual_filter_value_sets.test_without_deref
+^EXIT=0$
+^SIGNAL=0$
+java::B\.f:\(\)I#return_value!0#.* = 9$
+--
+java::B\.f:\(\)I#return_value!0#.* = .*byte_extract_.*_endian
+^warning: ignoring
+--
+When B.f is called on `a_or_b`, it is guarded by a conditional which implies
+that `a_or_b` must be a B. Symex should filter the value set for `a_or_b` to
+remove anything which doesn't satisfy that condition. It will then be able
+to determine that the return value of B.f is 9. If it thinks that `a_or_b`
+might contain an A then it will create a more complicated expression for the
+return value of B.f, which will include byte_extract_little_endian or
+byte_extract_big_endian, as this is what it will produce when trying to read
+the field `int flag` from a class that doesn't have any fields.

jbmc/regression/jbmc/virtual_filter_value_sets/Container.class

@@ -0,0 +1,40 @@
+class A {
+  public int f() { return 1; }
+};
+
+class B extends A {
+  public int flag;
+
+  public int f() { return flag; }
+};
+
+class Container {
+  public A a_field;
+}
+
+class virtual_filter_value_sets {
+  public static void test_without_deref(boolean nondet_bool) {
+    A a = new A();
+
+    B b = new B();
+    b.flag = 9;
+
+    A a_or_b = nondet_bool ? a : b;
+    int retval = a_or_b.f();
+
+    assert false;
+  }
+
+  public static void test_with_deref(boolean nondet_bool) {
+    A a = new A();
+
+    B b = new B();
+    b.flag = 9;
+
+    Container c = new Container();
+    c.a_field = nondet_bool ? a : b;
+    int retval = c.a_field.f();
+
+    assert false;
+  }
+}