jdiff: cleanup command-line options

Remove no-refine-strings, which is no longer processed anywhere. Cleanup
handling of no-lazy-methods to do it centrally instead of making each
front-end do its own handling. Remove java options from help output as
those aren't actually accepted by jdiff.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -109,6 +109,8 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
   }
   options.set_option(
     "java-lift-clinit-calls", cmd.isset("java-lift-clinit-calls"));
+
+  options.set_option("lazy-methods", !cmd.isset("no-lazy-methods"));
 }
 
 prefix_filtert get_context(const optionst &options)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -94,7 +94,6 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("assertions", true);
   options.set_option("assumptions", true);
   options.set_option("built-in-assertions", true);
-  options.set_option("lazy-methods", true);
   options.set_option("propagation", true);
   options.set_option("refine-strings", true);
   options.set_option("simple-slice", true);
@@ -304,9 +303,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
 
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
-  if(cmdline.isset("no-lazy-methods"))
-    options.set_option("lazy-methods", false);
-
   if(cmdline.isset("symex-driven-lazy-loading"))
   {
     options.set_option("symex-driven-lazy-loading", true);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -58,11 +58,6 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
     exit(1);
   }
 
-  // TODO: improve this when language front ends have been
-  //   disentangled from command line parsing
-  // we always require these options
-  cmdline.set("no-lazy-methods");
-  cmdline.set("no-refine-strings");
   parse_java_language_options(cmdline, options);
 
   // check assertions
@@ -263,11 +258,10 @@ void jdiff_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     HELP_COVER
-    "Java Bytecode frontend options:\n"
-    JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
     "Other options:\n"
     " --version                    show version and exit\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
     "\n";
   // clang-format on

jbmc/src/jdiff/jdiff_parse_options.h

@@ -31,8 +31,6 @@ class goto_modelt;
   "(no-assertions)(no-assumptions)" \
   OPT_COVER \
   "(verbosity):(version)" \
-  "(no-lazy-methods)" /* should go away */ \
-  "(no-refine-strings)" /* should go away */ \
   OPT_TIMESTAMP \
   "u(unified)(change-impact)(forward-impact)(backward-impact)" \
   "(compact-output)"

jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -170,7 +170,6 @@ symbol_tablet load_java_class(
 {
   free_form_cmdlinet command_line;
   command_line.add_flag("no-lazy-methods");
-  command_line.add_flag("no-refine-strings");
   return load_java_class(
     java_class_name, class_path, main, std::move(java_lang), command_line);
 }
@@ -203,9 +202,5 @@ goto_modelt load_goto_model_from_java_class(
   const std::string &main)
 {
   return load_goto_model_from_java_class(
-    java_class_name,
-    class_path,
-    {"no-lazy-methods", "no-refine-strings"},
-    {},
-    main);
+    java_class_name, class_path, {"no-lazy-methods"}, {}, main);
 }

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

@@ -173,7 +173,6 @@ SCENARIO(
     {
       free_form_cmdlinet command_line;
       command_line.add_flag("no-lazy-methods");
-      command_line.add_flag("no-refine-strings");
       test_java_bytecode_languaget language;
       language.set_message_handler(null_message_handler);
       optionst options;