Properly separate gcc from non-gcc options to avoid repeated special case

Previously, any new non-gcc option (such as verbosity, native-compiler, etc
required handling this option in more than one place). This is no longer
necessary and instead testing for them via cmdline.get_value/cmdline.isset
suffices.

Author: Michael Tautschnig

src/goto-cc/gcc_cmdline.cpp

@@ -27,6 +27,40 @@ Function: gcc_cmdlinet::parse
 
 \*******************************************************************/
 
+// non-gcc options
+const char *goto_cc_options_with_separated_argument[]=
+{
+  "--verbosity",
+  "--function",
+  "--native-compiler",
+  "--native-linker",
+  "--print-rejected-preprocessed-source",
+  NULL
+};
+
+// non-gcc options
+const char *goto_cc_options_without_argument[]=
+{
+  "--show-symbol-table",
+  "--show-function-table",
+  "--ppc-macos",
+  "--i386-linux",
+  "--i386-win32",
+  "--i386-macos",
+  "--winx64",
+  "--string-abstraction",
+  "--no-library",
+  "--16",
+  "--32",
+  "--64",
+  "--little-endian",
+  "--big-endian",
+  "--no-arch",
+  "--partial-inlining",
+  "-?",
+  NULL
+};
+
 // separated or concatenated
 const char *gcc_options_with_argument[]=
 {
@@ -51,11 +85,6 @@ const char *gcc_options_with_argument[]=
 
 const char *gcc_options_with_separated_argument[]=
 {
-  "--verbosity", // non-gcc
-  "--function",  // non-gcc
-  "--native-compiler", // non-gcc
-  "--native-linker", // non-gcc
-  "--print-rejected-preprocessed-source", // non-gcc
   "-aux-info",
   "--param", // Apple only
   "-imacros",
@@ -94,25 +123,8 @@ const char *gcc_options_with_concatenated_argument[]=
 
 const char *gcc_options_without_argument[]=
 {
-  "--show-symbol-table", // NON-GCC
-  "--show-function-table", // NON-GCC
-  "--ppc-macos", // NON-GCC
-  "--i386-linux", // NON-GCC
-  "--i386-win32", // NON-GCC
-  "--i386-macos", // NON-GCC
-  "--winx64", // NON_GCC
-  "--string-abstraction", // NON-GCC
-  "--no-library", // NON-GCC
-  "--16", // NON-GCC
-  "--32", // NON-GCC
-  "--64", // NON-GCC
-  "--little-endian", // NON-GCC
-  "--big-endian", // NON-GCC
-  "--no-arch", // NON-GCC
-  "--partial-inlining", // NON-GCC
+  "--help",
   "-h",
-  "--help", // NON-GCC
-  "-?", // NON-GCC
   "-r", // for ld mimicking
   "-dylib", // for ld mimicking on MacOS
   "-c",
@@ -261,14 +273,55 @@ bool gcc_cmdlinet::parse_arguments(
     // file?
     if(argv_i=="-" || !has_prefix(argv_i, "-"))
     {
-      if(!spec_file)
+      if(!in_spec_file)
         add_infile_arg(argv_i);
       continue;
     }
 
-    // add to new_argv
-    if(!spec_file)
+    if(!in_spec_file)
+    {
+      argst::const_iterator next=it;
+      ++next;
+
+      bool found=false;
+
+      if(in_list(argv_i.c_str(),
+                 goto_cc_options_without_argument)) // without argument
+      {
+        set(argv_i);
+        found=true;
+      }
+
+      // separated only, and also allow concatenation with "="
+      for(const char **o=goto_cc_options_with_separated_argument;
+          *o!=NULL && !found;
+          ++o)
+      {
+        if(argv_i==*o) // separated
+        {
+          found=true;
+          if(next!=args.end())
+          {
+            set(argv_i, *next);
+            ++it;
+          }
+          else
+            set(argv_i, "");
+        }
+        // concatenated with "="
+        else if(has_prefix(argv_i, std::string(*o)+"="))
+        {
+          found=true;
+          set(*o, argv_i.substr(strlen(*o)+1));
+        }
+      }
+
+      if(found)
+        continue;
+
+      // add to new_argv
       add_arg(argv_i);
+    }
 
     // also store in cmdlinet
 

src/goto-cc/gcc_mode.cpp

@@ -565,20 +565,6 @@ int gcc_modet::preprocess(
     {
       // ignore
     }
-    else if(it->arg=="--function" ||
-            it->arg=="--verbosity" ||
-            it->arg=="--native-linker" ||
-            it->arg=="--print-rejected-preprocessed-source")
-    {
-      // ignore here
-      skip_next=true;
-    }
-    else if(it->arg=="--native-compiler")
-    {
-      ++it;
-      assert(it!=cmdline.parsed_argv.end());
-      compiler=it->arg.c_str();
-    }
     else
       new_argv.push_back(it->arg);
   }
@@ -634,10 +620,13 @@ Function: gcc_modet::run_gcc
 
 int gcc_modet::run_gcc()
 {
-  // build new argv
-  std::vector<std::string> new_argv(1);
+  assert(!cmdline.parsed_argv.empty());
 
+  // build new argv
+  std::vector<std::string> new_argv;
   new_argv.reserve(cmdline.parsed_argv.size());
+  for(const auto &a : cmdline.parsed_argv)
+    new_argv.push_back(a.arg);
 
   // overwrite argv[0]
   new_argv[0]=native_tool_name;

src/goto-cc/ld_cmdline.cpp

@@ -25,6 +25,14 @@ Function: ld_cmdlinet::parse
 
 \*******************************************************************/
 
+const char *goto_ld_options_with_argument[]=
+{
+  "--verbosity",
+  "--native-compiler",
+  "--native-linker",
+  NULL
+};
+
 const char *ld_options_with_argument[]=
 {
   "-a",
@@ -93,7 +101,6 @@ const char *ld_options_with_argument[]=
   "--wrap",
   "--hash-style",
   "-z",
-  "--verbosity", // non-ld
   "--arch", // Apple only
   "--ios_version_min", // Apple only
   "--macosx_version_min", // Apple only
@@ -258,13 +265,46 @@ bool ld_cmdlinet::parse(int argc, const char **argv)
       continue;
     }
 
+    bool found=false;
+
+    for(const char **o=goto_ld_options_with_argument;
+        *o!=NULL && !found;
+        ++o)
+    {
+      std::string os(*o);
+
+      // separated?
+      if(argv_i==os ||
+         (os.size()>=3 && os[0]=='-' && os[1]=='-' && "-"+argv_i==os))
+      {
+        found=true;
+        if(i!=argc-1)
+        {
+          set(os, argv[i+1]);
+          i++;
+        }
+        else
+        {
+          std::cerr << "Warning: missing argument for " << argv_i << std::endl;
+          set(os, ""); // end of command line
+        }
+      }
+      else if(os.size()>2 && has_prefix(argv_i, os+"=")) // concatenated, long
+      {
+        found=true;
+        set(os, argv[i]+os.size()+1);
+      }
+    }
+
+    // goto-ld-only command line argument found
+    if(found)
+      continue;
+
     // add to new_argv
     add_arg(argv_i);
 
     // also store in cmdlinet
 
-    bool found=false;
-
     for(const char **o=ld_options_without_argument; *o!=NULL && !found; o++)
     {
       std::string os(*o);