jdiff: Remove processing of unsupported options

The options 1) tested for by the code, 2) documented in --help output,
and 3) actually supported in the cmdlinet configuration were
inconsistent. All supported options are now documented in the --help
output, and testing-for of unsupported options has been removed.

Also, uses of goto_functions preprocessing was cleaned up to match what
Java bytecode might actually need and use.

Author: tautschnig

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -24,13 +24,10 @@ Author: Peter Schrammel
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
-#include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 
@@ -71,89 +68,8 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 
-  if(cmdline.isset("mm"))
-    options.set_option("mm", cmdline.get_value("mm"));
-
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options);
-
-  if(cmdline.isset("debug-level"))
-    options.set_option("debug-level", cmdline.get_value("debug-level"));
-
-  if(cmdline.isset("unwindset"))
-    options.set_option("unwindset", cmdline.get_value("unwindset"));
-
-  // constant propagation
-  if(cmdline.isset("no-propagation"))
-    options.set_option("propagation", false);
-  else
-    options.set_option("propagation", true);
-
-  // check array bounds
-  if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
-  else
-    options.set_option("bounds-check", false);
-
-  // check division by zero
-  if(cmdline.isset("div-by-zero-check"))
-    options.set_option("div-by-zero-check", true);
-  else
-    options.set_option("div-by-zero-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
-  else
-    options.set_option("signed-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
-  else
-    options.set_option("unsigned-overflow-check", false);
-
-  // check overflow/underflow
-  if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
-  else
-    options.set_option("float-overflow-check", false);
-
-  // check for NaN (not a number)
-  if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
-  else
-    options.set_option("nan-check", false);
-
-  // check pointers
-  if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
-  else
-    options.set_option("pointer-check", false);
-
-  // check for memory leaks
-  if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
-  else
-    options.set_option("memory-leak-check", false);
-
-  // check assertions
-  if(cmdline.isset("no-assertions"))
-    options.set_option("assertions", false);
-  else
-    options.set_option("assertions", true);
-
-  // use assumptions
-  if(cmdline.isset("no-assumptions"))
-    options.set_option("assumptions", false);
-  else
-    options.set_option("assumptions", true);
-
-  // magic error label
-  if(cmdline.isset("error-label"))
-    options.set_option("error-label", cmdline.get_values("error-label"));
-
-  options.set_option("show-properties", cmdline.isset("show-properties"));
 }
 
 /// invoke main modules
@@ -270,11 +186,8 @@ bool jdiff_parse_optionst::process_goto_program(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // remove returns, gcc vectors, complex
+    // remove returns
     remove_returns(goto_model);
-    remove_vector(goto_model);
-    remove_complex(goto_model);
-    rewrite_union(goto_model);
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
@@ -286,16 +199,13 @@ bool jdiff_parse_optionst::process_goto_program(
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 
-    // add loop ids
-    goto_model.goto_functions.compute_loop_numbers();
-
-    // remove skips such that trivial GOTOs are deleted and not considered
-    // for coverage annotation:
-    remove_skip(goto_model);
-
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
+      // remove skips such that trivial GOTOs are deleted and not considered for
+      // coverage annotation:
+      remove_skip(goto_model);
+
       const auto cover_config =
         get_cover_config(options, goto_model.symbol_table, ui_message_handler);
       if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
@@ -311,7 +221,6 @@ bool jdiff_parse_optionst::process_goto_program(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   return false;
@@ -334,8 +243,7 @@ void jdiff_parse_optionst::help()
     "\n"
     "Diff options:\n"
     HELP_SHOW_GOTO_FUNCTIONS
-    HELP_SHOW_PROPERTIES
-    " --syntactic                  do syntactic diff (default)\n"
+    " --show-loops                 show the loops in the programs\n"
     " -u | --unified               output unified diff\n"
     " --change-impact | \n"
     "  --forward-impact |\n"

jbmc/src/jdiff/jdiff_parse_options.h

@@ -28,7 +28,7 @@ class goto_modelt;
 #define JDIFF_OPTIONS \
   "(json-ui)" \
   OPT_SHOW_GOTO_FUNCTIONS \
-  OPT_SHOW_PROPERTIES \
+  "(show-loops)" \
   OPT_GOTO_CHECK_JAVA \
   OPT_COVER \
   "(verbosity):(version)" \