42 if(
c >=
'0' &&
c <=
'9')
44 else if(
c >=
'A' &&
c <=
'Z')
46 else if(
c >=
'a' &&
c <=
'z')
48 else if(
c ==
'_' ||
c ==
'$')
51 result +=
"_" + std::to_string(
c);
89 const symbolt &symbol = it->second;
103 typet &type = it.get_writeable_symbol().type;
117 for(code_typet::parameterst::iterator
118 it2=parameters.begin();
119 it2!=parameters.end();
145 typedef std::unordered_map<irep_idt, unsigned>
unique_tagst;
154 symbolt &symbol = it.get_writeable_symbol();
190 for(std::pair<unique_tagst::iterator, bool>
225 for(std::set<std::string>::const_iterator
252 std::vector<std::string>::iterator it =
285 goto_functionst::function_mapt::const_iterator
func_entry=
300 for(std::set<std::string>::const_iterator
320 for(std::set<std::string>::const_iterator
340 for(std::set<std::string>::const_iterator
344 os <<
"#include <" << *it <<
">\n";
354 os <<
"#ifndef NULL\n"
355 <<
"#define NULL ((void*)0)\n"
360 os <<
"#ifndef FENCE\n"
361 <<
"#define FENCE(x) ((void)0)\n"
366 os <<
"#ifndef IEEE_FLOAT_EQUAL\n"
367 <<
"#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n"
369 <<
"#ifndef IEEE_FLOAT_NOTEQUAL\n"
370 <<
"#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n"
456 for(find_symbols_sett::const_iterator
494 for(
const auto &parent : bases.
get_sub())
520 assert(component_name !=
"");
672 os <<
" __attribute__ ((__transparent_union__))";
674 os <<
" __attribute__ ((__packed__))";
696 for(c_enum_typet::memberst::iterator
708 it->set_base_name(
new_bn);
712 std::make_pair(
bn, it->get_base_name()));
718 os <<
" __attribute__ ((__packed__))";
725 std::list<irep_idt> &local_static,
742 std::unordered_set<irep_idt> typedef_names;
744 typedef_names.insert(
td.first);
769 std::unordered_set<irep_idt>
deps;
783 std::unordered_set<irep_idt> &dependencies)
812 std::pair<typedef_mapt::iterator, bool> entry=
816 (early && entry.first->second.type_decl_str.empty()))
828 std::ostringstream
oss;
831 entry.first->second.type_decl_str=
oss.str();
838 entry.first->second.early=
true;
876 if(system_symbols.is_symbol_internal_symbol(symbol, system_headers))
879 collect_typedefs(symbol.
type,
false);
895 std::map<std::string, typedef_infot>
to_insert;
898 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>
forward_deps,
902 if(!
td.second.type_decl_str.empty())
904 if(
td.second.dependencies.empty())
911 for(
const auto &d :
td.second.dependencies)
920 typedef_infot t=
to_insert.begin()->second;
932 std::unordered_set<irep_idt> &
r_deps =
r_it->second;
933 for(std::unordered_set<irep_idt>::iterator it =
r_deps.begin();
944 std::unordered_set<irep_idt> &
f_deps =
f_it->second;
947 f_deps.erase(t.typedef_name);
951 const auto td_entry=typedef_map.find(*it);
965 os <<
td.type_decl_str <<
'\n';
990 os <<
"// " << symbol.
name <<
'\n';
991 os <<
"// " << symbol.
location <<
'\n';
998 for(find_symbols_sett::const_iterator
1007 for(std::set<std::string>::const_iterator
1026 os <<
"// " << symbol.
name <<
'\n';
1027 os <<
"// " << symbol.
location <<
'\n';
1072 for(
auto &code :
b.statements())
1107 goto_functionst::function_mapt::const_iterator
func_entry=
1113 std::list<irep_idt>
type_decls, local_static;
1115 std::unordered_set<irep_idt> typedef_names;
1117 typedef_names.insert(
td.first);
1193 exprt::operandst::iterator &before)
1201 exprt::operandst::iterator
first_found=operands.end();
1270 const std::list<irep_idt> &local_static,
1276 for(std::list<irep_idt>::const_reverse_iterator
1277 it=local_static.rbegin();
1278 it!=local_static.rend();
1281 local_static_declst::const_iterator d_it=
1290 exprt::operandst::iterator before=
b.operands().end();
1297 dest_ptr->operands().insert(before, d);
1308 for(std::list<irep_idt>::const_reverse_iterator
1313 const typet &type=
ns.lookup(*it).type;
1326 skip.add_source_location().set_comment(
os_body.str());
1331 exprt::operandst::iterator before=
b.operands().end();
1386 if(
u_type_f.get_component(
u.get_component_name()).get_is_padding())
1396 u_type_f.get_component(
u.get_component_name());
1428 if(!
ns.lookup(
fn.get_identifier(), s))
1434 if(parameters.size()==arguments.size())
1436 code_typet::parameterst::const_iterator it=parameters.begin();
1439 const typet &type=
ns.follow(it->type());
1471 declared_enum_constants_mapt::const_iterator entry=
1475 entry->first!=entry->second)
1497 if(
bu.value().type() ==
comp.type())
1523 ns.follow(
bu.op().type()).id() ==
ID_union &&
bu.offset().is_zero())
1529 if(
bu.value().type() ==
comp.type())
1542 bu.source_location().get_function().empty())
1556 if(
bu.value().type() ==
comp.type())
1589 for(code_typet::parameterst::iterator
1614 return configuration;
1648 const bool use_all_headers,
1661 const bool use_all_headers,
1674 std::string base_name =
1683 const bool use_all_headers,
1686 const std::string
module,
1691 it != symbol_table.
end();
1694 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...
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 goto_instruction_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...
goto_instruction_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
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.
bool is_constant() const
Return whether the expression is a constant.
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.
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
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Replace a symbol expression by a given expression.
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
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.
irep_idt mode
Language mode.
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.
A tag-based type, i.e., typet with an identifier.
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
std::string cpp_type2name(const typet &type)
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)
static std::string clean_identifier(const irep_idt &id)
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)
static std::string clean_identifier(const irep_idt &id)
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.
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables,...
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
Collect type tags contained in src when the expression of such a type is not a pointer,...
find_symbols_sett find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables.
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 goto_instruction_codet &code)
Dump Goto-Program as C/C++ Source.
const std::string & id2string(const irep_idt &d)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_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.
bool can_cast_type< tag_typet >(const typet &type)
Check whether a reference to a typet is a tag_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()
static dump_c_configurationt default_configuration
The default used for dump-c and dump-cpp.
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()
Used for configuring the behaviour of expr2c and type2c.
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)