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 &&
136 symbol_tablet::symbolst::iterator it=
143 for(code_typet::parameterst::iterator
144 it2=parameters.begin();
145 it2!=parameters.end();
149 ns.
lookup(it2->get_identifier()).symbol_expr();
151 it2->type().id(ID_gcc_builtin_va_list);
163 if(target->type!=
ASSERT &&
164 !target->source_location.get_comment().empty())
167 dest.
operands().back().add_source_location().set_comment(
168 target->source_location.get_comment());
172 if(target->is_target() && !target->is_goto())
174 loopt::const_iterator loop_entry=
loop_map.find(target);
178 upper_bound->location_number > loop_entry->second->location_number))
211 dest.
operands().back().add_source_location().set_comment(
212 target->source_location.get_comment());
227 dest.
operands().back().add_source_location().set_comment(
"END_THREAD");
237 target->is_atomic_begin() ?
238 "__CPROVER_atomic_begin" :
239 "__CPROVER_atomic_end",
264 codet *latest_block=&dest;
267 if(target->is_target())
269 std::stringstream label;
270 label <<
"__CPROVER_DUMP_L" << target->target_number;
273 target_label=l.get_label();
279 for(goto_programt::instructiont::labelst::const_iterator
280 it=target->labels.begin();
281 it!=target->labels.end();
298 if(latest_block!=&dest)
324 const exprt this_va_list_expr=assign.
lhs();
331 if(
r.id()==ID_constant &&
335 f.arguments().push_back(this_va_list_expr);
336 f.arguments().back().type().id(ID_gcc_builtin_va_list);
340 else if(
r.id()==ID_address_of)
343 f.arguments().push_back(this_va_list_expr);
344 f.arguments().back().type().id(ID_gcc_builtin_va_list);
349 else if(
r.id()==ID_side_effect &&
353 f.arguments().push_back(this_va_list_expr);
354 f.arguments().back().type().id(ID_gcc_builtin_va_list);
363 if(next!=upper_bound &&
367 if(n_r.
id()==ID_dereference &&
374 f.arguments().push_back(type_of);
382 assert(
r.find(ID_C_va_arg_type).is_not_nil());
383 const typet &va_arg_type=
384 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
391 f.arguments().push_back(type_of);
400 f.arguments().push_back(this_va_list_expr);
401 f.arguments().back().type().id(ID_gcc_builtin_va_list);
402 f.arguments().push_back(
r);
414 if(assign.
rhs().
id()==ID_array)
452 while(next!=upper_bound && next->is_dead() && !next->is_target())
455 if(next!=upper_bound &&
479 upper_bound->location_number > entry->second);
483 if(next!=upper_bound &&
485 !next->is_target() &&
486 (next->is_assign() || next->is_function_call()))
488 exprt lhs=next->is_assign() ?
494 if(next->is_assign())
530 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
533 d.
cond()=loop_end->guard;
539 for( ; target!=loop_end; ++target)
555 assert(target->is_goto());
557 assert(target->targets.size()==1);
559 loopt::const_iterator loop_entry=
loop_map.find(target);
563 upper_bound->location_number > loop_entry->second->location_number))
565 else if(!target->guard.is_true())
578 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
588 if(target->get_target()==after_loop)
593 else if(target->guard.is_true())
606 for(++target; target!=loop_end; ++target)
612 if(loop_end->guard.is_false())
618 else if(!loop_end->guard.is_true())
640 f.
iter().
id(ID_side_effect);
675 const exprt &switch_var,
681 std::set<goto_programt::const_targett> unique_targets;
685 cases_it!=upper_bound && cases_it!=first_target;
688 if(cases_it->is_goto() &&
689 !cases_it->is_backwards_goto() &&
690 cases_it->guard.is_true())
692 default_target=cases_it->get_target();
695 first_target->location_number > default_target->location_number)
696 first_target=default_target;
698 last_target->location_number < default_target->location_number)
699 last_target=default_target;
701 cases.push_back(
caset(
706 unique_targets.insert(default_target);
711 else if(cases_it->is_goto() &&
712 !cases_it->is_backwards_goto() &&
713 (cases_it->guard.id()==ID_equal ||
714 cases_it->guard.id()==ID_or))
717 if(cases_it->guard.id()==ID_equal)
718 eqs.push_back(cases_it->guard);
720 eqs=cases_it->guard.operands();
724 for(exprt::operandst::const_reverse_iterator
726 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
729 if(e_it->id()!=ID_equal ||
734 cases.push_back(
caset(
738 cases_it->get_target()));
739 assert(cases.back().value.is_not_nil());
742 first_target->location_number>
743 cases.back().case_start->location_number)
744 first_target=cases.back().case_start;
746 last_target->location_number<
747 cases.back().case_start->location_number)
748 last_target=cases.back().case_start;
750 unique_targets.insert(cases.back().case_start);
759 if(unique_targets.size()<3)
763 if(cases_it==upper_bound ||
765 upper_bound->location_number < last_target->location_number) ||
767 last_target->location_number > default_target->location_number) ||
768 target->get_target()==default_target)
778 std::set<unsigned> &processed_locations)
780 std::map<goto_programt::const_targett, std::size_t> targets_done;
782 for(cases_listt::iterator it=cases.begin();
788 if(targets_done.find(it->case_start)!=targets_done.end())
795 case_end!=upper_bound;
798 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
802 dominators.
cfg[i_entry->second];
805 if(n.dominators.empty())
809 if(case_end==it->case_start)
816 if(n.dominators.find(it->case_start)==n.dominators.end())
819 if(!processed_locations.insert(case_end->location_number).second)
822 it->case_last=case_end;
825 targets_done[it->case_start]=1;
836 for(cases_listt::const_iterator it=cases.begin();
845 cases_listt::const_iterator last=--cases.end();
846 if(last->case_start==default_target &&
855 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
859 dominators.
cfg[i_entry->second];
861 if(!n.dominators.empty())
866 next_case==default_target &&
867 (!it->case_last->is_goto() ||
868 (it->case_last->guard.is_true() &&
869 it->case_last->get_target()==default_target)))
878 if(it->case_last->is_goto() &&
879 it->case_last->guard.is_true() &&
880 it->case_last->get_target()==default_target)
884 if(!it->case_last->is_goto())
899 exprt eq_cand=target->guard;
900 if(eq_cand.
id()==ID_or)
901 eq_cand=eq_cand.
op0();
903 if(target->is_backwards_goto() ||
904 eq_cand.
id()!=ID_equal ||
912 cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry=
915 if(dominators.
cfg[t_entry->second].dominators.
empty())
939 if(cases_start==target)
947 for(target=cases_start; target!=first_target; ++target)
950 std::set<unsigned> processed_locations;
969 for(cases_listt::const_iterator it=cases.begin();
973 it->case_last->location_number > max_target->location_number)
974 max_target=it->case_last;
976 std::map<goto_programt::const_targett, unsigned> targets_done;
981 for(cases_listt::const_iterator it=cases.begin();
987 if(it->value.is_nil())
994 if(targets_done.find(it->case_start)!=targets_done.end())
996 assert(it->case_selector==orig_target ||
997 !it->case_selector->is_target());
1002 while(cscp->code().get_statement()==ID_switch_case)
1006 cscp->code().swap(csc);
1012 if(it->case_selector!=orig_target)
1016 target=it->case_start;
1023 if(it->case_start!=(--cases.end())->case_start)
1026 goto_programt::instructiont i=*(it->case_selector);
1037 for( ; target!=after_last; ++target)
1042 targets_done[it->case_start]=s.
body().
operands().size();
1052 if(processed_locations.find(it->location_number)==
1053 processed_locations.end())
1055 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1059 dominators.
cfg[it_entry->second];
1061 if(!n.dominators.empty())
1081 bool has_else=
false;
1083 if(!target->is_backwards_goto())
1090 if(before_else==target)
1097 before_else->is_goto() &&
1098 before_else->get_target()->location_number > end_if->location_number &&
1099 before_else->guard.is_true() &&
1101 upper_bound->location_number>=
1102 before_else->get_target()->location_number);
1105 end_if=before_else->get_target();
1112 if(target->is_backwards_goto() ||
1114 upper_bound->location_number < end_if->location_number))
1130 for(++target; target!=before_else; ++target)
1135 for(++target; target!=end_if; ++target)
1140 for(++target; target!=end_if; ++target)
1163 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1164 dominators.cfg.entry_map.find(next);
1165 assert(i_entry!=dominators.cfg.entry_map.end());
1167 dominators.cfg[i_entry->second];
1169 if(!n.dominators.empty())
1173 if(target->get_target()==next)
1182 if(target->get_target()==loop_end &&
1187 if(!target->guard.is_true())
1190 i.
cond()=target->guard;
1207 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1208 dominators.cfg.entry_map.find(after_loop);
1209 assert(i_entry!=dominators.cfg.entry_map.end());
1211 dominators.cfg[i_entry->second];
1213 if(!n.dominators.empty())
1217 if(target->get_target()==after_loop)
1222 i.
cond()=target->guard;
1244 if(target->get_target()==next)
1248 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1252 dominators.
cfg[it_entry->second];
1256 if(n.dominators.empty())
1259 std::stringstream label;
1261 for(goto_programt::instructiont::labelst::const_iterator
1262 it=target->get_target()->labels.begin();
1263 it!=target->get_target()->labels.end();
1274 if(label.str().empty())
1275 label <<
"__CPROVER_DUMP_L" << target->get_target()->target_number;
1281 if(!target->guard.is_true())
1284 i.
cond()=target->guard;
1301 assert(target->is_start_thread());
1304 assert(thread_start->location_number > target->location_number);
1315 if(!next->is_goto())
1319 assert(this_end->is_end_thread());
1320 assert(thread_start->location_number > this_end->location_number);
1325 for(goto_programt::instructiont::labelst::const_iterator
1326 it=target->labels.begin();
1327 it!=target->labels.end();
1351 assert(next->is_goto() && next->guard.is_true());
1352 assert(!next->is_backwards_goto());
1353 assert(thread_start->location_number < next->get_target()->location_number);
1355 ++after_thread_start;
1359 assert(thread_start->location_number < thread_end->location_number);
1360 assert(thread_end->is_end_thread());
1363 thread_end->location_number < upper_bound->location_number);
1368 if(thread_start->is_function_call() &&
1370 after_thread_start==thread_end)
1392 for( ; thread_start!=thread_end; ++thread_start)
1395 for(goto_programt::instructiont::labelst::const_iterator
1396 it=target->labels.begin();
1397 it!=target->labels.end();
1435 if(type.
id()==ID_symbol)
1439 if(full_type.
id()==ID_pointer ||
1440 full_type.
id()==ID_array)
1444 else if(full_type.
id()==ID_struct ||
1445 full_type.
id()==ID_union)
1459 for(struct_union_typet::componentst::const_iterator
1460 it=components.begin();
1461 it!=components.end();
1465 assert(!identifier.
empty());
1469 else if(type.
id()==ID_c_enum_tag)
1478 assert(!identifier.
empty());
1481 else if(type.
id()==ID_pointer ||
1482 type.
id()==ID_array)
1495 code.
op0().
type().
id(ID_gcc_builtin_va_list);
1498 code.
op1().
id()==ID_side_effect &&
1517 if(!typedef_str.empty() &&
1530 call.
lhs().
id()==ID_typecast)
1539 if(it->id()==ID_code)
1547 if(statement==ID_label)
1552 assert(!label.
empty());
1561 else if(statement==ID_block)
1563 else if(statement==ID_ifthenelse)
1565 else if(statement==ID_dowhile)
1576 code=do_while.
body();
1581 const exprt &
function,
1584 if(
function.
id()!=ID_symbol)
1597 if(parameters.size()==arguments.size())
1599 code_typet::parameterst::const_iterator it=parameters.begin();
1602 if(
ns.
follow(it2->type()).
id()==ID_union)
1603 it2->type()=it->type();
1618 operands.size()>1 && i<operands.size();
1621 exprt::operandst::iterator it=operands.begin()+i;
1624 it->source_location().get_comment().
empty())
1629 bool has_decl=
false;
1639 operands.insert(operands.begin()+i+1,
1640 it->operands().begin(), it->operands().end());
1641 operands.erase(operands.begin()+i);
1651 if(operands.empty() && parent_stmt!=ID_nil)
1653 else if(operands.size()==1 &&
1654 parent_stmt!=ID_nil &&
1655 to_code(code.
op0()).get_statement()!=ID_decl)
1666 type.
remove(ID_C_constant);
1668 if(type.
id()==ID_symbol)
1674 symbol_tablet::symbolst::iterator it=
1677 assert(it->second.is_type);
1681 else if(type.
id()==ID_array)
1683 else if(type.
id()==ID_struct ||
1684 type.
id()==ID_union)
1689 for(struct_union_typet::componentst::iterator
1834 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1839 else if(!no_typecast &&
1840 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1841 expr.
id()==ID_array || expr.
id()==ID_vector))
1853 if(expr.
id()==ID_union &&
1860 if(expr.
id()==ID_typecast &&
1864 if(expr.
id()==ID_union ||
1865 expr.
id()==ID_struct)
1870 assert(expr.
type().
id()==ID_symbol);
1878 if(!typedef_str.
empty() &&
1882 else if(expr.
id()==ID_array ||
1883 expr.
id()==ID_vector)
1886 expr.
get_bool(ID_C_string_constant))
1895 if(!typedef_str.
empty() &&
1899 else if(expr.
id()==ID_side_effect)
1903 if(statement==ID_nondet)
1910 for(symbol_tablet::symbolst::const_iterator
1915 if(it->second.type.id()!=ID_code)
1934 if(expr.
type().
get(ID_C_c_type)!=
"")
1937 suffix=expr.
type().
get(ID_C_c_type);
1950 base_name=
"nondet_"+std::to_string(count);
1958 symbol.
name=base_name;
1959 symbol.
type=code_type;
1978 else if(expr.
id()==ID_isnan ||
1981 else if(expr.
id()==ID_constant)
1983 if(expr.
type().
id()==ID_floatbv)
1989 else if(expr.
type().
id()==ID_pointer)
1991 else if(expr.
type().
id()==ID_bool ||
1992 expr.
type().
id()==ID_c_bool)
2000 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
2005 else if(expr.
id()==ID_typecast)
2014 if(!typedef_str.empty() &&
2018 assert(expr.
type().
id()!=ID_union &&
2019 expr.
type().
id()!=ID_struct);
2022 else if(expr.
id()==ID_symbol)
2024 if(expr.
type().
id()!=ID_code)
2030 symbol.
type.
id()!=ID_code &&
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const codet & then_case() const
const typet & follow(const typet &src) const
const exprt & return_value() const
struct configt::ansi_ct ansi_c
const code_declt & to_code_decl(const codet &code)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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)
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)
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
instructionst instructions
The list of instructions in the goto program.
void convert_assign_rec(const code_assignt &assign, codet &dest)
const codet & body() const
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
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)
const irep_idt & get_value() const
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.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
exprt::operandst argumentst
unsignedbv_typet size_type()
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)
const id_sett & typedef_names
static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)
const exprt & case_op() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
loop_last_stackt loop_last_stack
instructionst::const_iterator const_targett
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The boolean constant true.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
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
const irep_idt & get(const irep_namet &name) const
A label for branch targets.
std::set< std::string > & system_headers
const code_returnt & to_code_return(const codet &code)
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
const code_switch_caset & to_code_switch_case(const codet &code)
bitvector_typet index_type()
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
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)
code_blockt & toplevel_block
bool has_return_value() const
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
A function call side effect.
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)
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)
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
A ‘do while’ instruction.
const source_locationt & source_location() const
const exprt & iter() const
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
exprt::operandst & arguments()
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
#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
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
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
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
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)