Merge pull request #3518 from peterschrammel/no-cmdline-in-goto-model

Remove cmdlinet from init/lazy_goto_model

Author: peterschrammel

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -77,6 +77,9 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("function"))
+    options.set_option("function", cmdline.get_value("function"));
+
   parse_java_language_options(cmdline, options);
 
   // check assertions
@@ -352,7 +355,8 @@ int janalyzer_parse_optionst::doit()
 
   try
   {
-    goto_model = initialize_goto_model(cmdline, get_message_handler(), options);
+    goto_model =
+      initialize_goto_model(cmdline.args, get_message_handler(), options);
   }
 
   catch(const char *e)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -108,6 +108,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   jbmc_parse_optionst::set_default_options(options);
+
+  if(cmdline.isset("function"))
+    options.set_option("function", cmdline.get_value("function"));
+
   parse_java_language_options(cmdline, options);
   parse_java_object_factory_options(cmdline, options);
 
@@ -550,7 +554,7 @@ int jbmc_parse_optionst::doit()
     // Use symex-driven lazy loading:
     lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
       *this, options, get_message_handler());
-    lazy_goto_model.initialize(cmdline, options);
+    lazy_goto_model.initialize(cmdline.args, options);
 
     class_hierarchy =
       util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
@@ -630,7 +634,7 @@ int jbmc_parse_optionst::get_goto_program(
   {
     lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
       *this, options, get_message_handler());
-    lazy_goto_model.initialize(cmdline, options);
+    lazy_goto_model.initialize(cmdline.args, options);
 
     class_hierarchy =
       util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -172,20 +172,18 @@ SCENARIO("test_value_set_analysis",
   {
     config.set_arch("none");
     config.main = "";
-    cmdlinet command_line;
 
     // This classpath is the default, but the config object
     // is global and previous unit tests may have altered it
-    command_line.set("java-cp-include-files", "CustomVSATest.class");
     config.java.classpath={"."};
-    command_line.args.push_back("pointer-analysis/CustomVSATest.jar");
 
-    register_language(new_java_bytecode_language);
     optionst options;
-    parse_java_language_options(command_line, options);
+    options.set_option("java-cp-include-files", "CustomVSATest.class");
+
+    register_language(new_java_bytecode_language);
 
-    goto_modelt goto_model =
-      initialize_goto_model(command_line, null_message_handler, options);
+    goto_modelt goto_model = initialize_goto_model(
+      {"pointer-analysis/CustomVSATest.jar"}, null_message_handler, options);
 
     null_message_handlert message_handler;
     remove_java_new(goto_model, message_handler);

src/cbmc/cbmc_parse_options.cpp

@@ -111,6 +111,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   cbmc_parse_optionst::set_default_options(options);
   parse_c_object_factory_options(cmdline, options);
 
+  if(cmdline.isset("function"))
+    options.set_option("function", cmdline.get_value("function"));
+
   if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
   {
     error() << "--cover and --unwinding-assertions must not be given together"
@@ -403,6 +406,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("validate-ssa-equation", true);
   }
 
+  if(cmdline.isset("validate-goto-model"))
+  {
+    options.set_option("validate-goto-model", true);
+  }
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 
@@ -594,7 +602,8 @@ int cbmc_parse_optionst::get_goto_program(
 
   try
   {
-    goto_model = initialize_goto_model(cmdline, ui_message_handler, options);
+    goto_model =
+      initialize_goto_model(cmdline.args, ui_message_handler, options);
 
     if(cmdline.isset("show-symbol-table"))
     {

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -88,7 +88,10 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
-  #if 0
+  if(cmdline.isset("function"))
+    options.set_option("function", cmdline.get_value("function"));
+
+#if 0
   if(cmdline.isset("c89"))
     config.ansi_c.set_c89();
 
@@ -106,9 +109,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("cpp11"))
     config.cpp.set_cpp11();
-  #endif
+#endif
 
-  #if 0
+#if 0
   // check assertions
   if(cmdline.isset("no-assertions"))
     options.set_option("assertions", false);
@@ -124,7 +127,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   // magic error label
   if(cmdline.isset("error-label"))
     options.set_option("error-label", cmdline.get_values("error-label"));
-  #endif
+#endif
 
   // Select a specific analysis
   if(cmdline.isset("taint"))
@@ -298,6 +301,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       }
     }
   }
+
+  if(cmdline.isset("validate-goto-model"))
+  {
+    options.set_option("validate-goto-model", true);
+  }
 }
 
 /// For the task, build the appropriate kind of analyzer
@@ -390,7 +398,8 @@ int goto_analyzer_parse_optionst::doit()
 
   try
   {
-    goto_model = initialize_goto_model(cmdline, get_message_handler(), options);
+    goto_model =
+      initialize_goto_model(cmdline.args, get_message_handler(), options);
   }
 
   catch(const char *e)

src/goto-programs/initialize_goto_model.cpp

@@ -14,10 +14,10 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 
-#include <util/cmdline.h>
 #include <util/config.h>
 #include <util/message.h>
 #include <util/object_factory_parameters.h>
+#include <util/options.h>
 #include <util/unicode.h>
 
 #include <langapi/mode.h>
@@ -30,12 +30,11 @@ Author: Daniel Kroening, [email protected]
 #include "read_goto_binary.h"
 
 goto_modelt initialize_goto_model(
-  const cmdlinet &cmdline,
+  const std::vector<std::string> &files,
   message_handlert &message_handler,
   const optionst &options)
 {
   messaget msg(message_handler);
-  const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
     throw invalid_command_line_argument_exceptiont(
@@ -124,7 +123,7 @@ goto_modelt initialize_goto_model(
 
   bool entry_point_generation_failed=false;
 
-  if(binaries_provided_start && cmdline.isset("function"))
+  if(binaries_provided_start && options.is_set("function"))
   {
     // Rebuild the entry-point, using the language annotation of the
     // existing __CPROVER_start function:
@@ -139,7 +138,7 @@ goto_modelt initialize_goto_model(
     if(binaries.empty())
     {
       // Enable/disable stub generation for opaque methods
-      bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
+      bool stubs_enabled = options.is_set("generate-opaque-stubs");
       language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
     }
 
@@ -166,7 +165,7 @@ goto_modelt initialize_goto_model(
     goto_model.goto_functions,
     message_handler);
 
-  if(cmdline.isset("validate-goto-model"))
+  if(options.is_set("validate-goto-model"))
   {
     goto_model.validate(validation_modet::EXCEPTION);
   }

src/goto-programs/initialize_goto_model.h

@@ -14,12 +14,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_model.h"
 
-class cmdlinet;
 class message_handlert;
 class optionst;
 
 goto_modelt initialize_goto_model(
-  const cmdlinet &cmdline,
+  const std::vector<std::string> &files,
   message_handlert &message_handler,
   const optionst &options);
 

src/goto-programs/lazy_goto_model.cpp

@@ -9,10 +9,10 @@
 
 #include <langapi/mode.h>
 
-#include <util/cmdline.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
+#include <util/options.h>
 #include <util/unicode.h>
 
 #include <langapi/language.h>
@@ -105,16 +105,14 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
 /// language implements `languaget::convert_lazy_method`; any method not handled
 /// there must be populated eagerly. See `lazy_goto_modelt::get_goto_function`
 /// for more detail.
-/// \param cmdline: command-line arguments specifying source files and GOTO
-///   binaries to load
+/// \param files: source files and GOTO binaries to load
 /// \param options: options to pass on to the language front-ends
 void lazy_goto_modelt::initialize(
-  const cmdlinet &cmdline,
+  const std::vector<std::string> &files,
   const optionst &options)
 {
   messaget msg(message_handler);
 
-  const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
     throw invalid_command_line_argument_exceptiont(
@@ -201,7 +199,7 @@ void lazy_goto_modelt::initialize(
 
   bool entry_point_generation_failed=false;
 
-  if(binaries_provided_start && cmdline.isset("function"))
+  if(binaries_provided_start && options.is_set("function"))
   {
     // Rebuild the entry-point, using the language annotation of the
     // existing __CPROVER_start function:
@@ -216,7 +214,7 @@ void lazy_goto_modelt::initialize(
     if(binaries.empty())
     {
       // Enable/disable stub generation for opaque methods
-      bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
+      bool stubs_enabled = options.is_set("generate-opaque-stubs");
       language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
     }
 

src/goto-programs/lazy_goto_model.h

@@ -13,7 +13,6 @@
 #include "lazy_goto_functions_map.h"
 #include "goto_convert_functions.h"
 
-class cmdlinet;
 class optionst;
 
 /// A GOTO model that produces function bodies on demand. It owns a
@@ -28,7 +27,7 @@ class optionst;
 /// The typical use case looks like:
 ///
 ///     lazy_goto_modelt model(...callback parameters...);
-///     model.initialize(cmdline, options);
+///     model.initialize(cmdline.args, options);
 ///     model.get_goto_function("needed_function1")
 ///     model.get_goto_function("needed_function2");
 ///     ...
@@ -179,7 +178,8 @@ class lazy_goto_modelt : public abstract_goto_modelt
       message_handler);
   }
 
-  void initialize(const cmdlinet &cmdline, const optionst &options);
+  void
+  initialize(const std::vector<std::string> &files, const optionst &options);
 
   /// Eagerly loads all functions from the symbol table.
   void load_all_functions() const;

src/langapi/language_ui.cpp

@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 #include <iostream>
 
-#include <util/namespace.h>
 #include <util/cmdline.h>
 #include <util/config.h>
+#include <util/namespace.h>
+#include <util/options.h>
 #include <util/unicode.h>
 
 #include "language.h"
@@ -112,8 +113,12 @@ bool language_uit::final()
 {
   language_files.set_message_handler(*message_handler);
 
+  // TODO: This should be moved elsewhere because it is not used in
+  //       this repository.
   // Enable/disable stub generation for opaque methods
-  bool stubs_enabled=_cmdline.isset("generate-opaque-stubs");
+  bool stubs_enabled = false;
+  if(options != nullptr)
+    stubs_enabled = options->is_set("generate-opaque-stubs");
   language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
 
   if(language_files.final(symbol_table))