goto_instrt_parse_options, util/cmdline: refactor

src/goto-instrument/goto_instrument_parse_options: add
--add-cmd-line-arg option, refactor code around.

src/util/cmdline: refactor, do not interpret every "--{string}" as
option for CBMC.

Author: vmihalko

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 #include <memory>
+#include <sstream>
 
 #include <util/config.h>
 #include <util/exception_utils.h>
@@ -93,7 +94,6 @@ Author: Daniel Kroening, [email protected]
 #include "interrupt.h"
 #include "k_induction.h"
 #include "mmio.h"
-#include "model_argc_argv.h"
 #include "nondet_static.h"
 #include "nondet_volatile.h"
 #include "points_to.h"
@@ -1050,10 +1050,38 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     unsigned max_argc=
       safe_string2unsigned(cmdline.get_value("model-argc-argv"));
+    std::list<std::string> argv;
+    argv.resize(max_argc);
 
     log.status() << "Adding up to " << max_argc << " command line arguments"
                  << messaget::eom;
-    if(model_argc_argv(goto_model, max_argc, ui_message_handler))
+
+    if(model_argc_argv(
+         goto_model, argv, true /*model_argv*/, ui_message_handler))
+      throw 0;
+  }
+
+  if(cmdline.isset("add-cmd-line-arg"))
+  {
+    const std::list<std::string> &argv = cmdline.get_values("add-cmd-line-arg");
+    unsigned argc = 0;
+
+    std::stringstream ss;
+    ss << "[";
+    std::string sep = "";
+    for(auto const &arg : argv)
+    {
+      ss << sep << "\"" << arg << "\"";
+      argc++;
+      sep = ", ";
+    }
+    ss << "]";
+
+    log.status() << "Adding " << argc << " arguments: " << ss.str()
+                 << messaget::eom;
+
+    if(model_argc_argv(
+         goto_model, argv, false /*model_argv*/, ui_message_handler))
       throw 0;
   }
 
@@ -1827,7 +1855,8 @@ void goto_instrument_parse_optionst::help()
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS
     " --add-library                add models of C library functions\n"
-    " --model-argc-argv <n>        model up to <n> command line arguments\n"
+    HELP_CONFIG_LIBRARY
+    HELP_ARGC_ARGV
     // NOLINTNEXTLINE(whitespace/line_length)
     " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
     HELP_REPLACE_CALLS

src/goto-instrument/goto_instrument_parse_options.h

@@ -38,6 +38,7 @@ Author: Daniel Kroening, [email protected]
 #include "dump_c.h"
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
+#include "model_argc_argv.h"
 #include "nondet_volatile.h"
 #include "replace_calls.h"
 #include "uninitialized.h"
@@ -93,7 +94,8 @@ Author: Daniel Kroening, [email protected]
   "(interpreter)(show-reaching-definitions)" \
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
-  "(horn)(skip-loops):(model-argc-argv):" \
+  "(horn)(skip-loops):" \
+  OPT_ARGC_ARGV \
   "(" FLAG_LOOP_CONTRACTS ")" \
   "(" FLAG_REPLACE_CALL "):" \
   "(" FLAG_ENFORCE_CONTRACT "):" \

src/util/cmdline.cpp

@@ -305,7 +305,7 @@ bool cmdlinet::parse_arguments(int argc, const char **argv)
           i++;
           if(i == argc)
             return true;
-          if(argv[i][0] == '-' && argv[i][1] != 0)
+          if(options[*optnr].optstring != "add-cmd-line-arg" && argv[i][0] == '-' && argv[i][1] != 0)
             return true;
           options[*optnr].values.push_back(argv[i]);
         }