58 for(natural_loopst::loop_mapt::const_iterator
63 assert(!l_it->second.empty());
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)
95 if(instruction.is_dead())
97 dead_map[instruction.dead_symbol().get_identifier()] =
98 instruction.location_number;
109 if(instruction.is_assign())
111 const exprt &l = instruction.get_assign().lhs();
112 const exprt &
r = instruction.get_assign().rhs();
116 r.id() == ID_side_effect &&
122 else if(l.
type().
id()==ID_pointer &&
123 l.
type().
get(ID_C_typedef)==
"va_list" &&
125 r.id()==ID_typecast &&
142 if(target->type!=
ASSERT &&
143 !target->source_location.get_comment().empty())
146 dest.
statements().back().add_source_location().set_comment(
147 target->source_location.get_comment());
151 if(target->is_target() && !target->is_goto())
157 upper_bound->location_number > loop_entry->second->location_number))
174 dest.
add(target->get_function_call());
178 dest.
add(target->get_other());
193 dest.
statements().back().add_source_location().set_comment(
194 target->source_location.get_comment());
209 dest.
statements().back().add_source_location().set_comment(
"END_THREAD");
220 dest.
add(std::move(f));
247 if(target->is_target())
249 std::stringstream label;
254 latest_block->
add(std::move(l));
259 for(goto_programt::instructiont::labelst::const_iterator
260 it=target->labels.begin();
261 it!=target->labels.end();
276 latest_block->
add(std::move(l));
281 if(latest_block!=&dest)
307 const exprt this_va_list_expr=assign.
lhs();
310 if(
r.id()==ID_constant &&
315 {this_va_list_expr});
317 dest.
add(std::move(f));
320 r.id() == ID_side_effect &&
328 dest.
add(std::move(f));
330 else if(
r.id() == ID_plus)
334 {this_va_list_expr});
348 if(next!=upper_bound &&
351 const exprt &n_r = next->get_assign().rhs();
353 n_r.
id() == ID_dereference &&
356 f.lhs() = next->get_assign().lhs();
358 type_of.arguments().push_back(f.lhs());
359 f.arguments().push_back(type_of);
361 dest.
add(std::move(f));
367 assert(
r.find(ID_C_va_arg_type).is_not_nil());
368 const typet &va_arg_type=
369 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
375 type_of.arguments().push_back(deref);
376 f.arguments().push_back(type_of);
380 dest.
add(std::move(void_f));
386 {this_va_list_expr,
r});
388 dest.
add(std::move(f));
398 if(assign.
rhs().
id()==ID_array)
423 target->return_value().id() != ID_side_effect ||
435 while(next!=upper_bound && next->is_dead() && !next->is_target())
438 if(next!=upper_bound &&
462 upper_bound->location_number > entry->second);
466 if(next!=upper_bound &&
468 !next->is_target() &&
469 (next->is_assign() || next->is_function_call()))
471 exprt lhs = next->is_assign() ? next->get_assign().lhs()
472 : next->get_function_call().lhs();
476 if(next->is_assign())
501 dest.
add(std::move(d));
513 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
522 for( ; target!=loop_end; ++target)
529 dest.
add(std::move(d));
538 assert(target->is_goto());
540 assert(target->targets.size()==1);
546 upper_bound->location_number > loop_entry->second->location_number))
548 else if(!target->guard.is_true())
561 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
573 if(target->get_target()==after_loop)
578 else if(target->guard.is_true())
589 for(++target; target!=loop_end; ++target)
595 if(loop_end->guard.is_false())
599 else if(!loop_end->guard.is_true())
609 if(w.body().has_operands() &&
613 w.body().operands().pop_back();
614 increment.
id(ID_side_effect);
622 else if(w.body().has_operands() &&
632 w.body().operands().pop_back();
641 dest.
add(std::move(w));
649 const exprt &switch_var,
655 std::set<goto_programt::const_targett> unique_targets;
659 cases_it!=upper_bound && cases_it!=first_target;
662 if(cases_it->is_goto() &&
663 !cases_it->is_backwards_goto() &&
664 cases_it->guard.is_true())
666 default_target=cases_it->get_target();
669 first_target->location_number > default_target->location_number)
670 first_target=default_target;
672 last_target->location_number < default_target->location_number)
673 last_target=default_target;
675 cases.push_back(
caset(
680 unique_targets.insert(default_target);
685 else if(cases_it->is_goto() &&
686 !cases_it->is_backwards_goto() &&
687 (cases_it->guard.id()==ID_equal ||
688 cases_it->guard.id()==ID_or))
691 if(cases_it->guard.id()==ID_equal)
692 eqs.push_back(cases_it->guard);
694 eqs=cases_it->guard.operands();
698 for(exprt::operandst::const_reverse_iterator
700 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
703 if(e_it->id()!=ID_equal ||
708 cases.push_back(
caset(
712 cases_it->get_target()));
713 assert(cases.back().value.is_not_nil());
716 first_target->location_number>
717 cases.back().case_start->location_number)
718 first_target=cases.back().case_start;
720 last_target->location_number<
721 cases.back().case_start->location_number)
722 last_target=cases.back().case_start;
724 unique_targets.insert(cases.back().case_start);
733 if(unique_targets.size()<3)
737 if(cases_it==upper_bound ||
739 upper_bound->location_number < last_target->location_number) ||
741 last_target->location_number > default_target->location_number) ||
742 target->get_target()==default_target)
752 std::set<unsigned> &processed_locations)
754 std::set<goto_programt::const_targett> targets_done;
756 for(cases_listt::iterator it=cases.begin();
762 if(!targets_done.insert(it->case_start).second)
769 case_end!=upper_bound;
772 const auto &case_end_node = dominators.
get_node(case_end);
779 if(case_end==it->case_start)
786 if(!dominators.
dominates(it->case_start, case_end_node))
789 if(!processed_locations.insert(case_end->location_number).second)
792 it->case_last=case_end;
804 for(cases_listt::const_iterator it=cases.begin();
813 cases_listt::const_iterator last=--cases.end();
814 if(last->case_start==default_target &&
829 next_case == default_target &&
830 (!it->case_last->is_goto() ||
831 (it->case_last->get_condition().is_true() &&
832 it->case_last->get_target() == default_target)))
841 if(it->case_last->is_goto() &&
842 it->case_last->guard.is_true() &&
843 it->case_last->get_target()==default_target)
847 if(!it->case_last->is_goto())
862 exprt eq_cand=target->guard;
863 if(eq_cand.
id()==ID_or)
866 if(target->is_backwards_goto() ||
867 eq_cand.
id()!=ID_equal ||
899 if(cases_start==target)
907 for(target=cases_start; target!=first_target; ++target)
910 std::set<unsigned> processed_locations;
929 for(cases_listt::const_iterator it=cases.begin();
933 it->case_last->location_number > max_target->location_number)
934 max_target=it->case_last;
936 std::map<goto_programt::const_targett, unsigned> targets_done;
941 for(cases_listt::const_iterator it=cases.begin();
947 if(it->value.is_nil())
950 csc.case_op()=it->value;
954 if(targets_done.find(it->case_start)!=targets_done.end())
956 assert(it->case_selector==orig_target ||
957 !it->case_selector->is_target());
965 csc.code().swap(cscp->
code());
972 if(it->case_selector!=orig_target)
976 target=it->case_start;
983 if(it->case_start!=(--cases.end())->case_start)
997 for( ; target!=after_last; ++target)
1002 targets_done[it->case_start]=s.
body().
operands().size();
1012 if(processed_locations.find(it->location_number)==
1013 processed_locations.end())
1022 dest.
add(std::move(s));
1035 bool has_else=
false;
1037 if(!target->is_backwards_goto())
1044 if(before_else==target)
1051 before_else->is_goto() &&
1052 before_else->get_target()->location_number > end_if->location_number &&
1053 before_else->guard.is_true() &&
1055 upper_bound->location_number>=
1056 before_else->get_target()->location_number);
1059 end_if=before_else->get_target();
1063 if(target->is_backwards_goto() ||
1065 upper_bound->location_number < end_if->location_number))
1082 for(++target; target!=before_else; ++target)
1088 for(++target; target!=end_if; ++target)
1094 for(++target; target!=end_if; ++target)
1099 dest.
add(std::move(i));
1122 if(target->get_target()==next)
1131 if(target->get_target()==loop_end &&
1142 dest.
add(std::move(i));
1156 if(target->get_target()==after_loop)
1166 dest.
add(std::move(i));
1181 if(target->get_target()==next)
1191 std::stringstream label;
1193 for(goto_programt::instructiont::labelst::const_iterator
1194 it=target->get_target()->labels.begin();
1195 it!=target->get_target()->labels.end();
1209 if(label.str().empty())
1210 label <<
CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1224 dest.
add(std::move(i));
1234 assert(target->is_start_thread());
1237 assert(thread_start->location_number > target->location_number);
1248 if(!next->is_goto())
1252 assert(this_end->is_end_thread());
1253 assert(thread_start->location_number > this_end->location_number);
1258 for(goto_programt::instructiont::labelst::const_iterator
1259 it=target->labels.begin();
1260 it!=target->labels.end();
1272 dest.
add(std::move(b));
1283 assert(next->is_goto() && next->guard.is_true());
1284 assert(!next->is_backwards_goto());
1285 assert(thread_start->location_number < next->get_target()->location_number);
1287 ++after_thread_start;
1291 assert(thread_start->location_number < thread_end->location_number);
1292 assert(thread_end->is_end_thread());
1295 thread_end->location_number < upper_bound->location_number);
1301 thread_start->is_function_call() &&
1302 thread_start->get_function_call().arguments().size() == 1 &&
1303 after_thread_start == thread_end)
1319 for( ; thread_start!=thread_end; ++thread_start)
1323 for(goto_programt::instructiont::labelst::const_iterator
1324 it=target->labels.begin();
1325 it!=target->labels.end();
1337 dest.
add(std::move(b));
1362 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1379 else if(type.
id()==ID_c_enum_tag)
1388 assert(!identifier.
empty());
1391 else if(type.
id()==ID_pointer ||
1392 type.
id()==ID_array)
1405 code.
op1().
id()==ID_side_effect &&
1424 if(!typedef_str.
empty() &&
1437 call.
lhs().
id()==ID_typecast)
1445 if(op.id() == ID_code)
1453 if(statement==ID_label)
1458 assert(!label.
empty());
1466 else if(statement==ID_block)
1468 else if(statement==ID_ifthenelse)
1470 else if(statement==ID_dowhile)
1481 code=do_while.
body();
1486 const exprt &
function,
1489 if(
function.
id()!=ID_symbol)
1502 if(parameters.size()==arguments.size())
1504 code_typet::parameterst::const_iterator it=parameters.begin();
1505 for(
auto &argument : arguments)
1508 argument.type().id() == ID_union ||
1509 argument.type().id() == ID_union_tag)
1511 argument.type() = it->type();
1527 operands.size()>1 && i<operands.size();
1530 exprt::operandst::iterator it=operands.begin()+i;
1533 it->source_location().get_comment().
empty())
1538 bool has_decl=
false;
1548 operands.insert(operands.begin()+i+1,
1549 it->operands().begin(), it->operands().end());
1550 operands.erase(operands.begin()+i);
1560 if(operands.empty() && parent_stmt!=ID_nil)
1562 else if(operands.size()==1 &&
1563 parent_stmt!=ID_nil &&
1574 type.
remove(ID_C_constant);
1576 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1585 "Symbol "+
id2string(identifier)+
" should be a type");
1589 else if(type.
id()==ID_array)
1591 else if(type.
id()==ID_struct ||
1592 type.
id()==ID_union)
1597 for(struct_union_typet::componentst::iterator
1603 else if(type.
id() == ID_c_bit_field)
1621 if(expr.
is_nil() ||
to_code(expr).get_statement() != ID_block)
1627 block.
statements().back().get_statement() != ID_label)
1708 code =
code_blockt({i_t_e, then_label, else_label});
1741 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1746 else if(!no_typecast &&
1747 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1748 expr.
id()==ID_array || expr.
id()==ID_vector))
1761 expr.
id() == ID_union && expr.
type().
id() != ID_union &&
1762 expr.
type().
id() != ID_union_tag)
1768 if(expr.
id()==ID_typecast &&
1772 if(expr.
id()==ID_union ||
1773 expr.
id()==ID_struct)
1779 expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag,
1780 "union/struct expressions should have a tag type");
1788 if(!typedef_str.
empty() &&
1792 else if(expr.
id()==ID_array ||
1793 expr.
id()==ID_vector)
1796 expr.
get_bool(ID_C_string_constant))
1805 if(!typedef_str.
empty() &&
1809 else if(expr.
id()==ID_side_effect)
1813 if(statement==ID_nondet)
1820 for(symbol_tablet::symbolst::const_iterator
1825 if(it->second.type.id()!=ID_code)
1847 suffix=expr.
type().
get(ID_C_c_type);
1854 if(base_name.
empty())
1865 symbol.
name=base_name;
1883 else if(expr.
id()==ID_isnan ||
1886 else if(expr.
id()==ID_constant)
1888 if(expr.
type().
id()==ID_floatbv)
1894 else if(expr.
type().
id()==ID_pointer)
1897 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
1902 else if(expr.
id()==ID_typecast)
1904 if(expr.
type().
id() == ID_c_bit_field)
1911 if(!typedef_str.
empty() &&
1915 assert(expr.
type().
id()!=ID_union &&
1916 expr.
type().
id()!=ID_struct);
1919 else if(expr.
id()==ID_symbol)
1921 if(expr.
type().
id()!=ID_code)
1927 symbol.
type.
id()!=ID_code &&
1948 if(src->get_code().source_location().is_not_nil())
1950 else if(src->source_location.is_not_nil())