Add regression test for new option

Author: antlechner

jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml

@@ -0,0 +1,32 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+  <modelVersion>4.0.0</modelVersion>
+  <groupId>org.cprover.regression</groupId>
+  <artifactId>regression</artifactId>
+  <version>1.0-SNAPSHOT</version>
+
+  <build>
+    <finalName>jar-file</finalName>
+    <plugins>
+      <plugin>
+        <groupId>org.apache.maven.plugins</groupId>
+        <artifactId>maven-jar-plugin</artifactId>
+        <configuration>
+          <archive>
+            <manifest>
+              <mainClass>org.cprover.regression.RelevantClass</mainClass>
+            </manifest>
+          </archive>
+        </configuration>
+      </plugin>
+    </plugins>
+  </build>
+
+  <properties>
+   <maven.compiler.source>1.8</maven.compiler.source>
+   <maven.compiler.target>1.8</maven.compiler.target>
+  </properties>
+
+</project>

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/IrrelevantClass.java

@@ -0,0 +1,6 @@
+package org.cprover.first;
+
+public class IrrelevantClass {
+
+  public static void notImportant() { assert true; }
+}

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelatedClass.java

@@ -0,0 +1,3 @@
+package org.cprover.first;
+
+public class RelatedClass { public int i; }

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelevantClass.java

@@ -0,0 +1,10 @@
+package org.cprover.first;
+
+import org.cprover.second.RelatedClassOtherPkg;
+
+public class RelevantClass {
+
+  public static void entry(RelatedClass rc, RelatedClassOtherPkg rcop) {
+    assert false;
+  }
+}

jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar

@@ -0,0 +1,18 @@
+CORE
+target/jar-file.jar
+--verbosity 10 --ignore-manifest-main-class
+^EXIT=6$
+^SIGNAL=0$
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+no entry point
+--
+--
+This test checks that when JBMC is given a JAR file whose manifest specifies a
+main class, we can ignore this main class and instead load all classes of the
+JAR file with the option --ignore-manifest-main-class.
+Without this option, IrrelevantClass would not be loaded as it is not reachable
+from RelevantClass (the main class).