From a0d9f3ee1def9cce2842573a5dad486390220201 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 30 Dec 2024 17:08:48 +0100
Subject: [PATCH 1/4] Compile book-examples/BinarySearch test sources

Add pom.xml for compilation,
move sources
remove obsolete pre-compiled class files.
---
 .../BinarySearch/BinarySearch.class           | Bin 549 -> 0 bytes
 .../book-examples/BinarySearch/pom.xml        |  30 ++++++++++++++++++
 .../BinarySearch/runtime_exception.desc       |   2 +-
 .../{ => src/main/java}/BinarySearch.java     |   0
 jbmc/regression/book-examples/pom.xml         |  21 ++++++++++++
 jbmc/regression/pom.xml                       |   1 +
 6 files changed, 53 insertions(+), 1 deletion(-)
 delete mode 100644 jbmc/regression/book-examples/BinarySearch/BinarySearch.class
 create mode 100644 jbmc/regression/book-examples/BinarySearch/pom.xml
 rename jbmc/regression/book-examples/BinarySearch/{ => src/main/java}/BinarySearch.java (100%)
 create mode 100644 jbmc/regression/book-examples/pom.xml

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

literal 549
zcmYjNO;6iE5Pf5>9r6JLic5ij#Gw)dK@NNfiIM}ADn$zIA&3hXHpVIr#*R!3;@9+o
z#Dxp$p%RDu0RBP$4CSpsRrWA5@6F7<xBL9^Gz74P`4Vi*7VxQnIf45njKe`wV6Utm
z3)I)-ED%h#!#Mb!U3P=?NOvPL)9u99(XmcLgWpLtI1jG`6YYaA*6D30(5ZjEC#ZBs
zFf~?ATCLTVz|m={Zw1zg0oOXpc(brBMafN&9wb?OMv(RU|AB;p@y<Z|7l*q4E?ep(
zS?UMhLSt-dRC}YRuXP0q4o!?U1Xa^&L^}T2_|feJ{s7Cc_!H(>;LG7Kx<n0TVRq_&
zAdh*w!06_rV2pL;Z2(1-h>9rZj9LE8D;?%td%r$x)`w2Cqw1d8Sonp{i#2t6hov0e
zq3EgRJzP)iFV;@Y*!{o1o_gS}4WqY|N1Nu1HHR85=E<$m!8Ub`kF7T?jAMd`s+dHT
m-Yo23ij~FwCZ<{0++W8BRthtmEJMAZEFv|l$OVs-g^#cQ3t!&=

diff --git a/jbmc/regression/book-examples/BinarySearch/pom.xml b/jbmc/regression/book-examples/BinarySearch/pom.xml
new file mode 100644
index 00000000000..2b35936a565
--- /dev/null
+++ b/jbmc/regression/book-examples/BinarySearch/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.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>
diff --git a/jbmc/regression/book-examples/BinarySearch/runtime_exception.desc b/jbmc/regression/book-examples/BinarySearch/runtime_exception.desc
index 5279b047b37..fc095ac4902 100644
--- a/jbmc/regression/book-examples/BinarySearch/runtime_exception.desc
+++ b/jbmc/regression/book-examples/BinarySearch/runtime_exception.desc
@@ -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$
diff --git a/jbmc/regression/book-examples/BinarySearch/BinarySearch.java b/jbmc/regression/book-examples/BinarySearch/src/main/java/BinarySearch.java
similarity index 100%
rename from jbmc/regression/book-examples/BinarySearch/BinarySearch.java
rename to jbmc/regression/book-examples/BinarySearch/src/main/java/BinarySearch.java
diff --git a/jbmc/regression/book-examples/pom.xml b/jbmc/regression/book-examples/pom.xml
new file mode 100644
index 00000000000..089f23b787b
--- /dev/null
+++ b/jbmc/regression/book-examples/pom.xml
@@ -0,0 +1,21 @@
+<?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>
+    </modules>
+
+</project>
diff --git a/jbmc/regression/pom.xml b/jbmc/regression/pom.xml
index 9cb0f685389..8631fb6272d 100644
--- a/jbmc/regression/pom.xml
+++ b/jbmc/regression/pom.xml
@@ -15,6 +15,7 @@
 
     <modules>
         <module>jbmc</module>
+        <module>book-examples</module>
     </modules>
 
     <build>

From 68f3ff0fef6c5f1af766e82c2c312584fb01a6e0 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 30 Dec 2024 17:15:04 +0100
Subject: [PATCH 2/4] Compile book-examples/LocatorHandler test sources

Add pom.xml for compilation,
move sources
remove obsolete pre-compiled class files.
---
 .../LocatorHandler/IdLocator.class            | Bin 330 -> 0 bytes
 .../LocatorHandler/Locator.class              | Bin 95 -> 0 bytes
 .../LocatorHandler/LocatorHandler$1.class     | Bin 684 -> 0 bytes
 .../LocatorHandler$LocatorType.class          | Bin 1032 -> 0 bytes
 .../LocatorHandler/LocatorHandler.class       | Bin 1336 -> 0 bytes
 .../LocatorHandler/XPathLocator.class         | Bin 339 -> 0 bytes
 .../book-examples/LocatorHandler/pom.xml      |  30 ++++++++++++++++++
 .../{ => src/main/java}/IdLocator.java        |   0
 .../{ => src/main/java}/Locator.java          |   0
 .../{ => src/main/java}/LocatorHandler.java   |   0
 .../{ => src/main/java}/XPathLocator.java     |   0
 .../LocatorHandler/test_inputs.desc           |   2 +-
 jbmc/regression/book-examples/pom.xml         |   1 +
 13 files changed, 32 insertions(+), 1 deletion(-)
 delete mode 100644 jbmc/regression/book-examples/LocatorHandler/IdLocator.class
 delete mode 100644 jbmc/regression/book-examples/LocatorHandler/Locator.class
 delete mode 100644 jbmc/regression/book-examples/LocatorHandler/LocatorHandler$1.class
 delete mode 100644 jbmc/regression/book-examples/LocatorHandler/LocatorHandler$LocatorType.class
 delete mode 100644 jbmc/regression/book-examples/LocatorHandler/LocatorHandler.class
 delete mode 100644 jbmc/regression/book-examples/LocatorHandler/XPathLocator.class
 create mode 100644 jbmc/regression/book-examples/LocatorHandler/pom.xml
 rename jbmc/regression/book-examples/LocatorHandler/{ => src/main/java}/IdLocator.java (100%)
 rename jbmc/regression/book-examples/LocatorHandler/{ => src/main/java}/Locator.java (100%)
 rename jbmc/regression/book-examples/LocatorHandler/{ => src/main/java}/LocatorHandler.java (100%)
 rename jbmc/regression/book-examples/LocatorHandler/{ => src/main/java}/XPathLocator.java (100%)

diff --git a/jbmc/regression/book-examples/LocatorHandler/IdLocator.class b/jbmc/regression/book-examples/LocatorHandler/IdLocator.class
deleted file mode 100644
index 6945bb7cb8a3b824e7023c3e229c7f5e6deffe63..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 330
zcmZXPF;BxV5QX14ZB5fcOQ6h*EdyQHT3C>fkRlk0vOB3&T!lmmF8_-OiGd%$k3u{{
zRR#w8?tQ*Hzx(`p{{V1-QH%&fjYEw@<4Dk%yUO`1!DyVW&5N0qrdmxGzH!xRHpv97
z>w0MggVa^_Zu6Ae=E3A8Ns`uuDKpc!ptrE)AKkN{m)<VJv#*<(KuD7R(*^OO-ZX{1
zabe!UuH`%!>7$KfL3c+5!#{)f`Pvp<ptrvWqVXidDHQjkX)Y@~ZFCqlvr9%5$k`j@
gm5IV0@AwBQHbm%BpZpe)_o%{vKK9v4dsGU8Zw_oiJ^%m!

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

literal 95
zcmX^0Z`VEs1_l!bc6J6<b_O;^2Cm@z(xT*4x6GVWMg|_A{N%)v{35-q#Ii(226iZy
lkwE|?pr4bNm#*)hl$DxX0@TUKzyvf31Q;2Zfg}?H3jndz6+8d{

diff --git a/jbmc/regression/book-examples/LocatorHandler/LocatorHandler$1.class b/jbmc/regression/book-examples/LocatorHandler/LocatorHandler$1.class
deleted file mode 100644
index dbf7819189f4605ec7b98e9781508f7533a4dfa5..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 684
zcmaJ<-%k@k5dQXh?Y8BBvw##tK`6E5L1N;Y#%K^iV+$s2(1fS$-G**m_sI5&;V<G@
zO^h*yKfpiAID2BuJ!rDCGvEC9W;3%tetx?K@EAK)+{SVR9Q6uWD-N!5+;L!y<1WWK
z!*-+pL8Z~CC(aw)Bob+24~2=fw142>@?0`_ryYj!(?~0$(q{~XR{Mm(-%DZ&&UclO
zN7MI1X$NAc$y0M&`b1de@Qrh}pNi-mb;>ZkgrV9`rZ$oX$`vi-AMkK2E(DS9n@A@U
zWzKps9VIcx2FLvXTWAERpc-Hs%>WP3Vpw%0yIPpD-J_&GjYbDb>UiJU#0F@i$q?py
zG#)Vo9b=^3(_%7_6Uz9@aXcK$C}o(-7g3+QBR{H{o8a%kl`e#yI^OkG`?UM-x+e_9
zx36Ce4jI<|pT-j#D<gEa1lo$%c^Pidmdmtt7S`QNoJDvB0qI#nV-&~&T3^AgzgIuQ
z`{YjH3w;0h3jV7MmIxLz_z@oQEMgf&)M?aB(gn;BLn-6&F;BKf5|RY)-*DVQ&s~&P
c%VG;u5BON3`yNS+@;PaQW%_|j*nGb73yfTwDF6Tf

diff --git a/jbmc/regression/book-examples/LocatorHandler/LocatorHandler$LocatorType.class b/jbmc/regression/book-examples/LocatorHandler/LocatorHandler$LocatorType.class
deleted file mode 100644
index e323700784493da77da61a1ec12a480ae19b4fda..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1032
zcmah{VQ<n<6g{tfP$=ETVCq2ToT37oFcd#Q7M8hXBxExIiHn~KtJtL!Q_2$mm9oSc
zjb@+yQO5gf<JxHOHR;WJ=e%>zz3=|``Q<x+8ftNHJXG-r1qEpZB^4Sr#cwNy1(m=p
z!FU|QvWR5`6^6*G7rWg<hD3Wj(A}}qegDp2&|0=_ID3{pnHUp>T-!$vb^FvZoP2;>
zXOLRY8I*i)xBYUz!?5;xK0SJ_TT>ysUMT*D%J;^nWM`>u+Q!jz)Hj^2-nZyP@idO#
zFl-mvXZpEbv2=S_>9~$*59`JG22#Sl)zckQi1~`#)<-0q`df`5+AwX?-C?--k7TW4
zkAb^yO{yr~F^9J9P90K`3j&BW29|%h9FX3(r=!L^mpjx~wKJYN1LMFH6{o{bP!>gN
zNQs9|YuH9r!4rmTm=$~|4Xb#nVGVaQEFh_28A*o4>*fhhG!O%8Y*W6KLNVa?xPN90
zT=KLSPQdUi*b;AI>VbQI9weNm-mKCDYBaWTGb7vp6v+^f%!;B2;fP}eH$Yvd-93t8
zsWY%okggzqpdG_4`bRxXBK|5eKEDRZJ5^J>^cj&WaKV>C{4AYlzgf7AoQG3;h$S*s
zA=3varOn(Wq8~jtnC|+zf^}gXcRkJqVq|y2H*!FQh*kayev(q;OT;b^_cki`Hi^hL
mg5()Z&k3I)(YXK<*}}!izWROS36t;uOB7XNaTKxG%=`j7+}>IM

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

literal 1336
zcma)6TT|0e5dKbENE-sZLFFdiiqaxf6h$m3$VDmzbjqOMi)j;SFs4kBBEC5M4fz8;
z_<}f7W@JX+{UiPh$31BZ6mZ5&d(Q4=&$qkZ?#Zt|-+urY#*&CA`U7aiO%X8+_%SFV
zg<AoHF(lx&2m$?m+~LMyzT6dXPlSXKKkf?{6%oXUfCnPd7!xoq;30#QF$~q5(q+q1
zEdh@hnzE&WY?sXC51T4OG|u0cwpKE%Y0Z-Jx~ed+HHOA9&CqOu@b)EE7<^MDh5UnA
z%}^K1@A9g-%$*q`98X`7O^xfW(PtMmiy@SCgU!i?qN`?_!pmj5<XRa<`?4GImYmXM
zV?C9#P0d(OpE?sik#9Otdr3%wUM+;Da0Y}Dww(gIYbV?k>fjifbGBS~yC846iTlS2
zx?8uHE0xWHI;-(2qxFRh@_-UL(IsI5lM)_diYVLOl<guBKP_Pfvl80T!O(u3++>aG
z8PhD8#Phg>Czz9v!Bgth%V%`l4aC9ciF{2NX9#2z*UZpTpNW91gas@T*~f8~@*8Tw
z=KNPFs?|Qk(0R(_s?}-ejpyELcA-do)Oe~Lt@HD|$`Jo0Q_&1rcP51N6Y;B^WDqS|
zHf`&LW)~US&gpf622IcmMcrO{^A8U~4p`;9<qQY+$t2Ee_qpgax4~mpoLj&UQ&dYc
zRpqD|Gy-;+rj-VL4Oi&4Md?1WP&;oQNnQ|Z=%Tfov=r@(_J-sE*jExfxJYZGV`S(d
zS*kkV5-yV#Ajqp^;fH?{n1}YAeR%pS@D6?<g`O??b2|s-eq7EZBfbh6KA~qHjk{<%
zgs^%5|IcJH5~x7*y{@2X{t(hCCDOc?jI{iRbC5fS_Shcbd!4+K5J~nSP8AH$2PO?a
z=E(M(s#rraifBO@A$&x{sV!E`AJ^yve|FG|>y-Bmk^>OpG09Iq0_i(qY}hFa2uH#d
tM0O$gKEvnzhQ_n(ag+vlqzOi05~O&LL>ui9l3Hm;$WNcfFfL4V`~_nhD%1b~

diff --git a/jbmc/regression/book-examples/LocatorHandler/XPathLocator.class b/jbmc/regression/book-examples/LocatorHandler/XPathLocator.class
deleted file mode 100644
index 7d495e0e0f96df9f7fbbe7a30f5fe8e969ac8afa..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 339
zcmZWku}%U(5Ph=;te%I!Db|!=Aq^d9Lqc^?6UfDO@7TbS^DbEy{>#e5!VmDHh_gx}
ziN(&$dpmDt-q+#d6Tk@F5CPf}9f?@tiqM#t(zpjgx1Vg(UJVOXu7-1GO}QEmQbKK7
zEj6K)m{LFPUNdbMDl3?YlPXt5s;u$&NY>oiYzddi%d>K8-{C4dCJ>YH{{@6_UhQnI
zXU320oT~2pIT7l(CPb$ng!bR1PuWK2jv$Y_2tj|4q6fi7`FeIu{OV|MmR#L)7M{6%
j2fcA2aK<tGAq5KpoHM@pZDRg{kslDD$x`;lNTBr%9Zf~=

diff --git a/jbmc/regression/book-examples/LocatorHandler/pom.xml b/jbmc/regression/book-examples/LocatorHandler/pom.xml
new file mode 100644
index 00000000000..71a4f0c5244
--- /dev/null
+++ b/jbmc/regression/book-examples/LocatorHandler/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.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>
diff --git a/jbmc/regression/book-examples/LocatorHandler/IdLocator.java b/jbmc/regression/book-examples/LocatorHandler/src/main/java/IdLocator.java
similarity index 100%
rename from jbmc/regression/book-examples/LocatorHandler/IdLocator.java
rename to jbmc/regression/book-examples/LocatorHandler/src/main/java/IdLocator.java
diff --git a/jbmc/regression/book-examples/LocatorHandler/Locator.java b/jbmc/regression/book-examples/LocatorHandler/src/main/java/Locator.java
similarity index 100%
rename from jbmc/regression/book-examples/LocatorHandler/Locator.java
rename to jbmc/regression/book-examples/LocatorHandler/src/main/java/Locator.java
diff --git a/jbmc/regression/book-examples/LocatorHandler/LocatorHandler.java b/jbmc/regression/book-examples/LocatorHandler/src/main/java/LocatorHandler.java
similarity index 100%
rename from jbmc/regression/book-examples/LocatorHandler/LocatorHandler.java
rename to jbmc/regression/book-examples/LocatorHandler/src/main/java/LocatorHandler.java
diff --git a/jbmc/regression/book-examples/LocatorHandler/XPathLocator.java b/jbmc/regression/book-examples/LocatorHandler/src/main/java/XPathLocator.java
similarity index 100%
rename from jbmc/regression/book-examples/LocatorHandler/XPathLocator.java
rename to jbmc/regression/book-examples/LocatorHandler/src/main/java/XPathLocator.java
diff --git a/jbmc/regression/book-examples/LocatorHandler/test_inputs.desc b/jbmc/regression/book-examples/LocatorHandler/test_inputs.desc
index e671317f037..d41b24c11ba 100644
--- a/jbmc/regression/book-examples/LocatorHandler/test_inputs.desc
+++ b/jbmc/regression/book-examples/LocatorHandler/test_inputs.desc
@@ -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$
diff --git a/jbmc/regression/book-examples/pom.xml b/jbmc/regression/book-examples/pom.xml
index 089f23b787b..b680fe747a3 100644
--- a/jbmc/regression/book-examples/pom.xml
+++ b/jbmc/regression/book-examples/pom.xml
@@ -16,6 +16,7 @@
 
     <modules>
         <module>BinarySearch</module>
+        <module>LocatorHandler</module>
     </modules>
 
 </project>

From 7d7a192fa4470c84867b458a17c3abe3ad47ebeb Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 30 Dec 2024 17:16:57 +0100
Subject: [PATCH 3/4] Compile book-examples/SignalUtil test sources

Add pom.xml for compilation,
move sources
remove obsolete pre-compiled class files.
---
 .../SignalUtil/EquivalenceCheck.class         | Bin 698 -> 0 bytes
 .../book-examples/SignalUtil/SignalUtil.class | Bin 520 -> 0 bytes
 .../SignalUtil/equivalence_check.desc         |   2 +-
 .../book-examples/SignalUtil/pom.xml          |  30 ++++++++++++++++++
 .../{ => src/main/java}/EquivalenceCheck.java |   0
 .../{ => src/main/java}/SignalUtil.java       |   0
 jbmc/regression/book-examples/pom.xml         |   1 +
 7 files changed, 32 insertions(+), 1 deletion(-)
 delete mode 100644 jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.class
 delete mode 100644 jbmc/regression/book-examples/SignalUtil/SignalUtil.class
 create mode 100644 jbmc/regression/book-examples/SignalUtil/pom.xml
 rename jbmc/regression/book-examples/SignalUtil/{ => src/main/java}/EquivalenceCheck.java (100%)
 rename jbmc/regression/book-examples/SignalUtil/{ => src/main/java}/SignalUtil.java (100%)

diff --git a/jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.class b/jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.class
deleted file mode 100644
index 1ad1523184f7a9ffa3d3bfe716ff4ba2683229f2..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 698
zcmZWmT~8B16g_u8y6v(Etpc@05kV<nY&5({h^9aSL3k*V*zhvlPGDf&mEA4B#25Jk
zK7$DmP2}AlWxTU3kif&-xnJkpb7%hk`}GIF0$#Z&pjv=~aTibURGSG0&s^B3I+%3v
z98(Ua2@j`5lE^q!QJ5^NM6?6hAyA8uTU4P+mk4HUc86d!qK+gCZKzOgcE7Y`yseuF
zrH#lJ!H$TPj{8X~-B*dOtsHgLu?S@7%f`O+58n}NUpvfLThqk3MD2wl;Gt`T!DcG_
z!;j)?pC`ZQ2YnfCGwQ~^TvdAL$X(vo2jW<G@G$7X#ejns9$sR`Lk%;8vaZ$x5$@GL
zT(7$l$5BiezRTob*25g;xpa%#Y9B~HCAiH@?59+*U`w=<H@!X9d(m5dpj%KQ;I}1=
zc4VSr*}0j_JEmPO@WZw+$)8l<Pov?o7S5gt(tEIdz)_uV;@h6P0G+a9V2EulOR`4x
zy<P)~C~?GpibrfUco!D;1JyGaCm5?<!sKIp`;LL%us>fQccm%KjMB|oO;i}9X-9j|
yJ}r}AgmZ+k3_%s-QNEG6kZAylCFdOZ6FAlnSmsX{_a$q*4a0k{7kkWsfy#e!B7s~0

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

literal 520
zcmYjN%TB^T6g|@x3Z*=KrW<t!E+iUv8be}2f<axN?5Eg3v4Uxff52Dh-W3a1CNBH{
zzsVTS6a*)kx%ZrV=bX9o_4Dxw;27H$bZnT|G_fU+KJ`a_d?uh*Yh3~3e0=8#6x;sD
zyP7<>UU(zjfJ~)5?#ZAlLto(qX~Y9R60qAHzdw?}ZR`gp)R1m;$WU$7E@%*X(Ikik
zgaT30NYE0<cVgMQzm$)EYP@$OV0Ffmu;(>>Wm{Y+9}MM_v|%8ndX|O)B~_>ga@4P1
zyF;%RV-Ff<R7(dRf)vj*QJqmRruN?<-k4}Gd8QLmAj90AHy{g(D2rUesLO+eXxVv2
z)|ob5k<pyNw6QZ|QBQ;_^a8hXw8#`GsYG{^x{f>wiF}!r68Rz}=Ukb{gl2uiFz8xY
sx;ELOo}6=DU^?-1=1f<9g=ESc{cQRa{tb{@I4E8IL53P@Of{_k0$vA9rvLx|

diff --git a/jbmc/regression/book-examples/SignalUtil/equivalence_check.desc b/jbmc/regression/book-examples/SignalUtil/equivalence_check.desc
index 65097c88880..47c44af6494 100644
--- a/jbmc/regression/book-examples/SignalUtil/equivalence_check.desc
+++ b/jbmc/regression/book-examples/SignalUtil/equivalence_check.desc
@@ -1,6 +1,6 @@
 CORE
 EquivalenceCheck.check
-
+-cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/book-examples/SignalUtil/pom.xml b/jbmc/regression/book-examples/SignalUtil/pom.xml
new file mode 100644
index 00000000000..9ff50908386
--- /dev/null
+++ b/jbmc/regression/book-examples/SignalUtil/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.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>
diff --git a/jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.java b/jbmc/regression/book-examples/SignalUtil/src/main/java/EquivalenceCheck.java
similarity index 100%
rename from jbmc/regression/book-examples/SignalUtil/EquivalenceCheck.java
rename to jbmc/regression/book-examples/SignalUtil/src/main/java/EquivalenceCheck.java
diff --git a/jbmc/regression/book-examples/SignalUtil/SignalUtil.java b/jbmc/regression/book-examples/SignalUtil/src/main/java/SignalUtil.java
similarity index 100%
rename from jbmc/regression/book-examples/SignalUtil/SignalUtil.java
rename to jbmc/regression/book-examples/SignalUtil/src/main/java/SignalUtil.java
diff --git a/jbmc/regression/book-examples/pom.xml b/jbmc/regression/book-examples/pom.xml
index b680fe747a3..c9f4a68ee31 100644
--- a/jbmc/regression/book-examples/pom.xml
+++ b/jbmc/regression/book-examples/pom.xml
@@ -17,6 +17,7 @@
     <modules>
         <module>BinarySearch</module>
         <module>LocatorHandler</module>
+        <module>SignalUtil</module>
     </modules>
 
 </project>

From 60a7a6c798379ec5d79f2da88c887232fb1e0bcf 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 4/4] Compile book-examples/StringUtil test sources

Add pom.xml for compilation,
move sources
remove obsolete pre-compiled class files.
---
 .../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
 jbmc/regression/book-examples/pom.xml         |   1 +
 5 files changed, 32 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..5ba1b032679
--- /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>
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
diff --git a/jbmc/regression/book-examples/pom.xml b/jbmc/regression/book-examples/pom.xml
index c9f4a68ee31..5c3610baaf2 100644
--- a/jbmc/regression/book-examples/pom.xml
+++ b/jbmc/regression/book-examples/pom.xml
@@ -18,6 +18,7 @@
         <module>BinarySearch</module>
         <module>LocatorHandler</module>
         <module>SignalUtil</module>
+        <module>StringUtil</module>
     </modules>
 
 </project>