Skip to content

Commit a0dbf74

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#5684 from peterschrammel/use-java-cprover-api
Use cprover-api Maven dependency in java-models-library
2 parents 203bb3c + e4cd6ac commit a0dbf74

File tree

716 files changed

+765
-728
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

716 files changed

+765
-728
lines changed

‎jbmc/lib/java-models-library

‎jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../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/jbmc-concurrency/get-current-thread/A.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-concurrency/get-current-thread/A.java

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ public class A
88
// expected verification success
99
public void me()
1010
{
11-
int g = CProver.getCurrentThreadID();
11+
int g = CProver.getCurrentThreadId();
1212
assert(g == 0);
1313
}
1414

@@ -40,7 +40,7 @@ public void me_bug()
4040
public void me2()
4141
{
4242
CProver.startThread(333);
43-
g = CProver.getCurrentThreadID();
43+
g = CProver.getCurrentThreadId();
4444
assert(g == 1);
4545
CProver.endThread(333);
4646
}
@@ -51,7 +51,7 @@ public void me2()
5151
public void me3()
5252
{
5353
CProver.startThread(333);
54-
int i = CProver.getCurrentThreadID();
54+
int i = CProver.getCurrentThreadId();
5555
assert(g == 1);
5656
CProver.endThread(333);
5757
}
@@ -83,7 +83,7 @@ public void me6()
8383

8484
public void check()
8585
{
86-
g = CProver.getCurrentThreadID();
86+
g = CProver.getCurrentThreadId();
8787
assert(g == 1);
8888
}
8989
}
@@ -94,7 +94,7 @@ class B implements Runnable
9494
@Override
9595
public void run()
9696
{
97-
g = CProver.getCurrentThreadID();
97+
g = CProver.getCurrentThreadId();
9898
assert(g == 1);
9999
}
100100
}
@@ -106,7 +106,7 @@ class C extends Thread
106106
@Override
107107
public void run()
108108
{
109-
g = CProver.getCurrentThreadID();
109+
g = CProver.getCurrentThreadId();
110110
assert(g == 1);
111111
}
112112
}

‎jbmc/regression/jbmc-concurrency/get-current-thread/B.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-concurrency/get-current-thread/C.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-concurrency/get-current-thread/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
A
3-
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
A
3-
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
A
3-
--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED

‎jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-concurrency/several-threads/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/several-threads/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎jbmc/regression/jbmc-concurrency/several-threads/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading --unwind 3
3+
--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading --unwind 3
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
Sync
3-
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
Sync
3-
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
Sync
3-
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
3+
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --show-goto-functions --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
ATOMIC_BEGIN

‎jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Sync
3-
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
3+
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --java-threading
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
3+
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --show-goto-functions
44
^EXIT=0$
55
^SIGNAL=0$
66
ATOMIC_BEGIN

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
3+
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --show-goto-functions
44
^EXIT=0$
55
^SIGNAL=0$
66
ATOMIC_BEGIN

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
A
3-
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
A
3-
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-concurrency/synchronized/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Sync
3-
--java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-generics/type_erasure/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
TestClass
3-
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/alsoImplementsInterface.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test
3-
--function Test.alsoImplementsInterface --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function Test.alsoImplementsInterface --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/callingSuperCproverNondetInitialize.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test
3-
--function Test.callingSuperCproverNondetInitialize --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function Test.callingSuperCproverNondetInitialize --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/inheritanceFromAbstractClass.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test
3-
--function Test.inheritanceFromAbstractClass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function Test.inheritanceFromAbstractClass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/inheritanceTwoLevels.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test
3-
--function Test.inheritanceTwoLevels --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function Test.inheritanceTwoLevels --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/override.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test
3-
--function Test.override --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
3+
--function Test.override --cp `../../../../scripts/format_classpath.sh . ../../../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$

0 commit comments

Comments
 (0)