Skip to content

Commit 9354403

Browse files
committed
JBMC: enable unwinding assertions by default
We changed the default for CBMC in 9b52a38 in the interest of producing sound verification results. We should do the same for JBMC.
1 parent ae7d311 commit 9354403

File tree

12 files changed

+21
-16
lines changed

12 files changed

+21
-16
lines changed

doc/man/jbmc.1

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -349,6 +349,9 @@ remove assignments unrelated to property
349349
generate unwinding assertions (cannot be
350350
used with \fB\-\-cover\fR)
351351
.TP
352+
\fB\-\-no\-unwinding\-assertions\fR
353+
do not generate unwinding assertions
354+
.TP
352355
\fB\-\-partial\-loops\fR
353356
permit paths with partial loops
354357
.TP

jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.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.fromNonDetArray --depth 10000 --unwind 5 --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace
3+
--function Test.fromNonDetArray --depth 10000 --unwind 5 --no-unwinding-assertions --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED

jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.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.check --unwind 10 --max-nondet-string-length 10 --java-assume-inputs-non-null
3+
--function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
THOROUGH
22
Test
3-
--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --sat-solver cadical
3+
--function Test.check --max-nondet-string-length 50 --unwind 50 --no-unwinding-assertions --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --sat-solver cadical
44
VERIFICATION SUCCESSFUL
55
^EXIT=0$
66
^SIGNAL=0$

jbmc/regression/jbmc/NondetArray2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
NondetArray2
3-
--function NondetArray2.main --unwind 5
3+
--function NondetArray2.main --unwind 5 --no-unwinding-assertions
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

jbmc/regression/jbmc/NondetArray3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
NondetArray3
3-
--function NondetArray3.main --unwind 5
3+
--function NondetArray3.main --unwind 5 --no-unwinding-assertions
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

jbmc/regression/jbmc/dynamic-multi-dimensional-array/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.f --unwind 2
3+
--function TestClass.f --unwind 2 --no-unwinding-assertions
44
^EXIT=0$
55
^SIGNAL=0$
66
--

jbmc/regression/jbmc/enum/test_enum1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Enum1
3-
--java-unwind-enum-static --unwind 3
3+
--java-unwind-enum-static --unwind 3 --no-unwinding-assertions
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

jbmc/regression/jbmc/nondet_propagation1/andNot_Pass.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
andNot_Pass
3-
--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100 --function andNot_Pass.main
3+
--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --no-unwinding-assertions --max-nondet-string-length 100 --function andNot_Pass.main
44
^\[java::andNot_Pass\.main:\(\[Ljava/lang/String;\)V.assertion\.3\] line 40 assertion at file andNot_Pass\.java line 40 function java::andNot_Pass.main:\(\[Ljava/lang/String;\)V bytecode-index 52: FAILURE$
55
^\*\* 1 of \d+ failed
66
VERIFICATION FAILED

jbmc/regression/jbmc/nondet_propagation1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
andNot_Bug
3-
--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100 --function andNot_Bug.main
3+
--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --no-unwinding-assertions --max-nondet-string-length 100 --function andNot_Bug.main
44
^EXIT=0$
55
^SIGNAL=0$
66
--

0 commit comments

Comments
 (0)