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 if(instruction.is_dead())
96 dead_map[instruction.dead_symbol().get_identifier()] =
97 instruction.location_number;
108 if(instruction.is_assign())
110 const exprt &l = instruction.assign_lhs();
111 const exprt &
r = instruction.assign_rhs();
115 r.id() == ID_side_effect &&
121 else if(l.
type().
id()==ID_pointer &&
122 l.
type().
get(ID_C_typedef)==
"va_list" &&
124 r.id()==ID_typecast &&
141 if(target->type!=
ASSERT &&
142 !target->source_location.get_comment().empty())
145 dest.
statements().back().add_source_location().set_comment(
146 target->source_location.get_comment());
150 if(target->is_target() && !target->is_goto())
156 upper_bound->location_number > loop_entry->second->location_number))
173 dest.
add(target->get_function_call());
177 dest.
add(target->get_other());
192 dest.
statements().back().add_source_location().set_comment(
193 target->source_location.get_comment());
208 dest.
statements().back().add_source_location().set_comment(
"END_THREAD");
219 dest.
add(std::move(f));
246 if(target->is_target())
248 std::stringstream label;
253 latest_block->
add(std::move(l));
258 for(goto_programt::instructiont::labelst::const_iterator
259 it=target->labels.begin();
260 it!=target->labels.end();
275 latest_block->
add(std::move(l));
280 if(latest_block!=&dest)
289 const code_assignt a{target->assign_lhs(), target->assign_rhs()};
304 const exprt this_va_list_expr = target->assign_lhs();
307 if(
r.id()==ID_constant &&
312 {this_va_list_expr});
314 dest.
add(std::move(f));
317 r.id() == ID_side_effect &&
325 dest.
add(std::move(f));
327 else if(
r.id() == ID_plus)
331 {this_va_list_expr});
345 if(next!=upper_bound &&
348 const exprt &n_r = next->assign_rhs();
350 n_r.
id() == ID_dereference &&
353 f.lhs() = next->assign_lhs();
355 type_of.arguments().push_back(f.lhs());
356 f.arguments().push_back(type_of);
358 dest.
add(std::move(f));
364 assert(
r.find(ID_C_va_arg_type).is_not_nil());
365 const typet &va_arg_type=
366 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
372 type_of.arguments().push_back(deref);
373 f.arguments().push_back(type_of);
377 dest.
add(std::move(void_f));
383 {this_va_list_expr,
r});
385 dest.
add(std::move(f));
395 if(assign.
rhs().
id()==ID_array)
420 target->return_value().id() != ID_side_effect ||
432 while(next!=upper_bound && next->is_dead() && !next->is_target())
435 if(next!=upper_bound &&
459 upper_bound->location_number > entry->second);
463 if(next!=upper_bound &&
465 !next->is_target() &&
466 (next->is_assign() || next->is_function_call()))
469 next->is_assign() ? next->assign_lhs() : next->get_function_call().lhs();
473 if(next->is_assign())
498 dest.
add(std::move(d));
510 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
519 for( ; target!=loop_end; ++target)
526 dest.
add(std::move(d));
535 assert(target->is_goto());
537 assert(target->targets.size()==1);
543 upper_bound->location_number > loop_entry->second->location_number))
545 else if(!target->guard.is_true())
558 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
570 if(target->get_target()==after_loop)
575 else if(target->guard.is_true())
586 for(++target; target!=loop_end; ++target)
592 if(loop_end->guard.is_false())
596 else if(!loop_end->guard.is_true())
606 if(w.body().has_operands() &&
610 w.body().operands().pop_back();
611 increment.
id(ID_side_effect);
619 else if(w.body().has_operands() &&
629 w.body().operands().pop_back();
638 dest.
add(std::move(w));
646 const exprt &switch_var,
652 std::set<goto_programt::const_targett> unique_targets;
656 cases_it!=upper_bound && cases_it!=first_target;
659 if(cases_it->is_goto() &&
660 !cases_it->is_backwards_goto() &&
661 cases_it->guard.is_true())
663 default_target=cases_it->get_target();
666 first_target->location_number > default_target->location_number)
667 first_target=default_target;
669 last_target->location_number < default_target->location_number)
670 last_target=default_target;
672 cases.push_back(
caset(
677 unique_targets.insert(default_target);
682 else if(cases_it->is_goto() &&
683 !cases_it->is_backwards_goto() &&
684 (cases_it->guard.id()==ID_equal ||
685 cases_it->guard.id()==ID_or))
688 if(cases_it->guard.id()==ID_equal)
689 eqs.push_back(cases_it->guard);
691 eqs=cases_it->guard.operands();
695 for(exprt::operandst::const_reverse_iterator
697 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
700 if(e_it->id()!=ID_equal ||
705 cases.push_back(
caset(
709 cases_it->get_target()));
710 assert(cases.back().value.is_not_nil());
713 first_target->location_number>
714 cases.back().case_start->location_number)
715 first_target=cases.back().case_start;
717 last_target->location_number<
718 cases.back().case_start->location_number)
719 last_target=cases.back().case_start;
721 unique_targets.insert(cases.back().case_start);
730 if(unique_targets.size()<3)
734 if(cases_it==upper_bound ||
736 upper_bound->location_number < last_target->location_number) ||
738 last_target->location_number > default_target->location_number) ||
739 target->get_target()==default_target)
749 std::set<unsigned> &processed_locations)
751 std::set<goto_programt::const_targett> targets_done;
753 for(cases_listt::iterator it=cases.begin();
759 if(!targets_done.insert(it->case_start).second)
766 case_end!=upper_bound;
769 const auto &case_end_node = dominators.
get_node(case_end);
776 if(case_end==it->case_start)
783 if(!dominators.
dominates(it->case_start, case_end_node))
786 if(!processed_locations.insert(case_end->location_number).second)
789 it->case_last=case_end;
801 for(cases_listt::const_iterator it=cases.begin();
810 cases_listt::const_iterator last=--cases.end();
811 if(last->case_start==default_target &&
826 next_case == default_target &&
827 (!it->case_last->is_goto() ||
828 (it->case_last->get_condition().is_true() &&
829 it->case_last->get_target() == default_target)))
838 if(it->case_last->is_goto() &&
839 it->case_last->guard.is_true() &&
840 it->case_last->get_target()==default_target)
844 if(!it->case_last->is_goto())
859 exprt eq_cand=target->guard;
860 if(eq_cand.
id()==ID_or)
863 if(target->is_backwards_goto() ||
864 eq_cand.
id()!=ID_equal ||
896 if(cases_start==target)
904 for(target=cases_start; target!=first_target; ++target)
907 std::set<unsigned> processed_locations;
926 for(cases_listt::const_iterator it=cases.begin();
930 it->case_last->location_number > max_target->location_number)
931 max_target=it->case_last;
933 std::map<goto_programt::const_targett, unsigned> targets_done;
938 for(cases_listt::const_iterator it=cases.begin();
944 if(it->value.is_nil())
947 csc.case_op()=it->value;
951 if(targets_done.find(it->case_start)!=targets_done.end())
953 assert(it->case_selector==orig_target ||
954 !it->case_selector->is_target());
962 csc.code().swap(cscp->
code());
969 if(it->case_selector!=orig_target)
973 target=it->case_start;
980 if(it->case_start!=(--cases.end())->case_start)
994 for( ; target!=after_last; ++target)
999 targets_done[it->case_start]=s.
body().
operands().size();
1009 if(processed_locations.find(it->location_number)==
1010 processed_locations.end())
1019 dest.
add(std::move(s));
1032 bool has_else=
false;
1034 if(!target->is_backwards_goto())
1041 if(before_else==target)
1048 before_else->is_goto() &&
1049 before_else->get_target()->location_number > end_if->location_number &&
1050 before_else->guard.is_true() &&
1052 upper_bound->location_number>=
1053 before_else->get_target()->location_number);
1056 end_if=before_else->get_target();
1060 if(target->is_backwards_goto() ||
1062 upper_bound->location_number < end_if->location_number))
1079 for(++target; target!=before_else; ++target)
1085 for(++target; target!=end_if; ++target)
1091 for(++target; target!=end_if; ++target)
1096 dest.
add(std::move(i));
1119 if(target->get_target()==next)
1128 if(target->get_target()==loop_end &&
1139 dest.
add(std::move(i));
1153 if(target->get_target()==after_loop)
1163 dest.
add(std::move(i));
1178 if(target->get_target()==next)
1188 std::stringstream label;
1190 for(goto_programt::instructiont::labelst::const_iterator
1191 it=target->get_target()->labels.begin();
1192 it!=target->get_target()->labels.end();
1206 if(label.str().empty())
1207 label <<
CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1221 dest.
add(std::move(i));
1231 assert(target->is_start_thread());
1234 assert(thread_start->location_number > target->location_number);
1245 if(!next->is_goto())
1249 assert(this_end->is_end_thread());
1250 assert(thread_start->location_number > this_end->location_number);
1255 for(goto_programt::instructiont::labelst::const_iterator
1256 it=target->labels.begin();
1257 it!=target->labels.end();
1269 dest.
add(std::move(b));
1280 assert(next->is_goto() && next->guard.is_true());
1281 assert(!next->is_backwards_goto());
1282 assert(thread_start->location_number < next->get_target()->location_number);
1284 ++after_thread_start;
1288 assert(thread_start->location_number < thread_end->location_number);
1289 assert(thread_end->is_end_thread());
1292 thread_end->location_number < upper_bound->location_number);
1298 thread_start->is_function_call() &&
1299 thread_start->call_arguments().size() == 1 &&
1300 after_thread_start == thread_end)
1316 for( ; thread_start!=thread_end; ++thread_start)
1320 for(goto_programt::instructiont::labelst::const_iterator
1321 it=target->labels.begin();
1322 it!=target->labels.end();
1334 dest.
add(std::move(b));
1359 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1376 else if(type.
id()==ID_c_enum_tag)
1385 assert(!identifier.
empty());
1388 else if(type.
id()==ID_pointer ||
1389 type.
id()==ID_array)
1402 code.
op1().
id()==ID_side_effect &&
1421 if(!typedef_str.
empty() &&
1434 call.
lhs().
id()==ID_typecast)
1442 if(op.id() == ID_code)
1450 if(statement==ID_label)
1455 assert(!label.
empty());
1463 else if(statement==ID_block)
1465 else if(statement==ID_ifthenelse)
1467 else if(statement==ID_dowhile)
1478 code=do_while.
body();
1483 const exprt &
function,
1486 if(
function.
id()!=ID_symbol)
1499 if(parameters.size()==arguments.size())
1501 code_typet::parameterst::const_iterator it=parameters.begin();
1502 for(
auto &argument : arguments)
1505 argument.type().id() == ID_union ||
1506 argument.type().id() == ID_union_tag)
1508 argument.type() = it->type();
1524 operands.size()>1 && i<operands.size();
1527 exprt::operandst::iterator it=operands.begin()+i;
1530 it->source_location().get_comment().
empty())
1535 bool has_decl=
false;
1545 operands.insert(operands.begin()+i+1,
1546 it->operands().begin(), it->operands().end());
1547 operands.erase(operands.begin()+i);
1557 if(operands.empty() && parent_stmt!=ID_nil)
1559 else if(operands.size()==1 &&
1560 parent_stmt!=ID_nil &&
1571 type.
remove(ID_C_constant);
1573 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1582 "Symbol "+
id2string(identifier)+
" should be a type");
1586 else if(type.
id()==ID_array)
1588 else if(type.
id()==ID_struct ||
1589 type.
id()==ID_union)
1594 for(struct_union_typet::componentst::iterator
1600 else if(type.
id() == ID_c_bit_field)
1618 if(expr.
is_nil() ||
to_code(expr).get_statement() != ID_block)
1624 block.
statements().back().get_statement() != ID_label)
1705 code =
code_blockt({i_t_e, then_label, else_label});
1738 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1743 else if(!no_typecast &&
1744 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1745 expr.
id()==ID_array || expr.
id()==ID_vector))
1758 expr.
id() == ID_union && expr.
type().
id() != ID_union &&
1759 expr.
type().
id() != ID_union_tag)
1765 if(expr.
id()==ID_typecast &&
1769 if(expr.
id()==ID_union ||
1770 expr.
id()==ID_struct)
1776 expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag,
1777 "union/struct expressions should have a tag type");
1785 if(!typedef_str.
empty() &&
1789 else if(expr.
id()==ID_array ||
1790 expr.
id()==ID_vector)
1793 expr.
get_bool(ID_C_string_constant))
1802 if(!typedef_str.
empty() &&
1806 else if(expr.
id()==ID_side_effect)
1810 if(statement==ID_nondet)
1817 for(symbol_tablet::symbolst::const_iterator
1822 if(it->second.type.id()!=ID_code)
1844 suffix=expr.
type().
get(ID_C_c_type);
1851 if(base_name.
empty())
1862 symbol.
name=base_name;
1880 else if(expr.
id()==ID_isnan ||
1883 else if(expr.
id()==ID_constant)
1885 if(expr.
type().
id()==ID_floatbv)
1891 else if(expr.
type().
id()==ID_pointer)
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->get_code().source_location().is_not_nil())
1947 else if(src->source_location.is_not_nil())