39 std::stringstream func_decl_stream;
40 std::stringstream compound_body_stream;
41 std::stringstream global_var_stream;
42 std::stringstream global_decl_stream;
43 std::stringstream func_body_stream;
53 if(symbol.
type.
id()!=ID_code)
59 for(code_typet::parameterst::iterator
60 it2=parameters.begin();
61 it2!=parameters.end();
64 typet &type=it2->type();
66 if(type.
id()==ID_symbol &&
67 type.
get_bool(ID_C_transparent_union))
73 new_type_sym.
type.
set(ID_C_transparent_union,
true);
76 symbols_transparent.
add(new_type_sym);
79 type.
remove(ID_C_transparent_union);
86 typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
87 unique_tagst unique_tags;
91 std::set<std::string> symbols_sorted;
100 if((symbol.
type.
id()==ID_union || symbol.
type.
id()==ID_struct) &&
104 symbol.
type.
set(ID_tag, ID_anonymous);
107 else if(symbol.
type.
id()==ID_c_enum &&
111 symbol.
type.
add(ID_tag).
set(ID_C_base_name, ID_anonymous);
115 const std::string name_str=
id2string(it->first);
117 (symbol.
type.
id()==ID_union ||
118 symbol.
type.
id()==ID_struct ||
119 symbol.
type.
id()==ID_c_enum))
121 std::string new_tag=symbol.
type.
id()==ID_c_enum?
126 if(tag_pos!=std::string::npos)
127 new_tag.erase(0, tag_pos+4);
128 const std::string new_tag_base=new_tag;
130 for(std::pair<unique_tagst::iterator, bool>
131 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
132 !unique_entry.second;
133 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
135 new_tag=new_tag_base+
"$"+
136 std::to_string(unique_entry.first->second);
137 ++(unique_entry.first->second);
140 if(symbol.
type.
id()==ID_c_enum)
142 symbol.
type.
add(ID_tag).
set(ID_C_base_name, new_tag);
146 symbol.
type.
set(ID_tag, new_tag);
154 bool inserted=symbols_sorted.insert(name_str).second;
161 bool skip_function_main=
false;
162 for(std::set<std::string>::const_iterator
163 it=symbols_sorted.begin();
164 it!=symbols_sorted.end();
172 (type_id==ID_struct ||
173 type_id==ID_incomplete_struct ||
175 type_id==ID_incomplete_union ||
180 global_decl_stream <<
"// " << symbol.
name <<
'\n';
181 global_decl_stream <<
"// " << symbol.
location <<
'\n';
183 if(type_id==ID_c_enum)
195 else if(symbol.
type.
id()==ID_code)
197 goto_functionst::function_mapt::const_iterator func_entry=
201 func_entry->second.body_available() &&
202 (symbol.
name==ID_main ||
204 skip_function_main=
true;
209 for(std::set<std::string>::const_iterator
210 it=symbols_sorted.begin();
211 it!=symbols_sorted.end();
216 if(symbol.
type.
id()!=ID_code ||
229 for(std::set<std::string>::const_iterator
230 it=symbols_sorted.begin();
231 it!=symbols_sorted.end();
237 (symbol.
type.
id()==ID_struct ||
238 symbol.
type.
id()==ID_incomplete_struct ||
239 symbol.
type.
id()==ID_union ||
240 symbol.
type.
id()==ID_incomplete_union))
243 compound_body_stream);
248 for(std::set<std::string>::const_iterator
252 os <<
"#include <" << *it <<
">\n";
256 if(global_var_stream.str().find(
"NULL")!=std::string::npos ||
257 func_body_stream.str().find(
"NULL")!=std::string::npos)
259 os <<
"#ifndef NULL\n" 260 <<
"#define NULL ((void*)0)\n" 263 if(func_body_stream.str().find(
"FENCE")!=std::string::npos)
265 os <<
"#ifndef FENCE\n" 266 <<
"#define FENCE(x) ((void)0)\n" 269 if(func_body_stream.str().find(
"IEEE_FLOAT_")!=std::string::npos)
271 os <<
"#ifndef IEEE_FLOAT_EQUAL\n" 272 <<
"#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n" 274 <<
"#ifndef IEEE_FLOAT_NOTEQUAL\n" 275 <<
"#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n" 279 if(!global_decl_stream.str().empty())
280 os << global_decl_stream.str() <<
'\n';
284 if(!func_decl_stream.str().empty())
285 os << func_decl_stream.str() <<
'\n';
286 if(!compound_body_stream.str().empty())
287 os << compound_body_stream.str() <<
'\n';
288 if(!global_var_stream.str().empty())
289 os << global_var_stream.str() <<
'\n';
290 os << func_body_stream.str();
296 std::ostream &os_body)
302 if(symbol.
type.
id()==ID_struct ||
303 symbol.
type.
id()==ID_union ||
304 symbol.
type.
id()==ID_c_enum)
310 const typet &unresolved,
314 if(type.
id()==ID_symbol)
323 else if(type.
id()==ID_c_enum_tag)
332 else if(type.
id()==ID_array || type.
id()==ID_pointer)
340 if(type.
id()==ID_array)
345 for(find_symbols_sett::const_iterator
355 else if(type.
id()==ID_struct || type.
id()==ID_union)
357 else if(type.
id()==ID_c_enum)
363 const typet &unresolved,
375 const irept &bases = type.
find(ID_bases);
376 std::stringstream base_decls;
414 std::stringstream struct_body;
416 for(struct_union_typet::componentst::const_iterator
424 if(comp_type.
id()==ID_code ||
430 while(non_array_type->
id()==ID_array)
435 if(non_array_type->
id()!=ID_pointer)
443 struct_body <<
indent(1) <<
"// " << comp_name <<
'\n';
448 std::string fake_unique_name=
"NO/SUCH/NS::"+
id2string(comp_name);
452 if(comp_type.
id()==ID_c_bit_field &&
459 if(s.find(
"__CPROVER_bitvector")==std::string::npos)
463 else if(comp_type.
id()==ID_signedbv)
467 struct_body <<
"long long int " << comp_name
470 struct_body <<
"__signedbv<" << t.
get_width() <<
"> " 475 else if(comp_type.
id()==ID_unsignedbv)
479 struct_body <<
"unsigned long long " << comp_name
482 struct_body <<
"__unsignedbv<" << t.
get_width() <<
"> " 490 struct_body <<
";\n";
493 typet unresolved_clean=unresolved;
494 typedef_typest::const_iterator td_entry=
499 unresolved_clean.
remove(ID_C_typedef);
500 typedef_str=td_entry->second;
501 std::pair<typedef_mapt::iterator, bool> td_map_entry=
504 if(!td_map_entry.first->second.early)
505 td_map_entry.first->second.type_decl_str=
"";
510 if(!base_decls.str().empty())
513 os <<
": " << base_decls.str();
517 os << struct_body.str();
532 if(type.
get_bool(ID_C_transparent_union))
533 os <<
" __attribute__ ((__transparent_union__))";
535 os <<
" __attribute__ ((__packed__))";
536 if(!typedef_str.
empty())
537 os <<
" " << typedef_str;
548 const irep_idt &name=tag.get(ID_C_base_name);
557 for(c_enum_typet::memberst::iterator
562 const irep_idt bn=it->get_base_name();
569 it->set_base_name(new_bn);
573 std::make_pair(bn, it->get_base_name()));
579 os <<
" __attribute__ ((__packed__))";
584 #define ADD_TO_SYSTEM_LIBRARY(v, header) \ 585 for(size_t i=0; i<sizeof(v)/sizeof(char*); ++i) \ 586 system_library_map.insert( \ 587 std::make_pair(v[i], header)) 592 const char* ctype_syms[]=
594 "isalnum",
"isalpha",
"isblank",
"iscntrl",
"isdigit",
"isgraph",
595 "islower",
"isprint",
"ispunct",
"isspace",
"isupper",
"isxdigit",
601 const char* fcntl_syms[]=
603 "creat",
"fcntl",
"open" 608 const char* locale_syms[]=
615 const char* math_syms[]=
617 "acos",
"acosh",
"asin",
"asinh",
"atan",
"atan2",
"atanh",
618 "cbrt",
"ceil",
"copysign",
"cos",
"cosh",
"erf",
"erfc",
"exp",
619 "exp2",
"expm1",
"fabs",
"fdim",
"floor",
"fma",
"fmax",
"fmin",
620 "fmod",
"fpclassify",
"frexp",
"hypot",
"ilogb",
"isfinite",
621 "isinf",
"isnan",
"isnormal",
"j0",
"j1",
"jn",
"ldexp",
"lgamma",
622 "llrint",
"llround",
"log",
"log10",
"log1p",
"log2",
"logb",
623 "lrint",
"lround",
"modf",
"nan",
"nearbyint",
"nextafter",
"pow",
624 "remainder",
"remquo",
"rint",
"round",
"scalbln",
"scalbn",
625 "signbit",
"sin",
"sinh",
"sqrt",
"tan",
"tanh",
"tgamma",
626 "trunc",
"y0",
"y1",
"yn" 631 const char* pthread_syms[]=
633 "pthread_cleanup_pop",
"pthread_cleanup_push",
634 "pthread_cond_broadcast",
"pthread_cond_destroy",
635 "pthread_cond_init",
"pthread_cond_signal",
636 "pthread_cond_timedwait",
"pthread_cond_wait",
"pthread_create",
637 "pthread_detach",
"pthread_equal",
"pthread_exit",
638 "pthread_getspecific",
"pthread_join",
"pthread_key_delete",
639 "pthread_mutex_destroy",
"pthread_mutex_init",
640 "pthread_mutex_lock",
"pthread_mutex_trylock",
641 "pthread_mutex_unlock",
"pthread_once",
"pthread_rwlock_destroy",
642 "pthread_rwlock_init",
"pthread_rwlock_rdlock",
643 "pthread_rwlock_unlock",
"pthread_rwlock_wrlock",
644 "pthread_rwlockattr_destroy",
"pthread_rwlockattr_getpshared",
645 "pthread_rwlockattr_init",
"pthread_rwlockattr_setpshared",
646 "pthread_self",
"pthread_setspecific",
648 "tag-__pthread_internal_list",
"tag-__pthread_mutex_s",
654 const char* setjmp_syms[]=
656 "_longjmp",
"_setjmp",
"longjmp",
"longjmperror",
"setjmp",
657 "siglongjmp",
"sigsetjmp" 662 const char* stdio_syms[]=
664 "asprintf",
"clearerr",
"fclose",
"fdopen",
"feof",
"ferror",
665 "fflush",
"fgetc",
"fgetln",
"fgetpos",
"fgets",
"fgetwc",
666 "fgetws",
"fileno",
"fopen",
"fprintf",
"fpurge",
"fputc",
667 "fputs",
"fputwc",
"fputws",
"fread",
"freopen",
"fropen",
668 "fscanf",
"fseek",
"fsetpos",
"ftell",
"funopen",
"fwide",
669 "fwopen",
"fwprintf",
"fwrite",
"getc",
"getchar",
"getdelim",
670 "getline",
"gets",
"getw",
"getwc",
"getwchar",
"mkdtemp",
671 "mkstemp",
"mktemp",
"perror",
"printf",
"putc",
"putchar",
672 "puts",
"putw",
"putwc",
"putwchar",
"remove",
"rewind",
"scanf",
673 "setbuf",
"setbuffer",
"setlinebuf",
"setvbuf",
"snprintf",
674 "sprintf",
"sscanf",
"swprintf",
"sys_errlist",
675 "sys_nerr",
"tempnam",
"tmpfile",
"tmpnam",
"ungetc",
"ungetwc",
676 "vasprintf",
"vfprintf",
"vfscanf",
"vfwprintf",
"vprintf",
677 "vscanf",
"vsnprintf",
"vsprintf",
"vsscanf",
"vswprintf",
678 "vwprintf",
"wprintf",
680 "tag-__sFILE",
"tag-__sbuf",
681 "tag-_IO_FILE",
"tag-_IO_marker",
686 const char* stdlib_syms[]=
688 "abort",
"abs",
"atexit",
"atof",
"atoi",
"atol",
"atoll",
689 "bsearch",
"calloc",
"div",
"exit",
"free",
"getenv",
"labs",
690 "ldiv",
"llabs",
"lldiv",
"malloc",
"mblen",
"mbstowcs",
"mbtowc",
691 "qsort",
"rand",
"realloc",
"srand",
"strtod",
"strtof",
"strtol",
692 "strtold",
"strtoll",
"strtoul",
"strtoull",
"system",
"wcstombs",
698 const char* string_syms[]=
700 "strcat",
"strncat",
"strchr",
"strrchr",
"strcmp",
"strncmp",
701 "strcpy",
"strncpy",
"strerror",
"strlen",
"strpbrk",
"strspn",
702 "strcspn",
"strstr",
"strtok" 707 const char* time_syms[]=
709 "asctime",
"asctime_r",
"ctime",
"ctime_r",
"difftime",
"gmtime",
710 "gmtime_r",
"localtime",
"localtime_r",
"mktime",
"strftime",
712 "tag-timespec",
"tag-timeval",
"tag-tm" 717 const char* unistd_syms[]=
719 "_exit",
"access",
"alarm",
"chdir",
"chown",
"close",
"dup",
720 "dup2",
"execl",
"execle",
"execlp",
"execv",
"execve",
"execvp",
721 "fork",
"fpathconf",
"getcwd",
"getegid",
"geteuid",
"getgid",
722 "getgroups",
"getlogin",
"getpgrp",
"getpid",
"getppid",
"getuid",
723 "isatty",
"link",
"lseek",
"pathconf",
"pause",
"pipe",
"read",
724 "rmdir",
"setgid",
"setpgid",
"setsid",
"setuid",
"sleep",
725 "sysconf",
"tcgetpgrp",
"tcsetpgrp",
"ttyname",
"ttyname_r",
731 const char* sys_select_syms[]=
740 const char* sys_socket_syms[]=
742 "accept",
"bind",
"connect",
749 const char* sys_stat_syms[]=
751 "fstat",
"lstat",
"stat",
766 const char* sys_wait_syms[]=
810 name_str==
"__func__" ||
811 name_str==
"__FUNCTION__" ||
812 name_str==
"__PRETTY_FUNCTION__" ||
816 name_str==
"envp_size'")
825 if(
has_prefix(file_str,
"gcc_builtin_headers_") &&
829 if(name_str==
"__builtin_va_start" ||
830 name_str==
"__builtin_va_end" ||
831 symbol.
name==ID_gcc_builtin_va_arg)
837 system_library_mapt::const_iterator it=
849 if(file_str.find(
"/bits/")==std::string::npos)
864 std::list<irep_idt> &local_static,
865 std::list<irep_idt> &local_type_decls)
887 std::unordered_set<irep_idt, irep_id_hash> typedef_names;
889 typedef_names.insert(td.first);
925 std::unordered_set<irep_idt, irep_id_hash> deps;
949 std::unordered_set<irep_idt, irep_id_hash> &dependencies)
954 std::unordered_set<irep_idt, irep_id_hash> local_deps;
956 if(type.
id()==ID_code)
961 for(
const auto ¶m : code_type.
parameters())
964 else if(type.
id()==ID_pointer || type.
id()==ID_array)
968 else if(type.
id()==ID_symbol)
975 const irep_idt &typedef_str=type.
get(ID_C_typedef);
977 if(!typedef_str.
empty())
979 std::pair<typedef_mapt::iterator, bool> entry=
983 (early && entry.first->second.type_decl_str.empty()))
985 if(typedef_str==
"__gnuc_va_list" || typedef_str ==
"va_list")
995 std::ostringstream oss;
996 oss <<
"typedef " <<
make_decl(typedef_str, t) <<
';';
998 entry.first->second.type_decl_str=oss.str();
999 entry.first->second.dependencies=local_deps;
1005 entry.first->second.early=
true;
1007 for(
const auto &d : local_deps)
1011 td_entry->second.early=
true;
1015 dependencies.insert(typedef_str);
1018 dependencies.insert(local_deps.begin(), local_deps.end());
1040 std::map<std::string, symbolt> symbols_sorted;
1042 symbols_sorted.insert(
1043 {
id2string(symbol_entry.first), symbol_entry.second});
1045 for(
const auto &symbol_entry : symbols_sorted)
1047 const symbolt &symbol=symbol_entry.second;
1056 typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
1080 std::vector<typedef_infot> typedefs_sorted;
1085 std::map<std::string, typedef_infot> to_insert;
1087 typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
1088 id_sett typedefs_done;
1089 std::unordered_map<irep_idt, id_sett, irep_id_hash>
1090 forward_deps, reverse_deps;
1093 if(!td.second.type_decl_str.empty())
1095 if(td.second.dependencies.empty())
1097 to_insert.insert({id2string(td.first), td.second});
1101 forward_deps.insert({td.first, td.second.dependencies});
1102 for(
const auto &d : td.second.dependencies)
1103 reverse_deps[d].insert(td.first);
1107 while(!to_insert.empty())
1112 to_insert.erase(to_insert.begin());
1114 typedefs_sorted.push_back(t);
1119 if(r_it==reverse_deps.end())
1123 id_sett &r_deps=r_it->second;
1124 for(id_sett::iterator it=r_deps.begin(); it!=r_deps.end(); )
1126 auto f_it=forward_deps.find(*it);
1127 if(f_it==forward_deps.end())
1129 it=r_deps.erase(it);
1134 id_sett &f_deps=f_it->second;
1143 to_insert.insert({
id2string(*it), td_entry->second});
1144 forward_deps.erase(*it);
1145 it=r_deps.erase(it);
1154 for(
const auto &td : typedefs_sorted)
1155 os << td.type_decl_str <<
'\n';
1157 if(!typedefs_sorted.empty())
1182 os <<
"// " << symbol.
name <<
'\n';
1183 os <<
"// " << symbol.
location <<
'\n';
1189 std::set<std::string> symbols_sorted;
1190 for(find_symbols_sett::const_iterator
1195 bool inserted=symbols_sorted.insert(
id2string(*it)).second;
1199 for(std::set<std::string>::const_iterator
1200 it=symbols_sorted.begin();
1201 it!=symbols_sorted.end();
1209 d.copy_to_operands(symbol.
value);
1213 local_static_decls[symbol.
name]=d;
1216 os <<
"// " << symbol.
name <<
'\n';
1217 os <<
"// " << symbol.
location <<
'\n';
1219 std::list<irep_idt> empty_static, empty_types;
1228 const bool skip_main,
1229 std::ostream &os_decl,
1230 std::ostream &os_body,
1239 goto_functionst::function_mapt::const_iterator func_entry=
1242 func_entry->second.body_available())
1245 std::list<irep_idt> type_decls, local_static;
1247 std::unordered_set<irep_idt, irep_id_hash> typedef_names;
1249 typedef_names.insert(td.first);
1253 func_entry->second.body,
1281 os_body <<
"// " << symbol.
name <<
'\n';
1282 os_body <<
"// " << symbol.
location <<
'\n';
1291 symbol.
name!=ID_main)
1293 os_decl <<
"// " << symbol.
name <<
'\n';
1294 os_decl <<
"// " << symbol.
location <<
'\n';
1307 exprt::operandst::iterator &before)
1315 exprt::operandst::iterator first_found=operands.end();
1322 if(it->id()==ID_code &&
1334 found=syms.find(identifier)!=syms.end();
1355 if(first_found==operands.end())
1372 if(first_found!=operands.end())
1384 const std::list<irep_idt> &local_static,
1386 std::list<irep_idt> &type_decls)
1390 for(std::list<irep_idt>::const_reverse_iterator
1391 it=local_static.rbegin();
1392 it!=local_static.rend();
1395 local_static_declst::const_iterator d_it=
1396 local_static_decls.find(*it);
1400 std::list<irep_idt> redundant;
1404 exprt::operandst::iterator before=b.
operands().end();
1411 dest_ptr->
operands().insert(before, d);
1418 const std::list<irep_idt> &type_decls)
1422 for(std::list<irep_idt>::const_reverse_iterator
1423 it=type_decls.rbegin();
1424 it!=type_decls.rend();
1430 std::ostringstream os_body;
1431 os_body << *it <<
" */\n";
1441 exprt::operandst::iterator before=b.
operands().end();
1448 dest_ptr->
operands().insert(before, skip);
1460 if(expr.
id()==ID_struct)
1472 exprt::operandst::iterator o_it=old_ops.begin();
1473 for(struct_union_typet::componentst::const_iterator
1474 it=old_components.begin();
1475 it!=old_components.end();
1478 const bool is_zero_bit_field=
1479 it->type().id()==ID_c_bit_field &&
1482 if(!it->get_is_padding() && !is_zero_bit_field)
1491 else if(expr.
id()==ID_union)
1497 !u_type_f.
get_bool(ID_C_transparent_union))
1504 else if(u.
op().
id()==ID_constant &&
1525 else if(expr.
id()==ID_typecast &&
1526 expr.
op0().
id()==ID_typecast &&
1532 else if(expr.
id()==ID_code &&
1548 if(parameters.size()==arguments.size())
1550 code_typet::parameterst::const_iterator it=parameters.begin();
1554 if(type.
id()==ID_union &&
1555 type.
get_bool(ID_C_transparent_union))
1557 if(it2->id()==ID_typecast &&
1562 if(it2->id()==ID_constant &&
1565 const typet &comp_type=
1568 if(comp_type.
id()==ID_pointer)
1578 else if(expr.
id()==ID_constant &&
1579 expr.
type().
id()==ID_signedbv)
1584 if(!cformat.
empty())
1586 declared_enum_constants_mapt::const_iterator entry=
1590 entry->first!=entry->second)
1591 expr.
set(ID_C_cformat, entry->second);
1594 expr.
remove(ID_C_cformat);
1605 if(type.
id()==ID_code)
1611 for(code_typet::parameterst::iterator
1618 if(type.
id()==ID_array)
1622 (type.
id()!=ID_union && type.
id()!=ID_struct) ||
1646 const bool use_system_headers,
1647 const bool use_all_headers,
1658 const bool use_system_headers,
1659 const bool use_all_headers,
const irep_idt & get_statement() const
const irep_idt & get_name() const
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
std::unordered_set< irep_idt, irep_id_hash > convertedt
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
void collect_typedefs(const typet &type, bool early)
Fixed-width bit-vector with unsigned binary interpretation.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
targett add_instruction()
Adds an instruction at the end.
void init_system_library_map()
const std::string & id2string(const irep_idt &d)
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)
#define forall_symbols(it, expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
void set_comment(const irep_idt &comment)
declared_enum_constants_mapt declared_enum_constants
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const irep_idt & get_function() const
std::unordered_map< irep_idt, code_declt, irep_id_hash > local_static_declst
const irep_idt & get_identifier() const
std::string type_to_string(const typet &type)
std::ostream & operator<<(std::ostream &out, dump_ct &src)
languaget * new_ansi_c_language()
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
const irep_idt & get_value() const
std::string expr_to_string(const exprt &expr)
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
const componentst & components() const
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt, irep_id_hash > &dependencies)
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
void set_identifier(const irep_idt &identifier)
exprt::operandst argumentst
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
const goto_functionst & goto_functions
#define CHECK_RETURN(CONDITION)
bool get_bool(const irep_namet &name) const
#define POSTCONDITION(CONDITION)
convertedt converted_enum
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
const bool use_all_headers
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
#define Forall_symbols(it, expr)
std::string make_decl(const irep_idt &identifier, const typet &type)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
typedef_typest typedef_types
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
A reference into the symbol table.
A declaration of a local variable.
#define Forall_expr(it, expr)
virtual std::string id() const
unsigned long_long_int_width
Fixed-width bit-vector with two's complement interpretation.
system_library_mapt system_library_map
static irep_idt entry_point()
union constructor from single element
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
const irep_idt & get(const irep_namet &name) const
void gather_global_typedefs()
#define PRECONDITION(CONDITION)
const exprt & size() const
Base class for tree-like data structures with sharing.
languaget * new_cpp_language()
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
function_mapt function_map
std::set< std::string > system_headers
convertedt converted_global
bool has_operands() const
std::size_t get_width() const
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
Dump Goto-Program as C/C++ Source.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool ignore(const symbolt &symbol)
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
const irep_idt & get_file() const
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Base type of C structs and unions, and C++ classes.
void cleanup_expr(exprt &expr)
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
irept & add(const irep_namet &name)
const std::string & get_string(const irep_namet &name) const
void convert_compound_enum(const typet &type, std::ostream &os)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
#define Forall_subtypes(it, type)
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
void operator()(std::ostream &out)
irep_idt get_component_name() const
#define Forall_operands(it, expr)
bool has_symbol(const irep_idt &name) const
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
static std::string indent(const unsigned n)
bool get_is_padding() const
Expression to hold a symbol (variable)
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)
const code_blockt & to_code_block(const codet &code)
bool has_suffix(const std::string &s, const std::string &suffix)
void dump_typedefs(std::ostream &os) const
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
A statement in a programming language.
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
void remove(const irep_namet &name)
const typet & subtype() const
convertedt converted_compound
#define DATA_INVARIANT(CONDITION, REASON)
void cleanup_type(typet &type)
symbol_tablet copied_symbol_table
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
struct constructor from list of elements
std::unordered_map< irep_idt, irep_idt, irep_id_hash > declared_enum_constants_mapt
std::vector< c_enum_membert > memberst
const irept & find(const irep_namet &name) const
void find_symbols(const exprt &src, find_symbols_sett &dest)
const typet & return_type() const
void set(const irep_namet &name, const irep_idt &value)
const componentt & get_component(const irep_idt &component_name) const
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett
#define ADD_TO_SYSTEM_LIBRARY(v, header)
#define forall_irep(it, irep)