Add instanceof test cases

The first five of these are split up pieces of the existing
instanceof1, and the final two are new.

The first three (testing array and primitive classids) don't
work at present; those dealing with ordinary reference types (3-7)
do.

Author: smowton

regression/cbmc-java/instanceof1/instanceof1.class

@@ -2,18 +2,6 @@ class instanceof1
 {
   public static void main(String[] args)
   {
-    // absolutely everything is an Object
     assert args instanceof Object;
-    assert int.class instanceof Object;
-    
-    // args is an array
-    assert args instanceof Object[];
-    
-    // string literals are strings
-    assert "" instanceof String;
-
-    // need a negative example, too
-    Object o=new Object();
-    assert ! (o instanceof String);
   }
 };

regression/cbmc-java/instanceof1/instanceof1.java

@@ -0,0 +1,7 @@
+class instanceof2
+{
+  public static void main(String[] args)
+  {
+    assert int.class instanceof Object;
+  }
+};

regression/cbmc-java/instanceof2/instanceof2.class

@@ -0,0 +1,8 @@
+KNOWNBUG
+instanceof2.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof2/instanceof2.java

@@ -0,0 +1,7 @@
+class instanceof3
+{
+  public static void main(String[] args)
+  {
+    assert args instanceof Object[];
+  }
+};

regression/cbmc-java/instanceof2/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+instanceof3.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof3/instanceof3.class

@@ -0,0 +1,7 @@
+class instanceof4
+{
+  public static void main(String[] args)
+  {
+    assert "" instanceof String;
+  }
+};

regression/cbmc-java/instanceof3/instanceof3.java

@@ -0,0 +1,8 @@
+CORE
+instanceof4.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof3/test.desc

@@ -0,0 +1,8 @@
+class instanceof5
+{
+  public static void main(String[] args)
+  {
+    Object o=new Object();
+    assert ! (o instanceof String);
+  }
+};

regression/cbmc-java/instanceof4/instanceof4.class

@@ -0,0 +1,8 @@
+CORE
+instanceof5.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof4/instanceof4.java

@@ -0,0 +1,15 @@
+class instanceof6
+{
+  public static void main(String[] args)
+  {
+    A[] as = { new A(), new B() };
+    assert(as[0] instanceof A);
+    assert(as[1] instanceof A);
+  }
+};
+
+class A {
+}
+
+class B extends A {
+}

regression/cbmc-java/instanceof4/test.desc

@@ -0,0 +1,8 @@
+CORE
+instanceof6.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof5/instanceof5.class

@@ -0,0 +1,15 @@
+class instanceof7
+{
+  public static void main(String[] args)
+  {
+    A[] as = { new A(), new B() };
+    assert(!(as[0] instanceof B));
+    assert(as[1] instanceof B);
+  }
+};
+
+class A {
+}
+
+class B extends A {
+}

regression/cbmc-java/instanceof5/instanceof5.java

@@ -0,0 +1,8 @@
+CORE
+instanceof7.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring