Remove shadowing "options" from jdiff/goto_diff methods

As these inherit from language_uit, there is already an options member
available. Also do not make functions virtual unnecessarily, there is not
inheritance anywhere.

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -164,9 +164,9 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget
 
   virtual void register_languages();
 
-  virtual void get_command_line_options(optionst &options);
+  void get_command_line_options(optionst &options);
 
-  virtual bool process_goto_program(const optionst &options);
+  bool process_goto_program(const optionst &options);
   bool set_properties();
 
   virtual int perform_analysis(const optionst &options);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -81,7 +81,7 @@ ::jdiff_parse_optionst::jdiff_parse_optionst(
 {
 }
 
-void jdiff_parse_optionst::get_command_line_options(optionst &options)
+void jdiff_parse_optionst::get_command_line_options()
 {
   if(config.set(cmdline))
   {
@@ -200,8 +200,7 @@ int jdiff_parse_optionst::doit()
   // command line options
   //
 
-  optionst options;
-  get_command_line_options(options);
+  get_command_line_options();
   eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
@@ -220,10 +219,10 @@ int jdiff_parse_optionst::doit()
 
   goto_modelt goto_model1, goto_model2;
 
-  int get_goto_program_ret = get_goto_program(options, *this, goto_model1);
+  int get_goto_program_ret = get_goto_program(*this, goto_model1);
   if(get_goto_program_ret != -1)
     return get_goto_program_ret;
-  get_goto_program_ret = get_goto_program(options, languages2, goto_model2);
+  get_goto_program_ret = get_goto_program(languages2, goto_model2);
   if(get_goto_program_ret != -1)
     return get_goto_program_ret;
 
@@ -284,7 +283,6 @@ int jdiff_parse_optionst::doit()
 }
 
 int jdiff_parse_optionst::get_goto_program(
-  const optionst &options,
   jdiff_languagest &languages,
   goto_modelt &goto_model)
 {
@@ -327,7 +325,7 @@ int jdiff_parse_optionst::get_goto_program(
     goto_convert(
       goto_model.symbol_table, goto_model.goto_functions, ui_message_handler);
 
-    if(process_goto_program(options, goto_model))
+    if(process_goto_program(goto_model))
       return CPROVER_EXIT_INTERNAL_ERROR;
 
     // if we had a second argument then we will handle it next
@@ -338,9 +336,7 @@ int jdiff_parse_optionst::get_goto_program(
   return -1; // no error, continue
 }
 
-bool jdiff_parse_optionst::process_goto_program(
-  const optionst &options,
-  goto_modelt &goto_model)
+bool jdiff_parse_optionst::process_goto_program(goto_modelt &goto_model)
 {
   try
   {

jbmc/src/jdiff/jdiff_parse_options.h

@@ -59,15 +59,11 @@ class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest
   ui_message_handlert ui_message_handler;
   jdiff_languagest languages2;
 
-  virtual void get_command_line_options(optionst &options);
+  void get_command_line_options();
 
-  virtual int get_goto_program(
-    const optionst &options,
-    jdiff_languagest &languages,
-    goto_modelt &goto_model);
+  int get_goto_program(jdiff_languagest &languages, goto_modelt &goto_model);
 
-  virtual bool
-  process_goto_program(const optionst &options, goto_modelt &goto_model);
+  bool process_goto_program(goto_modelt &goto_model);
 
   void preprocessing();
 };

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -169,9 +169,9 @@ class goto_analyzer_parse_optionst:
 
   virtual void register_languages();
 
-  virtual void get_command_line_options(optionst &options);
+  void get_command_line_options(optionst &options);
 
-  virtual bool process_goto_program(const optionst &options);
+  bool process_goto_program(const optionst &options);
   bool set_properties();
 
   virtual int perform_analysis(const optionst &options);

src/goto-diff/goto_diff_languages.h

@@ -15,17 +15,25 @@ Author: Peter Schrammel
 #include <langapi/language_ui.h>
 #include <goto-programs/goto_model.h>
 
+#include <util/options.h>
+
 class goto_diff_languagest:public language_uit
 {
 public:
   explicit goto_diff_languagest(
     const cmdlinet &cmdline,
-    ui_message_handlert &ui_message_handler) :
-  language_uit(cmdline, ui_message_handler)
+    ui_message_handlert &ui_message_handler)
+    : language_uit(cmdline, ui_message_handler, new optionst)
   {
     register_languages();
   }
 
+  ~goto_diff_languagest()
+  {
+    delete options;
+    options = nullptr;
+  }
+
 protected:
   virtual void register_languages();
 };

src/goto-diff/goto_diff_parse_options.cpp

@@ -19,7 +19,6 @@ Author: Peter Schrammel
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
-#include <util/options.h>
 #include <util/version.h>
 
 #include <langapi/language.h>
@@ -79,7 +78,7 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst(
 {
 }
 
-void goto_diff_parse_optionst::get_command_line_options(optionst &options)
+void goto_diff_parse_optionst::get_command_line_options()
 {
   if(config.set(cmdline))
   {
@@ -88,16 +87,16 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   }
 
   if(cmdline.isset("program-only"))
-    options.set_option("program-only", true);
+    options->set_option("program-only", true);
 
   if(cmdline.isset("show-vcc"))
-    options.set_option("show-vcc", true);
+    options->set_option("show-vcc", true);
 
   if(cmdline.isset("cover"))
-    parse_cover_options(cmdline, options);
+    parse_cover_options(cmdline, *options);
 
   if(cmdline.isset("mm"))
-    options.set_option("mm", cmdline.get_value("mm"));
+    options->set_option("mm", cmdline.get_value("mm"));
 
   if(cmdline.isset("c89"))
     config.ansi_c.set_c89();
@@ -118,107 +117,107 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
     config.cpp.set_cpp11();
 
   // all checks supported by goto_check
-  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, (*options));
 
   if(cmdline.isset("debug-level"))
-    options.set_option("debug-level", cmdline.get_value("debug-level"));
+    options->set_option("debug-level", cmdline.get_value("debug-level"));
 
   if(cmdline.isset("slice-by-trace"))
-    options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
+    options->set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
 
   if(cmdline.isset("unwindset"))
-    options.set_option("unwindset", cmdline.get_value("unwindset"));
+    options->set_option("unwindset", cmdline.get_value("unwindset"));
 
   // constant propagation
   if(cmdline.isset("no-propagation"))
-    options.set_option("propagation", false);
+    options->set_option("propagation", false);
   else
-    options.set_option("propagation", true);
+    options->set_option("propagation", true);
 
   // check array bounds
   if(cmdline.isset("bounds-check"))
-    options.set_option("bounds-check", true);
+    options->set_option("bounds-check", true);
   else
-    options.set_option("bounds-check", false);
+    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);
+    options->set_option("div-by-zero-check", true);
   else
-    options.set_option("div-by-zero-check", false);
+    options->set_option("div-by-zero-check", false);
 
   // check overflow/underflow
   if(cmdline.isset("signed-overflow-check"))
-    options.set_option("signed-overflow-check", true);
+    options->set_option("signed-overflow-check", true);
   else
-    options.set_option("signed-overflow-check", false);
+    options->set_option("signed-overflow-check", false);
 
   // check overflow/underflow
   if(cmdline.isset("unsigned-overflow-check"))
-    options.set_option("unsigned-overflow-check", true);
+    options->set_option("unsigned-overflow-check", true);
   else
-    options.set_option("unsigned-overflow-check", false);
+    options->set_option("unsigned-overflow-check", false);
 
   // check overflow/underflow
   if(cmdline.isset("float-overflow-check"))
-    options.set_option("float-overflow-check", true);
+    options->set_option("float-overflow-check", true);
   else
-    options.set_option("float-overflow-check", false);
+    options->set_option("float-overflow-check", false);
 
   // check for NaN (not a number)
   if(cmdline.isset("nan-check"))
-    options.set_option("nan-check", true);
+    options->set_option("nan-check", true);
   else
-    options.set_option("nan-check", false);
+    options->set_option("nan-check", false);
 
   // check pointers
   if(cmdline.isset("pointer-check"))
-    options.set_option("pointer-check", true);
+    options->set_option("pointer-check", true);
   else
-    options.set_option("pointer-check", false);
+    options->set_option("pointer-check", false);
 
   // check for memory leaks
   if(cmdline.isset("memory-leak-check"))
-    options.set_option("memory-leak-check", true);
+    options->set_option("memory-leak-check", true);
   else
-    options.set_option("memory-leak-check", false);
+    options->set_option("memory-leak-check", false);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
-    options.set_option("assertions", false);
+    options->set_option("assertions", false);
   else
-    options.set_option("assertions", true);
+    options->set_option("assertions", true);
 
   // use assumptions
   if(cmdline.isset("no-assumptions"))
-    options.set_option("assumptions", false);
+    options->set_option("assumptions", false);
   else
-    options.set_option("assumptions", true);
+    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("error-label", cmdline.get_values("error-label"));
 
   // generate unwinding assertions
   if(cmdline.isset("cover"))
-    options.set_option("unwinding-assertions", false);
+    options->set_option("unwinding-assertions", false);
   else
-    options.set_option(
-      "unwinding-assertions",
-      cmdline.isset("unwinding-assertions"));
+    options->set_option(
+      "unwinding-assertions", cmdline.isset("unwinding-assertions"));
 
   // generate unwinding assumptions otherwise
-  options.set_option("partial-loops", cmdline.isset("partial-loops"));
+  options->set_option("partial-loops", cmdline.isset("partial-loops"));
 
-  if(options.get_bool_option("partial-loops") &&
-     options.get_bool_option("unwinding-assertions"))
+  if(
+    options->get_bool_option("partial-loops") &&
+    options->get_bool_option("unwinding-assertions"))
   {
     error() << "--partial-loops and --unwinding-assertions"
             << " must not be given together" << eom;
     exit(1);
   }
 
-  options.set_option("show-properties", cmdline.isset("show-properties"));
+  options->set_option("show-properties", cmdline.isset("show-properties"));
 }
 
 /// invoke main modules
@@ -234,8 +233,7 @@ int goto_diff_parse_optionst::doit()
   // command line options
   //
 
-  optionst options;
-  get_command_line_options(options);
+  get_command_line_options();
   eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
@@ -254,12 +252,10 @@ int goto_diff_parse_optionst::doit()
 
   goto_modelt goto_model1, goto_model2;
 
-  int get_goto_program_ret=
-    get_goto_program(options, *this, goto_model1);
+  int get_goto_program_ret = get_goto_program(*this, goto_model1);
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
-  get_goto_program_ret=
-    get_goto_program(options, languages2, goto_model2);
+  get_goto_program_ret = get_goto_program(languages2, goto_model2);
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
@@ -316,15 +312,14 @@ int goto_diff_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
+  syntactic_difft sd(goto_model1, goto_model2, *options, ui_message_handler);
   sd();
   sd.output_functions();
 
   return CPROVER_EXIT_SUCCESS;
 }
 
 int goto_diff_parse_optionst::get_goto_program(
-  const optionst &options,
   goto_diff_languagest &languages,
   goto_modelt &goto_model)
 {
@@ -371,7 +366,7 @@ int goto_diff_parse_optionst::get_goto_program(
       goto_model.goto_functions,
       ui_message_handler);
 
-    if(process_goto_program(options, goto_model))
+    if(process_goto_program(goto_model))
       return CPROVER_EXIT_INTERNAL_ERROR;
 
     // if we had a second argument then we will handle it next
@@ -382,9 +377,7 @@ int goto_diff_parse_optionst::get_goto_program(
   return -1; // no error, continue
 }
 
-bool goto_diff_parse_optionst::process_goto_program(
-  const optionst &options,
-  goto_modelt &goto_model)
+bool goto_diff_parse_optionst::process_goto_program(goto_modelt &goto_model)
 {
   try
   {
@@ -417,7 +410,7 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
-    goto_check(options, goto_model);
+    goto_check(*options, goto_model);
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);
@@ -435,7 +428,7 @@ bool goto_diff_parse_optionst::process_goto_program(
       // for coverage annotation:
       remove_skip(goto_model);
 
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
+      if(instrument_cover_goals(*options, goto_model, get_message_handler()))
         return true;
     }