26 if(src.find(
' ')==std::string::npos &&
27 src.find(
'"')==std::string::npos &&
28 src.find(
'&')==std::string::npos &&
29 src.find(
'|')==std::string::npos &&
30 src.find(
'(')==std::string::npos &&
31 src.find(
')')==std::string::npos &&
32 src.find(
'<')==std::string::npos &&
33 src.find(
'>')==std::string::npos &&
34 src.find(
'^')==std::string::npos)
44 for(
const char ch : src)
59 if(src.find(
' ')==std::string::npos &&
60 src.find(
'"')==std::string::npos &&
61 src.find(
'*')==std::string::npos &&
62 src.find(
'$')==std::string::npos &&
63 src.find(
'\\')==std::string::npos &&
64 src.find(
'?')==std::string::npos &&
65 src.find(
'&')==std::string::npos &&
66 src.find(
'|')==std::string::npos &&
67 src.find(
'>')==std::string::npos &&
68 src.find(
'<')==std::string::npos &&
69 src.find(
'^')==std::string::npos &&
70 src.find(
'\'')==std::string::npos)
81 for(
const char ch : src)
95 const std::string &line,
99 std::string error_msg=line;
104 const char *tptr=line.c_str();
106 std::string
file, line_no, column, _error_msg,
function;
120 else if(
has_prefix(tptr,
" column ") && state != 4)
126 else if(
has_prefix(tptr,
" function ") && state != 4)
132 else if(*tptr==
':' && state!=4)
134 if(tptr[1]==
' ' && previous!=
':')
138 while(*tptr==
' ') tptr++;
163 saved_error_location.
set_line(line_no);
165 error_msg=_error_msg;
168 else if(
has_prefix(line,
"In file included from "))
173 const char *tptr=line.c_str();
175 std::string
file, line_no;
190 else if(isdigit(*tptr))
203 saved_error_location.
set_line(line_no);
215 std::istream &errors,
221 while(std::getline(errors, line))
227 std::istream &instream,
228 std::ostream &outstream,
233 std::ofstream tmp(tmp_file());
242 tmp << instream.rdbuf();
246 bool result=
c_preprocess(tmp_file(), outstream, message_handler);
273 const std::string &path,
274 std::ostream &outstream,
308 const std::string &
file,
309 std::ostream &outstream,
324 std::ofstream command_file(command_file_name());
328 command_file << char(0xef) << char(0xbb) << char(0xbf);
330 command_file <<
"/nologo" <<
'\n';
331 command_file <<
"/E" <<
'\n';
336 command_file <<
"/source-charset:utf-8" <<
'\n';
338 command_file <<
"/D__CPROVER__" <<
"\n";
343 command_file <<
"\"/D__PTRDIFF_TYPE__=long long int\"" <<
"\n";
345 command_file <<
"/D_WIN64" <<
"\n";
352 "Pointer difference expected to be long int typed");
353 command_file <<
"/D__PTRDIFF_TYPE__=long" <<
'\n';
359 "Pointer difference expected to be int typed");
360 command_file <<
"/D__PTRDIFF_TYPE__=int" <<
"\n";
364 command_file <<
"/J" <<
"\n";
367 command_file <<
"/D" <<
shell_quote(define) <<
"\n";
370 command_file <<
"/I" <<
shell_quote(include_path) <<
"\n";
373 command_file <<
"/FI" <<
shell_quote(include_file) <<
"\n";
382 std::string command =
"CL @\"" + command_file_name() +
"\"";
383 command +=
" 2> \"" + stderr_file() +
"\"";
388 run(
"cl", {
"cl",
"@" + command_file_name()},
"", outstream, stderr_file());
391 std::ifstream stderr_stream(stderr_file());
405 std::istream &instream,
406 std::ostream &outstream)
422 std::getline(instream, line);
425 line[0]==
'#' && (line[1]==
'#' || line[1]==
' ' || line[1]==
'\t'))
429 else if(line.size()>=3 &&
430 line[0]==
'/' && line[1]==
'*' && line[2]==
' ')
432 outstream << line.c_str()+3 <<
"\n";
435 outstream << line <<
"\n";
441 const std::string &
file,
442 std::ostream &outstream,
454 std::vector<std::string> command = {
455 "mwcceppc",
"-E",
"-P",
"-D__CPROVER__",
"-ppopt",
"line",
"-ppopt full"};
458 command.push_back(
" -D" + define);
461 command.push_back(
" -I" + include_path);
465 command.push_back(
" -include");
466 command.push_back(include_file);
470 command.push_back(opt);
473 command.push_back(
file);
474 command.push_back(
"-o");
475 command.push_back(tmpi());
477 int result =
run(command[0], command,
"",
"", stderr_file());
479 std::ifstream stream_i(tmpi());
489 message.
error() <<
"Preprocessing failed (fopen failed)" 495 std::ifstream stderr_stream(stderr_file());
509 const std::string &
file,
510 std::ostream &outstream,
523 std::vector<std::string> argv;
526 argv.push_back(
"clang");
528 argv.push_back(
"gcc");
530 argv.push_back(
"-E");
531 argv.push_back(
"-D__CPROVER__");
537 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
538 argv.push_back(
"-m16");
540 argv.push_back(
"-mips16");
544 if(arch ==
"i386" || arch ==
"x86_64")
545 argv.push_back(
"-m32");
546 else if(arch ==
"x32")
547 argv.push_back(
"-mx32");
549 argv.push_back(
"-mabi=32");
550 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
551 argv.push_back(
"-m32");
552 else if(arch ==
"s390" || arch ==
"s390x")
553 argv.push_back(
"-m31");
554 else if(arch ==
"sparc" || arch ==
"sparc64")
555 argv.push_back(
"-m32");
559 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
560 argv.push_back(
"-m64");
562 argv.push_back(
"-mabi=64");
563 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
564 argv.push_back(
"-m64");
565 else if(arch ==
"s390" || arch ==
"s390x")
566 argv.push_back(
"-m64");
567 else if(arch ==
"sparc" || arch ==
"sparc64")
568 argv.push_back(
"-m64");
573 argv.push_back(
"-fshort-wchar");
576 argv.push_back(
"-funsigned-char");
579 argv.push_back(
"-nostdinc");
592 argv.push_back(
"-std=gnu++98");
596 argv.push_back(
"-std=gnu++03");
600 argv.push_back(
"-std=gnu++11");
604 argv.push_back(
"-std=gnu++14");
613 argv.push_back(
"-std=gnu++89");
617 argv.push_back(
"-std=gnu99");
621 argv.push_back(
"-std=gnu11");
627 argv.push_back(
"-D" + define);
630 argv.push_back(
"-I" + include_path);
634 argv.push_back(
"-include");
635 argv.push_back(include_file);
647 case configt::ansi_ct::flavourt::GCC_C: command+=
" -x c";
break;
648 case configt::ansi_ct::flavourt::GCC_CPP: command+=
" -x c++";
break;
656 argv.push_back(
file);
659 result =
run(argv[0], argv,
"", outstream, stderr_file());
662 std::ifstream stderr_stream(stderr_file());
676 const std::string &
file,
677 std::ostream &outstream,
689 std::vector<std::string> argv;
691 argv.push_back(
"armcc");
692 argv.push_back(
"-E");
693 argv.push_back(
"-D__CPROVER__");
696 argv.push_back(
"--bigend");
698 argv.push_back(
"--littleend");
701 argv.push_back(
"--unsigned_chars");
703 argv.push_back(
"--signed_chars");
709 argv.push_back(
"--c90");
714 argv.push_back(
"--c99");
719 argv.push_back(
"-D" + define);
722 argv.push_back(
"-I" + include_path);
725 argv.push_back(
file);
730 result =
run(argv[0], argv,
"", outstream, stderr_file());
733 std::ifstream stderr_stream(stderr_file());
747 const std::string &
file,
748 std::ostream &outstream,
754 std::ifstream infile(
file);
773 while(infile.read(&ch, 1))
782 "#include <stdlib.h>\n" 788 std::ostringstream out;
bool c_preprocess_visual_studio(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
struct configt::ansi_ct ansi_c
void set_function(const irep_idt &function)
bool c_preprocess_codewarrior(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
const std::string & id2string(const irep_idt &d)
std::wstring widen(const char *s)
static std::string shell_quote(const std::string &src)
quote a string for bash and CMD
std::list< std::string > defines
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
signedbv_typet pointer_diff_type()
mstreamt & warning() const
preprocessort preprocessor
std::list< std::string > include_files
bool c_preprocess_gcc_clang(const std::string &, std::ostream &, message_handlert &, configt::ansi_ct::preprocessort)
ANSI-C preprocessing.
static bool is_dot_i_file(const std::string &path)
ANSI-C preprocessing.
source_locationt source_location
void set_file(const irep_idt &file)
bool c_preprocess_arm(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
void set_line(const irep_idt &line)
enum configt::cppt::cpp_standardt cpp_standard
void set_column(const irep_idt &column)
signedbv_typet signed_long_int_type()
int run(const std::string &what, const std::vector< std::string > &argv)
bool has_prefix(const std::string &s, const std::string &prefix)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::size_t pointer_width
void postprocess_codewarrior(std::istream &instream, std::ostream &outstream)
post-processing specifically for CodeWarrior
enum configt::ansi_ct::c_standardt c_standard
std::size_t wchar_t_width
bool test_c_preprocessor(message_handlert &message_handler)
const char c_test_program[]
tests ANSI-C preprocessing
static void error_parse(std::istream &errors, bool warning_only, messaget &message)
static void error_parse_line(const std::string &line, bool warning_only, messaget &message)
bool has_suffix(const std::string &s, const std::string &suffix)
signedbv_typet signed_int_type()
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
signedbv_typet signed_long_long_int_type()
std::list< std::string > preprocessor_options
std::size_t short_int_width
bool c_preprocess_none(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
std::list< std::string > include_paths