cprover
dump_c_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dump Goto-Program as C/C++ Source
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
14 
15 #include <set>
16 #include <string>
17 
18 #include <util/language.h>
19 
20 #include <langapi/mode.h>
21 
22 class dump_ct
23 {
24 public:
26  const goto_functionst &_goto_functions,
27  const bool use_system_headers,
28  const bool use_all_headers,
29  const namespacet &_ns,
30  language_factoryt factory):
31  goto_functions(_goto_functions),
32  copied_symbol_table(_ns.get_symbol_table()),
34  language(factory()),
35  use_all_headers(use_all_headers)
36  {
37  if(use_system_headers)
39  }
40 
41  virtual ~dump_ct()
42  {
43  delete language;
44  }
45 
46  void operator()(std::ostream &out);
47 
48 protected:
51  const namespacet ns;
53  const bool use_all_headers;
54 
55  typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
57 
58  std::set<std::string> system_headers;
59 
60  typedef std::unordered_map<irep_idt, std::string, irep_id_hash>
63 
64  typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash>
67 
69  {
71  std::string type_decl_str;
72  bool early;
73  std::unordered_set<irep_idt, irep_id_hash> dependencies;
74 
75  explicit typedef_infot(const irep_idt &name):
76  typedef_name(name),
77  type_decl_str(""),
78  early(false)
79  {
80  }
81  };
82  typedef std::map<irep_idt, typedef_infot> typedef_mapt;
83  typedef_mapt typedef_map;
84  typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
85  typedef_typest typedef_types;
86 
88 
89  std::string type_to_string(const typet &type);
90  std::string expr_to_string(const exprt &expr);
91 
92  bool ignore(const symbolt &symbol);
93  bool ignore(const typet &type);
94 
95  static std::string indent(const unsigned n)
96  {
97  return std::string(2*n, ' ');
98  }
99 
100  std::string make_decl(
101  const irep_idt &identifier,
102  const typet &type)
103  {
104  symbol_exprt sym(identifier, type);
105  code_declt d(sym);
106 
107  std::string d_str=expr_to_string(d);
108  assert(!d_str.empty());
109  assert(*d_str.rbegin()==';');
110 
111  return d_str.substr(0, d_str.size()-1);
112  }
113 
114  void collect_typedefs(const typet &type, bool early);
116  const typet &type,
117  bool early,
118  std::unordered_set<irep_idt, irep_id_hash> &dependencies);
119  void gather_global_typedefs();
120  void dump_typedefs(std::ostream &os) const;
121 
123  const symbolt &symbol,
124  std::ostream &os_body);
125  void convert_compound(
126  const typet &type,
127  const typet &unresolved,
128  bool recursive,
129  std::ostream &os);
130  void convert_compound(
131  const struct_union_typet &type,
132  const typet &unresolved,
133  bool recursive,
134  std::ostream &os);
136  const typet &type,
137  std::ostream &os);
138 
139  typedef std::unordered_map<irep_idt, code_declt, irep_id_hash>
141 
143  const symbolt &symbol,
144  std::ostream &os,
145  local_static_declst &local_static_decls);
146 
148  const symbolt &symbol,
149  const bool skip_main,
150  std::ostream &os_decl,
151  std::ostream &os_body,
152  local_static_declst &local_static_decls);
153 
155  code_blockt &b,
156  const std::list<irep_idt> &local_static,
157  local_static_declst &local_static_decls,
158  std::list<irep_idt> &type_decls);
159 
161  code_blockt &b,
162  const std::list<irep_idt> &type_decls);
163 
164  void cleanup_expr(exprt &expr);
165  void cleanup_type(typet &type);
166  void cleanup_decl(
167  code_declt &decl,
168  std::list<irep_idt> &local_static,
169  std::list<irep_idt> &local_type_decls);
170 };
171 
172 #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
The type of an expression.
Definition: type.h:20
std::unordered_set< irep_idt, irep_id_hash > convertedt
Definition: dump_c_class.h:55
void collect_typedefs(const typet &type, bool early)
Definition: dump_c.cpp:923
void init_system_library_map()
Definition: dump_c.cpp:589
void insert_local_static_decls(code_blockt &b, const std::list< irep_idt > &local_static, local_static_declst &local_static_decls, std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1382
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:66
const namespacet ns
Definition: dump_c_class.h:51
std::unordered_map< irep_idt, code_declt, irep_id_hash > local_static_declst
Definition: dump_c_class.h:140
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1626
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1635
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt, irep_id_hash > &dependencies)
Definition: dump_c.cpp:946
std::map< irep_idt, typedef_infot > typedef_mapt
Definition: dump_c_class.h:82
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const goto_functionst & goto_functions
Definition: dump_c_class.h:49
convertedt converted_enum
Definition: dump_c_class.h:56
std::unordered_set< irep_idt, irep_id_hash > dependencies
Definition: dump_c_class.h:73
const bool use_all_headers
Definition: dump_c_class.h:53
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:100
typedef_typest typedef_types
Definition: dump_c_class.h:85
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1416
A declaration of a local variable.
Definition: std_code.h:192
system_library_mapt system_library_map
Definition: dump_c_class.h:62
std::string type_decl_str
Definition: dump_c_class.h:71
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:308
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:862
The symbol table.
Definition: symbol_table.h:52
dump_ct(const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const namespacet &_ns, language_factoryt factory)
Definition: dump_c_class.h:25
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Abstract interface to support a programming language.
void gather_global_typedefs()
Definition: dump_c.cpp:1034
std::unordered_map< irep_idt, std::string, irep_id_hash > system_library_mapt
Definition: dump_c_class.h:61
std::set< std::string > system_headers
Definition: dump_c_class.h:58
convertedt converted_global
Definition: dump_c_class.h:56
bool ignore(const symbolt &symbol)
Definition: dump_c.cpp:805
typedef_mapt typedef_map
Definition: dump_c_class.h:83
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:294
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1453
std::unordered_map< typet, irep_idt, irep_hash > typedef_typest
Definition: dump_c_class.h:84
Base class for all expressions.
Definition: expr.h:46
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:541
void operator()(std::ostream &out)
Definition: dump_c.cpp:37
Sequential composition.
Definition: std_code.h:63
static std::string indent(const unsigned n)
Definition: dump_c_class.h:95
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void convert_function_declaration(const symbolt &symbol, const bool skip_main, std::ostream &os_decl, std::ostream &os_body, local_static_declst &local_static_decls)
Definition: dump_c.cpp:1226
languaget * language
Definition: dump_c_class.h:52
void dump_typedefs(std::ostream &os) const
Definition: dump_c.cpp:1076
virtual ~dump_ct()
Definition: dump_c_class.h:41
typedef_infot(const irep_idt &name)
Definition: dump_c_class.h:75
convertedt converted_compound
Definition: dump_c_class.h:56
void cleanup_type(typet &type)
Definition: dump_c.cpp:1600
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:50
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
Definition: dump_c.cpp:1161
std::unordered_map< irep_idt, irep_idt, irep_id_hash > declared_enum_constants_mapt
Definition: dump_c_class.h:65
languaget *(* language_factoryt)()
Definition: mode.h:21