Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compile Java regression test sources (2/n) #8548

Merged
merged 4 commits into from
Jan 3, 2025
Merged

Compile Java regression test sources (2/n) #8548

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a0d9f3e
Compile book-examples/BinarySearch test sources
peterschrammel Dec 30, 2024
68f3ff0
Compile book-examples/LocatorHandler test sources
peterschrammel Dec 30, 2024
7d7a192
Compile book-examples/SignalUtil test sources
peterschrammel Dec 30, 2024
60a7a6c
Compile book-examples/StringUtil test sources
peterschrammel Dec 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file removed jbmc/regression/book-examples/BinarySearch/BinarySearch.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/book-examples/BinarySearch/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
<?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.book-examples.BinarySearch</artifactId>
<version>1.0-SNAPSHOT</version>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.book-examples</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<build>
<plugins>
<plugin>
<artifactId>maven-jar-plugin</artifactId>
<executions>
<execution>
<id>default-jar</id>
<phase>none</phase>
</execution>
</executions>
</plugin>
</plugins>
</build>

</project>
2 changes: 1 addition & 1 deletion jbmc/regression/book-examples/BinarySearch/runtime_exception.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
BinarySearch.binarySearch
--throw-runtime-exceptions --unwind 2
--throw-runtime-exceptions --unwind 2 -cp target/classes
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
0 ...k-examples/BinarySearch/BinarySearch.java → ...arySearch/src/main/java/BinarySearch.java
View file
Open in desktop
File renamed without changes.
Binary file removed jbmc/regression/book-examples/LocatorHandler/IdLocator.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/book-examples/LocatorHandler/Locator.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/book-examples/LocatorHandler/LocatorHandler$1.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/book-examples/LocatorHandler/LocatorHandler$LocatorType.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/book-examples/LocatorHandler/LocatorHandler.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/book-examples/LocatorHandler/XPathLocator.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/book-examples/LocatorHandler/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
<?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.book-examples.LocatorHandler</artifactId>
<version>1.0-SNAPSHOT</version>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.book-examples</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<build>
<plugins>
<plugin>
<artifactId>maven-jar-plugin</artifactId>
<executions>
<execution>
<id>default-jar</id>
<phase>none</phase>
</execution>
</executions>
</plugin>
</plugins>
</build>

</project>
0 ...ok-examples/LocatorHandler/IdLocator.java → ...catorHandler/src/main/java/IdLocator.java
View file
Open in desktop
File renamed without changes.
0 ...book-examples/LocatorHandler/Locator.java → ...LocatorHandler/src/main/java/Locator.java
View file
Open in desktop
File renamed without changes.
0 ...amples/LocatorHandler/LocatorHandler.java → ...Handler/src/main/java/LocatorHandler.java
View file
Open in desktop
File renamed without changes.
0 ...examples/LocatorHandler/XPathLocator.java → ...orHandler/src/main/java/XPathLocator.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/book-examples/LocatorHandler/test_inputs.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
LocatorHandler.autoLocator
--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`
--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`
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Binary file removed jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/book-examples/SignalUtil/SignalUtil.class
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion jbmc/regression/book-examples/SignalUtil/equivalence_check.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
EquivalenceCheck.check

-cp target/classes
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
30 changes: 30 additions & 0 deletions jbmc/regression/book-examples/SignalUtil/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
<?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.book-examples.SignalUtil</artifactId>
<version>1.0-SNAPSHOT</version>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.book-examples</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<build>
<plugins>
<plugin>
<artifactId>maven-jar-plugin</artifactId>
<executions>
<execution>
<id>default-jar</id>
<phase>none</phase>
</execution>
</executions>
</plugin>
</plugins>
</build>

</project>
0 ...examples/SignalUtil/EquivalenceCheck.java → ...lUtil/src/main/java/EquivalenceCheck.java
View file
Open in desktop
File renamed without changes.
0 .../book-examples/SignalUtil/SignalUtil.java → .../SignalUtil/src/main/java/SignalUtil.java
View file
Open in desktop
File renamed without changes.
Binary file removed jbmc/regression/book-examples/StringUtil/StringUtil.class
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion jbmc/regression/book-examples/StringUtil/functional_property.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
StringUtil.getLastToken
--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`
--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`
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
30 changes: 30 additions & 0 deletions jbmc/regression/book-examples/StringUtil/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
<?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.book-examples.StringUtil</artifactId>
<version>1.0-SNAPSHOT</version>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression.book-examples</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<build>
<plugins>
<plugin>
<artifactId>maven-jar-plugin</artifactId>
<executions>
<execution>
<id>default-jar</id>
<phase>none</phase>
</execution>
</executions>
</plugin>
</plugins>
</build>

</project>
0 .../book-examples/StringUtil/StringUtil.java → .../StringUtil/src/main/java/StringUtil.java
View file
Open in desktop
File renamed without changes.
24 changes: 24 additions & 0 deletions jbmc/regression/book-examples/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
<?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.book-examples</artifactId>
<version>1.0-SNAPSHOT</version>
<packaging>pom</packaging>

<parent>
<groupId>org.cprover.regression</groupId>
<artifactId>regression</artifactId>
<version>1.0-SNAPSHOT</version>
</parent>

<modules>
<module>BinarySearch</module>
<module>LocatorHandler</module>
<module>SignalUtil</module>
<module>StringUtil</module>
</modules>

</project>
1 change: 1 addition & 0 deletions jbmc/regression/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@

<modules>
<module>jbmc</module>
<module>book-examples</module>
</modules>

<build>
Expand Down
Loading