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;
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 &&
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));
392 f.
arguments().push_back(this_va_list_expr);
393 f.
arguments().back().type().id(ID_gcc_builtin_va_list);
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);
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());
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=
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=
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;
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();
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 &&
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
1687 if(expr.
is_nil() ||
to_code(expr).get_statement() != ID_block)
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())