cprover
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{
62 if(path.empty())
64
65 // check extension
66
67 const char *ext=strrchr(path.c_str(), '.');
68 if(ext!=nullptr && std::string(ext)==".ipp")
69 {
70 std::ifstream infile(path);
71
72 char ch;
73
74 while(infile.read(&ch, 1))
75 outstream << ch;
76
77 return false;
78 }
79
81}
82
84 std::istream &instream,
85 const std::string &path)
86{
87 // store the path
88
89 parse_path=path;
90
91 // preprocessing
92
93 std::ostringstream o_preprocessed;
94
96
98 return true;
99
100 std::istringstream i_preprocessed(o_preprocessed.str());
101
102 // parsing
103
105 cpp_parser.set_file(path);
109
110 bool result=cpp_parser.parse();
111
112 // save result
114
115 // save some memory
117
118 return result;
119}
120
122 symbol_table_baset &symbol_table,
123 const std::string &module)
124{
125 if(module.empty())
126 return false;
127
128 symbol_tablet new_symbol_table;
129
130 if(cpp_typecheck(
131 cpp_parse_tree, new_symbol_table, module, get_message_handler()))
132 return true;
133
134 remove_internal_symbols(new_symbol_table, get_message_handler(), false);
135
136 return linking(symbol_table, new_symbol_table, get_message_handler());
137}
138
144
145void cpp_languaget::show_parse(std::ostream &out)
146{
147 for(const auto &i : cpp_parse_tree.items)
148 show_parse(out, i);
149}
150
152 std::ostream &out,
153 const cpp_itemt &item)
154{
155 if(item.is_linkage_spec())
156 {
157 const cpp_linkage_spect &linkage_spec=
158 item.get_linkage_spec();
159
160 out << "LINKAGE " << linkage_spec.linkage().get(ID_value) << ":\n";
161
162 for(const auto &i : linkage_spec.items())
163 show_parse(out, i);
164
165 out << '\n';
166 }
167 else if(item.is_namespace_spec())
168 {
170 item.get_namespace_spec();
171
172 out << "NAMESPACE " << namespace_spec.get_namespace()
173 << ":\n";
174
175 for(const auto &i : namespace_spec.items())
176 show_parse(out, i);
177
178 out << '\n';
179 }
180 else if(item.is_using())
181 {
182 const cpp_usingt &cpp_using=item.get_using();
183
184 out << "USING ";
185 if(cpp_using.get_namespace())
186 out << "NAMESPACE ";
187 out << cpp_using.name().pretty() << '\n';
188 out << '\n';
189 }
190 else if(item.is_declaration())
191 {
192 item.get_declaration().output(out);
193 }
194 else
195 out << "UNKNOWN: " << item.pretty() << '\n';
196}
197
198std::unique_ptr<languaget> new_cpp_language()
199{
201}
202
204 const exprt &expr,
205 std::string &code,
206 const namespacet &ns)
207{
208 code=expr2cpp(expr, ns);
209 return false;
210}
211
213 const typet &type,
214 std::string &code,
215 const namespacet &ns)
216{
217 code=type2cpp(type, ns);
218 return false;
219}
220
222 const typet &type,
223 std::string &name,
224 const namespacet &)
225{
226 name=cpp_type2name(type);
227 return false;
228}
229
231 const std::string &code,
232 const std::string &,
233 exprt &expr,
234 const namespacet &ns)
235{
236 expr.make_nil();
237
238 // no preprocessing yet...
239
240 std::istringstream i_preprocessed(code);
241
242 // parsing
243
248
249 bool result=cpp_parser.parse();
250
251 if(cpp_parser.parse_tree.items.empty())
252 result=true;
253 else
254 {
255 // TODO
256 // expr.swap(cpp_parser.parse_tree.declarations.front());
257
258 // typecheck it
260 }
261
262 // save some memory
264
265 return result;
266}
267
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:563
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 typecheck(symbol_table_baset &symbol_table, const std::string &module) 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
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
std::string parse_path
std::set< std::string > extensions() const override
~cpp_languaget() override
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
bool parse(std::istream &instream, const std::string &path) override
void modules_provided(std::set< std::string > &modules) override
cpp_parse_treet cpp_parse_tree
void show_parse(std::ostream &out) override
const itemst & items() const
void swap(cpp_parse_treet &cpp_parse_tree)
virtual void clear() override
Definition cpp_parser.h:29
cpp_parse_treet parse_tree
Definition cpp_parser.h:25
virtual bool parse() override
ansi_c_parsert::modet mode
Definition cpp_parser.h:46
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:454
message_handlert & get_message_handler()
Definition message.h:184
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
mstreamt & result() const
Definition message.h:409
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
std::istream * in
Definition parser.h:26
void set_file(const irep_idt &file)
Definition parser.h:85
messaget log
Definition parser.h:136
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.
cpp_parsert cpp_parser
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:503
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition expr2cpp.cpp:496
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:1565
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.
Author: Diffblue Ltd.
dstringt irep_idt