CBMC
Loading...
Searching...
No Matches
gcc_version.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: GCC Mode
4
5Author: Daniel Kroening, 2018
6
7\*******************************************************************/
8
9#include "gcc_version.h"
10
11#include <util/run.h>
12#include <util/string2int.h>
13#include <util/string_utils.h>
14#include <util/tempfile.h>
15
16#include <fstream>
17
18void gcc_versiont::get(const std::string &executable)
19{
20 temporary_filet tmp_file_in("goto-gcc.", ".in");
21 temporary_filet tmp_file_out("goto-gcc.", ".out");
22 temporary_filet tmp_file_err("goto-gcc.", ".err");
23
24 {
25 std::ofstream out(tmp_file_in());
26
27 out << "#if defined(__clang_major__)\n"
28 "clang __clang_major__ __clang_minor__ __clang_patchlevel__\n"
29 "#elif defined(__BCC__)\n"
30 "bcc 0 0 0\n"
31 "#else\n"
32 "gcc __GNUC__ __GNUC_MINOR__ __GNUC_PATCHLEVEL__\n"
33 "#endif\n"
34 "default_c_standard __STDC_VERSION__\n";
35 }
36
37 // some variants output stuff on stderr, say Apple LLVM,
38 // which we silence.
39 int result = run(
41 {executable, "-E", "-", "-o", "-"},
44 tmp_file_err());
45
48
49 if(result >= 0)
50 {
51 std::ifstream in(tmp_file_out());
52 std::string line;
53
54 while(!in.fail() && std::getline(in, line))
55 {
56 if(line.empty() || line[0] == '#')
57 continue;
58
59 auto split = split_string(line, ' ');
60
61 if(split.size() >= 4)
62 {
63 if(split[0] == "gcc")
65 else if(split[0] == "bcc")
67 else if(split[0] == "clang")
69
73 }
74 else if(split.size() == 2 && split[0] == "default_c_standard")
75 {
76 if(split[1] == "199901L")
78 else if(split[1] == "201112L")
80 else if(split[1] == "201710L")
82 else if(split[1] == "202000L" || split[1] == "202311L")
84 }
85 }
86
88 {
89 // Grab the default C++ standard. Unfortunately this requires another
90 // run, as the compiler can't preprocess two files in one go.
91
92 temporary_filet cpp_in("goto-gcc.", ".cpp");
93 temporary_filet cpp_out("goto-gcc.", ".out");
94 temporary_filet cpp_err("goto-gcc.", ".err");
95
96 {
97 std::ofstream out(cpp_in());
98 out << "default_cxx_standard __cplusplus\n";
99 }
100
101 result = run(
103 {executable, "-E", "-x", "c++", "-", "-o", "-"},
104 cpp_in(),
105 cpp_out(),
106 cpp_err());
107
108 if(result >= 0)
109 {
110 std::ifstream in2(cpp_out());
111
112 while(!in2.fail() && std::getline(in2, line))
113 {
114 if(line.empty() || line[0] == '#')
115 continue;
116
117 auto split = split_string(line, ' ');
118
119 if(split.size() == 2 && split[0] == "default_cxx_standard")
120 {
121 if(split[1] == "199711L")
123 else if(split[1] == "201103L")
125 else if(split[1] == "201402L")
127 else if(split[1] == "201703L")
129 }
130 }
131 }
132 }
133 }
134}
135
137 unsigned _major,
138 unsigned _minor,
139 unsigned _patchlevel) const
140{
141 return v_major > _major || (v_major == _major && v_minor > _minor) ||
142 (v_major == _major && v_minor == _minor &&
144}
145
146std::ostream &operator<<(std::ostream &out, const gcc_versiont &v)
147{
148 return out << v.v_major << '.' << v.v_minor << '.' << v.v_patchlevel;
149}
150
151void configure_gcc(const gcc_versiont &gcc_version)
152{
153 // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
154 if(
155 gcc_version.flavor == gcc_versiont::flavort::GCC &&
156 gcc_version.is_at_least(7u))
157 {
158 config.ansi_c.ts_18661_3_Floatn_types = true;
159 }
160
161 const auto gcc_float128_minor_version =
162 config.ansi_c.arch == "x86_64" ? 3u : 5u;
163
164 // __float128 exists (as a typedef) since gcc 4.5 everywhere,
165 // and since 4.3 on x86_64
166 config.ansi_c.gcc__float128_type =
167 gcc_version.flavor == gcc_versiont::flavort::GCC &&
169 config.ansi_c.__float128_is_keyword =
170 gcc_version.flavor == gcc_versiont::flavort::CLANG ||
171 (gcc_version.flavor == gcc_versiont::flavort::GCC &&
172 config.ansi_c.arch == "arm64" &&
174 config.ansi_c.gcc__float128_type);
175
176 config.ansi_c.float16_type =
177 (gcc_version.flavor == gcc_versiont::flavort::GCC &&
178 gcc_version.is_at_least(12u)) ||
179 (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
180 gcc_version.is_at_least(15u));
181
182 config.ansi_c.bf16_type =
183 (gcc_version.flavor == gcc_versiont::flavort::GCC &&
184 gcc_version.is_at_least(13u)) ||
185 (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
186 gcc_version.is_at_least(15u));
187
188 config.ansi_c.fp16_type =
189 (gcc_version.flavor == gcc_versiont::flavort::GCC &&
190 gcc_version.is_at_least(4u, 5u) &&
191 (config.ansi_c.arch == "arm" || config.ansi_c.arch == "arm64")) ||
192 (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
193 gcc_version.is_at_least(6u));
194}
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
struct configt::ansi_ct ansi_c
bool is_at_least(unsigned v_major, unsigned v_minor=0, unsigned v_patchlevel=0) const
void get(const std::string &executable)
configt::cppt::cpp_standardt default_cxx_standard
Definition gcc_version.h:40
configt::ansi_ct::c_standardt default_c_standard
Definition gcc_version.h:39
unsigned v_patchlevel
Definition gcc_version.h:22
unsigned v_minor
Definition gcc_version.h:22
unsigned v_major
Definition gcc_version.h:22
enum gcc_versiont::flavort flavor
std::ostream & operator<<(std::ostream &out, const gcc_versiont &v)
void configure_gcc(const gcc_versiont &gcc_version)
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:48
unsigned unsafe_string2unsigned(const std::string &str, int base)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)