cprover
ansi_c_language.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ansi_c_language.h"
10 
11 #include <cstring>
12 #include <sstream>
13 #include <fstream>
14 
15 #include <util/config.h>
16 #include <util/get_base_name.h>
17 
18 #include <linking/linking.h>
20 
21 #include "ansi_c_entry_point.h"
22 #include "ansi_c_typecheck.h"
23 #include "ansi_c_parser.h"
24 #include "expr2c.h"
25 #include "c_preprocess.h"
27 #include "type2name.h"
28 
29 std::set<std::string> ansi_c_languaget::extensions() const
30 {
31  return { "c", "i" };
32 }
33 
34 void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
35 {
36  modules.insert(get_base_name(parse_path, true));
37 }
38 
41  std::istream &instream,
42  const std::string &path,
43  std::ostream &outstream)
44 {
45  // stdin?
46  if(path=="")
47  return c_preprocess(instream, outstream, get_message_handler());
48 
49  return c_preprocess(path, outstream, get_message_handler());
50 }
51 
53  std::istream &instream,
54  const std::string &path)
55 {
56  // store the path
57  parse_path=path;
58 
59  // preprocessing
60  std::ostringstream o_preprocessed;
61 
62  if(preprocess(instream, path, o_preprocessed))
63  return true;
64 
65  std::istringstream i_preprocessed(o_preprocessed.str());
66 
67  // parsing
68 
69  std::string code;
71  std::istringstream codestr(code);
72 
74  ansi_c_parser.set_file(ID_built_in);
75  ansi_c_parser.in=&codestr;
78  ansi_c_parser.cpp98=false; // it's not C++
79  ansi_c_parser.cpp11=false; // it's not C++
81 
83 
84  bool result=ansi_c_parser.parse();
85 
86  if(!result)
87  {
89  ansi_c_parser.set_file(path);
90  ansi_c_parser.in=&i_preprocessed;
93  }
94 
95  // save result
97 
98  // save some memory
100 
101  return result;
102 }
103 
105  symbol_tablet &symbol_table,
106  const std::string &module)
107 {
108  symbol_tablet new_symbol_table;
109 
110  if(ansi_c_typecheck(
111  parse_tree,
112  new_symbol_table,
113  module,
115  {
116  return true;
117  }
118 
119  remove_internal_symbols(new_symbol_table);
120 
121  if(linking(symbol_table, new_symbol_table, get_message_handler()))
122  return true;
123 
124  return false;
125 }
126 
128 {
129  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
130  return true;
131 
132  return false;
133 }
134 
135 void ansi_c_languaget::show_parse(std::ostream &out)
136 {
137  parse_tree.output(out);
138 }
139 
141 {
142  return new ansi_c_languaget;
143 }
144 
146  const exprt &expr,
147  std::string &code,
148  const namespacet &ns)
149 {
150  code=expr2c(expr, ns);
151  return false;
152 }
153 
155  const typet &type,
156  std::string &code,
157  const namespacet &ns)
158 {
159  code=type2c(type, ns);
160  return false;
161 }
162 
164  const typet &type,
165  std::string &name,
166  const namespacet &ns)
167 {
168  name=type2name(type, ns);
169  return false;
170 }
171 
173  const std::string &code,
174  const std::string &module,
175  exprt &expr,
176  const namespacet &ns)
177 {
178  expr.make_nil();
179 
180  // no preprocessing yet...
181 
182  std::istringstream i_preprocessed(
183  "void __my_expression = (void) (\n"+code+"\n);");
184 
185  // parsing
186 
189  ansi_c_parser.in=&i_preprocessed;
193 
194  bool result=ansi_c_parser.parse();
195 
196  if(ansi_c_parser.parse_tree.items.empty())
197  result=true;
198  else
199  {
200  expr=ansi_c_parser.parse_tree.items.front().declarator().value();
201 
202  // typecheck it
204  }
205 
206  // save some memory
208 
209  // now remove that (void) cast
210  if(expr.id()==ID_typecast &&
211  expr.type().id()==ID_empty &&
212  expr.operands().size()==1)
213  expr=expr.op0();
214 
215  return result;
216 }
217 
219 {
220 }
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:85
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
struct configt::ansi_ct ansi_c
~ansi_c_languaget() override
std::string parse_path
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:29
exprt & op0()
Definition: expr.h:84
ANSI-C Linking.
std::istream * in
Definition: parser.h:26
ANSI-C Language Type Checking.
languaget * new_ansi_c_language()
ansi_c_parse_treet parse_tree
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1336
typet & type()
Definition: expr.h:60
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
bool parse(std::istream &instream, const std::string &path) override
configt config
Definition: config.cpp:21
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
void ansi_c_internal_additions(std::string &code)
void output(std::ostream &out) const
const irep_idt & id() const
Definition: irep.h:189
flavourt mode
Definition: config.h:105
virtual bool parse() override
Definition: ansi_c_parser.h:37
void remove_internal_symbols(symbol_tablet &symbol_table)
A symbol is EXPORTED if it is a * non-static function with body that is not extern inline * symbol us...
void set_file(const irep_idt &file)
Definition: parser.h:85
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::string type2c(const typet &type, const namespacet &ns)
Definition: expr2c.cpp:3882
void ansi_c_scanner_init()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
bool for_has_scope
Definition: config.h:45
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
void show_parse(std::ostream &out) override
Type Naming for C.
message_handlert & get_message_handler()
Definition: message.h:127
bool ansi_c_entry_point(symbol_tablet &symbol_table, const std::string &standard_main, message_handlert &message_handler)
Base class for all expressions.
Definition: expr.h:46
ansi_c_parsert ansi_c_parser
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3874
void make_nil()
Definition: irep.h:243
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
void set_line_no(unsigned _line_no)
Definition: parser.h:80
void swap(ansi_c_parse_treet &other)
dstringt irep_idt
Definition: irep.h:32
std::set< std::string > extensions() const override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Remove symbols that are internal only.
operandst & operands()
Definition: expr.h:70
void modules_provided(std::set< std::string > &modules) override
virtual void clear() override
Definition: ansi_c_parser.h:42
bool final(symbol_tablet &symbol_table) override