57 for(natural_loopst::loop_mapt::const_iterator
62 assert(!l_it->second.empty());
72 it=l_it->second.begin();
73 it!=l_it->second.end();
77 if((*it)->get_target()==loop_start &&
78 (*it)->location_number>loop_end->location_number)
82 if(!
loop_map.insert(std::make_pair(loop_start, loop_end)).second)
94 dead_map[target->get_dead().get_identifier()] = target->location_number;
102 if(target->is_assign())
104 const exprt &l = target->get_assign().lhs();
105 const exprt &
r = target->get_assign().rhs();
109 r.id() == ID_side_effect &&
115 else if(l.
type().
id()==ID_pointer &&
116 l.
type().
get(ID_C_typedef)==
"va_list" &&
118 r.id()==ID_typecast &&
134 if(target->type!=
ASSERT &&
135 !target->source_location.get_comment().empty())
138 dest.
statements().back().add_source_location().set_comment(
139 target->source_location.get_comment());
143 if(target->is_target() && !target->is_goto())
149 upper_bound->location_number > loop_entry->second->location_number))
166 dest.
add(target->get_function_call());
170 dest.
add(target->get_other());
185 dest.
statements().back().add_source_location().set_comment(
186 target->source_location.get_comment());
201 dest.
statements().back().add_source_location().set_comment(
"END_THREAD");
212 dest.
add(std::move(f));
239 if(target->is_target())
241 std::stringstream label;
246 latest_block->
add(std::move(l));
251 for(goto_programt::instructiont::labelst::const_iterator
252 it=target->labels.begin();
253 it!=target->labels.end();
268 latest_block->
add(std::move(l));
273 if(latest_block!=&dest)
299 const exprt this_va_list_expr=assign.
lhs();
302 if(
r.id()==ID_constant &&
307 {this_va_list_expr});
309 dest.
add(std::move(f));
312 r.id() == ID_side_effect &&
320 dest.
add(std::move(f));
322 else if(
r.id() == ID_plus)
326 {this_va_list_expr});
340 if(next!=upper_bound &&
343 const exprt &n_r = next->get_assign().rhs();
345 n_r.
id() == ID_dereference &&
348 f.lhs() = next->get_assign().lhs();
350 type_of.arguments().push_back(f.lhs());
351 f.arguments().push_back(type_of);
353 dest.
add(std::move(f));
359 assert(
r.find(ID_C_va_arg_type).is_not_nil());
360 const typet &va_arg_type=
361 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
367 type_of.arguments().push_back(deref);
368 f.arguments().push_back(type_of);
372 dest.
add(std::move(void_f));
378 {this_va_list_expr,
r});
380 dest.
add(std::move(f));
390 if(assign.
rhs().
id()==ID_array)
429 while(next!=upper_bound && next->is_dead() && !next->is_target())
432 if(next!=upper_bound &&
456 upper_bound->location_number > entry->second);
460 if(next!=upper_bound &&
462 !next->is_target() &&
463 (next->is_assign() || next->is_function_call()))
465 exprt lhs = next->is_assign() ? next->get_assign().lhs()
466 : next->get_function_call().lhs();
470 if(next->is_assign())
495 dest.
add(std::move(d));
507 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
516 for( ; target!=loop_end; ++target)
523 dest.
add(std::move(d));
532 assert(target->is_goto());
534 assert(target->targets.size()==1);
540 upper_bound->location_number > loop_entry->second->location_number))
542 else if(!target->guard.is_true())
555 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
567 if(target->get_target()==after_loop)
572 else if(target->guard.is_true())
583 for(++target; target!=loop_end; ++target)
589 if(loop_end->guard.is_false())
593 else if(!loop_end->guard.is_true())
603 if(w.body().has_operands() &&
607 w.body().operands().pop_back();
608 increment.
id(ID_side_effect);
616 else if(w.body().has_operands() &&
626 w.body().operands().pop_back();
635 dest.
add(std::move(w));
643 const exprt &switch_var,
649 std::set<goto_programt::const_targett> unique_targets;
653 cases_it!=upper_bound && cases_it!=first_target;
656 if(cases_it->is_goto() &&
657 !cases_it->is_backwards_goto() &&
658 cases_it->guard.is_true())
660 default_target=cases_it->get_target();
663 first_target->location_number > default_target->location_number)
664 first_target=default_target;
666 last_target->location_number < default_target->location_number)
667 last_target=default_target;
669 cases.push_back(
caset(
674 unique_targets.insert(default_target);
679 else if(cases_it->is_goto() &&
680 !cases_it->is_backwards_goto() &&
681 (cases_it->guard.id()==ID_equal ||
682 cases_it->guard.id()==ID_or))
685 if(cases_it->guard.id()==ID_equal)
686 eqs.push_back(cases_it->guard);
688 eqs=cases_it->guard.operands();
692 for(exprt::operandst::const_reverse_iterator
694 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
697 if(e_it->id()!=ID_equal ||
702 cases.push_back(
caset(
706 cases_it->get_target()));
707 assert(cases.back().value.is_not_nil());
710 first_target->location_number>
711 cases.back().case_start->location_number)
712 first_target=cases.back().case_start;
714 last_target->location_number<
715 cases.back().case_start->location_number)
716 last_target=cases.back().case_start;
718 unique_targets.insert(cases.back().case_start);
727 if(unique_targets.size()<3)
731 if(cases_it==upper_bound ||
733 upper_bound->location_number < last_target->location_number) ||
735 last_target->location_number > default_target->location_number) ||
736 target->get_target()==default_target)
746 std::set<unsigned> &processed_locations)
748 std::set<goto_programt::const_targett> targets_done;
750 for(cases_listt::iterator it=cases.begin();
756 if(!targets_done.insert(it->case_start).second)
763 case_end!=upper_bound;
766 const auto &case_end_node = dominators.
get_node(case_end);
773 if(case_end==it->case_start)
780 if(!dominators.
dominates(it->case_start, case_end_node))
783 if(!processed_locations.insert(case_end->location_number).second)
786 it->case_last=case_end;
798 for(cases_listt::const_iterator it=cases.begin();
807 cases_listt::const_iterator last=--cases.end();
808 if(last->case_start==default_target &&
823 next_case == default_target &&
824 (!it->case_last->is_goto() ||
825 (it->case_last->get_condition().is_true() &&
826 it->case_last->get_target() == default_target)))
835 if(it->case_last->is_goto() &&
836 it->case_last->guard.is_true() &&
837 it->case_last->get_target()==default_target)
841 if(!it->case_last->is_goto())
856 exprt eq_cand=target->guard;
857 if(eq_cand.
id()==ID_or)
860 if(target->is_backwards_goto() ||
861 eq_cand.
id()!=ID_equal ||
893 if(cases_start==target)
901 for(target=cases_start; target!=first_target; ++target)
904 std::set<unsigned> processed_locations;
923 for(cases_listt::const_iterator it=cases.begin();
927 it->case_last->location_number > max_target->location_number)
928 max_target=it->case_last;
930 std::map<goto_programt::const_targett, unsigned> targets_done;
935 for(cases_listt::const_iterator it=cases.begin();
941 if(it->value.is_nil())
944 csc.case_op()=it->value;
948 if(targets_done.find(it->case_start)!=targets_done.end())
950 assert(it->case_selector==orig_target ||
951 !it->case_selector->is_target());
959 csc.code().swap(cscp->
code());
966 if(it->case_selector!=orig_target)
970 target=it->case_start;
977 if(it->case_start!=(--cases.end())->case_start)
991 for( ; target!=after_last; ++target)
996 targets_done[it->case_start]=s.
body().
operands().size();
1006 if(processed_locations.find(it->location_number)==
1007 processed_locations.end())
1016 dest.
add(std::move(s));
1029 bool has_else=
false;
1031 if(!target->is_backwards_goto())
1038 if(before_else==target)
1045 before_else->is_goto() &&
1046 before_else->get_target()->location_number > end_if->location_number &&
1047 before_else->guard.is_true() &&
1049 upper_bound->location_number>=
1050 before_else->get_target()->location_number);
1053 end_if=before_else->get_target();
1057 if(target->is_backwards_goto() ||
1059 upper_bound->location_number < end_if->location_number))
1076 for(++target; target!=before_else; ++target)
1082 for(++target; target!=end_if; ++target)
1088 for(++target; target!=end_if; ++target)
1093 dest.
add(std::move(i));
1116 if(target->get_target()==next)
1125 if(target->get_target()==loop_end &&
1136 dest.
add(std::move(i));
1150 if(target->get_target()==after_loop)
1160 dest.
add(std::move(i));
1175 if(target->get_target()==next)
1185 std::stringstream label;
1187 for(goto_programt::instructiont::labelst::const_iterator
1188 it=target->get_target()->labels.begin();
1189 it!=target->get_target()->labels.end();
1203 if(label.str().empty())
1204 label <<
CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1218 dest.
add(std::move(i));
1228 assert(target->is_start_thread());
1231 assert(thread_start->location_number > target->location_number);
1242 if(!next->is_goto())
1246 assert(this_end->is_end_thread());
1247 assert(thread_start->location_number > this_end->location_number);
1252 for(goto_programt::instructiont::labelst::const_iterator
1253 it=target->labels.begin();
1254 it!=target->labels.end();
1266 dest.
add(std::move(b));
1277 assert(next->is_goto() && next->guard.is_true());
1278 assert(!next->is_backwards_goto());
1279 assert(thread_start->location_number < next->get_target()->location_number);
1281 ++after_thread_start;
1285 assert(thread_start->location_number < thread_end->location_number);
1286 assert(thread_end->is_end_thread());
1289 thread_end->location_number < upper_bound->location_number);
1295 thread_start->is_function_call() &&
1296 thread_start->get_function_call().arguments().size() == 1 &&
1297 after_thread_start == thread_end)
1313 for( ; thread_start!=thread_end; ++thread_start)
1317 for(goto_programt::instructiont::labelst::const_iterator
1318 it=target->labels.begin();
1319 it!=target->labels.end();
1331 dest.
add(std::move(b));
1356 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1373 else if(type.
id()==ID_c_enum_tag)
1382 assert(!identifier.
empty());
1385 else if(type.
id()==ID_pointer ||
1386 type.
id()==ID_array)
1399 code.
op1().
id()==ID_side_effect &&
1418 if(!typedef_str.
empty() &&
1431 call.
lhs().
id()==ID_typecast)
1440 if(it->id()==ID_code)
1448 if(statement==ID_label)
1453 assert(!label.
empty());
1461 else if(statement==ID_block)
1463 else if(statement==ID_ifthenelse)
1465 else if(statement==ID_dowhile)
1476 code=do_while.
body();
1481 const exprt &
function,
1484 if(
function.
id()!=ID_symbol)
1497 if(parameters.size()==arguments.size())
1499 code_typet::parameterst::const_iterator it=parameters.begin();
1502 if(it2->type().id() == ID_union || it2->type().id() == ID_union_tag)
1503 it2->type()=it->type();
1518 operands.size()>1 && i<operands.size();
1521 exprt::operandst::iterator it=operands.begin()+i;
1524 it->source_location().get_comment().
empty())
1529 bool has_decl=
false;
1539 operands.insert(operands.begin()+i+1,
1540 it->operands().begin(), it->operands().end());
1541 operands.erase(operands.begin()+i);
1551 if(operands.empty() && parent_stmt!=ID_nil)
1553 else if(operands.size()==1 &&
1554 parent_stmt!=ID_nil &&
1565 type.
remove(ID_C_constant);
1567 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1576 "Symbol "+
id2string(identifier)+
" should be a type");
1580 else if(type.
id()==ID_array)
1582 else if(type.
id()==ID_struct ||
1583 type.
id()==ID_union)
1588 for(struct_union_typet::componentst::iterator
1610 if(expr.
is_nil() ||
to_code(expr).get_statement() != ID_block)
1616 block.
statements().back().get_statement() != ID_label)
1697 code =
code_blockt({i_t_e, then_label, else_label});
1730 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1735 else if(!no_typecast &&
1736 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1737 expr.
id()==ID_array || expr.
id()==ID_vector))
1750 expr.
id() == ID_union && expr.
type().
id() != ID_union &&
1751 expr.
type().
id() != ID_union_tag)
1757 if(expr.
id()==ID_typecast &&
1761 if(expr.
id()==ID_union ||
1762 expr.
id()==ID_struct)
1768 expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag,
1769 "union/struct expressions should have a tag type");
1777 if(!typedef_str.
empty() &&
1781 else if(expr.
id()==ID_array ||
1782 expr.
id()==ID_vector)
1785 expr.
get_bool(ID_C_string_constant))
1794 if(!typedef_str.
empty() &&
1798 else if(expr.
id()==ID_side_effect)
1802 if(statement==ID_nondet)
1809 for(symbol_tablet::symbolst::const_iterator
1814 if(it->second.type.id()!=ID_code)
1836 suffix=expr.
type().
get(ID_C_c_type);
1843 if(base_name.
empty())
1854 symbol.
name=base_name;
1872 else if(expr.
id()==ID_isnan ||
1875 else if(expr.
id()==ID_constant)
1877 if(expr.
type().
id()==ID_floatbv)
1883 else if(expr.
type().
id()==ID_pointer)
1885 else if(expr.
type().
id()==ID_bool ||
1886 expr.
type().
id()==ID_c_bool)
1894 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
1899 else if(expr.
id()==ID_typecast)
1901 if(expr.
type().
id() == ID_c_bit_field)
1908 if(!typedef_str.
empty() &&
1912 assert(expr.
type().
id()!=ID_union &&
1913 expr.
type().
id()!=ID_struct);
1916 else if(expr.
id()==ID_symbol)
1918 if(expr.
type().
id()!=ID_code)
1924 symbol.
type.
id()!=ID_code &&
1945 if(src->code.source_location().is_not_nil())
1947 else if(src->source_location.is_not_nil())