Merge pull request #8273 from tautschnig/jbmc-unwinding-assertions

JBMC: enable unwinding assertions by default

Author: kroening

doc/man/jbmc.1

@@ -349,6 +349,9 @@ remove assignments unrelated to property
 generate unwinding assertions (cannot be
 used with \fB\-\-cover\fR)
 .TP
+\fB\-\-no\-unwinding\-assertions\fR
+do not generate unwinding assertions
+.TP
 \fB\-\-partial\-loops\fR
 permit paths with partial loops
 .TP

jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc

@@ -1,6 +1,6 @@
 CORE
 Test
---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
+--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
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED

jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc

@@ -1,6 +1,6 @@
 CORE
 Test
---function Test.check --unwind 10 --max-nondet-string-length 10 --java-assume-inputs-non-null
+--function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -1,6 +1,6 @@
 THOROUGH
 Test
---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
+--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
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetArray2/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetArray2
---function NondetArray2.main --unwind 5
+--function NondetArray2.main --unwind 5 --no-unwinding-assertions
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetArray3/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetArray3
---function NondetArray3.main --unwind 5
+--function NondetArray3.main --unwind 5 --no-unwinding-assertions
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/dynamic-multi-dimensional-array/test.desc

@@ -1,6 +1,6 @@
 CORE
 TestClass
---function TestClass.f --unwind 2
+--function TestClass.f --unwind 2 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/enum/test_enum1.desc

@@ -1,6 +1,6 @@
 CORE
 Enum1
---java-unwind-enum-static --unwind 3
+--java-unwind-enum-static --unwind 3 --no-unwinding-assertions
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/nondet_propagation1/andNot_Pass.desc

@@ -1,6 +1,6 @@
 CORE
 andNot_Pass
---depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100 --function andNot_Pass.main
+--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
 ^\[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$
 ^\*\* 1 of \d+ failed
 VERIFICATION FAILED

jbmc/regression/jbmc/nondet_propagation1/test.desc

@@ -1,6 +1,6 @@
 CORE
 andNot_Bug
---depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100  --function andNot_Bug.main
+--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
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/output-options/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Main
---verbosity 10 --unwind 2 --disable-uncaught-exception-check --throw-assertion-error
+--verbosity 10 --unwind 2 --no-unwinding-assertions --disable-uncaught-exception-check --throw-assertion-error
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -205,10 +205,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     }
   }
 
+  // generate unwinding assertions
+  options.set_option(
+    "unwinding-assertions",
+    cmdline.isset("unwinding-assertions") ||
+      !cmdline.isset("no-unwinding-assertions"));
+
   if(cmdline.isset("unwind"))
   {
     options.set_option("unwind", cmdline.get_value("unwind"));
-    if(!cmdline.isset("unwinding-assertions"))
+    if(!options.get_bool_option("unwinding-assertions"))
     {
       log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
                        "sound verification results"
@@ -229,7 +235,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option(
       "unwindset", cmdline.get_comma_separated_values("unwindset"));
-    if(!cmdline.isset("unwinding-assertions"))
+    if(!options.get_bool_option("unwinding-assertions"))
     {
       log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
                        "sound verification results"
@@ -258,10 +264,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("no-assumptions"))
     options.set_option("assumptions", false);
 
-  // generate unwinding assertions
-  if(cmdline.isset("unwinding-assertions"))
-    options.set_option("unwinding-assertions", true);
-
   // generate unwinding assumptions otherwise
   if(cmdline.isset("partial-loops"))
   {