15 #if defined(__linux__) || \ 16 defined(__FreeBSD_kernel__) || \ 18 defined(__unix__) || \ 19 defined(__CYGWIN__) || \ 35 #define GCC_DEFINES_16 \ 36 " -D__INT_MAX__=32767"\ 38 " -D__SCHAR_MAX__=127"\ 39 " -D__SHRT_MAX__=32767"\ 40 " -D__INT32_TYPE__=long"\ 41 " -D__LONG_LONG_MAX__=2147483647L"\ 42 " -D__LONG_MAX__=2147483647" \ 43 " -D__SIZE_TYPE__=\"unsigned int\""\ 44 " -D__PTRDIFF_TYPE__=int"\ 45 " -D__WINT_TYPE__=\"unsigned int\""\ 46 " -D__INTMAX_TYPE__=\"long long int\""\ 47 " -D__UINTMAX_TYPE__=\"long long unsigned int\""\ 48 " -D__INTPTR_TYPE__=\"int\""\ 49 " -D__UINTPTR_TYPE__=\"unsigned int\"" 51 #define GCC_DEFINES_32 \ 52 " -D__INT_MAX__=2147483647"\ 54 " -D__SCHAR_MAX__=127"\ 55 " -D__SHRT_MAX__=32767"\ 56 " -D__INT32_TYPE__=int"\ 57 " -D__LONG_LONG_MAX__=9223372036854775807LL"\ 58 " -D__LONG_MAX__=2147483647L" \ 59 " -D__SIZE_TYPE__=\"long unsigned int\""\ 60 " -D__PTRDIFF_TYPE__=int"\ 61 " -D__WINT_TYPE__=\"unsigned int\""\ 62 " -D__INTMAX_TYPE__=\"long long int\""\ 63 " -D__UINTMAX_TYPE__=\"long long unsigned int\""\ 64 " -D__INTPTR_TYPE__=\"long int\""\ 65 " -D__UINTPTR_TYPE__=\"long unsigned int\"" 67 #define GCC_DEFINES_LP64 \ 68 " -D__INT_MAX__=2147483647"\ 70 " -D__SCHAR_MAX__=127"\ 71 " -D__SHRT_MAX__=32767"\ 72 " -D__INT32_TYPE__=int"\ 73 " -D__LONG_LONG_MAX__=9223372036854775807LL"\ 74 " -D__LONG_MAX__=9223372036854775807L"\ 75 " -D__SIZE_TYPE__=\"long unsigned int\""\ 76 " -D__PTRDIFF_TYPE__=long"\ 77 " -D__WINT_TYPE__=\"unsigned int\""\ 78 " -D__INTMAX_TYPE__=\"long int\""\ 79 " -D__UINTMAX_TYPE__=\"long unsigned int\""\ 80 " -D__INTPTR_TYPE__=\"long int\""\ 81 " -D__UINTPTR_TYPE__=\"long unsigned int\"" 83 #define GCC_DEFINES_LLP64 \ 84 " -D__INT_MAX__=2147483647"\ 86 " -D__SCHAR_MAX__=127"\ 87 " -D__SHRT_MAX__=32767"\ 88 " -D__INT32_TYPE__=int"\ 89 " -D__LONG_LONG_MAX__=9223372036854775807LL"\ 90 " -D__LONG_MAX__=2147483647"\ 91 " -D__SIZE_TYPE__=\"long long unsigned int\""\ 92 " -D__PTRDIFF_TYPE__=\"long long\""\ 93 " -D__WINT_TYPE__=\"unsigned int\""\ 94 " -D__INTMAX_TYPE__=\"long long int\""\ 95 " -D__UINTMAX_TYPE__=\"long long unsigned int\""\ 96 " -D__INTPTR_TYPE__=\"long long int\""\ 97 " -D__UINTPTR_TYPE__=\"long long unsigned int\"" 102 if(src.
id()==ID_signedbv)
105 else if(src.
id()==ID_unsignedbv)
118 if(src.find(
' ')==std::string::npos &&
119 src.find(
'"')==std::string::npos &&
120 src.find(
'&')==std::string::npos &&
121 src.find(
'|')==std::string::npos &&
122 src.find(
'(')==std::string::npos &&
123 src.find(
')')==std::string::npos &&
124 src.find(
'<')==std::string::npos &&
125 src.find(
'>')==std::string::npos &&
126 src.find(
'^')==std::string::npos)
136 for(
const char ch : src)
151 if(src.find(
' ')==std::string::npos &&
152 src.find(
'"')==std::string::npos &&
153 src.find(
'*')==std::string::npos &&
154 src.find(
'$')==std::string::npos &&
155 src.find(
'\\')==std::string::npos &&
156 src.find(
'?')==std::string::npos &&
157 src.find(
'&')==std::string::npos &&
158 src.find(
'|')==std::string::npos &&
159 src.find(
'>')==std::string::npos &&
160 src.find(
'<')==std::string::npos &&
161 src.find(
'^')==std::string::npos &&
162 src.find(
'\'')==std::string::npos)
173 for(
const char ch : src)
187 const std::string &line,
191 std::string error_msg=line;
196 const char *tptr=line.c_str();
198 std::string
file, line_no, column, _error_msg,
function;
206 if(strncmp(tptr,
" line ", 6)==0 && state!=4)
212 else if(strncmp(tptr,
" column ", 8)==0 && state!=4)
218 else if(strncmp(tptr,
" function ", 10)==0 && state!=4)
224 else if(*tptr==
':' && state!=4)
226 if(tptr[1]==
' ' && previous!=
':')
230 while(*tptr==
' ') tptr++;
253 saved_error_location.
set_file(file);
255 saved_error_location.
set_line(line_no);
257 error_msg=_error_msg;
260 else if(
has_prefix(line,
"In file included from "))
265 const char *tptr=line.c_str();
267 std::string
file, line_no;
282 else if(isdigit(*tptr))
293 saved_error_location.
set_file(file);
295 saved_error_location.
set_line(line_no);
307 std::istream &errors,
313 while(std::getline(errors, line))
319 std::istream &instream,
320 std::ostream &outstream,
325 std::ofstream tmp(tmp_file());
334 tmp << instream.rdbuf();
338 bool result=
c_preprocess(tmp_file(), outstream, message_handler);
346 const char *ext=strrchr(path.c_str(),
'.');
349 if(std::string(ext)==
".i" ||
350 std::string(ext)==
".ii")
371 const std::string &path,
372 std::ostream &outstream,
406 const std::string &
file,
407 std::ostream &outstream,
422 std::ofstream command_file(command_file_name);
426 command_file << char(0xef) << char(0xbb) << char(0xbf);
428 command_file <<
"/nologo" <<
"\n";
429 command_file <<
"/E" <<
"\n";
430 command_file <<
"/D__CPROVER__" <<
"\n";
435 command_file <<
"\"/D__PTRDIFF_TYPE__=long long int\"" <<
"\n";
437 command_file <<
"/D_WIN64" <<
"\n";
441 command_file <<
"/D__PTRDIFF_TYPE__=int" <<
"\n";
442 command_file <<
"/U_WIN64" <<
"\n";
446 command_file <<
"/J" <<
"\n";
449 command_file <<
"/D__STDC_VERSION__=199901L" <<
"\n";
450 command_file <<
"/D__STDC_IEC_559__=1" <<
"\n";
451 command_file <<
"/D__STDC_IEC_559_COMPLEX__=1" <<
"\n";
452 command_file <<
"/D__STDC_ISO_10646__=1" <<
"\n";
455 command_file <<
"/D" <<
shell_quote(define) <<
"\n";
458 command_file <<
"/I" <<
shell_quote(include_path) <<
"\n";
461 command_file <<
"/FI" <<
shell_quote(include_file) <<
"\n";
470 std::string command=
"CL @\""+command_file_name+
"\"";
471 command+=
" > \""+tmpi+
"\"";
472 command+=
" 2> \""+stderr_file+
"\"";
476 int result=system(command.c_str());
478 std::ifstream instream(tmpi);
482 unlink(tmpi.c_str());
483 unlink(stderr_file.c_str());
484 unlink(command_file_name.c_str());
485 message.
error() <<
"CL Preprocessing failed (open failed)" 490 outstream << instream.rdbuf();
493 unlink(tmpi.c_str());
494 unlink(command_file_name.c_str());
497 std::ifstream stderr_stream(stderr_file);
500 unlink(stderr_file.c_str());
513 std::istream &instream,
514 std::ostream &outstream)
530 std::getline(instream, line);
533 line[0]==
'#' && (line[1]==
'#' || line[1]==
' ' || line[1]==
'\t'))
537 else if(line.size()>=3 &&
538 line[0]==
'/' && line[1]==
'*' && line[2]==
' ')
540 outstream << line.c_str()+3 <<
"\n";
543 outstream << line <<
"\n";
549 const std::string &
file,
550 std::ostream &outstream,
564 command=
"mwcceppc -E -P -D__CPROVER__ -ppopt line -ppopt full";
581 command+=
" \""+file+
"\"";
582 command+=
" -o \""+tmpi+
"\"";
583 command+=
" 2> \""+stderr_file+
"\"";
585 result=system(command.c_str());
587 std::ifstream stream_i(tmpi);
594 unlink(tmpi.c_str());
598 unlink(tmpi.c_str());
599 unlink(stderr_file.c_str());
600 message.
error() <<
"Preprocessing failed (fopen failed)" 606 std::ifstream stderr_stream(stderr_file);
609 unlink(stderr_file.c_str());
622 const std::string &
file,
623 std::ostream &outstream,
643 command +=
" -E -undef -D__CPROVER__";
647 command+=
" -D__DBL_MIN_EXP__=\"(-1021)\"";
648 command+=
" -D__FLT_MIN__=1.17549435e-38F";
649 command+=
" -D__DEC64_SUBNORMAL_MIN__=0.000000000000001E-383DD";
650 command+=
" -D__CHAR_BIT__=8";
651 command+=
" -D__DBL_DENORM_MIN__=4.9406564584124654e-324";
652 command+=
" -D__FLT_EVAL_METHOD__=0";
653 command+=
" -D__DBL_MIN_10_EXP__=\"(-307)\"";
654 command+=
" -D__FINITE_MATH_ONLY__=0";
655 command+=
" -D__DEC64_MAX_EXP__=384";
656 command+=
" -D__SHRT_MAX__=32767";
657 command+=
" -D__LDBL_MAX__=1.18973149535723176502e+4932L";
658 command+=
" -D__DEC32_EPSILON__=1E-6DF";
659 command+=
" -D__SCHAR_MAX__=127";
660 command+=
" -D__USER_LABEL_PREFIX__=_";
661 command+=
" -D__DEC64_MIN_EXP__=\"(-383)\"";
662 command+=
" -D__DBL_DIG__=15";
663 command+=
" -D__FLT_EPSILON__=1.19209290e-7F";
664 command+=
" -D__LDBL_MIN__=3.36210314311209350626e-4932L";
665 command+=
" -D__DEC32_MAX__=9.999999E96DF";
666 command+=
" -D__DECIMAL_DIG__=21";
667 command+=
" -D__LDBL_HAS_QUIET_NAN__=1";
668 command+=
" -D__DYNAMIC__=1";
669 command+=
" -D__GNUC__=4";
670 command+=
" -D__FLT_HAS_DENORM__=1";
671 command+=
" -D__DBL_MAX__=1.7976931348623157e+308";
672 command+=
" -D__DBL_HAS_INFINITY__=1";
673 command+=
" -D__DEC32_MIN_EXP__=\"(-95)\"";
674 command+=
" -D__LDBL_HAS_DENORM__=1";
675 command+=
" -D__DEC32_MIN__=1E-95DF";
676 command+=
" -D__DBL_MAX_EXP__=1024";
677 command+=
" -D__DEC128_EPSILON__=1E-33DL";
678 command+=
" -D__SSE2_MATH__=1";
679 command+=
" -D__GXX_ABI_VERSION=1002";
680 command+=
" -D__FLT_MIN_EXP__=\"(-125)\"";
681 command+=
" -D__DBL_MIN__=2.2250738585072014e-308";
682 command+=
" -D__DBL_HAS_QUIET_NAN__=1";
683 command+=
" -D__DEC128_MIN__=1E-6143DL";
684 command+=
" -D__REGISTER_PREFIX__=";
685 command+=
" -D__DBL_HAS_DENORM__=1";
686 command+=
" -D__DEC_EVAL_METHOD__=2";
687 command+=
" -D__DEC128_MAX__=9.999999999999999999999999999999999E6144DL";
688 command+=
" -D__FLT_MANT_DIG__=24";
689 command+=
" -D__DEC64_EPSILON__=1E-15DD";
690 command+=
" -D__DEC128_MIN_EXP__=\"(-6143)\"";
691 command+=
" -D__DEC32_SUBNORMAL_MIN__=0.000001E-95DF";
692 command+=
" -D__FLT_RADIX__=2";
693 command+=
" -D__LDBL_EPSILON__=1.08420217248550443401e-19L";
694 command+=
" -D__k8=1";
695 command+=
" -D__LDBL_DIG__=18";
696 command+=
" -D__FLT_HAS_QUIET_NAN__=1";
697 command+=
" -D__FLT_MAX_10_EXP__=38";
698 command+=
" -D__FLT_HAS_INFINITY__=1";
699 command+=
" -D__DEC64_MAX__=9.999999999999999E384DD";
700 command+=
" -D__DEC64_MANT_DIG__=16";
701 command+=
" -D__DEC32_MAX_EXP__=96";
703 command+=
" -D__DEC128_SUBNORMAL_MIN__=0.000000000000000000000000000000001E-6143DL";
704 command+=
" -D__LDBL_MANT_DIG__=64";
705 command+=
" -D__CONSTANT_CFSTRINGS__=1";
706 command+=
" -D__DEC32_MANT_DIG__=7";
707 command+=
" -D__k8__=1";
708 command+=
" -D__pic__=2";
709 command+=
" -D__FLT_DIG__=6";
710 command+=
" -D__FLT_MAX_EXP__=128";
712 command+=
" -D__DBL_MANT_DIG__=53";
713 command+=
" -D__DEC64_MIN__=1E-383DD";
714 command+=
" -D__LDBL_MIN_EXP__=\"(-16381)\"";
715 command+=
" -D__LDBL_MAX_EXP__=16384";
716 command+=
" -D__LDBL_MAX_10_EXP__=4932";
717 command+=
" -D__DBL_EPSILON__=2.2204460492503131e-16";
718 command+=
" -D__GNUC_PATCHLEVEL__=1";
719 command+=
" -D__LDBL_HAS_INFINITY__=1";
720 command+=
" -D__INTMAX_MAX__=9223372036854775807L";
721 command+=
" -D__FLT_DENORM_MIN__=1.40129846e-45F";
722 command+=
" -D__PIC__=2";
723 command+=
" -D__FLT_MAX__=3.40282347e+38F";
724 command+=
" -D__FLT_MIN_10_EXP__=\"(-37)\"";
725 command+=
" -D__DEC128_MAX_EXP__=6144";
726 command+=
" -D__GNUC_MINOR__=2";
727 command+=
" -D__DBL_MAX_10_EXP__=308";
728 command+=
" -D__LDBL_DENORM_MIN__=3.64519953188247460253e-4951L";
729 command+=
" -D__DEC128_MANT_DIG__=34";
730 command+=
" -D__LDBL_MIN_10_EXP__=\"(-4931)\"";
734 command+=
" -D_Noreturn=\"__attribute__((__noreturn__))\"";
735 command+=
" -D__llvm__";
736 command+=
" -D__clang__";
761 command+=
" -D__WCHAR_TYPE__=\""+sig+
" short int\"";
763 command+=
" -D__WCHAR_TYPE__=\""+sig+
" int\"";
765 command+=
" -D__WCHAR_TYPE__=\""+sig+
" long int\"";
767 command+=
" -D__WCHAR_TYPE__=\""+sig+
" char\"";
773 command+=
" -D __CHAR_UNSIGNED__";
778 command+=
" -Dlinux -D__linux -D__linux__ -D__gnu_linux__";
779 command+=
" -Dunix -D__unix -D__unix__";
780 command+=
" -D__USE_UNIX98";
784 command+=
" -D__APPLE__ -D__MACH__";
786 command+=
" -D__APPLE_CC__";
790 command+=
" -D _WIN32";
793 command+=
" -D _M_IX86=Blend";
796 command+=
" -D _WIN64";
799 command+=
" -D _CHAR_UNSIGNED";
803 command+=
" -nostdinc";
817 command +=
" -D __STDC_VERSION__=199901L";
821 command +=
" -D __STDC_VERSION__=201112L";
825 command +=
" -D __STDC_IEC_559__=1";
826 command +=
" -D __STDC_IEC_559_COMPLEX__=1";
827 command +=
" -D __STDC_ISO_10646__=1";
847 case configt::ansi_ct::flavourt::GCC_C: command+=
" -x c";
break;
848 case configt::ansi_ct::flavourt::GCC_CPP: command+=
" -x c++";
break;
857 command+=
" \""+file+
"\"";
858 command+=
" -o \""+tmpi+
"\"";
859 command+=
" 2> \""+stderr_file+
"\"";
863 result=system(command.c_str());
865 std::ifstream instream(tmpi);
868 std::ifstream stderr_stream(stderr_file);
871 unlink(stderr_file.c_str());
875 outstream << instream.rdbuf();
877 unlink(tmpi.c_str());
881 unlink(tmpi.c_str());
882 message.
error() <<
"GCC preprocessing failed (open failed)" 887 command+=
" \""+file+
"\"";
888 command+=
" 2> \""+stderr_file+
"\"";
890 FILE *stream=popen(command.c_str(),
"r");
895 while((ch=fgetc(stream))!=EOF)
896 outstream << (
unsigned char)ch;
898 result=pclose(stream);
902 message.
error() <<
"GCC preprocessing failed (popen failed)" 908 std::ifstream stderr_stream(stderr_file);
911 unlink(stderr_file.c_str());
926 const std::string &
file,
927 std::ostream &outstream,
941 command=
"armcc -E -D__CPROVER__";
971 command+=
" -D__STDC__";
984 command+=
" \""+file+
"\"";
985 command+=
" > \""+tmpi+
"\"";
986 command+=
" 2> \""+stderr_file+
"\"";
990 result=system(command.c_str());
992 std::ifstream instream(tmpi);
996 outstream << instream.rdbuf();
998 unlink(tmpi.c_str());
1002 unlink(tmpi.c_str());
1003 unlink(stderr_file.c_str());
1004 message.
error() <<
"ARMCC preprocessing failed (fopen failed)" 1009 command+=
" \""+file+
"\"";
1010 command+=
" 2> \""+stderr_file+
"\"";
1012 FILE *stream=popen(command.c_str(),
"r");
1017 while((ch=fgetc(stream))!=EOF)
1018 outstream << (
unsigned char)ch;
1020 result=pclose(stream);
1024 unlink(stderr_file.c_str());
1025 message.
error() <<
"ARMCC preprocessing failed (popen failed)" 1032 std::ifstream stderr_stream(stderr_file);
1035 unlink(stderr_file.c_str());
1048 const std::string &
file,
1049 std::ostream &outstream,
1053 std::ifstream infile(
widen(file));
1055 std::ifstream infile(file);
1074 while(infile.read(&ch, 1))
1083 "#include <stdlib.h>\n" 1089 std::ostringstream out;
The type of an expression.
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 integer2string(const mp_integer &n, unsigned base)
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)
preprocessort preprocessor
const irep_idt & id() const
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)
void set_column(const irep_idt &column)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
void postprocess_codewarrior(std::istream &instream, std::ostream &outstream)
post-processing specifically for CodeWarrior
static std::string type_max(const typet &src)
produce a string with the maximum value of a given type
bool has_prefix(const std::string &s, const std::string &prefix)
enum configt::ansi_ct::c_standardt c_standard
bool test_c_preprocessor(message_handlert &message_handler)
bitvector_typet wchar_t_type()
const char c_test_program[]
tests ANSI-C preprocessing
static void error_parse(std::istream &errors, bool warning_only, messaget &message)
#define GCC_DEFINES_LLP64
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
static void error_parse_line(const std::string &line, bool warning_only, messaget &message)
std::list< std::string > preprocessor_options
bool c_preprocess_none(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
std::list< std::string > include_paths