goto-instrument/argc-argv2: add test case for new --add-cmd-line-arg

option

Author: vmihalko

regression/goto-instrument/argc-argv2/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  if(argc >= 2)
+  {
+    assert(argv[0][0] == 'A');
+    assert(argv[1][0] == 'B');
+  }
+
+  return 0;
+}

regression/goto-instrument/argc-argv2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--add-cmd-line-arg A --add-cmd-line-arg B
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/argc-argv2/test2.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--model-argc-argv 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1060,32 +1060,32 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     log.status() << "Adding up to " << max_argc << " command line arguments"
                  << messaget::eom;
 
-    if(model_argc_argv(goto_model, argv, true /*model_argv*/,
-			    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 = ", ";
+    for(auto const &arg : argv)
+    {
+      ss << sep << "\"" << arg << "\"";
+      argc++;
+      sep = ", ";
     }
     ss << "]";
 
     log.status() << "Adding " << argc << " arguments: " << ss.str()
-	    << messaget::eom;
+                 << messaget::eom;
 
-    if(model_argc_argv(goto_model, argv, false /*model_argv*/,
-			    ui_message_handler))
+    if(model_argc_argv(
+         goto_model, argv, false /*model_argv*/, ui_message_handler))
       throw 0;
   }
 

src/goto-instrument/goto_instrument_parse_options.h

@@ -32,8 +32,8 @@ Author: Daniel Kroening, [email protected]
 #include "contracts/contracts.h"
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
-#include "nondet_volatile.h"
 #include "model_argc_argv.h"
+#include "nondet_volatile.h"
 #include "replace_calls.h"
 
 #include "count_eloc.h"

src/goto-instrument/model_argc_argv.cpp

@@ -94,7 +94,8 @@ bool model_argc_argv(
   unsigned max_argc = argv_args.size();
   unsigned argc = argv_args.size();
 
-  if ( model_argv ) {
+  if(model_argv)
+  {
     oss << "int ARGC;\n"
         << "char *ARGV[1];\n"
         << "void " << goto_model.goto_functions.entry_point() << "()\n"
@@ -114,18 +115,21 @@ bool model_argc_argv(
         << "    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 << "}";
+  }
+  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());
 

src/goto-instrument/model_argc_argv.h

@@ -28,8 +28,9 @@ bool model_argc_argv(
 
 #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"
+#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