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);
75 std::stringstream func_decl_stream;
76 std::stringstream compound_body_stream;
77 std::stringstream global_var_stream;
78 std::stringstream global_decl_stream;
79 std::stringstream global_decl_header_stream;
80 std::stringstream func_body_stream;
89 const symbolt &symbol = it->second;
92 (symbol.
type.
id() == ID_union || symbol.
type.
id() == ID_struct) &&
98 else if(
mode == ID_cpp)
103 typet &type = it.get_writeable_symbol().type;
104 if(ts.type.id() == ID_union)
108 additional_symbols.
add(ts);
111 if(symbol.
type.
id()!=ID_code)
117 for(code_typet::parameterst::iterator
118 it2=parameters.begin();
119 it2!=parameters.end();
122 typet &type=it2->type();
124 if(type.
id() == ID_union_tag && type.
get_bool(ID_C_transparent_union))
130 new_type_sym.
type.
set(ID_C_transparent_union,
true);
133 additional_symbols.
add(new_type_sym);
136 type.
remove(ID_C_transparent_union);
140 for(
const auto &symbol_pair : additional_symbols.
symbols)
145 typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
146 unique_tagst unique_tags;
150 std::set<std::string> symbols_sorted;
154 symbolt &symbol = it.get_writeable_symbol();
155 bool tag_added=
false;
160 if((symbol.
type.
id()==ID_union || symbol.
type.
id()==ID_struct) &&
164 symbol.
type.
set(ID_tag, ID_anonymous);
167 else if(symbol.
type.
id()==ID_c_enum &&
171 symbol.
type.
add(ID_tag).
set(ID_C_base_name, ID_anonymous);
175 const std::string name_str =
id2string(it->first);
177 (symbol.
type.
id()==ID_union ||
178 symbol.
type.
id()==ID_struct ||
179 symbol.
type.
id()==ID_c_enum))
181 std::string new_tag=symbol.
type.
id()==ID_c_enum?
185 std::string::size_type tag_pos=new_tag.rfind(
"tag-");
186 if(tag_pos!=std::string::npos)
187 new_tag.erase(0, tag_pos+4);
188 const std::string new_tag_base=new_tag;
190 for(std::pair<unique_tagst::iterator, bool>
191 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
192 !unique_entry.second;
193 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
195 new_tag=new_tag_base+
"$"+
196 std::to_string(unique_entry.first->second);
197 ++(unique_entry.first->second);
200 if(symbol.
type.
id()==ID_c_enum)
202 symbol.
type.
add(ID_tag).
set(ID_C_base_name, new_tag);
206 symbol.
type.
set(ID_tag, new_tag);
211 if((!tag_added || symbol.
is_type) &&
216 bool inserted=symbols_sorted.insert(name_str).second;
223 bool skip_function_main=
false;
224 std::vector<std::string> header_files;
225 for(std::set<std::string>::const_iterator
226 it=symbols_sorted.begin();
227 it!=symbols_sorted.end();
235 (type_id==ID_struct ||
241 global_decl_stream <<
"// " << symbol.
name <<
'\n';
242 global_decl_stream <<
"// " << symbol.
location <<
'\n';
244 std::string location_file =
249 location_file.length() > 1 &&
250 location_file[location_file.length() - 1] ==
'h')
252 std::vector<std::string>::iterator it =
253 find(header_files.begin(), header_files.end(), location_file);
254 if(it == header_files.end())
256 header_files.push_back(location_file);
257 global_decl_header_stream <<
"#include \"" << location_file
262 if(type_id==ID_c_enum)
264 else if(type_id == ID_struct)
283 else if(symbol.
type.
id()==ID_code)
285 goto_functionst::function_mapt::const_iterator func_entry=
290 func_entry->second.body_available() &&
291 (symbol.
name == ID_main ||
294 skip_function_main=
true;
300 for(std::set<std::string>::const_iterator
301 it=symbols_sorted.begin();
302 it!=symbols_sorted.end();
307 if(symbol.
type.
id()!=ID_code ||
320 for(std::set<std::string>::const_iterator
321 it=symbols_sorted.begin();
322 it!=symbols_sorted.end();
329 (symbol.
type.
id() == ID_struct || symbol.
type.
id() == ID_union) &&
334 compound_body_stream);
340 for(std::set<std::string>::const_iterator
344 os <<
"#include <" << *it <<
">\n";
349 os << global_decl_header_stream.str() <<
'\n';
351 if(global_var_stream.str().find(
"NULL")!=std::string::npos ||
352 func_body_stream.str().find(
"NULL")!=std::string::npos)
354 os <<
"#ifndef NULL\n"
355 <<
"#define NULL ((void*)0)\n"
358 if(func_body_stream.str().find(
"FENCE")!=std::string::npos)
360 os <<
"#ifndef FENCE\n"
361 <<
"#define FENCE(x) ((void)0)\n"
364 if(func_body_stream.str().find(
"IEEE_FLOAT_")!=std::string::npos)
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"
375 os << global_decl_stream.str() <<
'\n';
381 os << func_decl_stream.str() <<
'\n';
383 os << compound_body_stream.str() <<
'\n';
385 os << global_var_stream.str() <<
'\n';
387 os << func_body_stream.str();
393 std::ostream &os_body)
403 if(symbol.
type.
id() == ID_struct)
409 else if(symbol.
type.
id() == ID_union)
415 else if(symbol.
type.
id() == ID_c_enum)
425 const typet &unresolved,
430 type.
id() == ID_c_enum_tag || type.
id() == ID_struct_tag ||
431 type.
id() == ID_union_tag)
439 else if(type.
id()==ID_array || type.
id()==ID_pointer)
451 if(type.
id()==ID_array)
456 for(find_symbols_sett::const_iterator
463 type_symbol.
type.
id() == ID_c_enum
465 : (type_symbol.
type.
id() == ID_union ? ID_union_tag
472 else if(type.
id()==ID_struct || type.
id()==ID_union)
474 else if(type.
id()==ID_c_enum)
480 const typet &unresolved,
492 const irept &bases = type.
find(ID_bases);
493 std::stringstream base_decls;
494 for(
const auto &parent : bases.
get_sub())
499 assert(parent.id() == ID_base);
500 assert(parent.get(ID_type) == ID_struct_tag);
503 parent.find(ID_type).get(ID_identifier);
504 const irep_idt &renamed_base_id=global_renaming[base_id];
507 convert_compound_rec(parsymb.
type, os);
509 base_decls <<
id2string(renamed_base_id) +
510 (parent_it+1==bases.
get_sub().end()?
"":
", ");
516 string constructor_args;
517 string constructor_body;
519 std::string component_name =
id2string(renaming[compo.get(ID_name)]);
520 assert(component_name !=
"");
522 if(it != struct_type.components().begin()) constructor_args +=
", ";
524 if(compo.type().id() == ID_pointer)
525 constructor_args +=
type_to_string(compo.type()) + component_name;
527 constructor_args +=
"const " +
type_to_string(compo.type()) +
"& " + component_name;
529 constructor_body +=
indent +
indent +
"this->"+component_name +
" = " + component_name +
";\n";
532 std::stringstream struct_body;
536 const typet &comp_type = comp.type();
539 comp_type.
id() != ID_code,
"struct member must not be of code type");
541 if(comp.get_bool(ID_from_base) || comp.get_is_padding())
544 const typet *non_array_type = &comp_type;
545 while(non_array_type->
id()==ID_array)
555 if(non_array_type->
id() != ID_pointer && !is_anon)
561 struct_body <<
indent(1) <<
"// " << comp.get_name() <<
'\n';
568 std::string fake_unique_name=
"NO/SUCH/NS::"+
id2string(comp_name);
569 typet comp_type_to_use = comp.type();
572 comp_type_to_use =
ns.
follow(comp.type());
573 comp_type_to_use.
remove(ID_tag);
575 recursive && (comp_type_to_use.
id() == ID_struct ||
576 comp_type_to_use.
id() == ID_union))
578 const auto &sub_comps =
580 for(
const auto &sc : sub_comps)
584 std::string s =
make_decl(fake_unique_name, comp_type_to_use);
587 if(comp_type.
id()==ID_c_bit_field &&
598 else if(comp_type.
id()==ID_signedbv)
602 struct_body <<
"long long int " << comp_name
604 else if(
mode == ID_cpp)
605 struct_body <<
"__signedbv<" << t.
get_width() <<
"> "
610 else if(comp_type.
id()==ID_unsignedbv)
614 struct_body <<
"unsigned long long " << comp_name
616 else if(
mode == ID_cpp)
617 struct_body <<
"__unsignedbv<" << t.
get_width() <<
"> "
625 struct_body <<
";\n";
628 typet unresolved_clean=unresolved;
633 td_entry.first.get(ID_identifier) == unresolved.
get(ID_identifier) &&
636 unresolved_clean.
remove(ID_C_typedef);
637 typedef_str = td_entry.second;
638 std::pair<typedef_mapt::iterator, bool> td_map_entry =
641 if(!td_map_entry.first->second.early)
642 td_map_entry.first->second.type_decl_str.clear();
649 if(!base_decls.str().empty())
652 os <<
": " << base_decls.str();
656 os << struct_body.str();
671 if(type.
get_bool(ID_C_transparent_union))
672 os <<
" __attribute__ ((__transparent_union__))";
674 os <<
" __attribute__ ((__packed__))";
675 if(!typedef_str.
empty())
676 os <<
" " << typedef_str;
696 for(c_enum_typet::memberst::iterator
701 const irep_idt bn=it->get_base_name();
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,
726 std::list<irep_idt> &local_type_decls)
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)
785 std::unordered_set<irep_idt> local_deps;
787 if(type.
id()==ID_code)
792 for(
const auto ¶m : code_type.
parameters())
795 else if(type.
id()==ID_pointer || type.
id()==ID_array)
801 type.
id() == ID_c_enum_tag || type.
id() == ID_struct_tag ||
802 type.
id() == ID_union_tag)
808 const irep_idt &typedef_str=type.
get(ID_C_typedef);
810 if(!typedef_str.
empty())
812 std::pair<typedef_mapt::iterator, bool> entry=
816 (early && entry.first->second.type_decl_str.empty()))
818 if(typedef_str==
"__gnuc_va_list" || typedef_str ==
"va_list")
828 std::ostringstream oss;
829 oss <<
"typedef " <<
make_decl(typedef_str, t) <<
';';
831 entry.first->second.type_decl_str=oss.str();
832 entry.first->second.dependencies=local_deps;
838 entry.first->second.early=
true;
840 for(
const auto &d : local_deps)
844 td_entry->second.early=
true;
848 dependencies.insert(typedef_str);
851 dependencies.insert(local_deps.begin(), local_deps.end());
861 std::map<std::string, symbolt> symbols_sorted;
863 symbols_sorted.insert(
864 {
id2string(symbol_entry.first), symbol_entry.second});
866 for(
const auto &symbol_entry : symbols_sorted)
868 const symbolt &symbol=symbol_entry.second;
875 typedef_types[symbol.
type]=typedef_str;
876 if(system_symbols.is_symbol_internal_symbol(symbol, system_headers))
877 typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
879 collect_typedefs(symbol.
type,
false);
890 std::vector<typedef_infot> typedefs_sorted;
895 std::map<std::string, typedef_infot> to_insert;
897 std::unordered_set<irep_idt> typedefs_done;
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())
906 to_insert.insert({
id2string(td.first), td.second});
910 forward_deps.insert({td.first, td.second.dependencies});
911 for(
const auto &d : td.second.dependencies)
912 reverse_deps[d].insert(td.first);
916 while(!to_insert.empty())
920 typedef_infot t=to_insert.begin()->second;
921 to_insert.erase(to_insert.begin());
923 typedefs_sorted.push_back(t);
927 auto r_it=reverse_deps.find(t.typedef_name);
928 if(r_it==reverse_deps.end())
932 std::unordered_set<irep_idt> &r_deps = r_it->second;
933 for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
936 auto f_it=forward_deps.find(*it);
937 if(f_it==forward_deps.end())
944 std::unordered_set<irep_idt> &f_deps = f_it->second;
946 PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
947 f_deps.erase(t.typedef_name);
951 const auto td_entry=typedef_map.find(*it);
953 to_insert.insert({
id2string(*it), td_entry->second});
954 forward_deps.erase(*it);
964 for(
const auto &td : typedefs_sorted)
965 os << td.type_decl_str <<
'\n';
967 if(!typedefs_sorted.empty())
990 os <<
"// " << symbol.
name <<
'\n';
991 os <<
"// " << symbol.
location <<
'\n';
997 std::set<std::string> symbols_sorted;
998 for(find_symbols_sett::const_iterator
1003 bool inserted=symbols_sorted.insert(
id2string(*it)).second;
1007 for(std::set<std::string>::const_iterator
1008 it=symbols_sorted.begin();
1009 it!=symbols_sorted.end();
1022 local_static_decls.emplace(symbol.
name, d);
1026 os <<
"// " << symbol.
name <<
'\n';
1027 os <<
"// " << symbol.
location <<
'\n';
1029 std::list<irep_idt> empty_static, empty_types;
1044 const symbolt *argc_sym=
nullptr;
1052 const symbolt *argv_sym=
nullptr;
1063 const symbolt *return_sym=
nullptr;
1064 if(!
ns.
lookup(
"return'", return_sym))
1074 if(code.get_statement()==ID_function_call)
1077 if(func.
id()==ID_symbol)
1096 const bool skip_main,
1097 std::ostream &os_decl,
1098 std::ostream &os_body,
1107 goto_functionst::function_mapt::const_iterator func_entry=
1110 func_entry->second.body_available())
1113 std::list<irep_idt> type_decls, local_static;
1115 std::unordered_set<irep_idt> typedef_names;
1117 typedef_names.insert(td.first);
1121 func_entry->second.body,
1152 os_body <<
"// " << symbol.
name <<
'\n';
1153 os_body <<
"// " << symbol.
location <<
'\n';
1170 symbol.
name!=ID_main)
1172 os_decl <<
"// " << symbol.
name <<
'\n';
1173 os_decl <<
"// " << symbol.
location <<
'\n';
1178 os_decl <<
"// " << symbol.
name <<
'\n';
1179 os_decl <<
"// " << symbol.
location <<
'\n';
1193 exprt::operandst::iterator &before)
1201 exprt::operandst::iterator first_found=operands.end();
1208 if(it->id()==ID_code &&
1220 found=syms.find(identifier)!=syms.end();
1241 if(first_found==operands.end())
1258 if(first_found!=operands.end())
1270 const std::list<irep_idt> &local_static,
1272 std::list<irep_idt> &type_decls)
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=
1282 local_static_decls.find(*it);
1286 std::list<irep_idt> redundant;
1290 exprt::operandst::iterator before=b.
operands().end();
1297 dest_ptr->
operands().insert(before, d);
1304 const std::list<irep_idt> &type_decls)
1308 for(std::list<irep_idt>::const_reverse_iterator
1309 it=type_decls.rbegin();
1310 it!=type_decls.rend();
1316 std::ostringstream os_body;
1317 os_body << *it <<
" */\n";
1319 type.
id() == ID_c_enum
1321 : (type.
id() == ID_union ? ID_union_tag : ID_struct_tag);
1331 exprt::operandst::iterator before=b.
operands().end();
1338 dest_ptr->
operands().insert(before, skip);
1350 if(expr.
id()==ID_struct)
1362 exprt::operandst::iterator o_it=old_ops.begin();
1363 for(
const auto &old_comp : old_components)
1365 const bool is_zero_bit_field =
1366 old_comp.type().id() == ID_c_bit_field &&
1369 if(!old_comp.get_is_padding() && !is_zero_bit_field)
1378 else if(expr.
id()==ID_union)
1384 !u_type_f.
get_bool(ID_C_transparent_union))
1411 expr.
id() == ID_typecast &&
1418 else if(expr.
id()==ID_code &&
1419 to_code(expr).get_statement()==ID_function_call &&
1434 if(parameters.size()==arguments.size())
1436 code_typet::parameterst::const_iterator it=parameters.begin();
1437 for(
auto &argument : arguments)
1440 if(type.
id()==ID_union &&
1441 type.
get_bool(ID_C_transparent_union))
1443 if(argument.id() == ID_typecast && argument.type() == type)
1448 argument.is_constant() &&
1451 const typet &comp_type=
1454 if(comp_type.
id()==ID_pointer)
1469 if(!cformat.
empty())
1471 declared_enum_constants_mapt::const_iterator entry=
1475 entry->first!=entry->second)
1476 expr.
set(ID_C_cformat, entry->second);
1479 expr.
remove(ID_C_cformat);
1484 expr.
id() == ID_byte_update_little_endian ||
1485 expr.
id() == ID_byte_update_big_endian)
1495 for(
const auto &comp : union_type.
components())
1499 exprt member1{ID_member};
1501 exprt designated_initializer1{ID_designated_initializer};
1503 designated_initializer1.add(ID_designator).move_to_sub(member1);
1505 exprt member2{ID_member};
1506 member2.
set(ID_component_name, comp.get_name());
1507 exprt designated_initializer2{ID_designated_initializer};
1509 designated_initializer2.add(ID_designator).move_to_sub(member2);
1511 binary_exprt initializer_list{std::move(designated_initializer1),
1512 ID_initializer_list,
1513 std::move(designated_initializer2)};
1514 expr.
swap(initializer_list);
1521 bu.
op().
id() == ID_side_effect &&
1527 for(
const auto &comp : union_type.
components())
1532 expr.
swap(union_expr);
1546 if(clean_init->id() != ID_struct || clean_init->has_operands())
1550 if(clean_init.has_value() && bu.
op() == *clean_init)
1554 for(
const auto &comp : union_type.
components())
1559 expr.
swap(union_expr);
1570 else if(expr.
id() == ID_member)
1583 if(type.
id()==ID_code)
1589 for(code_typet::parameterst::iterator
1596 if(type.
id()==ID_array)
1614 return configuration;
1625 else if(
mode == ID_cpp)
1639 else if(
mode == ID_cpp)
1647 const bool use_system_headers,
1648 const bool use_all_headers,
1649 const bool include_harness,
1654 src, use_system_headers, use_all_headers, include_harness, ns, ID_C);
1660 const bool use_system_headers,
1661 const bool use_all_headers,
1662 const bool include_harness,
1667 src, use_system_headers, use_all_headers, include_harness, ns, ID_cpp);
1674 std::string base_name =
1677 return (base_name == module && symbol_module == module);
1682 const bool use_system_headers,
1683 const bool use_all_headers,
1684 const bool include_harness,
1686 const std::string module,
1691 it != symbol_table.
end();
1694 symbolt &new_symbol = it.get_writeable_symbol();
1697 new_symbol.
type.
set(ID_C_do_not_dump, 0);
1701 new_symbol.
type.
set(ID_C_do_not_dump, 1);
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.
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...
const exprt & offset() const
const exprt & value() const
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.
code_operandst & statements()
void add(const codet &code)
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
const parameterst & parameters() const
const typet & return_type() const
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_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
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.
void update()
Update all indices.
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.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
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.
irep_idt get_component_name() const
void set_component_name(const irep_idt &component_name)
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.
const typet & base_type() const
The type of the data what we point to.
Replace a symbol expression by a given expression.
const irep_idt & get_statement() const
Fixed-width bit-vector with two's complement interpretation.
void set_comment(const irep_idt &comment)
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.
bool get_is_padding() const
Base type for structs and unions.
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool is_incomplete() const
A struct/union may be incomplete.
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
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
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.
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.
const irep_idt & get_identifier() const
void set_identifier(const irep_idt &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.
const source_locationt & source_location() const
Generic base class for unary expressions.
Union constructor from single element.
irep_idt get_component_name() const
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)
nonstd::optional< T > optionalt
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.
std::size_t long_long_int_width
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.
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)