Skip to content

Commit 736fb6e

Browse files
tautschnigtautschnig
authored
Merge pull request #8548 from peterschrammel/ps/compile-java-regression-test-sources2
Compile Java regression test sources (2/n)
2 parents 2d63d9b + 60a7a6c commit 736fb6e

28 files changed

+149
-4
lines changed

‎jbmc/regression/book-examples/BinarySearch/BinarySearch.class

-549 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/BinarySearch/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.book-examples.BinarySearch</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.book-examples</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/book-examples/BinarySearch/runtime_exception.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
BinarySearch.binarySearch
3-
--throw-runtime-exceptions --unwind 2
3+
--throw-runtime-exceptions --unwind 2 -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎jbmc/regression/book-examples/BinarySearch/BinarySearch.java ‎jbmc/regression/book-examples/BinarySearch/src/main/java/BinarySearch.java

File renamed without changes.

‎jbmc/regression/book-examples/LocatorHandler/IdLocator.class

-330 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/LocatorHandler/Locator.class

-95 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/LocatorHandler/LocatorHandler$1.class

-684 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/LocatorHandler/LocatorHandler$LocatorType.class

-1.01 KB
Binary file not shown.

‎jbmc/regression/book-examples/LocatorHandler/LocatorHandler.class

-1.3 KB
Binary file not shown.

‎jbmc/regression/book-examples/LocatorHandler/XPathLocator.class

-339 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/LocatorHandler/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.book-examples.LocatorHandler</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.book-examples</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/book-examples/LocatorHandler/IdLocator.java ‎jbmc/regression/book-examples/LocatorHandler/src/main/java/IdLocator.java

File renamed without changes.

‎jbmc/regression/book-examples/LocatorHandler/Locator.java ‎jbmc/regression/book-examples/LocatorHandler/src/main/java/Locator.java

File renamed without changes.

‎jbmc/regression/book-examples/LocatorHandler/LocatorHandler.java ‎jbmc/regression/book-examples/LocatorHandler/src/main/java/LocatorHandler.java

File renamed without changes.

‎jbmc/regression/book-examples/LocatorHandler/XPathLocator.java ‎jbmc/regression/book-examples/LocatorHandler/src/main/java/XPathLocator.java

File renamed without changes.

‎jbmc/regression/book-examples/LocatorHandler/test_inputs.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
LocatorHandler.autoLocator
3-
--max-nondet-string-length 10 --unwind 10 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
3+
--max-nondet-string-length 10 --unwind 10 --classpath `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.class

-698 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/SignalUtil/SignalUtil.class

-520 Bytes
Binary file not shown.

‎jbmc/regression/book-examples/SignalUtil/equivalence_check.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
EquivalenceCheck.check
3-
3+
-cp target/classes
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/book-examples/SignalUtil/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.book-examples.SignalUtil</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.book-examples</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.java ‎jbmc/regression/book-examples/SignalUtil/src/main/java/EquivalenceCheck.java

File renamed without changes.

‎jbmc/regression/book-examples/SignalUtil/SignalUtil.java ‎jbmc/regression/book-examples/SignalUtil/src/main/java/SignalUtil.java

File renamed without changes.

‎jbmc/regression/book-examples/StringUtil/StringUtil.class

-1.06 KB
Binary file not shown.

‎jbmc/regression/book-examples/StringUtil/functional_property.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
StringUtil.getLastToken
3-
--max-nondet-string-length 100 --unwind 2 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
3+
--max-nondet-string-length 100 --unwind 2 --classpath `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎jbmc/regression/book-examples/StringUtil/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.book-examples.StringUtil</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.book-examples</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/book-examples/StringUtil/StringUtil.java ‎jbmc/regression/book-examples/StringUtil/src/main/java/StringUtil.java

File renamed without changes.

‎jbmc/regression/book-examples/pom.xml

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.book-examples</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
<packaging>pom</packaging>
10+
11+
<parent>
12+
<groupId>org.cprover.regression</groupId>
13+
<artifactId>regression</artifactId>
14+
<version>1.0-SNAPSHOT</version>
15+
</parent>
16+
17+
<modules>
18+
<module>BinarySearch</module>
19+
<module>LocatorHandler</module>
20+
<module>SignalUtil</module>
21+
<module>StringUtil</module>
22+
</modules>
23+
24+
</project>

‎jbmc/regression/pom.xml

+1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515

1616
<modules>
1717
<module>jbmc</module>
18+
<module>book-examples</module>
1819
</modules>
1920

2021
<build>

0 commit comments

Comments
 (0)