Make --lazy-methods and --refine-strings default

These options are always required in practical
use cases. They can be disabled with --no-lazy-methods
and --no-refine-strings if needed for regression tests.

Author: peterschrammel

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

@@ -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 . ../../../src/java_bytecode/library/core-models.jar` --no-refine-strings --no-lazy-methods
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

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

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check --refine-strings --string-max-length 100
+--function Test.check --refine-strings --string-max-input-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 11 .* SUCCESS$

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

@@ -3,4 +3,4 @@ Test.class
 --refine-strings --function Test.test --cover location --trace --json-ui
 ^EXIT=0$
 ^SIGNAL=0$
-20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)
+20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)

jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc

@@ -1,6 +1,6 @@
 CORE
 annotations.class
---verbosity 10 --show-symbol-table --function annotations.main
+--no-lazy-methods --verbosity 10 --show-symbol-table --function annotations.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations

jbmc/regression/jbmc/coreModels/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
+--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$

jbmc/regression/jbmc/generic_class_bound1/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Gn.class
---cover location
+--cover location --no-lazy-methods --no-refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 .*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED

jbmc/regression/jbmc/lambda2/test_no_crash.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 SymStream.class
---verbosity 10 --show-goto-functions
+--no-lazy-methods --verbosity 10 --show-goto-functions
 ^EXIT=0
 ^SIGNAL=0
 --

jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
 ^EXIT=0$

jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)

jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
 ^EXIT=0$