Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
63 this->include_function_decls =
false;
69 this->include_function_bodies =
false;
75 this->include_global_decls =
false;
81 this->include_typedefs =
false;
87 this->include_global_vars =
false;
93 this->include_compounds =
false;
99 this->follow_compounds =
false;
105 this->include_headers =
true;
115 const bool use_system_headers,
116 const bool use_all_headers,
117 const bool include_harness,
134 const bool use_system_headers,
135 const bool use_all_headers,
136 const bool include_harness,
193 static std::string
indent(
const unsigned n)
195 return std::string(2*n,
' ');
206 assert(!d_str.empty());
207 assert(*d_str.rbegin()==
';');
209 return d_str.substr(0, d_str.size()-1);
216 std::unordered_set<irep_idt> &dependencies);
222 std::ostream &os_body);
225 const typet &unresolved,
230 const typet &unresolved,
246 const bool skip_main,
247 std::ostream &os_decl,
248 std::ostream &os_body,
253 const std::list<irep_idt> &local_static,
255 std::list<irep_idt> &type_decls);
259 const std::list<irep_idt> &type_decls);
265 std::list<irep_idt> &local_static,
266 std::list<irep_idt> &local_type_decls);
270 #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt > &dependencies)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
dump_c_configurationt enable_include_headers()
dump_c_configurationt disable_include_global_vars()
static std::string indent(const unsigned n)
const goto_functionst & goto_functions
static dump_c_configurationt default_configuration
The default used for dump-c and dump-cpp.
The type of an expression, extends irept.
Used for configuring the behaviour of dump_c.
Base type for structs and unions.
std::unique_ptr< languaget >(* language_factoryt)()
bool follow_compounds
Define whether to follow compunds recursively.
A codet representing the declaration of a local variable.
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)
system_library_symbolst system_symbols
Base class for all expressions.
dump_ct(const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &_ns, language_factoryt factory, const dump_c_configurationt config)
std::unique_ptr< languaget > language
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
dump_ct(const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &_ns, language_factoryt factory)
dump_c_configurationt disable_include_function_bodies()
Expression to hold a symbol (variable)
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
std::string expr_to_string(const exprt &expr)
convertedt converted_compound
dump_c_configurationt disable_include_typedefs()
std::set< std::string > system_headers
std::string make_decl(const irep_idt &identifier, const typet &type)
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
declared_enum_constants_mapt declared_enum_constants
bool include_typedefs
Include the typedefs in the dump.
convertedt converted_global
void cleanup_type(typet &type)
std::map< irep_idt, typedef_infot > typedef_mapt
void convert_compound_enum(const typet &type, std::ostream &os)
void cleanup_expr(exprt &expr)
std::unordered_map< irep_idt, code_declt > local_static_declst
std::unordered_set< irep_idt > convertedt
dump_c_configurationt disable_follow_compounds()
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Abstract interface to support a programming language.
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)
bool include_compounds
Include struct definitions in the dump.
void operator()(std::ostream &out)
bool include_headers
Include headers type declarations are borrowed from.
bool include_function_decls
Include the function declarations in the dump.
virtual ~dump_ct()=default
A collection of goto functions.
void set_use_all_headers(bool use)
bool include_global_decls
Include the global declarations in the dump.
dump_c_configurationt disable_include_function_decls()
dump_c_configurationt disable_include_compunds()
bool include_global_vars
Include global variable definitions in the dump.
std::unordered_map< typet, irep_idt, irep_hash > typedef_typest
std::unordered_set< irep_idt > dependencies
bool include_function_bodies
Include the functions in the dump.
symbol_tablet copied_symbol_table
typedef_infot(const irep_idt &name)
typedef_typest typedef_types
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
std::string type_decl_str
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
const dump_c_configurationt dump_c_config
static dump_c_configurationt type_header_configuration
The config used for dump-c-type-header.
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
void collect_typedefs(const typet &type, bool early)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
dump_c_configurationt disable_include_global_decls()
std::string type_to_string(const typet &type)
convertedt converted_enum
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.