26 const std::string &line,
35 const char *
tptr=line.c_str();
63 else if(*
tptr==
':' && state!=4)
65 if(
tptr[1]==
' ' && previous!=
':')
99 else if(
has_prefix(line,
"In file included from "))
104 const char *
tptr=line.c_str();
106 std::string
file, line_no;
146 std::istream &errors,
152 while(std::getline(errors, line))
204 const std::string &path,
239 const std::string &
file,
274 command_file <<
"\"/D__PTRDIFF_TYPE__=long long int\"" <<
"\n";
283 "Pointer difference expected to be long int typed");
290 "Pointer difference expected to be int typed");
351 line[0]==
'#' && (line[1]==
'#' || line[1]==
' ' || line[1]==
'\t'))
355 else if(line.size()>=3 &&
356 line[0]==
'/' && line[1]==
'*' && line[2]==
' ')
367 const std::string &
file,
380 std::vector<std::string> command = {
381 "mwcceppc",
"-E",
"-P",
"-D__CPROVER__",
"-ppopt",
"line",
"-ppopt full"};
384 command.push_back(
" -D" +
define);
391 command.push_back(
" -include");
396 command.push_back(
opt);
399 command.push_back(
file);
400 command.push_back(
"-o");
401 command.push_back(
tmpi());
415 message.
error() <<
"Preprocessing failed (fopen failed)"
435 const std::string &
file,
449 std::vector<std::string>
argv;
452 argv.push_back(
"clang");
454 argv.push_back(
"gcc");
456 argv.push_back(
"-E");
457 argv.push_back(
"-D__CPROVER__");
463 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
464 argv.push_back(
"-m16");
466 argv.push_back(
"-mips16");
470 if(arch ==
"i386" || arch ==
"x86_64")
471 argv.push_back(
"-m32");
472 else if(arch ==
"x32")
473 argv.push_back(
"-mx32");
475 argv.push_back(
"-mabi=32");
476 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
477 argv.push_back(
"-m32");
478 else if(arch ==
"s390" || arch ==
"s390x")
479 argv.push_back(
"-m31");
480 else if(arch ==
"sparc" || arch ==
"sparc64")
481 argv.push_back(
"-m32");
485 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
486 argv.push_back(
"-m64");
488 argv.push_back(
"-mabi=64");
489 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
490 argv.push_back(
"-m64");
491 else if(arch ==
"s390" || arch ==
"s390x")
492 argv.push_back(
"-m64");
493 else if(arch ==
"sparc" || arch ==
"sparc64")
494 argv.push_back(
"-m64");
499 argv.push_back(
"-fshort-wchar");
502 argv.push_back(
"-funsigned-char");
505 argv.push_back(
"-nostdinc");
520#if defined(__OpenBSD__)
522 argv.push_back(
"-std=c++98");
525 argv.push_back(
"-std=gnu++98");
529#if defined(__OpenBSD__)
531 argv.push_back(
"-std=c++03");
534 argv.push_back(
"-std=gnu++03");
538#if defined(__OpenBSD__)
540 argv.push_back(
"-std=c++11");
543 argv.push_back(
"-std=gnu++11");
547#if defined(__OpenBSD__)
549 argv.push_back(
"-std=c++14");
552 argv.push_back(
"-std=gnu++14");
556#if defined(__OpenBSD__)
558 argv.push_back(
"-std=c++17");
561 argv.push_back(
"-std=gnu++17");
570#if defined(__OpenBSD__)
572 argv.push_back(
"-std=c89");
575 argv.push_back(
"-std=gnu89");
579#if defined(__OpenBSD__)
581 argv.push_back(
"-std=c99");
584 argv.push_back(
"-std=gnu99");
588#if defined(__OpenBSD__)
590 argv.push_back(
"-std=c11");
593 argv.push_back(
"-std=gnu11");
606 argv.push_back(
"-include");
619 case configt::ansi_ct::flavourt::GCC_C: command+=
" -x c";
break;
620 case configt::ansi_ct::flavourt::GCC_CPP: command+=
" -x c++";
break;
648 const std::string &
file,
661 std::vector<std::string>
argv;
663 argv.push_back(
"armcc");
664 argv.push_back(
"-E");
665 argv.push_back(
"-D__CPROVER__");
668 argv.push_back(
"--bigend");
670 argv.push_back(
"--littleend");
673 argv.push_back(
"--unsigned_chars");
675 argv.push_back(
"--signed_chars");
681 argv.push_back(
"--c90");
686 argv.push_back(
"--c99");
719 const std::string &
file,
754 "#include <stdlib.h>\n"
760 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()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
bool has_prefix(const std::string &s, const std::string &prefix)
const std::string & id2string(const irep_idt &d)
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)
std::wstring widen(const char *s)