goto-instrument/model_argc_argv: add new option: --add-cmd-line-arg

Author: vmihalko

src/goto-instrument/model_argc_argv.cpp

@@ -30,15 +30,23 @@ Date: April 2016
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-/// Set up argv with up to max_argc pointers into an array of 4096 bytes.
+/// Set up argv to user-specified values (when model_argv is FALSE) or
+/// (when model_argv is TRUE) set up argv with up to max_argc pointers
+/// into a char array of 4096 bytes.
+///
 /// \param goto_model: Contains the input program's symbol table and
 ///   intermediate representation
-/// \param max_argc: User-specified maximum number of arguments to be modelled
+/// \param argv_args: User-specified cmd-line arguments (ARGV),
+///   when model_argv is TRUE then size of argv_args represents
+///   the maximum number of arguments to be modelled
+/// \param model_argv: If set to TRUE then modelling argv with up to
+///   max_argc pointers
 /// \param message_handler: message logging
 /// \return True, if and only if modelling succeeded
 bool model_argc_argv(
   goto_modelt &goto_model,
-  unsigned max_argc,
+  const std::list<std::string> &argv_args,
+  bool model_argv,
   message_handlert &message_handler)
 {
   messaget message(message_handler);
@@ -83,25 +91,46 @@ bool model_argc_argv(
   // guaranteed by POSIX (_POSIX_ARG_MAX):
   // http://pubs.opengroup.org/onlinepubs/009695399/basedefs/limits.h.html
   std::ostringstream oss;
-  oss << "int ARGC;\n"
-      << "char *ARGV[1];\n"
-      << "void " << goto_model.goto_functions.entry_point() << "()\n"
-      << "{\n"
-      << "  unsigned next=0u;\n"
-      << "  " CPROVER_PREFIX "assume(ARGC>=1);\n"
-      << "  " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
-      << "  char arg_string[4096];\n"
-      << "  " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
-      << "  for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
-      << "  {\n"
-      << "    unsigned len;\n"
-      << "    " CPROVER_PREFIX "assume(len<4096);\n"
-      << "    " CPROVER_PREFIX "assume(next+len<4096);\n"
-      << "    " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
-      << "    ARGV[i]=&(arg_string[next]);\n"
-      << "    next+=len+1;\n"
-      << "  }\n"
-      << "}";
+  unsigned max_argc = argv_args.size();
+  unsigned argc = argv_args.size();
+
+  if(model_argv)
+  {
+    oss << "int ARGC;\n"
+        << "char *ARGV[1];\n"
+        << "void " << goto_model.goto_functions.entry_point() << "()\n"
+        << "{\n"
+        << "  unsigned next=0u;\n"
+        << "  " CPROVER_PREFIX "assume(ARGC>=1);\n"
+        << "  " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
+        << "  char arg_string[4096];\n"
+        << "  " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
+        << "  for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
+        << "  {\n"
+        << "    unsigned len;\n"
+        << "    " CPROVER_PREFIX "assume(len<4096);\n"
+        << "    " CPROVER_PREFIX "assume(next+len<4096);\n"
+        << "    " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
+        << "    ARGV[i]=&(arg_string[next]);\n"
+        << "    next+=len+1;\n"
+        << "  }\n"
+        << "}";
+  }
+  else
+  { // model_argv = false, set each argv[i] explicitly
+    oss << "int ARGC = " << argc << ";\n"
+        << "char *ARGV[" << argc << "];\n"
+        << "void " << goto_model.goto_functions.entry_point() << "()\n"
+        << "{\n";
+    int i = 0;
+    for(auto const &arg : argv_args)
+    {
+      oss << "ARGV[" << i << "]=\"" << arg << "\";\n";
+      i++;
+    }
+    oss << "}";
+  }
+
   std::istringstream iss(oss.str());
 
   ansi_c_languaget ansi_c_language;

src/goto-instrument/model_argc_argv.h

@@ -14,12 +14,23 @@ Date: April 2016
 #ifndef CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H
 #define CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H
 
+#include <list>
+#include <string>
+
 class goto_modelt;
 class message_handlert;
 
 bool model_argc_argv(
   goto_modelt &,
-  unsigned max_argc,
+  const std::list<std::string> &argv_args,
+  bool model_argv,
   message_handlert &);
 
+#define OPT_ARGC_ARGV "(model-argc-argv):(add-cmd-line-arg):"
+
+#define HELP_ARGC_ARGV                                                         \
+  " --model-argc-argv <n>        model up to <n> command line arguments\n"     \
+  " --add-cmd-line-arg <arg>     add command line argument (may be "           \
+  "repeated)\n"
+
 #endif // CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H