jdiff: Remove processing of unsupported options

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,88 +68,9 @@ 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"));
 }
 
@@ -247,73 +165,64 @@ bool jdiff_parse_optionst::process_goto_program(
   const optionst &options,
   goto_modelt &goto_model)
 {
-  {
-    // remove function pointers
-    log.status() << "Removing function pointers and virtual functions"
-                 << messaget::eom;
-    remove_function_pointers(
-      ui_message_handler, goto_model, cmdline.isset("pointer-check"));
+  // remove function pointers
+  log.status() << "Removing function pointers and virtual functions"
+               << messaget::eom;
+  remove_function_pointers(
+    ui_message_handler, goto_model, cmdline.isset("pointer-check"));
 
-    // Java virtual functions -> explicit dispatch tables:
-    remove_virtual_functions(goto_model);
+  // Java virtual functions -> explicit dispatch tables:
+  remove_virtual_functions(goto_model);
 
-    // remove Java throw and catch
-    // This introduces instanceof, so order is important:
-    remove_exceptions_using_instanceof(goto_model, ui_message_handler);
+  // remove Java throw and catch
+  // This introduces instanceof, so order is important:
+  remove_exceptions_using_instanceof(goto_model, ui_message_handler);
 
-    // Java instanceof -> clsid comparison:
-    class_hierarchyt class_hierarchy(goto_model.symbol_table);
-    remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
+  // Java instanceof -> clsid comparison:
+  class_hierarchyt class_hierarchy(goto_model.symbol_table);
+  remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
 
-    mm_io(goto_model);
+  mm_io(goto_model);
 
-    // instrument library preconditions
-    instrument_preconditions(goto_model);
+  // instrument library preconditions
+  instrument_preconditions(goto_model);
 
-    // remove returns, gcc vectors, complex
-    remove_returns(goto_model);
-    remove_vector(goto_model);
-    remove_complex(goto_model);
-    rewrite_union(goto_model);
+  // remove returns
+  remove_returns(goto_model);
 
-    // add generic checks
-    log.status() << "Generic Property Instrumentation" << messaget::eom;
-    goto_check_java(options, goto_model, ui_message_handler);
+  // add generic checks
+  log.status() << "Generic Property Instrumentation" << messaget::eom;
+  goto_check_java(options, goto_model, ui_message_handler);
 
-    // checks don't know about adjusted float expressions
-    adjust_float_expressions(goto_model);
+  // checks don't know about adjusted float expressions
+  adjust_float_expressions(goto_model);
 
-    // recalculate numbers, etc.
-    goto_model.goto_functions.update();
+  // 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:
+  // 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);
 
-    // instrument cover goals
-    if(cmdline.isset("cover"))
-    {
-      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))
-        return true;
-    }
-
-    // label the assertions
-    // This must be done after adding assertions and
-    // before using the argument of the "property" option.
-    // Do not re-label after using the property slicer because
-    // this would cause the property identifiers to change.
-    label_properties(goto_model);
-
-    // remove any skips introduced since coverage instrumentation
-    remove_skip(goto_model);
-    goto_model.goto_functions.update();
+    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))
+      return true;
   }
 
+  // label the assertions
+  // This must be done after adding assertions and
+  // before using the argument of the "property" option.
+  // Do not re-label after using the property slicer because
+  // this would cause the property identifiers to change.
+  label_properties(goto_model);
+
+  // remove any skips introduced since coverage instrumentation
+  remove_skip(goto_model);
+
   return false;
 }
 
@@ -335,7 +244,7 @@ void jdiff_parse_optionst::help()
     "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

@@ -29,6 +29,7 @@ class goto_modelt;
   "(json-ui)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
+  "(show-loops)" \
   OPT_GOTO_CHECK_JAVA \
   OPT_COVER \
   "(verbosity):(version)" \

src/goto-diff/goto_diff_parse_options.cpp

@@ -64,6 +64,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
+  options.set_option("show-properties", cmdline.isset("show-properties"));
+
   // Options for process_goto_program
   options.set_option("rewrite-union", true);
 }
@@ -224,6 +226,7 @@ void goto_diff_parse_optionst::help()
     "\n"
     "Diff options:\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    HELP_SHOW_PROPERTIES
     " --show-loops                 show the loops in the programs\n"
     " -u | --unified               output unified diff\n"
     " --change-impact | \n"

src/goto-diff/goto_diff_parse_options.h

@@ -30,6 +30,7 @@ class optionst;
 #define GOTO_DIFF_OPTIONS \
   "(json-ui)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(show-loops)" \
   OPT_GOTO_CHECK \
   OPT_COVER \