23 const std::string &line,
27 std::string error_msg=line;
32 const char *tptr=line.c_str();
34 std::string file, line_no, column, _error_msg,
function;
48 else if(
has_prefix(tptr,
" column ") && state != 4)
54 else if(
has_prefix(tptr,
" function ") && state != 4)
60 else if(*tptr==
':' && state!=4)
62 if(tptr[1]==
' ' && previous!=
':')
66 while(*tptr==
' ') tptr++;
91 saved_error_location.
set_line(line_no);
96 else if(
has_prefix(line,
"In file included from "))
101 const char *tptr=line.c_str();
103 std::string file, line_no;
129 saved_error_location.
set_file(file);
131 saved_error_location.
set_line(line_no);
143 std::istream &errors,
149 while(std::getline(errors, line))
155 std::istream &instream,
156 std::ostream &outstream,
161 std::ofstream tmp(tmp_file());
170 tmp << instream.rdbuf();
174 bool result=
c_preprocess(tmp_file(), outstream, message_handler);
201 const std::string &path,
202 std::ostream &outstream,
236 const std::string &file,
237 std::ostream &outstream,
252 std::ofstream command_file(command_file_name());
256 command_file << char(0xef) << char(0xbb) << char(0xbf);
258 command_file <<
"/nologo" <<
'\n';
259 command_file <<
"/E" <<
'\n';
264 command_file <<
"/source-charset:utf-8" <<
'\n';
266 command_file <<
"/D__CPROVER__" <<
"\n";
271 command_file <<
"\"/D__PTRDIFF_TYPE__=long long int\"" <<
"\n";
273 command_file <<
"/D_WIN64" <<
"\n";
280 "Pointer difference expected to be long int typed");
281 command_file <<
"/D__PTRDIFF_TYPE__=long" <<
'\n';
287 "Pointer difference expected to be int typed");
288 command_file <<
"/D__PTRDIFF_TYPE__=int" <<
"\n";
292 command_file <<
"/J" <<
"\n";
295 command_file <<
"/D" <<
shell_quote(define) <<
"\n";
298 command_file <<
"/I" <<
shell_quote(include_path) <<
"\n";
301 command_file <<
"/FI" <<
shell_quote(include_file) <<
"\n";
311 run(
"cl", {
"cl",
"@" + command_file_name()},
"", outstream, stderr_file());
314 std::ifstream stderr_stream(stderr_file());
328 std::istream &instream,
329 std::ostream &outstream)
345 std::getline(instream, line);
348 line[0]==
'#' && (line[1]==
'#' || line[1]==
' ' || line[1]==
'\t'))
352 else if(line.size()>=3 &&
353 line[0]==
'/' && line[1]==
'*' && line[2]==
' ')
355 outstream << line.c_str()+3 <<
"\n";
358 outstream << line <<
"\n";
364 const std::string &file,
365 std::ostream &outstream,
377 std::vector<std::string> command = {
378 "mwcceppc",
"-E",
"-P",
"-D__CPROVER__",
"-ppopt",
"line",
"-ppopt full"};
381 command.push_back(
" -D" + define);
384 command.push_back(
" -I" + include_path);
388 command.push_back(
" -include");
389 command.push_back(include_file);
393 command.push_back(
opt);
396 command.push_back(file);
397 command.push_back(
"-o");
398 command.push_back(tmpi());
400 int result =
run(command[0], command,
"",
"", stderr_file());
402 std::ifstream stream_i(tmpi());
412 message.
error() <<
"Preprocessing failed (fopen failed)"
418 std::ifstream stderr_stream(stderr_file());
432 const std::string &file,
433 std::ostream &outstream,
446 std::vector<std::string> argv;
449 argv.push_back(
"clang");
451 argv.push_back(
"gcc");
453 argv.push_back(
"-E");
454 argv.push_back(
"-D__CPROVER__");
460 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
461 argv.push_back(
"-m16");
463 argv.push_back(
"-mips16");
467 if(arch ==
"i386" || arch ==
"x86_64")
468 argv.push_back(
"-m32");
469 else if(arch ==
"x32")
470 argv.push_back(
"-mx32");
472 argv.push_back(
"-mabi=32");
473 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
474 argv.push_back(
"-m32");
475 else if(arch ==
"s390" || arch ==
"s390x")
476 argv.push_back(
"-m31");
477 else if(arch ==
"sparc" || arch ==
"sparc64")
478 argv.push_back(
"-m32");
482 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
483 argv.push_back(
"-m64");
485 argv.push_back(
"-mabi=64");
486 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
487 argv.push_back(
"-m64");
488 else if(arch ==
"s390" || arch ==
"s390x")
489 argv.push_back(
"-m64");
490 else if(arch ==
"sparc" || arch ==
"sparc64")
491 argv.push_back(
"-m64");
496 argv.push_back(
"-fshort-wchar");
499 argv.push_back(
"-funsigned-char");
502 argv.push_back(
"-nostdinc");
517 #if defined(__OpenBSD__)
519 argv.push_back(
"-std=c++98");
522 argv.push_back(
"-std=gnu++98");
526 #if defined(__OpenBSD__)
528 argv.push_back(
"-std=c++03");
531 argv.push_back(
"-std=gnu++03");
535 #if defined(__OpenBSD__)
537 argv.push_back(
"-std=c++11");
540 argv.push_back(
"-std=gnu++11");
544 #if defined(__OpenBSD__)
546 argv.push_back(
"-std=c++14");
549 argv.push_back(
"-std=gnu++14");
553 #if defined(__OpenBSD__)
555 argv.push_back(
"-std=c++17");
558 argv.push_back(
"-std=gnu++17");
567 #if defined(__OpenBSD__)
569 argv.push_back(
"-std=c89");
572 argv.push_back(
"-std=gnu89");
576 #if defined(__OpenBSD__)
578 argv.push_back(
"-std=c99");
581 argv.push_back(
"-std=gnu99");
585 #if defined(__OpenBSD__)
587 argv.push_back(
"-std=c11");
590 argv.push_back(
"-std=gnu11");
596 argv.push_back(
"-D" + define);
599 argv.push_back(
"-I" + include_path);
603 argv.push_back(
"-include");
604 argv.push_back(include_file);
616 case configt::ansi_ct::flavourt::GCC_C: command+=
" -x c";
break;
617 case configt::ansi_ct::flavourt::GCC_CPP: command+=
" -x c++";
break;
625 argv.push_back(file);
628 result =
run(argv[0], argv,
"", outstream, stderr_file());
631 std::ifstream stderr_stream(stderr_file());
645 const std::string &file,
646 std::ostream &outstream,
658 std::vector<std::string> argv;
660 argv.push_back(
"armcc");
661 argv.push_back(
"-E");
662 argv.push_back(
"-D__CPROVER__");
665 argv.push_back(
"--bigend");
667 argv.push_back(
"--littleend");
670 argv.push_back(
"--unsigned_chars");
672 argv.push_back(
"--signed_chars");
678 argv.push_back(
"--c90");
683 argv.push_back(
"--c99");
688 argv.push_back(
"-D" + define);
691 argv.push_back(
"-I" + include_path);
694 argv.push_back(file);
699 result =
run(argv[0], argv,
"", outstream, stderr_file());
702 std::ifstream stderr_stream(stderr_file());
716 const std::string &file,
717 std::ostream &outstream,
738 while(infile.read(&ch, 1))
747 "#include <stdlib.h>\n"
753 std::ostringstream out;
bool c_preprocess_visual_studio(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
bool c_preprocess_arm(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
bool c_preprocess_none(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
static void error_parse(std::istream &errors, bool warning_only, messaget &message)
const char c_test_program[]
tests ANSI-C preprocessing
bool c_preprocess_codewarrior(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
static void error_parse_line(const std::string &line, bool warning_only, messaget &message)
void postprocess_codewarrior(std::istream &instream, std::ostream &outstream)
post-processing specifically for CodeWarrior
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
bool test_c_preprocessor(message_handlert &message_handler)
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.
signedbv_typet signed_long_int_type()
signedbv_typet signed_int_type()
signedbv_typet pointer_diff_type()
signedbv_typet signed_long_long_int_type()
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
void set_column(const irep_idt &column)
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
bool has_prefix(const std::string &s, const std::string &prefix)
int run(const std::string &what, const std::vector< std::string > &argv)
std::string shell_quote(const std::string &src)
quote a string for bash and CMD
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
std::list< std::string > include_paths
enum configt::ansi_ct::c_standardt c_standard
std::size_t pointer_width
std::list< std::string > include_files
std::list< std::string > preprocessor_options
std::list< std::string > defines
std::size_t wchar_t_width
preprocessort preprocessor
std::size_t short_int_width
enum configt::cppt::cpp_standardt cpp_standard
bool has_suffix(const std::string &s, const std::string &suffix)
#define widen_if_needed(s)