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 bool include_harness, const namespacet &_ns, language_factoryt factory) | |
virtual | ~dump_ct ()=default |
void | operator() (std::ostream &out) |
Protected Types | |
typedef std::unordered_set< irep_idt > | convertedt |
typedef std::unordered_map< irep_idt, irep_idt > | 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 > | local_static_declst |
Protected Member Functions | |
std::string | type_to_string (const typet &type) |
std::string | expr_to_string (const exprt &expr) |
std::string | make_decl (const irep_idt &identifier, const typet &type) |
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 for eventual output. More... | |
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 for eventual output. More... | |
void | gather_global_typedefs () |
Find all global typdefs in the symbol table and store them in typedef_types. More... | |
void | dump_typedefs (std::ostream &os) const |
Print all typedefs that are not covered via typedef struct xyz { ... More... | |
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) |
void | cleanup_harness (code_blockt &b) |
Replace CPROVER internal symbols in b by printable values and generate necessary declarations. More... | |
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 |
std::unique_ptr< languaget > | language |
const bool | harness |
convertedt | converted_compound |
convertedt | converted_global |
convertedt | converted_enum |
std::set< std::string > | system_headers |
system_library_symbolst | system_symbols |
declared_enum_constants_mapt | declared_enum_constants |
typedef_mapt | typedef_map |
typedef_typest | typedef_types |
Definition at line 24 of file dump_c_class.h.
|
protected |
Definition at line 55 of file dump_c_class.h.
|
protected |
Definition at line 62 of file dump_c_class.h.
|
protected |
Definition at line 131 of file dump_c_class.h.
|
protected |
Definition at line 79 of file dump_c_class.h.
|
protected |
Definition at line 81 of file dump_c_class.h.
|
inline |
Definition at line 27 of file dump_c_class.h.
References system_library_symbolst::set_use_all_headers(), and system_symbols.
|
virtualdefault |
|
protected |
Definition at line 587 of file dump_c.cpp.
References goto_programt::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 1209 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(), 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 |
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
b | Code block to be cleaned |
Definition at line 910 of file dump_c.cpp.
References code_blockt::add(), CPROVER_PREFIX, Forall_operands, code_function_callt::function(), symbol_exprt::get_identifier(), codet::get_statement(), irept::id(), id2string(), INITIALIZE_FUNCTION, replace_symbolt::insert(), namespacet::lookup(), symbolt::name, ns, symbol_exprt::set_identifier(), irept::swap(), to_code(), to_code_function_call(), to_symbol_expr(), and symbolt::type.
Referenced by convert_function_declaration().
|
protected |
Definition at line 1356 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 |
Find any typedef names contained in the input type and store their declaration strings in typedef_map for eventual output.
type | type to inspect for ID_C_typedef entry |
early | set to true to enforce that typedef is dumped before any function declarations or struct definitions |
Definition at line 637 of file dump_c.cpp.
References collect_typedefs_rec().
Referenced by convert_compound(), convert_function_declaration(), and gather_global_typedefs().
|
protected |
Find any typedef names contained in the input type and store their declaration strings in typedef_map for eventual output.
type | type to inspect for ID_C_typedef entry | |
early | set to true to enforce that typedef is dumped before any function declarations or struct definitions | |
[out] | dependencies | typedefs used in the declaration of a given typedef |
Definition at line 650 of file dump_c.cpp.
References dstringt::empty(), irept::get(), irept::id(), system_library_symbolst::is_type_internal(), namespacet::lookup(), make_decl(), ns, code_typet::parameters(), PRECONDITION, irept::remove(), code_typet::return_type(), typet::subtype(), system_headers, system_symbols, to_code_type(), to_symbol_type(), symbolt::type, and typedef_map.
Referenced by collect_typedefs().
|
protected |
Definition at line 311 of file dump_c.cpp.
References convert_compound_enum(), DATA_INVARIANT, find_non_pointer_type_symbols(), irept::id(), system_library_symbolst::is_symbol_internal_symbol(), symbolt::is_type, namespacet::lookup(), ns, typet::subtype(), system_headers, system_symbols, 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 364 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(), 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 297 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 544 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_table_baset::has_symbol(), irept::id(), id2string(), PRECONDITION, to_c_enum_type(), and type_to_string().
Referenced by convert_compound(), and operator()().
|
protected |
Definition at line 964 of file dump_c.cpp.
References cleanup_harness(), collect_typedefs(), converted_compound, converted_enum, copied_symbol_table, CPROVER_PREFIX, declared_enum_constants, goto_functionst::entry_point(), expr_to_string(), goto_functionst::function_map, goto_functions, harness, id2string(), 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 842 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 |
Print all typedefs that are not covered via typedef struct xyz { ...
} name;
[out] | os | output stream |
Definition at line 757 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 1391 of file dump_c.cpp.
References cleanup_expr(), language, and ns.
Referenced by convert_function_declaration(), convert_global_variable(), and make_decl().
|
protected |
Find all global typdefs in the symbol table and store them in typedef_types.
Definition at line 726 of file dump_c.cpp.
References collect_typedefs(), copied_symbol_table, dstringt::empty(), irept::get(), source_locationt::get_function(), id2string(), symbolt::is_macro, system_library_symbolst::is_symbol_internal_symbol(), symbolt::is_type, symbolt::location, PRECONDITION, symbol_table_baset::symbols, system_headers, system_symbols, symbolt::type, typedef_map, and typedef_types.
Referenced by operator()().
|
inlinestaticprotected |
Definition at line 87 of file dump_c_class.h.
Referenced by convert_compound().
|
protected |
Definition at line 1138 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 1172 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 92 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 34 of file dump_c.cpp.
References symbol_table_baset::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(), goto_functionst::entry_point(), irept::find(), goto_functionst::function_map, gather_global_typedefs(), irept::get(), irept::get_bool(), source_locationt::get_function(), irept::get_string(), symbol_tablet::get_writeable(), symbol_table_baset::get_writeable_ref(), goto_functions, harness, irept::id(), id2string(), symbolt::is_static_lifetime, system_library_symbolst::is_symbol_internal_symbol(), 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_table_baset::symbols, system_headers, system_symbols, to_code_type(), to_string(), to_symbol_type(), symbolt::type, and type_to_string().
|
protected |
Definition at line 1382 of file dump_c.cpp.
References cleanup_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 63 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 53 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(), and type_to_string().
|
protected |
Definition at line 51 of file dump_c_class.h.
Referenced by cleanup_expr(), cleanup_harness(), 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_compound(), convert_function_declaration(), gather_global_typedefs(), and operator()().
|
protected |
Definition at line 60 of file dump_c_class.h.
Referenced by collect_typedefs_rec(), convert_compound(), dump_ct(), gather_global_typedefs(), and operator()().
|
protected |
Definition at line 80 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 82 of file dump_c_class.h.
Referenced by convert_compound(), and gather_global_typedefs().