cprover
Loading...
Searching...
No Matches
ansi_c_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "ansi_c_language.h"
10
11#include <util/config.h>
12#include <util/get_base_name.h>
13#include <util/symbol_table.h>
14
15#include <linking/linking.h>
17
18#include "ansi_c_entry_point.h"
20#include "ansi_c_parser.h"
21#include "ansi_c_typecheck.h"
22#include "c_preprocess.h"
23#include "expr2c.h"
24#include "type2name.h"
25
26#include <fstream>
27
28std::set<std::string> ansi_c_languaget::extensions() const
29{
30 return { "c", "i" };
31}
32
33void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
34{
35 modules.insert(get_base_name(parse_path, true));
36}
37
40 std::istream &instream,
41 const std::string &path,
42 std::ostream &outstream)
43{
44 // stdin?
45 if(path.empty())
46 return c_preprocess(instream, outstream, get_message_handler());
47
48 return c_preprocess(path, outstream, get_message_handler());
49}
50
52 std::istream &instream,
53 const std::string &path)
54{
55 // store the path
56 parse_path=path;
57
58 // preprocessing
59 std::ostringstream o_preprocessed;
60
61 if(preprocess(instream, path, o_preprocessed))
62 return true;
63
64 std::istringstream i_preprocessed(o_preprocessed.str());
65
66 // parsing
67
68 std::string code;
70 std::istringstream codestr(code);
71
73 ansi_c_parser.set_file(ID_built_in);
74 ansi_c_parser.in=&codestr;
80 ansi_c_parser.cpp98=false; // it's not C++
81 ansi_c_parser.cpp11=false; // it's not C++
83
85
87
88 if(!result)
89 {
92 ansi_c_parser.in=&i_preprocessed;
95 }
96
97 // save result
99
100 // save some memory
102
103 return result;
104}
105
107 symbol_table_baset &symbol_table,
108 const std::string &module,
109 const bool keep_file_local)
110{
111 return typecheck(symbol_table, module, keep_file_local, {});
112}
113
115 symbol_table_baset &symbol_table,
116 const std::string &module,
117 const bool keep_file_local,
118 const std::set<irep_idt> &keep)
119{
120 symbol_tablet new_symbol_table;
121
124 new_symbol_table,
125 module,
127 {
128 return true;
129 }
130
132 new_symbol_table, this->get_message_handler(), keep_file_local, keep);
133
134 if(linking(symbol_table, new_symbol_table, get_message_handler()))
135 return true;
136
137 return false;
138}
139
141 symbol_table_baset &symbol_table)
142{
143 // This creates __CPROVER_start and __CPROVER_initialize:
144 return ansi_c_entry_point(
146}
147
148void ansi_c_languaget::show_parse(std::ostream &out)
149{
150 parse_tree.output(out);
151}
152
153std::unique_ptr<languaget> new_ansi_c_language()
154{
156}
157
159 const exprt &expr,
160 std::string &code,
161 const namespacet &ns)
162{
163 code=expr2c(expr, ns);
164 return false;
165}
166
168 const typet &type,
169 std::string &code,
170 const namespacet &ns)
171{
172 code=type2c(type, ns);
173 return false;
174}
175
177 const typet &type,
178 std::string &name,
179 const namespacet &ns)
180{
181 name=type2name(type, ns);
182 return false;
183}
184
186 const std::string &code,
187 const std::string &,
188 exprt &expr,
189 const namespacet &ns)
190{
191 expr.make_nil();
192
193 // no preprocessing yet...
194
195 std::istringstream i_preprocessed(
196 "void __my_expression = (void) (\n"+code+"\n);");
197
198 // parsing
199
202 ansi_c_parser.in=&i_preprocessed;
209
211
212 if(ansi_c_parser.parse_tree.items.empty())
213 result=true;
214 else
215 {
216 expr=ansi_c_parser.parse_tree.items.front().declarator().value();
217
218 // typecheck it
220 }
221
222 // save some memory
224
225 // now remove that (void) cast
226 if(expr.id()==ID_typecast &&
227 expr.type().id()==ID_empty &&
228 expr.operands().size()==1)
229 {
230 expr = to_typecast_expr(expr).op();
231 }
232
233 return result;
234}
235
bool ansi_c_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
void ansi_c_internal_additions(std::string &code, bool support_float16_type)
std::unique_ptr< languaget > new_ansi_c_language()
ansi_c_parsert ansi_c_parser
void ansi_c_scanner_init()
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
configt config
Definition config.cpp:25
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
~ansi_c_languaget() override
std::set< std::string > extensions() const override
void show_parse(std::ostream &out) override
bool parse(std::istream &instream, const std::string &path) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
std::string parse_path
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 type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
ansi_c_parse_treet parse_tree
c_object_factory_parameterst object_factory_params
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
void swap(ansi_c_parse_treet &other)
void output(std::ostream &out) const
bool ts_18661_3_Floatn_types
ansi_c_parse_treet parse_tree
virtual void clear() override
virtual bool parse() override
struct configt::ansi_ct ansi_c
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void make_nil()
Definition irep.h:454
const irep_idt & id() const
Definition irep.h:396
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
void set_line_no(unsigned _line_no)
Definition parser.h:80
The symbol table base class interface.
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4144
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4160
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.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
bool for_has_scope
Definition config.h:148
bool float16_type
Definition config.h:151
bool ts_18661_3_Floatn_types
Definition config.h:149
flavourt mode
Definition config.h:249
Author: Diffblue Ltd.
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition type2name.cpp:82
Type Naming for C.
dstringt irep_idt