Adding more classpath tests

Author: peterschrammel

jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.class

@@ -0,0 +1,9 @@
+package com.diffblue;
+
+class Test
+{
+  public static void main(String[] args)
+  {
+    assert true;
+  }
+}

jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.java

@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath src
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.

jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc

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

jbmc/regression/jbmc/classpath-class-with-one-dir/Test.class

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

jbmc/regression/jbmc/classpath-class-with-one-dir/Test.java

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

jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.class

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--classpath wrong
+^EXIT=6$
+^SIGNAL=0$
+the program has no entry point
+--
+--
+We override the default path. Hence, Test cannot be found.

jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.java

@@ -0,0 +1,7 @@
+KNOWNBUG
+src/Test.class
+
+--
+Parsing src/Test.class
+--
+Test class is not in src package. Therefore, this must fail.

jbmc/regression/jbmc/classpath-class-with-one-dir/test.desc

@@ -0,0 +1,9 @@
+package com.diffblue;
+
+class Test
+{
+  public static void main(String[] args)
+  {
+    assert true;
+  }
+}

jbmc/regression/jbmc/classpath-class-with-one-dir/test_override.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath test.jar
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.

jbmc/regression/jbmc/classpath-class-with-one-dir/test_prefix.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+test.jar
+--main-class Test.class
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.

jbmc/regression/jbmc/classpath-jar-incorrect-package/src/Test.java

@@ -0,0 +1,8 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    Test2.foo();
+    assert true;
+  }
+}

jbmc/regression/jbmc/classpath-jar-incorrect-package/test.jar

@@ -0,0 +1,7 @@
+class Test2
+{
+  public static void foo()
+  {
+    assert false;
+  }
+}

jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+--
+Test2 is found because . is default classpath.

jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+Test2.class
+^EXIT=6$
+--
+Invariant check failed
+--
+We don't allow two classes passed on the command line.

jbmc/regression/jbmc/classpath-two-classes/Test.class

@@ -0,0 +1,8 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    Test2.foo();
+    assert true;
+  }
+}

jbmc/regression/jbmc/classpath-two-classes/Test.java

@@ -0,0 +1,7 @@
+class Test2
+{
+  public static void foo()
+  {
+    assert false;
+  }
+}

jbmc/regression/jbmc/classpath-two-classes/Test2.class

@@ -0,0 +1,8 @@
+CORE
+libs/test.jar
+--main-class Test --classpath lib/test2.jar
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+--
+This is a correct way of dealing with two jars.

jbmc/regression/jbmc/classpath-two-classes/Test2.java

@@ -0,0 +1,8 @@
+CORE
+lib/test2.jar
+--main-class Test --classpath libs/test.jar
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+--
+This is a correct way of dealing with two jars.

jbmc/regression/jbmc/classpath-two-classes/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+libs/test.jar
+lib/test2.jar --main-class Test.class
+^EXIT=6$
+--
+Invariant check failed
+the program has no entry point
+--
+We don't allow two jar files passed on the command line.

jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath libs/test.jar:lib/test2.jar
+^EXIT=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is incorrect as it would search for a Test.class file.