25 if(src.find(
' ')==std::string::npos &&
26 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)
43 for(
const char ch : src)
58 if(src.find(
' ')==std::string::npos &&
59 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)
80 for(
const char ch : src)
94 const std::string &line,
98 std::string error_msg=line;
103 const char *tptr=line.c_str();
105 std::string
file, line_no, column, _error_msg,
function;
119 else if(
has_prefix(tptr,
" column ") && state != 4)
125 else if(
has_prefix(tptr,
" function ") && state != 4)
131 else if(*tptr==
':' && state!=4)
133 if(tptr[1]==
' ' && previous!=
':')
137 while(*tptr==
' ') tptr++;
162 saved_error_location.
set_line(line_no);
164 error_msg=_error_msg;
167 else if(
has_prefix(line,
"In file included from "))
172 const char *tptr=line.c_str();
174 std::string
file, line_no;
189 else if(isdigit(*tptr))
202 saved_error_location.
set_line(line_no);
214 std::istream &errors,
220 while(std::getline(errors, line))
226 std::istream &instream,
227 std::ostream &outstream,
232 std::ofstream tmp(tmp_file());
241 tmp << instream.rdbuf();
272 const std::string &path,
273 std::ostream &outstream,
307 const std::string &
file,
308 std::ostream &outstream,
323 std::ofstream command_file(command_file_name());
327 command_file << char(0xef) << char(0xbb) << char(0xbf);
329 command_file <<
"/nologo" <<
'\n';
330 command_file <<
"/E" <<
'\n';
335 command_file <<
"/source-charset:utf-8" <<
'\n';
337 command_file <<
"/D__CPROVER__" <<
"\n";
342 command_file <<
"\"/D__PTRDIFF_TYPE__=long long int\"" <<
"\n";
344 command_file <<
"/D_WIN64" <<
"\n";
351 "Pointer difference expected to be long int typed");
352 command_file <<
"/D__PTRDIFF_TYPE__=long" <<
'\n';
358 "Pointer difference expected to be int typed");
359 command_file <<
"/D__PTRDIFF_TYPE__=int" <<
"\n";
363 command_file <<
"/J" <<
"\n";
366 command_file <<
"/D" <<
shell_quote(define) <<
"\n";
369 command_file <<
"/I" <<
shell_quote(include_path) <<
"\n";
372 command_file <<
"/FI" <<
shell_quote(include_file) <<
"\n";
381 std::string command =
"CL @\"" + command_file_name() +
"\"";
382 command +=
" > \"" + tmpi() +
"\"";
383 command +=
" 2> \"" + stderr_file() +
"\"";
387 int result=system(command.c_str());
389 std::ifstream instream(tmpi());
393 message.
error() <<
"CL Preprocessing failed (open failed)" 398 outstream << instream.rdbuf();
403 std::ifstream stderr_stream(stderr_file());
417 std::istream &instream,
418 std::ostream &outstream)
434 std::getline(instream, line);
437 line[0]==
'#' && (line[1]==
'#' || line[1]==
' ' || line[1]==
'\t'))
441 else if(line.size()>=3 &&
442 line[0]==
'/' && line[1]==
'*' && line[2]==
' ')
444 outstream << line.c_str()+3 <<
"\n";
447 outstream << line <<
"\n";
453 const std::string &
file,
454 std::ostream &outstream,
468 command=
"mwcceppc -E -P -D__CPROVER__ -ppopt line -ppopt full";
485 command+=
" \""+
file+
"\"";
486 command +=
" -o \"" + tmpi() +
"\"";
487 command +=
" 2> \"" + stderr_file() +
"\"";
489 result=system(command.c_str());
491 std::ifstream stream_i(tmpi());
501 message.
error() <<
"Preprocessing failed (fopen failed)" 507 std::ifstream stderr_stream(stderr_file());
521 const std::string &
file,
522 std::ostream &outstream,
542 command +=
" -E -D__CPROVER__";
548 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
551 command +=
" -mips16";
555 if(arch ==
"i386" || arch ==
"x86_64")
557 else if(arch ==
"x32")
560 command +=
" -mabi=32";
561 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
563 else if(arch ==
"s390" || arch ==
"s390x")
565 else if(arch ==
"sparc" || arch ==
"sparc64")
570 if(arch ==
"i386" || arch ==
"x86_64" || arch ==
"x32")
573 command +=
" -mabi=64";
574 else if(arch ==
"powerpc" || arch ==
"ppc64" || arch ==
"ppc64le")
576 else if(arch ==
"s390" || arch ==
"s390x")
578 else if(arch ==
"sparc" || arch ==
"sparc64")
584 command +=
" -fshort-wchar";
587 command +=
" -funsigned-char";
590 command +=
" -nostdinc";
603 command +=
" -std=gnu++98";
607 command +=
" -std=gnu++03";
611 command +=
" -std=gnu++11";
615 command +=
" -std=gnu++14";
624 command +=
" -std=gnu++89";
628 command +=
" -std=gnu99";
632 command +=
" -std=gnu11";
655 case configt::ansi_ct::flavourt::GCC_C: command+=
" -x c";
break;
656 case configt::ansi_ct::flavourt::GCC_CPP: command+=
" -x c++";
break;
665 command+=
" \""+
file+
"\"";
666 command +=
" -o \"" + tmpi() +
"\"";
667 command +=
" 2> \"" + stderr_file() +
"\"";
671 result=system(command.c_str());
673 std::ifstream instream(tmpi());
676 std::ifstream stderr_stream(stderr_file());
681 outstream << instream.rdbuf();
686 message.
error() <<
"GCC preprocessing failed (open failed)" 691 command+=
" \""+
file+
"\"";
692 command +=
" 2> \"" + stderr_file() +
"\"";
694 FILE *stream=popen(command.c_str(),
"r");
699 while((ch=fgetc(stream))!=EOF)
700 outstream << (
unsigned char)ch;
702 result=pclose(stream);
706 message.
error() <<
"GCC preprocessing failed (popen failed)" 712 std::ifstream stderr_stream(stderr_file());
728 const std::string &
file,
729 std::ostream &outstream,
743 command=
"armcc -E -D__CPROVER__";
746 command +=
" --bigend";
748 command +=
" --littleend";
751 command +=
" --unsigned_chars";
753 command +=
" --signed_chars";
778 command+=
" \""+
file+
"\"";
779 command +=
" > \"" + tmpi() +
"\"";
780 command +=
" 2> \"" + stderr_file() +
"\"";
784 result=system(command.c_str());
786 std::ifstream instream(tmpi());
790 outstream << instream.rdbuf();
795 message.
error() <<
"ARMCC preprocessing failed (fopen failed)" 800 command+=
" \""+
file+
"\"";
801 command +=
" 2> \"" + stderr_file() +
"\"";
803 FILE *stream=popen(command.c_str(),
"r");
808 while((ch=fgetc(stream))!=EOF)
809 outstream << (
unsigned char)ch;
811 result=pclose(stream);
815 message.
error() <<
"ARMCC preprocessing failed (popen failed)" 822 std::ifstream stderr_stream(stderr_file());
836 const std::string &
file,
837 std::ostream &outstream,
843 std::ifstream infile(
file);
862 while(infile.read(&ch, 1))
871 "#include <stdlib.h>\n" 877 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.
static mstreamt & eom(mstreamt &m)
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()
bool has_prefix(const std::string &s, const std::string &prefix)
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)
goto_programt coverage_criteriont message_handlert & message_handler
signedbv_typet signed_int_type()
#define DATA_INVARIANT(CONDITION, REASON)
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