58 for(natural_loopst::loop_mapt::const_iterator
63 assert(!l_it->second.empty());
72 for(natural_loopst::natural_loopt::const_iterator
73 it=l_it->second.begin();
74 it!=l_it->second.end();
78 if((*it)->get_target()==loop_start &&
79 (*it)->location_number>loop_end->location_number)
83 if(!
loop_map.insert(std::make_pair(loop_start, loop_end)).second)
96 target->location_number;
104 if(target->is_assign())
110 if(
r.id()==ID_side_effect &&
113 assert(
r.has_operands());
117 else if(l.
type().
id()==ID_pointer &&
118 l.
type().
get(ID_C_typedef)==
"va_list" &&
120 r.id()==ID_typecast &&
133 for(code_typet::parameterst::iterator
134 it2=parameters.begin();
135 it2!=parameters.end();
139 ns.
lookup(it2->get_identifier()).symbol_expr();
141 it2->type().id(ID_gcc_builtin_va_list);
153 if(target->type!=
ASSERT &&
154 !target->source_location.get_comment().empty())
157 dest.
operands().back().add_source_location().set_comment(
158 target->source_location.get_comment());
162 if(target->is_target() && !target->is_goto())
164 loopt::const_iterator loop_entry=
loop_map.find(target);
168 upper_bound->location_number > loop_entry->second->location_number))
201 dest.
operands().back().add_source_location().set_comment(
202 target->source_location.get_comment());
217 dest.
operands().back().add_source_location().set_comment(
"END_THREAD");
226 target->is_atomic_begin() ?
227 "__CPROVER_atomic_begin" :
228 "__CPROVER_atomic_end",
254 codet *latest_block=&dest;
257 if(target->is_target())
259 std::stringstream label;
260 label <<
"__CPROVER_DUMP_L" << target->target_number;
263 target_label=l.get_label();
269 for(goto_programt::instructiont::labelst::const_iterator
270 it=target->labels.begin();
271 it!=target->labels.end();
288 if(latest_block!=&dest)
314 const exprt this_va_list_expr=assign.
lhs();
321 if(
r.id()==ID_constant &&
325 f.arguments().push_back(this_va_list_expr);
326 f.arguments().back().type().id(ID_gcc_builtin_va_list);
330 else if(
r.id()==ID_address_of)
333 f.arguments().push_back(this_va_list_expr);
334 f.arguments().back().type().id(ID_gcc_builtin_va_list);
339 else if(
r.id()==ID_side_effect &&
343 f.arguments().push_back(this_va_list_expr);
344 f.arguments().back().type().id(ID_gcc_builtin_va_list);
354 if(next!=upper_bound &&
358 if(n_r.
id()==ID_dereference &&
365 f.arguments().push_back(type_of);
373 assert(
r.find(ID_C_va_arg_type).is_not_nil());
374 const typet &va_arg_type=
375 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
382 f.arguments().push_back(type_of);
391 f.arguments().push_back(this_va_list_expr);
392 f.arguments().back().type().id(ID_gcc_builtin_va_list);
393 f.arguments().push_back(
r);
405 if(assign.
rhs().
id()==ID_array)
443 while(next!=upper_bound && next->is_dead() && !next->is_target())
446 if(next!=upper_bound &&
470 upper_bound->location_number > entry->second);
474 if(next!=upper_bound &&
476 !next->is_target() &&
477 (next->is_assign() || next->is_function_call()))
479 exprt lhs=next->is_assign() ?
485 if(next->is_assign())
521 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
524 d.
cond()=loop_end->guard;
530 for( ; target!=loop_end; ++target)
546 assert(target->is_goto());
548 assert(target->targets.size()==1);
550 loopt::const_iterator loop_entry=
loop_map.find(target);
554 upper_bound->location_number > loop_entry->second->location_number))
556 else if(!target->guard.is_true())
569 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
579 if(target->get_target()==after_loop)
584 else if(target->guard.is_true())
597 for(++target; target!=loop_end; ++target)
603 if(loop_end->guard.is_false())
609 else if(!loop_end->guard.is_true())
631 f.
iter().
id(ID_side_effect);
666 const exprt &switch_var,
672 std::set<goto_programt::const_targett> unique_targets;
676 cases_it!=upper_bound && cases_it!=first_target;
679 if(cases_it->is_goto() &&
680 !cases_it->is_backwards_goto() &&
681 cases_it->guard.is_true())
683 default_target=cases_it->get_target();
686 first_target->location_number > default_target->location_number)
687 first_target=default_target;
689 last_target->location_number < default_target->location_number)
690 last_target=default_target;
692 cases.push_back(
caset(
697 unique_targets.insert(default_target);
702 else if(cases_it->is_goto() &&
703 !cases_it->is_backwards_goto() &&
704 (cases_it->guard.id()==ID_equal ||
705 cases_it->guard.id()==ID_or))
708 if(cases_it->guard.id()==ID_equal)
709 eqs.push_back(cases_it->guard);
711 eqs=cases_it->guard.operands();
715 for(exprt::operandst::const_reverse_iterator
717 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
720 if(e_it->id()!=ID_equal ||
725 cases.push_back(
caset(
729 cases_it->get_target()));
730 assert(cases.back().value.is_not_nil());
733 first_target->location_number>
734 cases.back().case_start->location_number)
735 first_target=cases.back().case_start;
737 last_target->location_number<
738 cases.back().case_start->location_number)
739 last_target=cases.back().case_start;
741 unique_targets.insert(cases.back().case_start);
750 if(unique_targets.size()<3)
754 if(cases_it==upper_bound ||
756 upper_bound->location_number < last_target->location_number) ||
758 last_target->location_number > default_target->location_number) ||
759 target->get_target()==default_target)
769 std::set<unsigned> &processed_locations)
771 std::set<goto_programt::const_targett> targets_done;
773 for(cases_listt::iterator it=cases.begin();
779 if(!targets_done.insert(it->case_start).second)
786 case_end!=upper_bound;
789 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
793 dominators.
cfg[i_entry->second];
796 if(n.dominators.empty())
800 if(case_end==it->case_start)
807 if(n.dominators.find(it->case_start)==n.dominators.end())
810 if(!processed_locations.insert(case_end->location_number).second)
813 it->case_last=case_end;
825 for(cases_listt::const_iterator it=cases.begin();
834 cases_listt::const_iterator last=--cases.end();
835 if(last->case_start==default_target &&
844 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
848 dominators.
cfg[i_entry->second];
850 if(!n.dominators.empty())
855 next_case==default_target &&
856 (!it->case_last->is_goto() ||
857 (it->case_last->guard.is_true() &&
858 it->case_last->get_target()==default_target)))
867 if(it->case_last->is_goto() &&
868 it->case_last->guard.is_true() &&
869 it->case_last->get_target()==default_target)
873 if(!it->case_last->is_goto())
888 exprt eq_cand=target->guard;
889 if(eq_cand.
id()==ID_or)
890 eq_cand=eq_cand.
op0();
892 if(target->is_backwards_goto() ||
893 eq_cand.
id()!=ID_equal ||
901 cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry=
904 if(dominators.
cfg[t_entry->second].dominators.
empty())
928 if(cases_start==target)
936 for(target=cases_start; target!=first_target; ++target)
939 std::set<unsigned> processed_locations;
958 for(cases_listt::const_iterator it=cases.begin();
962 it->case_last->location_number > max_target->location_number)
963 max_target=it->case_last;
965 std::map<goto_programt::const_targett, unsigned> targets_done;
970 for(cases_listt::const_iterator it=cases.begin();
976 if(it->value.is_nil())
983 if(targets_done.find(it->case_start)!=targets_done.end())
985 assert(it->case_selector==orig_target ||
986 !it->case_selector->is_target());
991 while(cscp->code().get_statement()==ID_switch_case)
995 cscp->code().swap(csc);
1001 if(it->case_selector!=orig_target)
1005 target=it->case_start;
1012 if(it->case_start!=(--cases.end())->case_start)
1026 for( ; target!=after_last; ++target)
1031 targets_done[it->case_start]=s.
body().
operands().size();
1041 if(processed_locations.find(it->location_number)==
1042 processed_locations.end())
1044 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1048 dominators.
cfg[it_entry->second];
1050 if(!n.dominators.empty())
1070 bool has_else=
false;
1072 if(!target->is_backwards_goto())
1079 if(before_else==target)
1086 before_else->is_goto() &&
1087 before_else->get_target()->location_number > end_if->location_number &&
1088 before_else->guard.is_true() &&
1090 upper_bound->location_number>=
1091 before_else->get_target()->location_number);
1094 end_if=before_else->get_target();
1101 if(target->is_backwards_goto() ||
1103 upper_bound->location_number < end_if->location_number))
1119 for(++target; target!=before_else; ++target)
1124 for(++target; target!=end_if; ++target)
1129 for(++target; target!=end_if; ++target)
1152 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1154 assert(i_entry!=dominators.cfg.entry_map.end());
1156 dominators.cfg[i_entry->second];
1158 if(!n.dominators.empty())
1162 if(target->get_target()==next)
1171 if(target->get_target()==loop_end &&
1176 if(!target->guard.is_true())
1179 i.
cond()=target->guard;
1196 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1197 dominators.cfg.entry_map.find(after_loop);
1198 assert(i_entry!=dominators.cfg.entry_map.end());
1200 dominators.cfg[i_entry->second];
1202 if(!n.dominators.empty())
1206 if(target->get_target()==after_loop)
1211 i.
cond()=target->guard;
1233 if(target->get_target()==next)
1237 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1241 dominators.
cfg[it_entry->second];
1245 if(n.dominators.empty())
1248 std::stringstream label;
1250 for(goto_programt::instructiont::labelst::const_iterator
1251 it=target->get_target()->labels.begin();
1252 it!=target->get_target()->labels.end();
1263 if(label.str().empty())
1264 label <<
"__CPROVER_DUMP_L" << target->get_target()->target_number;
1270 if(!target->guard.is_true())
1273 i.
cond()=target->guard;
1290 assert(target->is_start_thread());
1293 assert(thread_start->location_number > target->location_number);
1304 if(!next->is_goto())
1308 assert(this_end->is_end_thread());
1309 assert(thread_start->location_number > this_end->location_number);
1314 for(goto_programt::instructiont::labelst::const_iterator
1315 it=target->labels.begin();
1316 it!=target->labels.end();
1340 assert(next->is_goto() && next->guard.is_true());
1341 assert(!next->is_backwards_goto());
1342 assert(thread_start->location_number < next->get_target()->location_number);
1344 ++after_thread_start;
1348 assert(thread_start->location_number < thread_end->location_number);
1349 assert(thread_end->is_end_thread());
1352 thread_end->location_number < upper_bound->location_number);
1358 thread_start->is_function_call() &&
1360 after_thread_start == thread_end)
1382 for( ; thread_start!=thread_end; ++thread_start)
1385 for(goto_programt::instructiont::labelst::const_iterator
1386 it=target->labels.begin();
1387 it!=target->labels.end();
1425 if(type.
id()==ID_symbol)
1429 if(full_type.
id()==ID_pointer ||
1430 full_type.
id()==ID_array)
1434 else if(full_type.
id()==ID_struct ||
1435 full_type.
id()==ID_union)
1449 for(struct_union_typet::componentst::const_iterator
1450 it=components.begin();
1451 it!=components.end();
1455 assert(!identifier.
empty());
1459 else if(type.
id()==ID_c_enum_tag)
1468 assert(!identifier.
empty());
1471 else if(type.
id()==ID_pointer ||
1472 type.
id()==ID_array)
1485 code.
op0().
type().
id(ID_gcc_builtin_va_list);
1488 code.
op1().
id()==ID_side_effect &&
1507 if(!typedef_str.empty() &&
1520 call.
lhs().
id()==ID_typecast)
1529 if(it->id()==ID_code)
1537 if(statement==ID_label)
1542 assert(!label.
empty());
1551 else if(statement==ID_block)
1553 else if(statement==ID_ifthenelse)
1555 else if(statement==ID_dowhile)
1566 code=do_while.
body();
1571 const exprt &
function,
1574 if(
function.
id()!=ID_symbol)
1587 if(parameters.size()==arguments.size())
1589 code_typet::parameterst::const_iterator it=parameters.begin();
1592 if(
ns.
follow(it2->type()).
id()==ID_union)
1593 it2->type()=it->type();
1608 operands.size()>1 && i<operands.size();
1611 exprt::operandst::iterator it=operands.begin()+i;
1614 it->source_location().get_comment().
empty())
1619 bool has_decl=
false;
1629 operands.insert(operands.begin()+i+1,
1630 it->operands().begin(), it->operands().end());
1631 operands.erase(operands.begin()+i);
1641 if(operands.empty() && parent_stmt!=ID_nil)
1643 else if(operands.size()==1 &&
1644 parent_stmt!=ID_nil &&
1645 to_code(code.
op0()).get_statement()!=ID_decl)
1656 type.
remove(ID_C_constant);
1658 if(type.
id()==ID_symbol)
1667 "Symbol "+
id2string(identifier)+
" should be a type");
1671 else if(type.
id()==ID_array)
1673 else if(type.
id()==ID_struct ||
1674 type.
id()==ID_union)
1679 for(struct_union_typet::componentst::iterator
1828 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1833 else if(!no_typecast &&
1834 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1835 expr.
id()==ID_array || expr.
id()==ID_vector))
1847 if(expr.
id()==ID_union &&
1854 if(expr.
id()==ID_typecast &&
1858 if(expr.
id()==ID_union ||
1859 expr.
id()==ID_struct)
1864 assert(expr.
type().
id()==ID_symbol);
1872 if(!typedef_str.
empty() &&
1876 else if(expr.
id()==ID_array ||
1877 expr.
id()==ID_vector)
1880 expr.
get_bool(ID_C_string_constant))
1889 if(!typedef_str.
empty() &&
1893 else if(expr.
id()==ID_side_effect)
1897 if(statement==ID_nondet)
1904 for(symbol_tablet::symbolst::const_iterator
1909 if(it->second.type.id()!=ID_code)
1928 if(expr.
type().
get(ID_C_c_type)!=
"")
1931 suffix=expr.
type().
get(ID_C_c_type);
1949 symbol.
name=base_name;
1969 else if(expr.
id()==ID_isnan ||
1972 else if(expr.
id()==ID_constant)
1974 if(expr.
type().
id()==ID_floatbv)
1980 else if(expr.
type().
id()==ID_pointer)
1982 else if(expr.
type().
id()==ID_bool ||
1983 expr.
type().
id()==ID_c_bool)
1991 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
1996 else if(expr.
id()==ID_typecast)
2005 if(!typedef_str.empty() &&
2009 assert(expr.
type().
id()!=ID_union &&
2010 expr.
type().
id()!=ID_struct);
2013 else if(expr.
id()==ID_symbol)
2015 if(expr.
type().
id()!=ID_code)
2021 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
Deprecated expression utility functions.
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.
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()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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)