26 if(expr.
id()!=ID_typecast)
65 for(natural_loopst::loop_mapt::const_iterator
70 assert(!l_it->second.empty());
79 for(natural_loopst::natural_loopt::const_iterator
80 it=l_it->second.begin();
81 it!=l_it->second.end();
85 if((*it)->get_target()==loop_start &&
86 (*it)->location_number>loop_end->location_number)
90 if(!
loop_map.insert(std::make_pair(loop_start, loop_end)).second)
101 if(target->is_dead())
103 target->location_number;
111 if(target->is_assign())
117 if(
r.id()==ID_side_effect &&
120 assert(
r.has_operands());
124 else if(l.
type().
id()==ID_pointer &&
125 l.
type().
get(ID_C_typedef)==
"va_list" &&
127 r.id()==ID_typecast &&
140 for(code_typet::parameterst::iterator
141 it2=parameters.begin();
142 it2!=parameters.end();
146 ns.
lookup(it2->get_identifier()).symbol_expr();
148 it2->type().id(ID_gcc_builtin_va_list);
160 if(target->type!=
ASSERT &&
161 !target->source_location.get_comment().empty())
164 dest.
operands().back().add_source_location().set_comment(
165 target->source_location.get_comment());
169 if(target->is_target() && !target->is_goto())
171 loopt::const_iterator loop_entry=
loop_map.find(target);
175 upper_bound->location_number > loop_entry->second->location_number))
208 dest.
operands().back().add_source_location().set_comment(
209 target->source_location.get_comment());
224 dest.
operands().back().add_source_location().set_comment(
"END_THREAD");
233 target->is_atomic_begin() ?
234 "__CPROVER_atomic_begin" :
235 "__CPROVER_atomic_end",
261 codet *latest_block=&dest;
264 if(target->is_target())
266 std::stringstream label;
267 label <<
"__CPROVER_DUMP_L" << target->target_number;
270 target_label=l.get_label();
276 for(goto_programt::instructiont::labelst::const_iterator
277 it=target->labels.begin();
278 it!=target->labels.end();
295 if(latest_block!=&dest)
321 const exprt this_va_list_expr=assign.
lhs();
328 if(
r.id()==ID_constant &&
332 f.arguments().push_back(this_va_list_expr);
333 f.arguments().back().type().id(ID_gcc_builtin_va_list);
337 else if(
r.id()==ID_address_of)
340 f.arguments().push_back(this_va_list_expr);
341 f.arguments().back().type().id(ID_gcc_builtin_va_list);
346 else if(
r.id()==ID_side_effect &&
350 f.arguments().push_back(this_va_list_expr);
351 f.arguments().back().type().id(ID_gcc_builtin_va_list);
361 if(next!=upper_bound &&
365 if(n_r.
id()==ID_dereference &&
372 f.arguments().push_back(type_of);
380 assert(
r.find(ID_C_va_arg_type).is_not_nil());
381 const typet &va_arg_type=
382 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
389 f.arguments().push_back(type_of);
398 f.arguments().push_back(this_va_list_expr);
399 f.arguments().back().type().id(ID_gcc_builtin_va_list);
400 f.arguments().push_back(
r);
412 if(assign.
rhs().
id()==ID_array)
450 while(next!=upper_bound && next->is_dead() && !next->is_target())
453 if(next!=upper_bound &&
477 upper_bound->location_number > entry->second);
481 if(next!=upper_bound &&
483 !next->is_target() &&
484 (next->is_assign() || next->is_function_call()))
486 exprt lhs=next->is_assign() ?
492 if(next->is_assign())
528 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
531 d.
cond()=loop_end->guard;
537 for( ; target!=loop_end; ++target)
553 assert(target->is_goto());
555 assert(target->targets.size()==1);
557 loopt::const_iterator loop_entry=
loop_map.find(target);
561 upper_bound->location_number > loop_entry->second->location_number))
563 else if(!target->guard.is_true())
576 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
586 if(target->get_target()==after_loop)
591 else if(target->guard.is_true())
604 for(++target; target!=loop_end; ++target)
610 if(loop_end->guard.is_false())
616 else if(!loop_end->guard.is_true())
638 f.
iter().
id(ID_side_effect);
673 const exprt &switch_var,
679 std::set<goto_programt::const_targett> unique_targets;
683 cases_it!=upper_bound && cases_it!=first_target;
686 if(cases_it->is_goto() &&
687 !cases_it->is_backwards_goto() &&
688 cases_it->guard.is_true())
690 default_target=cases_it->get_target();
693 first_target->location_number > default_target->location_number)
694 first_target=default_target;
696 last_target->location_number < default_target->location_number)
697 last_target=default_target;
699 cases.push_back(
caset(
704 unique_targets.insert(default_target);
709 else if(cases_it->is_goto() &&
710 !cases_it->is_backwards_goto() &&
711 (cases_it->guard.id()==ID_equal ||
712 cases_it->guard.id()==ID_or))
715 if(cases_it->guard.id()==ID_equal)
716 eqs.push_back(cases_it->guard);
718 eqs=cases_it->guard.operands();
722 for(exprt::operandst::const_reverse_iterator
724 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
727 if(e_it->id()!=ID_equal ||
732 cases.push_back(
caset(
736 cases_it->get_target()));
737 assert(cases.back().value.is_not_nil());
740 first_target->location_number>
741 cases.back().case_start->location_number)
742 first_target=cases.back().case_start;
744 last_target->location_number<
745 cases.back().case_start->location_number)
746 last_target=cases.back().case_start;
748 unique_targets.insert(cases.back().case_start);
757 if(unique_targets.size()<3)
761 if(cases_it==upper_bound ||
763 upper_bound->location_number < last_target->location_number) ||
765 last_target->location_number > default_target->location_number) ||
766 target->get_target()==default_target)
776 std::set<unsigned> &processed_locations)
778 std::map<goto_programt::const_targett, std::size_t> targets_done;
780 for(cases_listt::iterator it=cases.begin();
786 if(targets_done.find(it->case_start)!=targets_done.end())
793 case_end!=upper_bound;
796 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
800 dominators.
cfg[i_entry->second];
803 if(n.dominators.empty())
807 if(case_end==it->case_start)
814 if(n.dominators.find(it->case_start)==n.dominators.end())
817 if(!processed_locations.insert(case_end->location_number).second)
820 it->case_last=case_end;
823 targets_done[it->case_start]=1;
834 for(cases_listt::const_iterator it=cases.begin();
843 cases_listt::const_iterator last=--cases.end();
844 if(last->case_start==default_target &&
853 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
857 dominators.
cfg[i_entry->second];
859 if(!n.dominators.empty())
864 next_case==default_target &&
865 (!it->case_last->is_goto() ||
866 (it->case_last->guard.is_true() &&
867 it->case_last->get_target()==default_target)))
876 if(it->case_last->is_goto() &&
877 it->case_last->guard.is_true() &&
878 it->case_last->get_target()==default_target)
882 if(!it->case_last->is_goto())
897 exprt eq_cand=target->guard;
898 if(eq_cand.
id()==ID_or)
899 eq_cand=eq_cand.
op0();
901 if(target->is_backwards_goto() ||
902 eq_cand.
id()!=ID_equal ||
910 cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry=
913 if(dominators.
cfg[t_entry->second].dominators.
empty())
937 if(cases_start==target)
945 for(target=cases_start; target!=first_target; ++target)
948 std::set<unsigned> processed_locations;
967 for(cases_listt::const_iterator it=cases.begin();
971 it->case_last->location_number > max_target->location_number)
972 max_target=it->case_last;
974 std::map<goto_programt::const_targett, unsigned> targets_done;
979 for(cases_listt::const_iterator it=cases.begin();
985 if(it->value.is_nil())
992 if(targets_done.find(it->case_start)!=targets_done.end())
994 assert(it->case_selector==orig_target ||
995 !it->case_selector->is_target());
1000 while(cscp->code().get_statement()==ID_switch_case)
1004 cscp->code().swap(csc);
1010 if(it->case_selector!=orig_target)
1014 target=it->case_start;
1021 if(it->case_start!=(--cases.end())->case_start)
1035 for( ; target!=after_last; ++target)
1040 targets_done[it->case_start]=s.
body().
operands().size();
1050 if(processed_locations.find(it->location_number)==
1051 processed_locations.end())
1053 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1057 dominators.
cfg[it_entry->second];
1059 if(!n.dominators.empty())
1079 bool has_else=
false;
1081 if(!target->is_backwards_goto())
1088 if(before_else==target)
1095 before_else->is_goto() &&
1096 before_else->get_target()->location_number > end_if->location_number &&
1097 before_else->guard.is_true() &&
1099 upper_bound->location_number>=
1100 before_else->get_target()->location_number);
1103 end_if=before_else->get_target();
1110 if(target->is_backwards_goto() ||
1112 upper_bound->location_number < end_if->location_number))
1128 for(++target; target!=before_else; ++target)
1133 for(++target; target!=end_if; ++target)
1138 for(++target; target!=end_if; ++target)
1161 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1163 assert(i_entry!=dominators.cfg.entry_map.end());
1165 dominators.cfg[i_entry->second];
1167 if(!n.dominators.empty())
1171 if(target->get_target()==next)
1180 if(target->get_target()==loop_end &&
1185 if(!target->guard.is_true())
1188 i.
cond()=target->guard;
1205 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1206 dominators.cfg.entry_map.find(after_loop);
1207 assert(i_entry!=dominators.cfg.entry_map.end());
1209 dominators.cfg[i_entry->second];
1211 if(!n.dominators.empty())
1215 if(target->get_target()==after_loop)
1220 i.
cond()=target->guard;
1242 if(target->get_target()==next)
1246 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1250 dominators.
cfg[it_entry->second];
1254 if(n.dominators.empty())
1257 std::stringstream label;
1259 for(goto_programt::instructiont::labelst::const_iterator
1260 it=target->get_target()->labels.begin();
1261 it!=target->get_target()->labels.end();
1272 if(label.str().empty())
1273 label <<
"__CPROVER_DUMP_L" << target->get_target()->target_number;
1279 if(!target->guard.is_true())
1282 i.
cond()=target->guard;
1299 assert(target->is_start_thread());
1302 assert(thread_start->location_number > target->location_number);
1313 if(!next->is_goto())
1317 assert(this_end->is_end_thread());
1318 assert(thread_start->location_number > this_end->location_number);
1323 for(goto_programt::instructiont::labelst::const_iterator
1324 it=target->labels.begin();
1325 it!=target->labels.end();
1349 assert(next->is_goto() && next->guard.is_true());
1350 assert(!next->is_backwards_goto());
1351 assert(thread_start->location_number < next->get_target()->location_number);
1353 ++after_thread_start;
1357 assert(thread_start->location_number < thread_end->location_number);
1358 assert(thread_end->is_end_thread());
1361 thread_end->location_number < upper_bound->location_number);
1366 if(thread_start->is_function_call() &&
1368 after_thread_start==thread_end)
1391 for( ; thread_start!=thread_end; ++thread_start)
1394 for(goto_programt::instructiont::labelst::const_iterator
1395 it=target->labels.begin();
1396 it!=target->labels.end();
1434 if(type.
id()==ID_symbol)
1438 if(full_type.
id()==ID_pointer ||
1439 full_type.
id()==ID_array)
1443 else if(full_type.
id()==ID_struct ||
1444 full_type.
id()==ID_union)
1458 for(struct_union_typet::componentst::const_iterator
1459 it=components.begin();
1460 it!=components.end();
1464 assert(!identifier.
empty());
1468 else if(type.
id()==ID_c_enum_tag)
1477 assert(!identifier.
empty());
1480 else if(type.
id()==ID_pointer ||
1481 type.
id()==ID_array)
1494 code.
op0().
type().
id(ID_gcc_builtin_va_list);
1497 code.
op1().
id()==ID_side_effect &&
1516 if(!typedef_str.empty() &&
1529 call.
lhs().
id()==ID_typecast)
1538 if(it->id()==ID_code)
1546 if(statement==ID_label)
1551 assert(!label.
empty());
1560 else if(statement==ID_block)
1562 else if(statement==ID_ifthenelse)
1564 else if(statement==ID_dowhile)
1575 code=do_while.
body();
1580 const exprt &
function,
1583 if(
function.
id()!=ID_symbol)
1596 if(parameters.size()==arguments.size())
1598 code_typet::parameterst::const_iterator it=parameters.begin();
1601 if(
ns.
follow(it2->type()).
id()==ID_union)
1602 it2->type()=it->type();
1617 operands.size()>1 && i<operands.size();
1620 exprt::operandst::iterator it=operands.begin()+i;
1623 it->source_location().get_comment().
empty())
1628 bool has_decl=
false;
1638 operands.insert(operands.begin()+i+1,
1639 it->operands().begin(), it->operands().end());
1640 operands.erase(operands.begin()+i);
1650 if(operands.empty() && parent_stmt!=ID_nil)
1652 else if(operands.size()==1 &&
1653 parent_stmt!=ID_nil &&
1654 to_code(code.
op0()).get_statement()!=ID_decl)
1665 type.
remove(ID_C_constant);
1667 if(type.
id()==ID_symbol)
1676 "Symbol "+
id2string(identifier)+
" should be a type");
1680 else if(type.
id()==ID_array)
1682 else if(type.
id()==ID_struct ||
1683 type.
id()==ID_union)
1688 for(struct_union_typet::componentst::iterator
1833 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1838 else if(!no_typecast &&
1839 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1840 expr.
id()==ID_array || expr.
id()==ID_vector))
1852 if(expr.
id()==ID_union &&
1859 if(expr.
id()==ID_typecast &&
1863 if(expr.
id()==ID_union ||
1864 expr.
id()==ID_struct)
1869 assert(expr.
type().
id()==ID_symbol);
1877 if(!typedef_str.
empty() &&
1881 else if(expr.
id()==ID_array ||
1882 expr.
id()==ID_vector)
1885 expr.
get_bool(ID_C_string_constant))
1894 if(!typedef_str.
empty() &&
1898 else if(expr.
id()==ID_side_effect)
1902 if(statement==ID_nondet)
1909 for(symbol_tablet::symbolst::const_iterator
1914 if(it->second.type.id()!=ID_code)
1933 if(expr.
type().
get(ID_C_c_type)!=
"")
1936 suffix=expr.
type().
get(ID_C_c_type);
1954 symbol.
name=base_name;
1974 else if(expr.
id()==ID_isnan ||
1977 else if(expr.
id()==ID_constant)
1979 if(expr.
type().
id()==ID_floatbv)
1985 else if(expr.
type().
id()==ID_pointer)
1987 else if(expr.
type().
id()==ID_bool ||
1988 expr.
type().
id()==ID_c_bool)
1996 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
2001 else if(expr.
id()==ID_typecast)
2010 if(!typedef_str.empty() &&
2014 assert(expr.
type().
id()!=ID_union &&
2015 expr.
type().
id()!=ID_struct);
2018 else if(expr.
id()==ID_symbol)
2020 if(expr.
type().
id()!=ID_code)
2026 symbol.
type.
id()!=ID_code &&
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
exprt guard
Guard for gotos, assume, assert.
const goto_programt & goto_program
const irep_idt & get_statement() const
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
The type of an expression.
irep_idt name
The unique identifier.
const codet & then_case() const
const exprt & return_value() const
struct configt::ansi_ct ansi_c
const code_declt & to_code_decl(const codet &code)
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
const irep_idt & get_identifier() const
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const irep_idt & get_identifier() const
pointer_typet pointer_type(const typet &subtype)
const exprt & init() const
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, codet &dest)
targett insert_before(const_targett target)
Insertion before the given target.
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const exprt & cond() const
A continue for ‘for’ and ‘while’ loops.
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
const exprt & cond() const
const codet & body() const
void convert_assign_rec(const code_assignt &assign, codet &dest)
std::unordered_set< irep_idt > labels_in_use
const codet & body() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_function() const
void convert_labels(goto_programt::const_targett target, codet &dest)
void copy_to_operands(const exprt &expr)
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.
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
std::unordered_set< irep_idt > type_names_set
const irep_idt & get_value() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
std::vector< parametert > parameterst
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, codet &dest)
exprt value
Initial value of symbol.
const componentst & components() const
Dump Goto-Program as C/C++ Source.
exprt::operandst argumentst
unsignedbv_typet size_type()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
static const exprt & skip_typecast(const exprt &expr)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
std::unordered_set< irep_idt > const_removed
std::unordered_set< irep_idt > local_static_set
static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)
const std::unordered_set< irep_idt > & typedef_names
#define INVARIANT(CONDITION, REASON)
const exprt & case_op() const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
side_effect_exprt & to_side_effect_expr(exprt &expr)
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
This class represents an instruction in the GOTO intermediate representation.
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
loop_last_stackt loop_last_stack
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
The boolean constant true.
A declaration of a local variable.
#define Forall_expr(it, expr)
void cleanup_code(codet &code, const irep_idt parent_stmt)
void add_local_types(const typet &type)
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, codet &dest)
const exprt & cond() const
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void cleanup_expr(exprt &expr, bool no_typecast)
Operator to dereference a pointer.
Fixed-width bit-vector with two's complement interpretation.
const code_dowhilet & to_code_dowhile(const codet &code)
cfg_base_nodet< nodet, goto_programt::const_targett > nodet
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get(const irep_namet &name) const
instructionst::const_iterator const_targett
A label for branch targets.
std::set< std::string > & system_headers
const code_returnt & to_code_return(const codet &code)
bool has_prefix(const std::string &s, const std::string &prefix)
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const code_switch_caset & to_code_switch_case(const codet &code)
const typet & follow(const typet &) const
bitvector_typet index_type()
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
bool has_operands() const
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
The boolean constant false.
const codet & body() const
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
code_blockt & toplevel_block
bool has_return_value() const
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
A non-fatal assertion, which checks a condition then permits execution to continue.
A function call side effect.
An assumption, which must hold in subsequent code.
goto_programt::const_targett convert_return(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const exprt & value() const
const irep_idt & func_name
goto_programt::const_targett get_cases(goto_programt::const_targett target, goto_programt::const_targett upper_bound, const exprt &switch_var, cases_listt &cases, goto_programt::const_targett &first_target, goto_programt::const_targett &default_target)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
goto_programt::const_targett convert_throw(goto_programt::const_targett target, codet &dest)
Base type of C structs and unions, and C++ classes.
void set_statement(const irep_idt &statement)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
A break for ‘for’ and ‘while’ loops.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
A ‘do while’ instruction.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
const exprt & iter() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
exprt::operandst & arguments()
#define Forall_operands(it, expr)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
A statement in a programming language.
std::list< caset > cases_listt
void remove(const irep_namet &name)
const code_labelt & to_code_label(const codet &code)
const typet & subtype() const
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const exprt & cond() const
void remove_const(typet &type)
#define forall_goto_program_instructions(it, program)
const codet & else_case() const
const code_ifthenelset & to_code_ifthenelse(const codet &code)
void make_typecast(const typet &_type)
const codet & body() const
const irept & find(const irep_namet &name) const
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
const irep_idt & get_identifier() const
std::unordered_set< exprt, irep_hash > va_list_expr
void reserve_operands(operandst::size_type n)
const irep_idt & get_statement() const
symbol_tablet & symbol_table
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
void cleanup_code_block(codet &code, const irep_idt parent_stmt)
static bool has_labels(const codet &code)