Skip to content

Commit 4b9de00

Browse files
author
Daniel Kroening
committed
use compiler defaults for gcc defines
1 parent a4389fe commit 4b9de00

File tree

1 file changed

+24
-300
lines changed

1 file changed

+24
-300
lines changed

‎src/ansi-c/c_preprocess.cpp

+24-300
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,13 @@ Author: Daniel Kroening, [email protected]
88

99
#include "c_preprocess.h"
1010

11-
#include <cstdio>
12-
#include <cstdlib>
11+
#include <util/c_types.h>
12+
#include <util/config.h>
13+
#include <util/suffix.h>
14+
#include <util/tempfile.h>
15+
1316
#include <cstring>
17+
#include <fstream>
1418

1519
#if defined(__linux__) || \
1620
defined(__FreeBSD_kernel__) || \
@@ -21,95 +25,6 @@ Author: Daniel Kroening, [email protected]
2125
#include <unistd.h>
2226
#endif
2327

24-
#include <fstream>
25-
26-
#include <util/c_types.h>
27-
#include <util/config.h>
28-
#include <util/invariant.h>
29-
#include <util/message.h>
30-
#include <util/tempfile.h>
31-
#include <util/unicode.h>
32-
#include <util/arith_tools.h>
33-
#include <util/std_types.h>
34-
#include <util/prefix.h>
35-
36-
#define GCC_DEFINES_16 \
37-
" -D__INT_MAX__=32767"\
38-
" -D__CHAR_BIT__=8"\
39-
" -D__SCHAR_MAX__=127"\
40-
" -D__SHRT_MAX__=32767"\
41-
" -D__INT32_TYPE__=long"\
42-
" -D__LONG_LONG_MAX__=2147483647L"\
43-
" -D__LONG_MAX__=2147483647" \
44-
" -D__SIZE_TYPE__=\"unsigned int\""\
45-
" -D__PTRDIFF_TYPE__=int"\
46-
" -D__WINT_TYPE__=\"unsigned int\""\
47-
" -D__INTMAX_TYPE__=\"long long int\""\
48-
" -D__UINTMAX_TYPE__=\"long long unsigned int\""\
49-
" -D__INTPTR_TYPE__=\"int\""\
50-
" -D__UINTPTR_TYPE__=\"unsigned int\""
51-
52-
#define GCC_DEFINES_32 \
53-
" -D__INT_MAX__=2147483647"\
54-
" -D__CHAR_BIT__=8"\
55-
" -D__SCHAR_MAX__=127"\
56-
" -D__SHRT_MAX__=32767"\
57-
" -D__INT32_TYPE__=int"\
58-
" -D__LONG_LONG_MAX__=9223372036854775807LL"\
59-
" -D__LONG_MAX__=2147483647L" \
60-
" -D__SIZE_TYPE__=\"long unsigned int\""\
61-
" -D__PTRDIFF_TYPE__=int"\
62-
" -D__WINT_TYPE__=\"unsigned int\""\
63-
" -D__INTMAX_TYPE__=\"long long int\""\
64-
" -D__UINTMAX_TYPE__=\"long long unsigned int\""\
65-
" -D__INTPTR_TYPE__=\"long int\""\
66-
" -D__UINTPTR_TYPE__=\"long unsigned int\""
67-
68-
#define GCC_DEFINES_LP64 \
69-
" -D__INT_MAX__=2147483647"\
70-
" -D__CHAR_BIT__=8"\
71-
" -D__SCHAR_MAX__=127"\
72-
" -D__SHRT_MAX__=32767"\
73-
" -D__INT32_TYPE__=int"\
74-
" -D__LONG_LONG_MAX__=9223372036854775807LL"\
75-
" -D__LONG_MAX__=9223372036854775807L"\
76-
" -D__SIZE_TYPE__=\"long unsigned int\""\
77-
" -D__PTRDIFF_TYPE__=long"\
78-
" -D__WINT_TYPE__=\"unsigned int\""\
79-
" -D__INTMAX_TYPE__=\"long int\""\
80-
" -D__UINTMAX_TYPE__=\"long unsigned int\""\
81-
" -D__INTPTR_TYPE__=\"long int\""\
82-
" -D__UINTPTR_TYPE__=\"long unsigned int\""
83-
84-
#define GCC_DEFINES_LLP64 \
85-
" -D__INT_MAX__=2147483647"\
86-
" -D__CHAR_BIT__=8"\
87-
" -D__SCHAR_MAX__=127"\
88-
" -D__SHRT_MAX__=32767"\
89-
" -D__INT32_TYPE__=int"\
90-
" -D__LONG_LONG_MAX__=9223372036854775807LL"\
91-
" -D__LONG_MAX__=2147483647"\
92-
" -D__SIZE_TYPE__=\"long long unsigned int\""\
93-
" -D__PTRDIFF_TYPE__=\"long long\""\
94-
" -D__WINT_TYPE__=\"unsigned int\""\
95-
" -D__INTMAX_TYPE__=\"long long int\""\
96-
" -D__UINTMAX_TYPE__=\"long long unsigned int\""\
97-
" -D__INTPTR_TYPE__=\"long long int\""\
98-
" -D__UINTPTR_TYPE__=\"long long unsigned int\""
99-
100-
/// produce a string with the maximum value of a given type
101-
static std::string type_max(const typet &src)
102-
{
103-
if(src.id()==ID_signedbv)
104-
return integer2string(
105-
power(2, to_signedbv_type(src).get_width()-1)-1);
106-
else if(src.id()==ID_unsignedbv)
107-
return integer2string(
108-
power(2, to_unsignedbv_type(src).get_width()-1)-1);
109-
else
110-
UNREACHABLE;
111-
}
112-
11328
/// quote a string for bash and CMD
11429
static std::string shell_quote(const std::string &src)
11530
{
@@ -344,13 +259,7 @@ bool c_preprocess(
344259
/// ANSI-C preprocessing
345260
static bool is_dot_i_file(const std::string &path)
346261
{
347-
const char *ext=strrchr(path.c_str(), '.');
348-
if(ext==nullptr)
349-
return false;
350-
if(std::string(ext)==".i" ||
351-
std::string(ext)==".ii")
352-
return true;
353-
return false;
262+
return has_suffix(path, ".i") || has_suffix(path, ".ii");
354263
}
355264

356265
/// ANSI-C preprocessing
@@ -422,7 +331,7 @@ bool c_preprocess_visual_studio(
422331
{
423332
std::ofstream command_file(command_file_name);
424333

425-
// This marks the file as UTF-8, which Visual Studio
334+
// This marks the command file as UTF-8, which Visual Studio
426335
// understands.
427336
command_file << char(0xef) << char(0xbb) << char(0xbf);
428337

@@ -456,12 +365,6 @@ bool c_preprocess_visual_studio(
456365
if(config.ansi_c.char_is_unsigned)
457366
command_file << "/J" << "\n"; // This causes _CHAR_UNSIGNED to be defined
458367

459-
// Standard Defines, ANSI9899 6.10.8
460-
command_file << "/D__STDC_VERSION__=199901L" << "\n";
461-
command_file << "/D__STDC_IEC_559__=1" << "\n";
462-
command_file << "/D__STDC_IEC_559_COMPLEX__=1" << "\n";
463-
command_file << "/D__STDC_ISO_10646__=1" << "\n";
464-
465368
for(const auto &define : config.ansi_c.defines)
466369
command_file << "/D" << shell_quote(define) << "\n";
467370

@@ -651,192 +554,44 @@ bool c_preprocess_gcc_clang(
651554
else
652555
command="gcc";
653556

654-
command +=" -E -undef -D__CPROVER__";
655-
656-
command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
657-
658-
command+=" -D__DBL_MIN_EXP__=\"(-1021)\"";
659-
command+=" -D__FLT_MIN__=1.17549435e-38F";
660-
command+=" -D__DEC64_SUBNORMAL_MIN__=0.000000000000001E-383DD";
661-
command+=" -D__CHAR_BIT__=8";
662-
command+=" -D__DBL_DENORM_MIN__=4.9406564584124654e-324";
663-
command+=" -D__FLT_EVAL_METHOD__=0";
664-
command+=" -D__DBL_MIN_10_EXP__=\"(-307)\"";
665-
command+=" -D__FINITE_MATH_ONLY__=0";
666-
command+=" -D__DEC64_MAX_EXP__=384";
667-
command+=" -D__SHRT_MAX__=32767";
668-
command+=" -D__LDBL_MAX__=1.18973149535723176502e+4932L";
669-
command+=" -D__DEC32_EPSILON__=1E-6DF";
670-
command+=" -D__SCHAR_MAX__=127";
671-
command+=" -D__USER_LABEL_PREFIX__=_";
672-
command+=" -D__DEC64_MIN_EXP__=\"(-383)\"";
673-
command+=" -D__DBL_DIG__=15";
674-
command+=" -D__FLT_EPSILON__=1.19209290e-7F";
675-
command+=" -D__LDBL_MIN__=3.36210314311209350626e-4932L";
676-
command+=" -D__DEC32_MAX__=9.999999E96DF";
677-
command+=" -D__DECIMAL_DIG__=21";
678-
command+=" -D__LDBL_HAS_QUIET_NAN__=1";
679-
command+=" -D__DYNAMIC__=1";
680-
command+=" -D__GNUC__=4";
681-
command+=" -D__FLT_HAS_DENORM__=1";
682-
command+=" -D__DBL_MAX__=1.7976931348623157e+308";
683-
command+=" -D__DBL_HAS_INFINITY__=1";
684-
command+=" -D__DEC32_MIN_EXP__=\"(-95)\"";
685-
command+=" -D__LDBL_HAS_DENORM__=1";
686-
command+=" -D__DEC32_MIN__=1E-95DF";
687-
command+=" -D__DBL_MAX_EXP__=1024";
688-
command+=" -D__DEC128_EPSILON__=1E-33DL";
689-
command+=" -D__SSE2_MATH__=1";
690-
command+=" -D__GXX_ABI_VERSION=1002";
691-
command+=" -D__FLT_MIN_EXP__=\"(-125)\"";
692-
command+=" -D__DBL_MIN__=2.2250738585072014e-308";
693-
command+=" -D__DBL_HAS_QUIET_NAN__=1";
694-
command+=" -D__DEC128_MIN__=1E-6143DL";
695-
command+=" -D__REGISTER_PREFIX__=";
696-
command+=" -D__DBL_HAS_DENORM__=1";
697-
command+=" -D__DEC_EVAL_METHOD__=2";
698-
command+=" -D__DEC128_MAX__=9.999999999999999999999999999999999E6144DL";
699-
command+=" -D__FLT_MANT_DIG__=24";
700-
command+=" -D__DEC64_EPSILON__=1E-15DD";
701-
command+=" -D__DEC128_MIN_EXP__=\"(-6143)\"";
702-
command+=" -D__DEC32_SUBNORMAL_MIN__=0.000001E-95DF";
703-
command+=" -D__FLT_RADIX__=2";
704-
command+=" -D__LDBL_EPSILON__=1.08420217248550443401e-19L";
705-
command+=" -D__k8=1";
706-
command+=" -D__LDBL_DIG__=18";
707-
command+=" -D__FLT_HAS_QUIET_NAN__=1";
708-
command+=" -D__FLT_MAX_10_EXP__=38";
709-
command+=" -D__FLT_HAS_INFINITY__=1";
710-
command+=" -D__DEC64_MAX__=9.999999999999999E384DD";
711-
command+=" -D__DEC64_MANT_DIG__=16";
712-
command+=" -D__DEC32_MAX_EXP__=96";
713-
// NOLINTNEXTLINE(whitespace/line_length)
714-
command+=" -D__DEC128_SUBNORMAL_MIN__=0.000000000000000000000000000000001E-6143DL";
715-
command+=" -D__LDBL_MANT_DIG__=64";
716-
command+=" -D__CONSTANT_CFSTRINGS__=1";
717-
command+=" -D__DEC32_MANT_DIG__=7";
718-
command+=" -D__k8__=1";
719-
command+=" -D__pic__=2";
720-
command+=" -D__FLT_DIG__=6";
721-
command+=" -D__FLT_MAX_EXP__=128";
722-
// command+=" -D__BLOCKS__=1";
723-
command+=" -D__DBL_MANT_DIG__=53";
724-
command+=" -D__DEC64_MIN__=1E-383DD";
725-
command+=" -D__LDBL_MIN_EXP__=\"(-16381)\"";
726-
command+=" -D__LDBL_MAX_EXP__=16384";
727-
command+=" -D__LDBL_MAX_10_EXP__=4932";
728-
command+=" -D__DBL_EPSILON__=2.2204460492503131e-16";
729-
command+=" -D__GNUC_PATCHLEVEL__=1";
730-
command+=" -D__LDBL_HAS_INFINITY__=1";
731-
command+=" -D__INTMAX_MAX__=9223372036854775807L";
732-
command+=" -D__FLT_DENORM_MIN__=1.40129846e-45F";
733-
command+=" -D__PIC__=2";
734-
command+=" -D__FLT_MAX__=3.40282347e+38F";
735-
command+=" -D__FLT_MIN_10_EXP__=\"(-37)\"";
736-
command+=" -D__DEC128_MAX_EXP__=6144";
737-
command+=" -D__GNUC_MINOR__=2";
738-
command+=" -D__DBL_MAX_10_EXP__=308";
739-
command+=" -D__LDBL_DENORM_MIN__=3.64519953188247460253e-4951L";
740-
command+=" -D__DEC128_MANT_DIG__=34";
741-
command+=" -D__LDBL_MIN_10_EXP__=\"(-4931)\"";
557+
command +=" -E -D__CPROVER__";
558+
559+
if(config.ansi_c.pointer_width==16)
560+
command+=" -m16";
561+
else if(config.ansi_c.pointer_width==32)
562+
command+=" -m32";
563+
else if(config.ansi_c.pointer_width==64)
564+
command+=" -m64";
742565

743566
if(preprocessor==configt::ansi_ct::preprocessort::CLANG)
744567
{
568+
// not sure about the below
745569
command+=" -D_Noreturn=\"__attribute__((__noreturn__))\"";
746-
command+=" -D__llvm__";
747-
command+=" -D__clang__";
748-
}
749-
750-
if(config.ansi_c.int_width==16)
751-
command+=GCC_DEFINES_16;
752-
else if(config.ansi_c.int_width==32)
753-
{
754-
if(config.ansi_c.pointer_width==64)
755-
{
756-
if(config.ansi_c.long_int_width==32)
757-
command+=GCC_DEFINES_LLP64; // Windows, for instance
758-
else
759-
command+=GCC_DEFINES_LP64;
760-
}
761-
else
762-
command+=GCC_DEFINES_32;
763570
}
764571

765572
// The width of wchar_t depends on the OS!
766-
{
767-
command+=" -D__WCHAR_MAX__="+type_max(wchar_t_type());
768-
769-
std::string sig=config.ansi_c.wchar_t_is_unsigned?"unsigned":"signed";
770-
771-
if(config.ansi_c.wchar_t_width==config.ansi_c.short_int_width)
772-
command+=" -D__WCHAR_TYPE__=\""+sig+" short int\"";
773-
else if(config.ansi_c.wchar_t_width==config.ansi_c.int_width)
774-
command+=" -D__WCHAR_TYPE__=\""+sig+" int\"";
775-
else if(config.ansi_c.wchar_t_width==config.ansi_c.long_int_width)
776-
command+=" -D__WCHAR_TYPE__=\""+sig+" long int\"";
777-
else if(config.ansi_c.wchar_t_width==config.ansi_c.char_width)
778-
command+=" -D__WCHAR_TYPE__=\""+sig+" char\"";
779-
else
780-
UNREACHABLE;
781-
}
573+
if(config.ansi_c.wchar_t_width==config.ansi_c.short_int_width)
574+
command+=" -fshort-wchar";
782575

783576
if(config.ansi_c.char_is_unsigned)
784-
command+=" -D __CHAR_UNSIGNED__"; // gcc
785-
786-
switch(config.ansi_c.os)
787-
{
788-
case configt::ansi_ct::ost::OS_LINUX:
789-
command+=" -Dlinux -D__linux -D__linux__ -D__gnu_linux__";
790-
command+=" -Dunix -D__unix -D__unix__";
791-
command+=" -D__USE_UNIX98";
792-
break;
793-
794-
case configt::ansi_ct::ost::OS_MACOS:
795-
command+=" -D__APPLE__ -D__MACH__";
796-
// needs to be __APPLE_CPP__ for C++
797-
command+=" -D__APPLE_CC__";
798-
break;
799-
800-
case configt::ansi_ct::ost::OS_WIN:
801-
command+=" -D _WIN32";
802-
803-
if(config.ansi_c.mode!=configt::ansi_ct::flavourt::VISUAL_STUDIO)
804-
command+=" -D _M_IX86=Blend";
805-
806-
if(config.ansi_c.arch=="x86_64")
807-
command+=" -D _WIN64"; // yes, both _WIN32 and _WIN64 get defined
808-
809-
if(config.ansi_c.char_is_unsigned)
810-
command+=" -D _CHAR_UNSIGNED"; // This is Visual Studio
811-
break;
812-
813-
case configt::ansi_ct::ost::NO_OS:
814-
command+=" -nostdinc"; // make sure we don't mess with the system library
815-
break;
816-
817-
default:
818-
UNREACHABLE;
819-
}
577+
command+=" -funsigned-char";
820578

821579
// Standard Defines, ANSI9899 6.10.8
822580
switch(config.ansi_c.c_standard)
823581
{
824582
case configt::ansi_ct::c_standardt::C89:
825-
break; // __STDC_VERSION__ is not defined
583+
command+=" -std=c89";
584+
break;
826585

827586
case configt::ansi_ct::c_standardt::C99:
828-
command += " -D __STDC_VERSION__=199901L";
587+
command+=" -std=c99";
829588
break;
830589

831590
case configt::ansi_ct::c_standardt::C11:
832-
command += " -D __STDC_VERSION__=201112L";
591+
command+=" -std=c11";
833592
break;
834593
}
835594

836-
command += " -D __STDC_IEC_559__=1";
837-
command += " -D __STDC_IEC_559_COMPLEX__=1";
838-
command += " -D __STDC_ISO_10646__=1";
839-
840595
for(const auto &define : config.ansi_c.defines)
841596
command+=" -D"+shell_quote(define);
842597

@@ -951,37 +706,6 @@ bool c_preprocess_arm(
951706

952707
command="armcc -E -D__CPROVER__";
953708

954-
// command+=" -D__sizeof_int="+std::to_string(config.ansi_c.int_width/8);
955-
// command+=" -D__sizeof_long="+std::to_string(config.ansi_c.long_int_width/8);
956-
// command+=" -D__sizeof_ptr="+std::to_string(config.ansi_c.pointer_width/8);
957-
// command+=" -D__EDG_VERSION__=308";
958-
// command+=" -D__EDG__";
959-
// command+=" -D__CC_ARM=1";
960-
// command+=" -D__ARMCC_VERSION=410000";
961-
// command+=" -D__arm__";
962-
963-
// if(config.ansi_c.endianness==configt::ansi_ct::IS_BIG_ENDIAN)
964-
// command+=" -D__BIG_ENDIAN";
965-
966-
// if(config.ansi_c.char_is_unsigned)
967-
// command+=" -D__CHAR_UNSIGNED__";
968-
969-
if(config.ansi_c.os!=configt::ansi_ct::ost::OS_WIN)
970-
{
971-
command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
972-
973-
if(config.ansi_c.int_width==16)
974-
command+=GCC_DEFINES_16;
975-
else if(config.ansi_c.int_width==32)
976-
command+=GCC_DEFINES_32;
977-
else if(config.ansi_c.int_width==64)
978-
command+=GCC_DEFINES_LP64;
979-
}
980-
981-
// Standard Defines, ANSI9899 6.10.8
982-
command+=" -D__STDC__";
983-
// command+=" -D__STDC_VERSION__=199901L";
984-
985709
for(const auto &define : config.ansi_c.defines)
986710
command+=" "+shell_quote("-D"+define);
987711

0 commit comments

Comments
 (0)