74 for(code_typet::parameterst::iterator
75 it2=parameters.begin();
76 it2!=parameters.end();
102 typedef std::unordered_map<irep_idt, unsigned>
unique_tagst;
146 for(std::pair<unique_tagst::iterator, bool>
181 for(std::set<std::string>::const_iterator
208 std::vector<std::string>::iterator it =
241 goto_functionst::function_mapt::const_iterator
func_entry=
256 for(std::set<std::string>::const_iterator
276 for(std::set<std::string>::const_iterator
293 for(std::set<std::string>::const_iterator
297 os <<
"#include <" << *it <<
">\n";
307 os <<
"#ifndef NULL\n"
308 <<
"#define NULL ((void*)0)\n"
313 os <<
"#ifndef FENCE\n"
314 <<
"#define FENCE(x) ((void)0)\n"
319 os <<
"#ifndef IEEE_FLOAT_EQUAL\n"
320 <<
"#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n"
322 <<
"#ifndef IEEE_FLOAT_NOTEQUAL\n"
323 <<
"#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n"
409 for(find_symbols_sett::const_iterator
447 for(
const auto &parent : bases.
get_sub())
473 assert(component_name !=
"");
493 comp.get_is_padding())
604 os <<
" __attribute__ ((__transparent_union__))";
606 os <<
" __attribute__ ((__packed__))";
628 for(c_enum_typet::memberst::iterator
640 it->set_base_name(
new_bn);
644 std::make_pair(
bn, it->get_base_name()));
650 os <<
" __attribute__ ((__packed__))";
657 std::list<irep_idt> &local_static,
674 std::unordered_set<irep_idt> typedef_names;
676 typedef_names.insert(
td.first);
701 std::unordered_set<irep_idt>
deps;
715 std::unordered_set<irep_idt> &dependencies)
747 std::pair<typedef_mapt::iterator, bool> entry=
751 (early && entry.first->second.type_decl_str.empty()))
763 std::ostringstream
oss;
766 entry.first->second.type_decl_str=
oss.str();
773 entry.first->second.early=
true;
811 if(system_symbols.is_symbol_internal_symbol(symbol, system_headers))
814 collect_typedefs(symbol.
type,
false);
830 std::map<std::string, typedef_infot>
to_insert;
833 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>
forward_deps,
837 if(!
td.second.type_decl_str.empty())
839 if(
td.second.dependencies.empty())
846 for(
const auto &d :
td.second.dependencies)
855 typedef_infot t=
to_insert.begin()->second;
867 std::unordered_set<irep_idt> &
r_deps =
r_it->second;
868 for(std::unordered_set<irep_idt>::iterator it =
r_deps.begin();
879 std::unordered_set<irep_idt> &
f_deps =
f_it->second;
882 f_deps.erase(t.typedef_name);
886 const auto td_entry=typedef_map.find(*it);
900 os <<
td.type_decl_str <<
'\n';
927 os <<
"// " << symbol.
name <<
'\n';
928 os <<
"// " << symbol.
location <<
'\n';
935 for(find_symbols_sett::const_iterator
944 for(std::set<std::string>::const_iterator
963 os <<
"// " << symbol.
name <<
'\n';
964 os <<
"// " << symbol.
location <<
'\n';
1009 for(
auto &code :
b.statements())
1044 goto_functionst::function_mapt::const_iterator
func_entry=
1050 std::list<irep_idt>
type_decls, local_static;
1052 std::unordered_set<irep_idt> typedef_names;
1054 typedef_names.insert(
td.first);
1130 exprt::operandst::iterator &before)
1138 exprt::operandst::iterator
first_found=operands.end();
1157 found=
syms.find(identifier)!=
syms.end();
1207 const std::list<irep_idt> &local_static,
1213 for(std::list<irep_idt>::const_reverse_iterator
1214 it=local_static.rbegin();
1215 it!=local_static.rend();
1218 local_static_declst::const_iterator d_it=
1227 exprt::operandst::iterator before=
b.operands().end();
1234 dest_ptr->operands().insert(before, d);
1245 for(std::list<irep_idt>::const_reverse_iterator
1263 skip.add_source_location().set_comment(
os_body.str());
1268 exprt::operandst::iterator before=
b.operands().end();
1323 if(
u_type_f.get_component(
u.get_component_name()).get_is_padding())
1330 u.op().type().subtype().id()==
ID_empty &&
1331 (
u.op().is_zero() ||
1335 u_type_f.get_component(
u.get_component_name());
1373 if(parameters.size()==arguments.size())
1375 code_typet::parameterst::const_iterator it=parameters.begin();
1412 declared_enum_constants_mapt::const_iterator entry=
1416 entry->first!=entry->second)
1438 if(
bu.value().type() ==
comp.type())
1470 if(
bu.value().type() ==
comp.type())
1483 bu.source_location().get_function().empty())
1497 if(
bu.value().type() ==
comp.type())
1524 for(code_typet::parameterst::iterator
1553 return configuration;
1587 const bool use_all_headers,
1600 const bool use_all_headers,
1613 std::string base_name =
1622 const bool use_all_headers,
1625 const std::string
module,
1630 it != symbol_table.
end();
1633 symbolt &new_symbol = it.get_writeable_symbol();
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
std::size_t get_width() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
C enum tag type, i.e., c_enum_typet with an identifier.
std::vector< c_enum_membert > memberst
A codet representing sequential composition of program statements.
A codet representing the declaration of a local variable.
A codet representing the declaration of a local variable.
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
optionalt< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
codet representation of a function call statement.
exprt::operandst argumentst
A codet representing a skip statement.
std::vector< parametert > parameterst
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
optionalt< std::string > main
struct configt::ansi_ct ansi_c
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unordered_set< irep_idt > convertedt
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
void cleanup_expr(exprt &expr)
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)
std::string expr_to_string(const exprt &expr)
void operator()(std::ostream &out)
const goto_functionst & goto_functions
convertedt converted_compound
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...
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
typedef_typest typedef_types
symbol_tablet copied_symbol_table
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...
declared_enum_constants_mapt declared_enum_constants
std::string make_decl(const irep_idt &identifier, const typet &type)
convertedt converted_enum
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
std::set< std::string > system_headers
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ... } name;.
system_library_symbolst system_symbols
void convert_compound_enum(const typet &type, std::ostream &os)
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
const dump_c_configurationt dump_c_config
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
void cleanup_type(typet &type)
void cleanup_decl(code_frontend_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
std::string type_to_string(const typet &type)
std::unordered_map< irep_idt, code_frontend_declt > local_static_declst
static std::string indent(const unsigned n)
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)
convertedt converted_global
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
const std::string & get_string(const irep_idt &name) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Replace expression or type symbols by an expression or type, respectively.
const irep_idt & get_statement() const
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
const irep_idt & get_file() const
Struct constructor from list of elements.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Base type for structs and unions.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual iteratort begin() override
virtual iteratort end() override
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
exprt value
Initial value of symbol.
bool is_symbol_internal_symbol(const symbolt &symbol, std::set< std::string > &out_system_headers) const
To find out if a symbol is an internal symbol.
bool is_type_internal(const typet &type, std::set< std::string > &out_system_headers) const
Helper function to call is_symbol_internal_symbol on a nameless fake symbol with the given type,...
A tag-based type, i.e., typet with an identifier.
const irep_idt & get_identifier() const
void set_identifier(const irep_idt &identifier)
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
Union constructor from single element.
A union tag type, i.e., union_typet with an identifier.
Fixed-width bit-vector with unsigned binary interpretation.
std::ostream & operator<<(std::ostream &out, dump_ct &src)
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
static bool module_local_declaration(const symbolt &symbol, const std::string module)
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
static expr2c_configurationt expr2c_configuration()
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2cpp(const typet &type, const namespacet &ns)
std::string expr2cpp(const exprt &expr, const namespacet &ns)
#define Forall_operands(it, expr)
#define Forall_expr(it, expr)
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
std::unordered_set< irep_idt > find_symbols_sett
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
const code_function_callt & to_code_function_call(const codet &code)
Dump Goto-Program as C/C++ Source.
const std::string & id2string(const irep_idt &d)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define POSTCONDITION(CONDITION)
#define INITIALIZE_FUNCTION
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_blockt & to_code_block(const codet &code)
const codet & to_code(const exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
Used for configuring the behaviour of dump_c.
dump_c_configurationt disable_include_function_decls()
bool include_global_decls
Include the global declarations in the dump.
bool include_typedefs
Include the typedefs in the dump.
bool include_global_vars
Include global variable definitions in the dump.
static dump_c_configurationt default_configuration
The default used for dump-c and dump-cpp.
bool include_function_decls
Include the function declarations in the dump.
bool include_headers
Include headers type declarations are borrowed from.
bool include_compounds
Include struct definitions in the dump.
dump_c_configurationt disable_include_global_vars()
static dump_c_configurationt type_header_configuration
The config used for dump-c-type-header.
dump_c_configurationt disable_include_function_bodies()
dump_c_configurationt enable_include_headers()
bool include_function_bodies
Include the functions in the dump.
bool follow_compounds
Define whether to follow compunds recursively.
Used for configuring the behaviour of expr2c and type2c.
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)