cprover
|
#include <dump_c_class.h>
Classes | |
struct | typedef_infot |
Public Member Functions | |
dump_ct (const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const namespacet &_ns, language_factoryt factory) | |
virtual | ~dump_ct () |
void | operator() (std::ostream &out) |
Protected Types | |
typedef std::unordered_set< irep_idt, irep_id_hash > | convertedt |
typedef std::unordered_map< irep_idt, std::string, irep_id_hash > | system_library_mapt |
typedef std::unordered_map< irep_idt, irep_idt, irep_id_hash > | declared_enum_constants_mapt |
typedef std::map< irep_idt, typedef_infot > | typedef_mapt |
typedef std::unordered_map< typet, irep_idt, irep_hash > | typedef_typest |
typedef std::unordered_map< irep_idt, code_declt, irep_id_hash > | local_static_declst |
Protected Member Functions | |
void | init_system_library_map () |
std::string | type_to_string (const typet &type) |
std::string | expr_to_string (const exprt &expr) |
bool | ignore (const symbolt &symbol) |
bool | ignore (const typet &type) |
std::string | make_decl (const irep_idt &identifier, const typet &type) |
void | collect_typedefs (const typet &type, bool early) |
void | collect_typedefs_rec (const typet &type, bool early, std::unordered_set< irep_idt, irep_id_hash > &dependencies) |
void | gather_global_typedefs () |
void | dump_typedefs (std::ostream &os) const |
void | convert_compound_declaration (const symbolt &symbol, std::ostream &os_body) |
declare compound types More... | |
void | convert_compound (const typet &type, const typet &unresolved, bool recursive, std::ostream &os) |
void | convert_compound (const struct_union_typet &type, const typet &unresolved, bool recursive, std::ostream &os) |
void | convert_compound_enum (const typet &type, std::ostream &os) |
void | convert_global_variable (const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls) |
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) |
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) |
void | insert_local_type_decls (code_blockt &b, const std::list< irep_idt > &type_decls) |
void | cleanup_expr (exprt &expr) |
void | cleanup_type (typet &type) |
void | cleanup_decl (code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls) |
Static Protected Member Functions | |
static std::string | indent (const unsigned n) |
Protected Attributes | |
const goto_functionst & | goto_functions |
symbol_tablet | copied_symbol_table |
const namespacet | ns |
languaget * | language |
const bool | use_all_headers |
convertedt | converted_compound |
convertedt | converted_global |
convertedt | converted_enum |
std::set< std::string > | system_headers |
system_library_mapt | system_library_map |
declared_enum_constants_mapt | declared_enum_constants |
typedef_mapt | typedef_map |
typedef_typest | typedef_types |
Definition at line 22 of file dump_c_class.h.
|
protected |
Definition at line 55 of file dump_c_class.h.
|
protected |
Definition at line 65 of file dump_c_class.h.
|
protected |
Definition at line 140 of file dump_c_class.h.
|
protected |
Definition at line 61 of file dump_c_class.h.
|
protected |
Definition at line 82 of file dump_c_class.h.
|
protected |
Definition at line 84 of file dump_c_class.h.
|
inline |
Definition at line 25 of file dump_c_class.h.
References init_system_library_map().
|
inlinevirtual |
Definition at line 41 of file dump_c_class.h.
References language.
|
protected |
Definition at line 862 of file dump_c.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSIGN, copied_symbol_table, DECL, END_FUNCTION, irept::is_not_nil(), exprt::op0(), exprt::op1(), exprt::operands(), POSTCONDITION, irept::swap(), system_headers, and typedef_map.
Referenced by convert_global_variable(), and insert_local_static_decls().
|
protected |
Definition at line 1453 of file dump_c.cpp.
References code_function_callt::arguments(), base_type_eq(), cleanup_type(), struct_union_typet::components(), declared_enum_constants, dstringt::empty(), namespace_baset::follow(), Forall_expr, Forall_operands, code_function_callt::function(), irept::get(), irept::get_bool(), struct_union_typet::get_component(), union_exprt::get_component_name(), symbol_exprt::get_identifier(), codet::get_statement(), constant_exprt::get_value(), irept::id(), id2string(), exprt::is_zero(), namespacet::lookup(), exprt::move_to_operands(), ns, unary_exprt::op(), typecast_exprt::op(), exprt::op0(), exprt::operands(), code_typet::parameters(), PRECONDITION, irept::remove(), irept::set(), typet::subtype(), irept::swap(), to_c_bit_field_type(), to_code(), to_code_function_call(), to_code_type(), to_constant_expr(), to_struct_type(), to_symbol_expr(), to_typecast_expr(), to_union_expr(), to_union_type(), symbolt::type, and exprt::type().
Referenced by cleanup_type(), and expr_to_string().
|
protected |
Definition at line 1600 of file dump_c.cpp.
References cleanup_expr(), dstringt::empty(), Forall_subtypes, irept::get(), irept::id(), code_typet::parameters(), POSTCONDITION, code_typet::return_type(), array_typet::size(), to_array_type(), and to_code_type().
Referenced by cleanup_expr(), and type_to_string().
|
protected |
Definition at line 923 of file dump_c.cpp.
References collect_typedefs_rec().
Referenced by convert_compound(), convert_function_declaration(), and gather_global_typedefs().
|
protected |
Definition at line 946 of file dump_c.cpp.
References dstringt::empty(), irept::get(), irept::id(), ignore(), namespacet::lookup(), make_decl(), ns, code_typet::parameters(), PRECONDITION, irept::remove(), code_typet::return_type(), typet::subtype(), system_headers, to_code_type(), to_symbol_type(), symbolt::type, and typedef_map.
Referenced by collect_typedefs().
|
protected |
Definition at line 308 of file dump_c.cpp.
References convert_compound_enum(), DATA_INVARIANT, find_non_pointer_type_symbols(), irept::id(), ignore(), symbolt::is_type, namespacet::lookup(), ns, typet::subtype(), to_array_type(), to_c_enum_tag_type(), to_struct_union_type(), to_symbol_type(), and symbolt::type.
Referenced by convert_compound(), convert_compound_declaration(), and insert_local_type_decls().
|
protected |
Definition at line 361 of file dump_c.cpp.
References configt::ansi_c, collect_typedefs(), struct_union_typet::components(), config, convert_compound(), converted_compound, dstringt::empty(), irept::find(), namespace_baset::follow(), forall_irep, irept::get(), irept::get_bool(), struct_union_typet::componentt::get_is_padding(), struct_union_typet::componentt::get_name(), irept::get_sub(), bitvector_typet::get_width(), languaget::id(), irept::id(), id2string(), indent(), language, configt::ansi_ct::long_long_int_width, make_decl(), ns, POSTCONDITION, PRECONDITION, irept::remove(), typet::subtype(), to_c_bit_field_type(), to_signedbv_type(), to_unsignedbv_type(), exprt::type(), type_to_string(), typedef_map, typedef_types, and UNREACHABLE.
|
protected |
declare compound types
Definition at line 294 of file dump_c.cpp.
References convert_compound(), dstringt::empty(), source_locationt::get_function(), irept::id(), symbolt::location, symbolt::name, and symbolt::type.
Referenced by operator()().
|
protected |
Definition at line 541 of file dump_c.cpp.
References irept::add(), converted_enum, copied_symbol_table, declared_enum_constants, irept::find(), irept::get_bool(), irept::get_sub(), symbol_tablet::has_symbol(), irept::id(), id2string(), PRECONDITION, to_c_enum_type(), and type_to_string().
Referenced by convert_compound(), and operator()().
|
protected |
Definition at line 1226 of file dump_c.cpp.
References collect_typedefs(), converted_compound, converted_enum, copied_symbol_table, declared_enum_constants, goto_functions_templatet< goto_programt >::entry_point(), expr_to_string(), goto_functions_templatet< bodyT >::function_map, goto_functions, insert_local_static_decls(), insert_local_type_decls(), symbolt::location, make_decl(), symbolt::name, system_headers, symbolt::type, and typedef_map.
Referenced by operator()().
|
protected |
Definition at line 1161 of file dump_c.cpp.
References CHECK_RETURN, cleanup_decl(), converted_global, dstringt::empty(), expr_to_string(), find_symbols(), source_locationt::get_function(), irept::id(), id2string(), symbolt::is_extern, irept::is_nil(), irept::is_not_nil(), symbolt::is_static_lifetime, symbolt::is_type, symbolt::location, namespacet::lookup(), symbolt::name, ns, symbolt::symbol_expr(), symbolt::type, and symbolt::value.
Referenced by operator()().
|
protected |
Definition at line 1076 of file dump_c.cpp.
References id2string(), POSTCONDITION, PRECONDITION, typedef_map, and dump_ct::typedef_infot::typedef_name.
Referenced by operator()().
|
protected |
Definition at line 1635 of file dump_c.cpp.
References cleanup_expr(), languaget::from_expr(), language, and ns.
Referenced by convert_function_declaration(), convert_global_variable(), and make_decl().
|
protected |
Definition at line 1034 of file dump_c.cpp.
References collect_typedefs(), copied_symbol_table, dstringt::empty(), irept::get(), source_locationt::get_function(), id2string(), ignore(), symbolt::is_macro, symbolt::is_type, symbolt::location, PRECONDITION, symbol_tablet::symbols, symbolt::type, typedef_map, and typedef_types.
Referenced by operator()().
|
protected |
Definition at line 805 of file dump_c.cpp.
References CPROVER_PREFIX, source_locationt::get_file(), has_prefix(), has_suffix(), id2string(), symbolt::location, symbolt::name, size_type(), system_headers, system_library_map, and use_all_headers.
Referenced by collect_typedefs_rec(), convert_compound(), gather_global_typedefs(), ignore(), and operator()().
|
protected |
Definition at line 785 of file dump_c.cpp.
References ignore(), and symbolt::type.
|
inlinestaticprotected |
Definition at line 95 of file dump_c_class.h.
Referenced by convert_compound().
|
protected |
Definition at line 589 of file dump_c.cpp.
References ADD_TO_SYSTEM_LIBRARY.
Referenced by dump_ct().
|
protected |
Definition at line 1382 of file dump_c.cpp.
References CHECK_RETURN, cleanup_decl(), find_block_position_rec(), exprt::operands(), and PRECONDITION.
Referenced by convert_function_declaration().
|
protected |
Definition at line 1416 of file dump_c.cpp.
References exprt::add_source_location(), CHECK_RETURN, convert_compound(), find_block_position_rec(), namespacet::lookup(), ns, exprt::operands(), source_locationt::set_comment(), and exprt::type().
Referenced by convert_function_declaration().
Definition at line 100 of file dump_c_class.h.
References expr_to_string().
Referenced by collect_typedefs_rec(), convert_compound(), and convert_function_declaration().
void dump_ct::operator() | ( | std::ostream & | out | ) |
Definition at line 37 of file dump_c.cpp.
References symbol_tablet::add(), irept::add(), symbolt::base_name, CHECK_RETURN, config, convert_compound_declaration(), convert_compound_enum(), convert_function_declaration(), convert_global_variable(), copied_symbol_table, dump_typedefs(), dstringt::empty(), irept::find(), forall_symbols, Forall_symbols, goto_functions_templatet< bodyT >::function_map, gather_global_typedefs(), irept::get(), irept::get_bool(), source_locationt::get_function(), irept::get_string(), goto_functions, irept::id(), id2string(), ignore(), symbolt::is_static_lifetime, symbolt::is_type, symbolt::location, namespacet::lookup(), configt::main, symbolt::name, ns, code_typet::parameters(), PRECONDITION, irept::remove(), irept::set(), symbol_typet::set_identifier(), size_type(), symbol_tablet::symbols, system_headers, to_code_type(), to_symbol_type(), symbolt::type, and type_to_string().
|
protected |
Definition at line 1626 of file dump_c.cpp.
References cleanup_type(), languaget::from_type(), language, and ns.
Referenced by convert_compound(), convert_compound_enum(), and operator()().
|
protected |
Definition at line 56 of file dump_c_class.h.
Referenced by convert_compound(), and convert_function_declaration().
|
protected |
Definition at line 56 of file dump_c_class.h.
Referenced by convert_compound_enum(), and convert_function_declaration().
|
protected |
Definition at line 56 of file dump_c_class.h.
Referenced by convert_global_variable().
|
protected |
Definition at line 50 of file dump_c_class.h.
Referenced by cleanup_decl(), convert_compound_enum(), convert_function_declaration(), gather_global_typedefs(), and operator()().
|
protected |
Definition at line 66 of file dump_c_class.h.
Referenced by cleanup_expr(), convert_compound_enum(), and convert_function_declaration().
|
protected |
Definition at line 49 of file dump_c_class.h.
Referenced by convert_function_declaration(), and operator()().
|
protected |
Definition at line 52 of file dump_c_class.h.
Referenced by convert_compound(), expr_to_string(), type_to_string(), and ~dump_ct().
|
protected |
Definition at line 51 of file dump_c_class.h.
Referenced by cleanup_expr(), collect_typedefs_rec(), convert_compound(), convert_global_variable(), expr_to_string(), insert_local_type_decls(), operator()(), and type_to_string().
|
protected |
Definition at line 58 of file dump_c_class.h.
Referenced by cleanup_decl(), collect_typedefs_rec(), convert_function_declaration(), ignore(), and operator()().
|
protected |
Definition at line 62 of file dump_c_class.h.
Referenced by ignore().
|
protected |
Definition at line 83 of file dump_c_class.h.
Referenced by cleanup_decl(), collect_typedefs_rec(), convert_compound(), convert_function_declaration(), dump_typedefs(), and gather_global_typedefs().
|
protected |
Definition at line 85 of file dump_c_class.h.
Referenced by convert_compound(), and gather_global_typedefs().
|
protected |
Definition at line 53 of file dump_c_class.h.
Referenced by ignore().