From 28b4290532ad7ba4f1cc7ad772c42a74195cf2ff Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 30 Dec 2024 17:19:01 +0100
Subject: [PATCH] Compile book-examples/StringUtil test sources

---
 .../book-examples/StringUtil/StringUtil.class | Bin 1087 -> 0 bytes
 .../StringUtil/functional_property.desc       |   2 +-
 .../book-examples/StringUtil/pom.xml          |  30 ++++++++++++++++++
 .../{ => src/main/java}/StringUtil.java       |   0
 4 files changed, 31 insertions(+), 1 deletion(-)
 delete mode 100644 jbmc/regression/book-examples/StringUtil/StringUtil.class
 create mode 100644 jbmc/regression/book-examples/StringUtil/pom.xml
 rename jbmc/regression/book-examples/StringUtil/{ => src/main/java}/StringUtil.java (100%)

diff --git a/jbmc/regression/book-examples/StringUtil/StringUtil.class b/jbmc/regression/book-examples/StringUtil/StringUtil.class
deleted file mode 100644
index 97f2581462a5d3f5187125d1c69619573f03250c..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1087
zcmZuv+fEZv6kVrtqtk(wOA!P_6tPsLUa-nVqNy00R51ZbAU-&B1{fHoWM(jafM0<R
zB);&9nv_HneKhee{11b!nIa{@OtNS1efDLob<WSDFW&%+<AIJ8Ms!?7E;6H$$tRJ-
zwaB}!;f4+kBO1nZ6mV0+ErHHqGYD)ybZTDk*a^%P*R}-2vVc16cuqJYAmv6E1>{oA
zvIWu=$FraBY^~V-LR2i!QK?l;chU5nC_YZg;kpwD7?t_Zcf7Tiq2o?5T(iT98H5Y9
zP1_U5<tiKI8?)e=-ddqiI8`c-o=pm9VQqffb;4-fnI3_pWxLLn6WTtpmjskJqF)wh
z^J27ftMOKX(!*%|d}#U{*AfS_9!V$NCbU)_S2v%T+c6&vw^=z|b&nO%=W9ED)qdhc
z{L@W}V-Yk1ZAi1jz#WVmxQn8Jd$@1FKx>qn5a?-Ac=S*GS>LY_z22OrVbZ`9rUf$1
z`ni=2yGq=rQjHF3<an0-c5apQbLH|VsjIH-t%d9H6*5c)J1aqa9|GM`$^WF3b8&0B
zxw1rEC|kE>2aa!BCx|IgxWfa!k7W$;nWgv&MW!brN>2i{N18UnsKCGAU&$Xre58{=
zJFOZgd8_n|Mgcm}#VCm^x|w0K$Z(j(oR$9pMI1;oQc=$LW#u{&MJ1~w_AofmFIykb
z^G*_3MSgwic>m8YCi7W2Ux!qOJgI(yvWwncwXY8KJu(CRdq{nSwseS=@4e~)_ee3e
zVoXDZ423u~wD3z2R~K~BO<|ab^Q<Y7<OFffvdbish|ALkUYtV@BO*sH&d2;L^r4^Z
zTkr}4^dwGN!UcLVC%?cTJ%zIdagn_$H-WQd^$4v(h@s!eYq-Sj%O}!~$8&-9j$|GB
bE;M-`vh*3sS(&3@3KGV{=rV>GByi;~GE&r&

diff --git a/jbmc/regression/book-examples/StringUtil/functional_property.desc b/jbmc/regression/book-examples/StringUtil/functional_property.desc
index 90c6214cd0e..34d16a684b1 100644
--- a/jbmc/regression/book-examples/StringUtil/functional_property.desc
+++ b/jbmc/regression/book-examples/StringUtil/functional_property.desc
@@ -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$
diff --git a/jbmc/regression/book-examples/StringUtil/pom.xml b/jbmc/regression/book-examples/StringUtil/pom.xml
new file mode 100644
index 00000000000..932b82ba34b
--- /dev/null
+++ b/jbmc/regression/book-examples/StringUtil/pom.xml
@@ -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>
\ No newline at end of file
diff --git a/jbmc/regression/book-examples/StringUtil/StringUtil.java b/jbmc/regression/book-examples/StringUtil/src/main/java/StringUtil.java
similarity index 100%
rename from jbmc/regression/book-examples/StringUtil/StringUtil.java
rename to jbmc/regression/book-examples/StringUtil/src/main/java/StringUtil.java