CBMC
Loading...
Searching...
No Matches
cpp_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Module
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include "cpp_language.h"
13
14#include <util/config.h>
15#include <util/get_base_name.h>
16#include <util/symbol_table.h>
17
19#include <ansi-c/c_preprocess.h>
20#include <linking/linking.h>
22
24#include "cpp_parser.h"
25#include "cpp_type2name.h"
26#include "cpp_typecheck.h"
27#include "expr2cpp.h"
28
29#include <cstring>
30#include <fstream>
31
32std::set<std::string> cpp_languaget::extensions() const
33{
34 std::set<std::string> s;
35
36 s.insert("cpp");
37 s.insert("CPP");
38 s.insert("cc");
39 s.insert("cp");
40 s.insert("c++");
41 s.insert("ii");
42 s.insert("cxx");
43
44 #ifndef _WIN32
45 s.insert("C");
46 #endif
47
48 return s;
49}
50
51void cpp_languaget::modules_provided(std::set<std::string> &modules)
52{
53 modules.insert(get_base_name(parse_path, true));
54}
55
58 std::istream &instream,
59 const std::string &path,
60 std::ostream &outstream,
61 message_handlert &message_handler)
62{
63 if(path.empty())
64 return c_preprocess(instream, outstream, message_handler);
65
66 // check extension
67
68 const char *ext=strrchr(path.c_str(), '.');
69 if(ext!=nullptr && std::string(ext)==".ipp")
70 {
71 std::ifstream infile(path);
72
73 char ch;
74
75 while(infile.read(&ch, 1))
76 outstream << ch;
77
78 return false;
79 }
80
81 return c_preprocess(path, outstream, message_handler);
82}
83
85 std::istream &instream,
86 const std::string &path,
87 message_handlert &message_handler)
88{
89 // store the path
90
91 parse_path=path;
92
93 // preprocessing
94
95 std::ostringstream o_preprocessed;
96
98
99 if(preprocess(instream, path, o_preprocessed, message_handler))
100 return true;
101
102 std::istringstream i_preprocessed(o_preprocessed.str());
103
104 // parsing
105 cpp_parsert cpp_parser{message_handler};
106 cpp_parser.set_file(path);
108 cpp_parser.mode=config.ansi_c.mode;
109
110 bool result=cpp_parser.parse();
111
112 // save result
113 cpp_parse_tree.swap(cpp_parser.parse_tree);
114
115 return result;
116}
117
119 symbol_table_baset &symbol_table,
120 const std::string &module,
121 message_handlert &message_handler)
122{
123 if(module.empty())
124 return false;
125
126 symbol_tablet new_symbol_table;
127
128 if(cpp_typecheck(cpp_parse_tree, new_symbol_table, module, message_handler))
129 return true;
130
131 remove_internal_symbols(new_symbol_table, message_handler, false);
132
133 return linking(symbol_table, new_symbol_table, message_handler);
134}
135
137 symbol_table_baset &symbol_table,
138 message_handlert &message_handler)
139{
140 return ansi_c_entry_point(
141 symbol_table, message_handler, object_factory_params);
142}
143
145{
146 for(const auto &i : cpp_parse_tree.items)
147 show_parse(out, i);
148}
149
151 std::ostream &out,
152 const cpp_itemt &item)
153{
154 if(item.is_linkage_spec())
155 {
156 const cpp_linkage_spect &linkage_spec=
157 item.get_linkage_spec();
158
159 out << "LINKAGE " << linkage_spec.linkage().get(ID_value) << ":\n";
160
161 for(const auto &i : linkage_spec.items())
162 show_parse(out, i);
163
164 out << '\n';
165 }
166 else if(item.is_namespace_spec())
167 {
169 item.get_namespace_spec();
170
171 out << "NAMESPACE " << namespace_spec.get_namespace()
172 << ":\n";
173
174 for(const auto &i : namespace_spec.items())
175 show_parse(out, i);
176
177 out << '\n';
178 }
179 else if(item.is_using())
180 {
181 const cpp_usingt &cpp_using=item.get_using();
182
183 out << "USING ";
184 if(cpp_using.get_namespace())
185 out << "NAMESPACE ";
186 out << cpp_using.name().pretty() << '\n';
187 out << '\n';
188 }
189 else if(item.is_declaration())
190 {
191 item.get_declaration().output(out);
192 }
193 else
194 out << "UNKNOWN: " << item.pretty() << '\n';
195}
196
197std::unique_ptr<languaget> new_cpp_language()
198{
199 return std::make_unique<cpp_languaget>();
200}
201
203 const exprt &expr,
204 std::string &code,
205 const namespacet &ns)
206{
207 code=expr2cpp(expr, ns);
208 return false;
209}
210
212 const typet &type,
213 std::string &code,
214 const namespacet &ns)
215{
216 code=type2cpp(type, ns);
217 return false;
218}
219
221 const typet &type,
222 std::string &name,
223 const namespacet &)
224{
225 name=cpp_type2name(type);
226 return false;
227}
228
230 const std::string &code,
231 const std::string &,
232 exprt &expr,
233 const namespacet &ns,
234 message_handlert &message_handler)
235{
236 expr.make_nil();
237
238 // no preprocessing yet...
239
240 std::istringstream i_preprocessed(code);
241
242 // parsing
243 cpp_parsert cpp_parser{message_handler};
244 cpp_parser.set_file(irep_idt());
246
247 bool result=cpp_parser.parse();
248
249 if(cpp_parser.parse_tree.items.empty())
250 result=true;
251 else
252 {
253 // TODO
254 // expr.swap(cpp_parser.parse_tree.declarations.front());
255
256 // typecheck it
257 result = cpp_typecheck(expr, message_handler, ns);
258 }
259
260 return result;
261}
262
bool ansi_c_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
configt config
Definition config.cpp:25
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
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 from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
c_object_factory_parameterst object_factory_params
std::string parse_path
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
ANSI-C preprocessing.
void show_parse(std::ostream &out, message_handlert &) override
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::set< std::string > extensions() const override
~cpp_languaget() override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void modules_provided(std::set< std::string > &modules) override
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
Parses the given string into an expression.
cpp_parse_treet cpp_parse_tree
const itemst & items() const
void swap(cpp_parse_treet &cpp_parse_tree)
Base class for all expressions.
Definition expr.h:56
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void make_nil()
Definition irep.h:446
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table base class interface.
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
void cpp_internal_additions(std::ostream &out)
std::unique_ptr< languaget > new_cpp_language()
C++ Language Module.
C++ Parser.
std::string cpp_type2name(const typet &type)
C++ Language Module.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
std::string type2cpp(const typet &type, const namespacet &ns)
Definition expr2cpp.cpp:493
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition expr2cpp.cpp:486
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition linking.cpp:1130
ANSI-C Linking.
void remove_internal_symbols(symbol_table_baset &symbol_table, message_handlert &mh, const bool keep_file_local)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
Remove symbols that are internal only.
char * strrchr(const char *src, int c)
Definition string.c:987
Author: Diffblue Ltd.
dstringt irep_idt