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-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/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$

jbmc/regression/jbmc/lvt-groovy/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 DetectSplitPackagesTask.class
---show-symbol-table
+--show-symbol-table --no-lazy-methods --no-refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/provide_object_implementation/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 java/lang/Object.class
-
+--no-lazy-methods
 ^EXIT=6$
 ^SIGNAL=0$
 ^the program has no entry point$

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -45,7 +45,7 @@ Author: Daniel Kroening, [email protected]
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
-  string_refinement_enabled=cmd.isset("refine-strings");
+  string_refinement_enabled = !cmd.isset("no-refine-strings");
   throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
   assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check");
   throw_assertion_error = cmd.isset("throw-assertion-error");
@@ -69,7 +69,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
   if(cmd.isset("symex-driven-lazy-loading"))
     lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER;
-  else if(cmd.isset("lazy-methods"))
+  else if(!cmd.isset("no-lazy-methods"))
     lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;