Skip to content

Commit da589ff

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

File tree

2 files changed

+31
-302
lines changed

2 files changed

+31
-302
lines changed

‎src/ansi-c/c_preprocess.cpp

+26-301
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,14 @@ 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+
#include <util/unicode.h>
16+
1317
#include <cstring>
18+
#include <fstream>
1419

1520
#if defined(__linux__) || \
1621
defined(__FreeBSD_kernel__) || \
@@ -21,95 +26,6 @@ Author: Daniel Kroening, [email protected]
2126
#include <unistd.h>
2227
#endif
2328

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-
11329
/// quote a string for bash and CMD
11430
static std::string shell_quote(const std::string &src)
11531
{
@@ -344,13 +260,7 @@ bool c_preprocess(
344260
/// ANSI-C preprocessing
345261
static bool is_dot_i_file(const std::string &path)
346262
{
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;
263+
return has_suffix(path, ".i") || has_suffix(path, ".ii");
354264
}
355265

356266
/// ANSI-C preprocessing
@@ -422,7 +332,7 @@ bool c_preprocess_visual_studio(
422332
{
423333
std::ofstream command_file(command_file_name);
424334

425-
// This marks the file as UTF-8, which Visual Studio
335+
// This marks the command file as UTF-8, which Visual Studio
426336
// understands.
427337
command_file << char(0xef) << char(0xbb) << char(0xbf);
428338

@@ -456,12 +366,6 @@ bool c_preprocess_visual_studio(
456366
if(config.ansi_c.char_is_unsigned)
457367
command_file << "/J" << "\n"; // This causes _CHAR_UNSIGNED to be defined
458368

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-
465369
for(const auto &define : config.ansi_c.defines)
466370
command_file << "/D" << shell_quote(define) << "\n";
467371

@@ -651,192 +555,44 @@ bool c_preprocess_gcc_clang(
651555
else
652556
command="gcc";
653557

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)\"";
558+
command +=" -E -D__CPROVER__";
559+
560+
if(config.ansi_c.pointer_width==16)
561+
command+=" -m16";
562+
else if(config.ansi_c.pointer_width==32)
563+
command+=" -m32";
564+
else if(config.ansi_c.pointer_width==64)
565+
command+=" -m64";
742566

743567
if(preprocessor==configt::ansi_ct::preprocessort::CLANG)
744568
{
569+
// not sure about the below
745570
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;
763571
}
764572

765573
// 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-
}
574+
if(config.ansi_c.wchar_t_width==config.ansi_c.short_int_width)
575+
command+=" -fshort-wchar";
782576

783577
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;
578+
command+=" -funsigned-char";
799579

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-
}
820-
821-
// Standard Defines, ANSI9899 6.10.8
580+
// Set the standard
822581
switch(config.ansi_c.c_standard)
823582
{
824583
case configt::ansi_ct::c_standardt::C89:
825-
break; // __STDC_VERSION__ is not defined
584+
command+=" -std=gnu89";
585+
break;
826586

827587
case configt::ansi_ct::c_standardt::C99:
828-
command += " -D __STDC_VERSION__=199901L";
588+
command+=" -std=gnu99";
829589
break;
830590

831591
case configt::ansi_ct::c_standardt::C11:
832-
command += " -D __STDC_VERSION__=201112L";
592+
command+=" -std=gnu11";
833593
break;
834594
}
835595

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

@@ -951,37 +707,6 @@ bool c_preprocess_arm(
951707

952708
command="armcc -E -D__CPROVER__";
953709

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-
985710
for(const auto &define : config.ansi_c.defines)
986711
command+=" "+shell_quote("-D"+define);
987712

0 commit comments

Comments
 (0)