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())
47
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
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
77 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
78 ansi_c_parser.cpp98=false; // it's not C++
79 ansi_c_parser.cpp11=false; // it's not C++
81
83
85
86 if(!result)
87 {
93 }
94
95 // save result
97
98 // save some memory
100
101 return result;
102}
103
105 symbol_table_baset &symbol_table,
106 const std::string &module,
107 const bool keep_file_local)
108{
109 return typecheck(symbol_table, module, keep_file_local, {});
110}
111
113 symbol_table_baset &symbol_table,
114 const std::string &module,
115 const bool keep_file_local,
116 const std::set<irep_idt> &keep)
117{
118 symbol_tablet new_symbol_table;
119
122 new_symbol_table,
123 module,
125 {
126 return true;
127 }
128
130 new_symbol_table, this->get_message_handler(), keep_file_local, keep);
131
132 if(linking(symbol_table, new_symbol_table, get_message_handler()))
133 return true;
134
135 return false;
136}
137
139 symbol_table_baset &symbol_table)
140{
141 // This creates __CPROVER_start and __CPROVER_initialize:
142 return ansi_c_entry_point(
144}
145
146void ansi_c_languaget::show_parse(std::ostream &out)
147{
148 parse_tree.output(out);
149}
150
151std::unique_ptr<languaget> new_ansi_c_language()
152{
154}
155
157 const exprt &expr,
158 std::string &code,
159 const namespacet &ns)
160{
161 code=expr2c(expr, ns);
162 return false;
163}
164
166 const typet &type,
167 std::string &code,
168 const namespacet &ns)
169{
170 code=type2c(type, ns);
171 return false;
172}
173
175 const typet &type,
176 std::string &name,
177 const namespacet &ns)
178{
179 name=type2name(type, ns);
180 return false;
181}
182
184 const std::string &code,
185 const std::string &,
186 exprt &expr,
187 const namespacet &ns)
188{
189 expr.make_nil();
190
191 // no preprocessing yet...
192
193 std::istringstream i_preprocessed(
194 "void __my_expression = (void) (\n"+code+"\n);");
195
196 // parsing
197
203 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
205
207
208 if(ansi_c_parser.parse_tree.items.empty())
209 result=true;
210 else
211 {
212 expr=ansi_c_parser.parse_tree.items.front().declarator().value();
213
214 // typecheck it
216 }
217
218 // save some memory
220
221 // now remove that (void) cast
222 if(expr.id()==ID_typecast &&
223 expr.type().id()==ID_empty &&
224 expr.operands().size()==1)
225 {
226 expr = to_typecast_expr(expr).op();
227 }
228
229 return result;
230}
231
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)
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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
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.
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
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