Skip to content

Commit 5109eab

Browse files
committed
Add @<file> arguments to the original command line
Before, such arguments would not be handed on to the native compiler.
1 parent da63652 commit 5109eab

File tree

6 files changed

+24
-5
lines changed

6 files changed

+24
-5
lines changed

regression/goto-gcc/at_files/args

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
other.c

regression/goto-gcc/at_files/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int foo();
2+
3+
int main()
4+
{
5+
return foo();
6+
}

regression/goto-gcc/at_files/other.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int foo()
2+
{
3+
return 1;
4+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
@args
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

src/goto-cc/gcc_cmdline.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -252,7 +252,7 @@ bool gcc_cmdlinet::parse_arguments(
252252
line.erase(0, line.find_first_not_of("\t "));
253253

254254
if(!line.empty())
255-
parse_specs_line(line);
255+
parse_specs_line(line, false);
256256
}
257257

258258
continue;
@@ -428,7 +428,7 @@ bool gcc_cmdlinet::parse_arguments(
428428
}
429429

430430
/// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
431-
void gcc_cmdlinet::parse_specs_line(const std::string &line)
431+
void gcc_cmdlinet::parse_specs_line(const std::string &line, bool in_spec_file)
432432
{
433433
// initial whitespace has been stripped
434434
assert(!line.empty());
@@ -444,7 +444,7 @@ void gcc_cmdlinet::parse_specs_line(const std::string &line)
444444
args.push_back(line.substr(arg_start, arg_end-arg_start));
445445
}
446446

447-
parse_arguments(args, true);
447+
parse_arguments(args, in_spec_file);
448448
}
449449

450450
/// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
@@ -473,7 +473,7 @@ void gcc_cmdlinet::parse_specs()
473473
line=="*link:"))
474474
use_line=true;
475475
else if(use_line)
476-
parse_specs_line(line);
476+
parse_specs_line(line, true);
477477
else
478478
{
479479
// TODO need message interface

src/goto-cc/gcc_cmdline.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ class gcc_cmdlinet:public goto_cc_cmdlinet
3131

3232
bool parse_arguments(const argst &args, bool in_spec_file);
3333
void parse_specs();
34-
void parse_specs_line(const std::string &line);
34+
void parse_specs_line(const std::string &line, bool in_spec_file);
3535
};
3636

3737
#endif // CPROVER_GOTO_CC_GCC_CMDLINE_H

0 commit comments

Comments
 (0)