Merge pull request #1244 from tautschnig/goto-gcc-at-fix

goto-gcc: Add @<file> arguments to the original command line

Author: Daniel Kroening

regression/goto-gcc/at_files/args

@@ -0,0 +1 @@
+other.c

regression/goto-gcc/at_files/main.c

@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  return foo();
+}

regression/goto-gcc/at_files/other.c

@@ -0,0 +1,4 @@
+int foo()
+{
+  return 1;
+}

regression/goto-gcc/at_files/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+@args
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/goto-cc/gcc_cmdline.cpp

@@ -256,7 +256,7 @@ bool gcc_cmdlinet::parse_arguments(
         line.erase(0, line.find_first_not_of("\t "));
 
         if(!line.empty())
-          parse_specs_line(line);
+          parse_specs_line(line, false);
       }
 
       continue;
@@ -432,7 +432,7 @@ bool gcc_cmdlinet::parse_arguments(
 }
 
 /// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
-void gcc_cmdlinet::parse_specs_line(const std::string &line)
+void gcc_cmdlinet::parse_specs_line(const std::string &line, bool in_spec_file)
 {
   // initial whitespace has been stripped
   assert(!line.empty());
@@ -448,7 +448,7 @@ void gcc_cmdlinet::parse_specs_line(const std::string &line)
     args.push_back(line.substr(arg_start, arg_end-arg_start));
   }
 
-  parse_arguments(args, true);
+  parse_arguments(args, in_spec_file);
 }
 
 /// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
@@ -477,7 +477,7 @@ void gcc_cmdlinet::parse_specs()
              line=="*link:"))
       use_line=true;
     else if(use_line)
-      parse_specs_line(line);
+      parse_specs_line(line, true);
     else
     {
       // TODO need message interface

src/goto-cc/gcc_cmdline.h

@@ -31,7 +31,7 @@ class gcc_cmdlinet:public goto_cc_cmdlinet
 
   bool parse_arguments(const argst &args, bool in_spec_file);
   void parse_specs();
-  void parse_specs_line(const std::string &line);
+  void parse_specs_line(const std::string &line, bool in_spec_file);
 };
 
 #endif // CPROVER_GOTO_CC_GCC_CMDLINE_H