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;
118 else if(isdigit(*tptr))
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,
205 switch(
config.ansi_c.preprocessor)
213 path, outstream, message_handler,
config.ansi_c.preprocessor);
218 path, outstream, message_handler,
config.ansi_c.preprocessor);
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";
267 command_file <<
"/D__WORDSIZE=" <<
config.ansi_c.pointer_width <<
"\n";
271 command_file <<
"\"/D__PTRDIFF_TYPE__=long long int\"" <<
"\n";
273 command_file <<
"/D_WIN64" <<
"\n";
275 else if(
config.ansi_c.int_width == 16 &&
config.ansi_c.pointer_width == 32)
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";
291 if(
config.ansi_c.char_is_unsigned)
292 command_file <<
"/J" <<
"\n";
294 for(
const auto &define :
config.ansi_c.defines)
295 command_file <<
"/D" <<
shell_quote(define) <<
"\n";
297 for(
const auto &include_path :
config.ansi_c.include_paths)
298 command_file <<
"/I" <<
shell_quote(include_path) <<
"\n";
300 for(
const auto &include_file :
config.ansi_c.include_files)
301 command_file <<
"/FI" <<
shell_quote(include_file) <<
"\n";
309 run(
"cl", {
"cl",
"@" + command_file_name()},
"", outstream, stderr_file());
312 std::ifstream stderr_stream(stderr_file());
326 std::istream &instream,
327 std::ostream &outstream)
343 std::getline(instream, line);
346 line[0]==
'#' && (line[1]==
'#' || line[1]==
' ' || line[1]==
'\t'))
350 else if(line.size()>=3 &&
351 line[0]==
'/' && line[1]==
'*' && line[2]==
' ')
353 outstream << line.c_str()+3 <<
"\n";
356 outstream << line <<
"\n";
362 const std::string &
file,
363 std::ostream &outstream,
375 std::vector<std::string> command = {
376 "mwcceppc",
"-E",
"-P",
"-D__CPROVER__",
"-ppopt",
"line",
"-ppopt full"};
378 for(
const auto &define :
config.ansi_c.defines)
379 command.push_back(
" -D" + define);
381 for(
const auto &include_path :
config.ansi_c.include_paths)
382 command.push_back(
" -I" + include_path);
384 for(
const auto &include_file :
config.ansi_c.include_files)
386 command.push_back(
" -include");
387 command.push_back(include_file);
390 for(
const auto &opt :
config.ansi_c.preprocessor_options)
391 command.push_back(opt);
394 command.push_back(
file);
395 command.push_back(
"-o");
396 command.push_back(tmpi());
398 int result =
run(command[0], command,
"",
"", stderr_file());
400 std::ifstream stream_i(tmpi());
410 message.
error() <<
"Preprocessing failed (fopen failed)"
416 std::ifstream stderr_stream(stderr_file());
430 const std::string &
file,
431 std::ostream &outstream,
444 std::vector<std::string> argv;
447 argv.push_back(
"clang");
449 argv.push_back(
"gcc");
451 argv.push_back(
"-E");
452 argv.push_back(
"-D__CPROVER__");
456 if(
config.ansi_c.pointer_width == 16)
458 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
459 argv.push_back(
"-m16");
461 argv.push_back(
"-mips16");
463 else if(
config.ansi_c.pointer_width == 32)
465 if(arch ==
"i386" || arch ==
"x86_64")
466 argv.push_back(
"-m32");
467 else if(arch ==
"x32")
468 argv.push_back(
"-mx32");
470 argv.push_back(
"-mabi=32");
471 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
472 argv.push_back(
"-m32");
473 else if(arch ==
"s390" || arch ==
"s390x")
474 argv.push_back(
"-m31");
475 else if(arch ==
"sparc" || arch ==
"sparc64")
476 argv.push_back(
"-m32");
478 else if(
config.ansi_c.pointer_width == 64)
480 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
481 argv.push_back(
"-m64");
483 argv.push_back(
"-mabi=64");
484 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
485 argv.push_back(
"-m64");
486 else if(arch ==
"s390" || arch ==
"s390x")
487 argv.push_back(
"-m64");
488 else if(arch ==
"sparc" || arch ==
"sparc64")
489 argv.push_back(
"-m64");
493 if(
config.ansi_c.wchar_t_width ==
config.ansi_c.short_int_width)
494 argv.push_back(
"-fshort-wchar");
496 if(
config.ansi_c.char_is_unsigned)
497 argv.push_back(
"-funsigned-char");
500 argv.push_back(
"-nostdinc");
512 switch(
config.cpp.cpp_standard)
515#if defined(__OpenBSD__)
517 argv.push_back(
"-std=c++98");
520 argv.push_back(
"-std=gnu++98");
524#if defined(__OpenBSD__)
526 argv.push_back(
"-std=c++03");
529 argv.push_back(
"-std=gnu++03");
533#if defined(__OpenBSD__)
535 argv.push_back(
"-std=c++11");
538 argv.push_back(
"-std=gnu++11");
542#if defined(__OpenBSD__)
544 argv.push_back(
"-std=c++14");
547 argv.push_back(
"-std=gnu++14");
551#if defined(__OpenBSD__)
553 argv.push_back(
"-std=c++17");
556 argv.push_back(
"-std=gnu++17");
562 switch(
config.ansi_c.c_standard)
565#if defined(__OpenBSD__)
567 argv.push_back(
"-std=c89");
570 argv.push_back(
"-std=gnu89");
574#if defined(__OpenBSD__)
576 argv.push_back(
"-std=c99");
579 argv.push_back(
"-std=gnu99");
583#if defined(__OpenBSD__)
585 argv.push_back(
"-std=c11");
588 argv.push_back(
"-std=gnu11");
592#if defined(__OpenBSD__)
594 argv.push_back(
"-std=c17");
597 argv.push_back(
"-std=gnu17");
601#if defined(__OpenBSD__)
603 argv.push_back(
"-std=c2x");
606 argv.push_back(
"-std=gnu2x");
611 for(
const auto &define :
config.ansi_c.defines)
612 argv.push_back(
"-D" + define);
614 for(
const auto &include_path :
config.ansi_c.include_paths)
615 argv.push_back(
"-I" + include_path);
617 for(
const auto &include_file :
config.ansi_c.include_files)
619 argv.push_back(
"-include");
620 argv.push_back(include_file);
623 for(
const auto &opt :
config.ansi_c.preprocessor_options)
630 switch(
config.ansi_c.mode)
632 case configt::ansi_ct::flavourt::GCC_C: command+=
" -x c";
break;
633 case configt::ansi_ct::flavourt::GCC_CPP: command+=
" -x c++";
break;
641 argv.push_back(
file);
644 result =
run(argv[0], argv,
"", outstream, stderr_file());
647 std::ifstream stderr_stream(stderr_file());
661 const std::string &
file,
662 std::ostream &outstream,
674 std::vector<std::string> argv;
676 argv.push_back(
"armcc");
677 argv.push_back(
"-E");
678 argv.push_back(
"-D__CPROVER__");
681 argv.push_back(
"--bigend");
683 argv.push_back(
"--littleend");
685 if(
config.ansi_c.char_is_unsigned)
686 argv.push_back(
"--unsigned_chars");
688 argv.push_back(
"--signed_chars");
692 switch(
config.ansi_c.c_standard)
695 argv.push_back(
"--c90");
699 argv.push_back(
"--c99");
703 argv.push_back(
"--c11");
707 argv.push_back(
"--c17");
712 argv.push_back(
"--c17");
716 for(
const auto &define :
config.ansi_c.defines)
717 argv.push_back(
"-D" + define);
719 for(
const auto &include_path :
config.ansi_c.include_paths)
720 argv.push_back(
"-I" + include_path);
723 argv.push_back(
file);
728 result =
run(argv[0], argv,
"", outstream, stderr_file());
731 std::ifstream stderr_stream(stderr_file());
745 const std::string &
file,
746 std::ostream &outstream,
767 while(infile.read(&ch, 1))
776 "#include <stdlib.h>\n"
782 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()
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,...
bool has_suffix(const std::string &s, const std::string &suffix)
#define widen_if_needed(s)