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

Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions) #3423

Merged
merged 3 commits into from
Nov 17, 2018
Merged

Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions) #3423

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
079c4d2
Make tests use core-models from jbmc/lib/java-models-library
peterschrammel Nov 17, 2018
5b17b23
Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions)
peterschrammel Nov 14, 2018
71490ae
Move all concurrency tests into jbmc-concurrency
peterschrammel Nov 17, 2018
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
2 changes: 1 addition & 1 deletion jbmc/lib/java-models-library
Open in desktop
Submodule java-models-library updated 1 files
+7 −4 src/main/java/java/lang/Object.java
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
A.class
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^SIGNAL=0$
^VERIFICATION FAILED$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
A.class
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
A.class
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
A.class
--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
A.class
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^SIGNAL=0$
^VERIFICATION FAILED
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
A.class
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^SIGNAL=0$
^VERIFICATION FAILED$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/several-threads/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/several-threads/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
A.class
--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^SIGNAL=0$
^VERIFICATION FAILED$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/several-threads/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3
--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading --unwind 3
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
Sync.class
--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
Sync.class
--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
Sync.class
--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Sync.class
--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
ATOMIC_BEGIN
ATOMIC_END
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
A.class
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
A.class
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
0 jbmc/regression/jbmc/synchronized/Sync.class → .../jbmc-concurrency/synchronized/Sync.class
View file
Open in desktop
File renamed without changes.
0 jbmc/regression/jbmc/synchronized/Sync.java → ...n/jbmc-concurrency/synchronized/Sync.java
View file
Open in desktop
File renamed without changes.
9 changes: 9 additions & 0 deletions jbmc/regression/jbmc-concurrency/synchronized/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
Sync.class
--java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
--
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-generics/type_erasure/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
TestClass.class
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
EXIT=0
SIGNAL=0
VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumArg.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumArg.class
--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumArgField/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumArgField.class
--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumOpaqueReturn.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
NondetEnumOpaqueReturn.class
--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^VERIFICATION FAILED$
--
--
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/coreModels/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
test.class
--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/enum_values_clone/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE symex-driven-lazy-loading-expected-failure
com/diffblue/regression/EnumIter.class
--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
--
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/enum_values_clone_name/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE symex-driven-lazy-loading-expected-failure
com/diffblue/regression/EnumIter.class
--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=0$
^SIGNAL=0$
--
Loading