regression test with multiple JARs/classpath

Author: Matthias Güdemann

regression/cbmc-java/jar-file3/A.jar

@@ -0,0 +1,19 @@
+public class jarfile3
+{
+  public class A
+  {
+    int x=1;
+  }
+  public class B
+  {
+    int x=1;
+  }
+
+  void f(int i)
+  {
+    A a=new A();
+    B b=new B();
+    assert(a.x==1);
+    assert(b.x==1);
+  }
+}

regression/cbmc-java/jar-file3/B.jar

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