Tests for JBMC classpath problems

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

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

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

@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+--classpath src
+^EXIT=6$
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.
+Issue: 2864

jbmc/regression/jbmc/classpath-class-with-jar/Test.java

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

jbmc/regression/jbmc/classpath-class-with-jar/src/TestJar.java

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

jbmc/regression/jbmc/classpath-class-with-jar/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--classpath `../../../../scripts/format_classpath.sh src.jar .`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

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

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

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

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

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

@@ -1,6 +1,6 @@
 CORE
-test.class
--classpath my_cp:.
+Test.class
+--classpath src
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--classpath wrong
+^EXIT=6$
+^SIGNAL=0$
+the program has no entry point
+--
+--
+We override the default path. Hence, Test cannot be found.
+Currently fails because symex-driven lazy-loading aborts without an error message.

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

@@ -0,0 +1,9 @@
+KNOWNBUG
+src/Test.class
+
+^EXIT=6$
+--
+Parsing src/Test.class
+--
+Test class is not in src package. Therefore, this must fail.
+Issue: 2864

jbmc/regression/jbmc/classpath-class-with-two-dirs/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.class
+--classpath `../../../../scripts/format_classpath.sh my_cp .`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+Test.class
+--classpath ./NotHere.jar
+^EXIT=0$
+^SIGNAL=0$
+^Warning: file './NotHere.jar' does not exist$
+--
+--
+Issue: 2864

jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath `../../../../scripts/format_classpath.sh ./NotHere .`
+^EXIT=0$
+^SIGNAL=0$
+^Warning: path './NotHere' does not exist$
+--
+--

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

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

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

@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+--classpath test.jar
+^EXIT=6$
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.
+Issue: 2864

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

@@ -0,0 +1,10 @@
+KNOWNBUG
+test.jar
+--main-class Test.class
+^EXIT=6$
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.
+Issue: 2864

jbmc/regression/jbmc/classpath-jar-with-two-jars/test.desc

@@ -0,0 +1,8 @@
+CORE
+C.jar
+--function jarfile3.f -classpath `../../../../scripts/format_classpath.sh A.jar B.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -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-jars/test2.desc

@@ -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-jars/test_incorrect.desc

@@ -0,0 +1,10 @@
+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.
+Issue: 2864

jbmc/regression/jbmc/classpath-two-jars/test_incorrect2.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath `../../../../scripts/format_classpath.sh libs/test.jar lib/test2.jar`
+^EXIT=6$
+--
+--
+This is incorrect as it would search for a Test.class file outside the jar files.
+Issue: 2864