Merge pull request #490 from smowton/use_remove_instanceof

Use remove instanceof

Author: kroening

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;
+  }
+};