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");
252 codet *latest_block=&dest;
255 if(target->is_target())
257 std::stringstream label;
261 target_label=l.get_label();
267 for(goto_programt::instructiont::labelst::const_iterator
268 it=target->labels.begin();
269 it!=target->labels.end();
289 if(latest_block!=&dest)
315 const exprt this_va_list_expr=assign.
lhs();
322 if(
r.id()==ID_constant &&
326 f.arguments().push_back(this_va_list_expr);
327 f.arguments().back().type().id(ID_gcc_builtin_va_list);
331 else if(
r.id()==ID_address_of)
334 f.arguments().push_back(this_va_list_expr);
335 f.arguments().back().type().id(ID_gcc_builtin_va_list);
340 else if(
r.id()==ID_side_effect &&
344 f.arguments().push_back(this_va_list_expr);
345 f.arguments().back().type().id(ID_gcc_builtin_va_list);
355 if(next!=upper_bound &&
359 if(n_r.
id()==ID_dereference &&
366 f.arguments().push_back(type_of);
374 assert(
r.find(ID_C_va_arg_type).is_not_nil());
375 const typet &va_arg_type=
376 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
383 f.arguments().push_back(type_of);
392 f.arguments().push_back(this_va_list_expr);
393 f.arguments().back().type().id(ID_gcc_builtin_va_list);
394 f.arguments().push_back(
r);
406 if(assign.
rhs().
id()==ID_array)
444 while(next!=upper_bound && next->is_dead() && !next->is_target())
447 if(next!=upper_bound &&
471 upper_bound->location_number > entry->second);
475 if(next!=upper_bound &&
477 !next->is_target() &&
478 (next->is_assign() || next->is_function_call()))
480 exprt lhs=next->is_assign() ?
486 if(next->is_assign())
522 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
525 d.
cond()=loop_end->guard;
533 for( ; target!=loop_end; ++target)
549 assert(target->is_goto());
551 assert(target->targets.size()==1);
553 loopt::const_iterator loop_entry=
loop_map.find(target);
557 upper_bound->location_number > loop_entry->second->location_number))
559 else if(!target->guard.is_true())
572 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
585 if(target->get_target()==after_loop)
590 else if(target->guard.is_true())
603 for(++target; target!=loop_end; ++target)
609 if(loop_end->guard.is_false())
615 else if(!loop_end->guard.is_true())
631 f.iter().id(ID_side_effect);
635 f.body().swap(w.
body());
670 const exprt &switch_var,
676 std::set<goto_programt::const_targett> unique_targets;
680 cases_it!=upper_bound && cases_it!=first_target;
683 if(cases_it->is_goto() &&
684 !cases_it->is_backwards_goto() &&
685 cases_it->guard.is_true())
687 default_target=cases_it->get_target();
690 first_target->location_number > default_target->location_number)
691 first_target=default_target;
693 last_target->location_number < default_target->location_number)
694 last_target=default_target;
696 cases.push_back(
caset(
701 unique_targets.insert(default_target);
706 else if(cases_it->is_goto() &&
707 !cases_it->is_backwards_goto() &&
708 (cases_it->guard.id()==ID_equal ||
709 cases_it->guard.id()==ID_or))
712 if(cases_it->guard.id()==ID_equal)
713 eqs.push_back(cases_it->guard);
715 eqs=cases_it->guard.operands();
719 for(exprt::operandst::const_reverse_iterator
721 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
724 if(e_it->id()!=ID_equal ||
729 cases.push_back(
caset(
733 cases_it->get_target()));
734 assert(cases.back().value.is_not_nil());
737 first_target->location_number>
738 cases.back().case_start->location_number)
739 first_target=cases.back().case_start;
741 last_target->location_number<
742 cases.back().case_start->location_number)
743 last_target=cases.back().case_start;
745 unique_targets.insert(cases.back().case_start);
754 if(unique_targets.size()<3)
758 if(cases_it==upper_bound ||
760 upper_bound->location_number < last_target->location_number) ||
762 last_target->location_number > default_target->location_number) ||
763 target->get_target()==default_target)
773 std::set<unsigned> &processed_locations)
775 std::set<goto_programt::const_targett> targets_done;
777 for(cases_listt::iterator it=cases.begin();
783 if(!targets_done.insert(it->case_start).second)
790 case_end!=upper_bound;
793 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
797 dominators.
cfg[i_entry->second];
800 if(n.dominators.empty())
804 if(case_end==it->case_start)
811 if(n.dominators.find(it->case_start)==n.dominators.end())
814 if(!processed_locations.insert(case_end->location_number).second)
817 it->case_last=case_end;
829 for(cases_listt::const_iterator it=cases.begin();
838 cases_listt::const_iterator last=--cases.end();
839 if(last->case_start==default_target &&
848 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
852 dominators.
cfg[i_entry->second];
854 if(!n.dominators.empty())
859 next_case==default_target &&
860 (!it->case_last->is_goto() ||
861 (it->case_last->guard.is_true() &&
862 it->case_last->get_target()==default_target)))
871 if(it->case_last->is_goto() &&
872 it->case_last->guard.is_true() &&
873 it->case_last->get_target()==default_target)
877 if(!it->case_last->is_goto())
892 exprt eq_cand=target->guard;
893 if(eq_cand.
id()==ID_or)
894 eq_cand=eq_cand.
op0();
896 if(target->is_backwards_goto() ||
897 eq_cand.
id()!=ID_equal ||
905 cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry=
908 if(dominators.
cfg[t_entry->second].dominators.
empty())
934 if(cases_start==target)
942 for(target=cases_start; target!=first_target; ++target)
945 std::set<unsigned> processed_locations;
964 for(cases_listt::const_iterator it=cases.begin();
968 it->case_last->location_number > max_target->location_number)
969 max_target=it->case_last;
971 std::map<goto_programt::const_targett, unsigned> targets_done;
976 for(cases_listt::const_iterator it=cases.begin();
982 if(it->value.is_nil())
989 if(targets_done.find(it->case_start)!=targets_done.end())
991 assert(it->case_selector==orig_target ||
992 !it->case_selector->is_target());
997 while(cscp->code().get_statement()==ID_switch_case)
1001 cscp->code().swap(csc);
1007 if(it->case_selector!=orig_target)
1011 target=it->case_start;
1018 if(it->case_start!=(--cases.end())->case_start)
1032 for( ; target!=after_last; ++target)
1037 targets_done[it->case_start]=s.
body().
operands().size();
1047 if(processed_locations.find(it->location_number)==
1048 processed_locations.end())
1050 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1054 dominators.
cfg[it_entry->second];
1056 if(!n.dominators.empty())
1076 bool has_else=
false;
1078 if(!target->is_backwards_goto())
1085 if(before_else==target)
1092 before_else->is_goto() &&
1093 before_else->get_target()->location_number > end_if->location_number &&
1094 before_else->guard.is_true() &&
1096 upper_bound->location_number>=
1097 before_else->get_target()->location_number);
1100 end_if=before_else->get_target();
1104 if(target->is_backwards_goto() ||
1106 upper_bound->location_number < end_if->location_number))
1123 for(++target; target!=before_else; ++target)
1128 for(++target; target!=end_if; ++target)
1133 for(++target; target!=end_if; ++target)
1156 cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
1158 assert(i_entry!=dominators.cfg.entry_map.end());
1160 dominators.cfg[i_entry->second];
1162 if(!n.dominators.empty())
1166 if(target->get_target()==next)
1175 if(target->get_target()==loop_end &&
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)
1231 if(target->get_target()==next)
1235 cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry=
1239 dominators.
cfg[it_entry->second];
1243 if(n.dominators.empty())
1246 std::stringstream label;
1248 for(goto_programt::instructiont::labelst::const_iterator
1249 it=target->get_target()->labels.begin();
1250 it!=target->get_target()->labels.end();
1264 if(label.str().empty())
1265 label <<
CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1276 if(i.cond().is_true())
1289 assert(target->is_start_thread());
1292 assert(thread_start->location_number > target->location_number);
1303 if(!next->is_goto())
1307 assert(this_end->is_end_thread());
1308 assert(thread_start->location_number > this_end->location_number);
1313 for(goto_programt::instructiont::labelst::const_iterator
1314 it=target->labels.begin();
1315 it!=target->labels.end();
1339 assert(next->is_goto() && next->guard.is_true());
1340 assert(!next->is_backwards_goto());
1341 assert(thread_start->location_number < next->get_target()->location_number);
1343 ++after_thread_start;
1347 assert(thread_start->location_number < thread_end->location_number);
1348 assert(thread_end->is_end_thread());
1351 thread_end->location_number < upper_bound->location_number);
1357 thread_start->is_function_call() &&
1359 after_thread_start == thread_end)
1376 for( ; thread_start!=thread_end; ++thread_start)
1379 for(goto_programt::instructiont::labelst::const_iterator
1380 it=target->labels.begin();
1381 it!=target->labels.end();
1419 if(type.
id() == ID_symbol_type)
1423 if(full_type.
id()==ID_pointer ||
1424 full_type.
id()==ID_array)
1428 else if(full_type.
id()==ID_struct ||
1429 full_type.
id()==ID_union)
1441 assert(!identifier.
empty());
1445 else if(type.
id()==ID_c_enum_tag)
1454 assert(!identifier.
empty());
1457 else if(type.
id()==ID_pointer ||
1458 type.
id()==ID_array)
1471 code.
op0().
type().
id(ID_gcc_builtin_va_list);
1474 code.
op1().
id()==ID_side_effect &&
1493 if(!typedef_str.empty() &&
1506 call.
lhs().
id()==ID_typecast)
1515 if(it->id()==ID_code)
1523 if(statement==ID_label)
1528 assert(!label.
empty());
1537 else if(statement==ID_block)
1539 else if(statement==ID_ifthenelse)
1541 else if(statement==ID_dowhile)
1552 code=do_while.
body();
1557 const exprt &
function,
1560 if(
function.
id()!=ID_symbol)
1573 if(parameters.size()==arguments.size())
1575 code_typet::parameterst::const_iterator it=parameters.begin();
1578 if(
ns.
follow(it2->type()).
id()==ID_union)
1579 it2->type()=it->type();
1594 operands.size()>1 && i<operands.size();
1597 exprt::operandst::iterator it=operands.begin()+i;
1600 it->source_location().get_comment().
empty())
1605 bool has_decl=
false;
1615 operands.insert(operands.begin()+i+1,
1616 it->operands().begin(), it->operands().end());
1617 operands.erase(operands.begin()+i);
1627 if(operands.empty() && parent_stmt!=ID_nil)
1629 else if(operands.size()==1 &&
1630 parent_stmt!=ID_nil &&
1631 to_code(code.
op0()).get_statement()!=ID_decl)
1642 type.
remove(ID_C_constant);
1644 if(type.
id() == ID_symbol_type)
1653 "Symbol "+
id2string(identifier)+
" should be a type");
1657 else if(type.
id()==ID_array)
1659 else if(type.
id()==ID_struct ||
1660 type.
id()==ID_union)
1665 for(struct_union_typet::componentst::iterator
1693 block.
statements().back().get_statement() != ID_label)
1776 code =
code_blockt({i_t_e, then_label, else_label});
1809 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1814 else if(!no_typecast &&
1815 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1816 expr.
id()==ID_array || expr.
id()==ID_vector))
1828 if(expr.
id()==ID_union &&
1835 if(expr.
id()==ID_typecast &&
1839 if(expr.
id()==ID_union ||
1840 expr.
id()==ID_struct)
1846 "type of union/struct expressions");
1854 if(!typedef_str.
empty() &&
1858 else if(expr.
id()==ID_array ||
1859 expr.
id()==ID_vector)
1862 expr.
get_bool(ID_C_string_constant))
1871 if(!typedef_str.
empty() &&
1875 else if(expr.
id()==ID_side_effect)
1879 if(statement==ID_nondet)
1886 for(symbol_tablet::symbolst::const_iterator
1891 if(it->second.type.id()!=ID_code)
1910 if(expr.
type().
get(ID_C_c_type)!=
"")
1913 suffix=expr.
type().
get(ID_C_c_type);
1931 symbol.
name=base_name;
1951 else if(expr.
id()==ID_isnan ||
1954 else if(expr.
id()==ID_constant)
1956 if(expr.
type().
id()==ID_floatbv)
1962 else if(expr.
type().
id()==ID_pointer)
1964 else if(expr.
type().
id()==ID_bool ||
1965 expr.
type().
id()==ID_c_bool)
1973 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
1978 else if(expr.
id()==ID_typecast)
1987 if(!typedef_str.empty() &&
1991 assert(expr.
type().
id()!=ID_union &&
1992 expr.
type().
id()!=ID_struct);
1995 else if(expr.
id()==ID_symbol)
1997 if(expr.
type().
id()!=ID_code)
2003 symbol.
type.
id()!=ID_code &&
2024 if(src->code.source_location().is_not_nil())
2026 else if(src->source_location.is_not_nil())
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
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, extends irept.
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)
Semantic type conversion.
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
codet representing a switch statement.
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".
pointer_typet pointer_type(const typet &subtype)
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 instruction pointed-to by the given instruction iterator 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
codet representation of a continue statement (within a for or while loop).
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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 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)
Copy the given argument to the end of exprt's operands.
const irep_idt & get_identifier() const
code_operandst & statements()
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)
Move the given argument to the end of exprt's operands.
bool is_false() const
Return whether the expression is a constant representing false.
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 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.
bool is_true() const
Return whether the expression is a constant representing true.
codet representation of a goto statement.
typet & type()
Return the type of the expression.
exprt::operandst argumentst
unsignedbv_typet size_type()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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)
codet representation of an expression statement.
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
const exprt & case_op() const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an 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
void add(const codet &code)
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
The Boolean constant true.
A codet representing the 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)
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
codet representation of 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.
codet representation of a function call statement.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
codet representing a while statement.
const code_switch_caset & to_code_switch_case(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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 an exprt to a constant_exprt.
bool has_operands() const
Return true if there is at least one operand.
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
bool is_constant() const
Return whether the expression is a constant.
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 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 side_effect_exprt representation of 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 an exprt to an equal_exprt.
void copy_source_location(goto_programt::const_targett, codet &dst)
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 for structs and unions.
void set_statement(const irep_idt &statement)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
codet representation of a break statement (within a for or while loop).
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 typet to a struct_union_typet.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
codet representation of a do while statement.
const source_locationt & source_location() const
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
exprt::operandst & arguments()
#define Forall_operands(it, expr)
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
A codet representing a skip statement.
codet representation of an if-then-else statement.
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
codet representation of a switch-case, i.e. a case statement within a switch.
Data structure for representing an arbitrary statement in a program.
codet representation of a "return from a function" statement.
std::list< caset > cases_listt
void remove(const irep_namet &name)
codet representation of a for statement.
const code_labelt & to_code_label(const codet &code)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
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)
Create a typecast_exprt to the given 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 documentation for namespace_baset::lookup().
const irep_idt & get_identifier() const
const irep_idt & get_identifier() const
A codet representing an assignment in the program.
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)