44 std::map<irep_idt, goto_programt::targett> label_targets;
49 if(!it->labels.empty())
51 for(
auto label : it->labels)
53 label_targets.insert(std::make_pair(label, it));
60 if(it->is_catch() && it->code.get_statement()==ID_push_catch)
67 if(it->targets.empty())
69 bool handler_added=
true;
73 for(
const auto &handler : handler_list)
77 if(label_targets.find(handler.get_label())==label_targets.end())
87 for(
const auto &handler : handler_list)
88 it->targets.push_back(label_targets.at(handler.get_label()));
116 labelst::const_iterator l_it=
122 error() <<
"goto label `" << goto_label <<
"' not found" <<
eom;
126 i.
targets.push_back(l_it->second.first);
132 labelst::const_iterator l_it=
targets.
labels.find(goto_label);
137 error() <<
"goto label `" << goto_label <<
"' not found" <<
eom;
147 auto goto_stack=g_it.second;
148 const auto &label_stack=l_it->second.second;
149 bool stack_is_prefix = label_stack.size() <= goto_stack.size();
151 std::size_t idx = 0, ilim = label_stack.size();
152 idx != ilim && stack_is_prefix; ++idx)
154 stack_is_prefix &= goto_stack[idx] == label_stack[idx];
160 debug() <<
"encountered goto `" << goto_label
161 <<
"' that enters one or more lexical blocks; " 162 <<
"omitting constructors and destructors" <<
eom;
166 auto unwind_to_size=label_stack.size();
167 if(unwind_to_size<goto_stack.size())
170 debug() <<
"adding goto-destructor code on jump to `" 171 << goto_label <<
"'" <<
eom;
188 error() <<
"finish_gotos: unexpected goto" <<
eom;
203 assert(destination.
id()==ID_dereference);
204 assert(destination.
operands().size()==1);
216 label_expr.
set(ID_identifier, label.first);
223 t->make_goto(label.second.first);
248 i.get_target()->target_number = (++cnt);
255 auto it_goto_y = std::next(it);
258 it_goto_y == dest.
instructions.end() || !it_goto_y->is_goto() ||
259 !it_goto_y->guard.is_true() || it_goto_y->is_target())
262 auto it_z = std::next(it_goto_y);
268 if(it->get_target()->target_number == it_z->target_number)
270 it->set_target(it_goto_y->get_target());
272 it_goto_y->make_skip();
316 error() <<
"label statement expected to have one operand" <<
eom;
333 "op0 in magic thread creation label is null");
350 target->labels.push_front(label);
389 case_op_dest.push_back(code.
case_op());
401 error() <<
"GCC's switch-case-range statement expected to have " 402 <<
"three operands" <<
eom;
409 if(!lb.has_value() || !ub.has_value())
412 error() <<
"GCC's switch-case-range statement requires constant bounds" 419 warning() <<
"GCC's switch-case-range statement with empty case range" 451 if(statement==ID_block)
453 else if(statement==ID_decl)
455 else if(statement==ID_decl_type)
457 else if(statement==ID_expression)
459 else if(statement==ID_assign)
461 else if(statement==ID_init)
463 else if(statement==ID_assert)
465 else if(statement==ID_assume)
467 else if(statement==ID_function_call)
469 else if(statement==ID_label)
471 else if(statement==ID_gcc_local_label)
473 else if(statement==ID_switch_case)
475 else if(statement==ID_gcc_switch_case_range)
477 else if(statement==ID_for)
479 else if(statement==ID_while)
481 else if(statement==ID_dowhile)
483 else if(statement==ID_switch)
485 else if(statement==ID_break)
487 else if(statement==ID_return)
489 else if(statement==ID_continue)
491 else if(statement==ID_goto)
493 else if(statement==ID_gcc_computed_goto)
495 else if(statement==ID_skip)
497 else if(statement==ID_ifthenelse)
499 else if(statement==ID_start_thread)
501 else if(statement==ID_end_thread)
503 else if(statement==ID_atomic_begin)
505 else if(statement==ID_atomic_end)
507 else if(statement==ID_cpp_delete ||
508 statement==
"cpp_delete[]")
510 else if(statement==ID_msc_try_except)
512 else if(statement==ID_msc_try_finally)
514 else if(statement==ID_msc_leave)
516 else if(statement==ID_try_catch)
518 else if(statement==ID_CPROVER_try_catch)
520 else if(statement==ID_CPROVER_throw)
522 else if(statement==ID_CPROVER_try_finally)
524 else if(statement==ID_asm)
526 else if(statement==ID_static_assert)
532 if(assertion.is_false())
535 error() <<
"static assertion " 539 else if(assertion.is_true())
547 else if(statement==ID_dead)
549 else if(statement==ID_decl_block)
554 else if(statement==ID_push_catch ||
555 statement==ID_pop_catch ||
556 statement==ID_exception_landingpad)
610 error() <<
"expression statement takes one operand" <<
eom;
653 if(op.
id() != ID_symbol)
656 error() <<
"decl statement expects symbol as operand" <<
eom;
665 symbol.
type.
id()==ID_code)
678 initializer=code.
op1();
708 destructor.
arguments().push_back(this_expr);
731 if(rhs.id()==ID_side_effect &&
732 rhs.get(ID_statement)==ID_function_call)
734 if(rhs.operands().size()!=2)
737 error() <<
"function_call sideeffect takes two operands" <<
eom;
746 else if(rhs.id()==ID_side_effect &&
747 (rhs.get(ID_statement)==ID_cpp_new ||
748 rhs.get(ID_statement)==ID_cpp_new_array))
757 rhs.id() == ID_side_effect &&
758 (rhs.get(ID_statement) == ID_assign ||
759 rhs.get(ID_statement) == ID_postincrement ||
760 rhs.get(ID_statement) == ID_preincrement ||
761 rhs.get(ID_statement) == ID_statement_expression ||
762 rhs.get(ID_statement) == ID_gcc_conditional_expression))
767 if(lhs.
id() == ID_typecast)
770 lhs.
operands().size() == 1,
"Typecast must have one operand");
782 new_assign.
lhs() = lhs;
783 new_assign.
rhs() = rhs;
787 else if(rhs.id() == ID_side_effect)
795 new_assign.
lhs()=lhs;
796 new_assign.
rhs()=rhs;
805 if(lhs.
id()==ID_typecast)
819 new_assign.
lhs()=lhs;
820 new_assign.
rhs()=rhs;
834 error() <<
"init statement takes two operands" <<
eom;
839 codet assignment=code;
852 error() <<
"cpp_delete statement takes one operand" <<
eom;
861 const exprt &destructor=
862 static_cast<const exprt &
>(code.
find(ID_destructor));
867 delete_identifier=
"__delete_array";
869 delete_identifier=
"__delete";
886 convert(tmp_code, dest, ID_cpp);
893 exprt delete_symbol=
ns.
lookup(delete_identifier).symbol_expr();
901 delete_call.
function()=delete_symbol;
906 convert(delete_call, dest, ID_cpp);
921 t->source_location.
set(ID_property, ID_assertion);
922 t->source_location.set(
"user-provided",
true);
954 static_cast<const exprt&
>(code.
find(ID_C_spec_loop_invariant));
964 error() <<
"loop invariant is not side-effect free" <<
eom;
968 assert(loop->is_goto());
969 loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
1095 z->source_location=source_location;
1141 error() <<
"dowhile takes two operands" <<
eom;
1216 eq_expr.
lhs()=value;
1279 z->source_location=body_end_location;
1304 size_t case_number=1;
1307 const caset &case_ops=case_pair.second;
1309 assert(!case_ops.empty());
1316 guard_expr.add_source_location()=source_location;
1319 x->make_goto(case_pair.first);
1320 x->guard.
swap(guard_expr);
1321 x->source_location=source_location;
1347 error() <<
"break without target" <<
eom;
1369 error() <<
"return without target" <<
eom;
1377 error() <<
"return takes none or one operand" <<
eom;
1385 bool result_is_used=
1402 error() <<
"function must return value" <<
eom;
1418 error() <<
"function must not return value" <<
eom;
1440 error() <<
"continue without target" <<
eom;
1458 t->make_incomplete_goto(code);
1485 start_thread->code=code;
1499 error() <<
"end_thread expects no operands" <<
eom;
1513 error() <<
"atomic_begin expects no operands" <<
eom;
1527 error() <<
"atomic_end expects no operands" <<
eom;
1542 error() <<
"ifthenelse takes three operands" <<
eom;
1555 if(code.
cond().
id()==ID_and &&
1584 tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1590 std::list<exprt> &dest)
1594 dest.push_back(expr);
1630 v->make_goto(z, guard);
1631 v->source_location=source_location;
1699 bool has_else=!
is_empty(false_case);
1731 tmp_y.
swap(false_case);
1738 boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1742 tmp_w.
swap(true_case);
1747 x->source_location=tmp_w.
instructions.back().source_location;
1768 if(expr.
id()==ID_and || expr.
id()==ID_or)
1790 target_false->make_skip();
1791 target_false->source_location=source_location;
1794 guard, target_true, target_false, source_location, dest, mode);
1806 g->make_goto(target_true);
1822 if(guard.
id()==ID_not)
1824 assert(guard.
operands().size()==1);
1827 guard.
op0(), target_false, target_true, source_location, dest, mode);
1831 if(guard.
id()==ID_and)
1840 std::list<exprt> op;
1843 for(
const auto &expr : op)
1845 boolean_negate(expr), target_false, source_location, dest, mode);
1848 t_true->make_goto(target_true);
1850 t_true->source_location=source_location;
1854 else if(guard.
id()==ID_or)
1863 std::list<exprt> op;
1866 for(
const auto &expr : op)
1868 expr, target_true, source_location, dest, mode);
1871 t_false->make_goto(target_false);
1882 t_true->make_goto(target_true);
1887 t_false->make_goto(target_false);
1889 t_false->source_location=source_location;
1896 if(expr.
id()==ID_typecast &&
1900 if(expr.
id()==ID_address_of &&
1902 expr.
op0().
id()==ID_index &&
1908 if(index_op.
id()==ID_string_constant)
1909 return value=index_op.
get(ID_value),
false;
1910 else if(index_op.
id()==ID_array)
1914 if(it->is_constant())
1920 result+=
static_cast<char>(i);
1923 return value=
result,
false;
1927 if(expr.
id()==ID_string_constant)
1928 return value=expr.
get(ID_value),
false;
1940 error() <<
"expected string constant, but got: " 1951 if(expr.
id()==ID_symbol)
1956 return symbol.
value;
1958 else if(expr.
id()==ID_member)
1964 else if(expr.
id()==ID_index)
1977 const std::string &suffix,
2000 const std::string &suffix,
2011 assignment.rhs()=expr;
2014 convert(assignment, dest, mode);
2026 const std::size_t errors_before=
2041 catch(
const char *e)
2046 catch(
const std::string &e)
2061 const symbol_tablet::symbolst::const_iterator s_it=
2062 symbol_table.
symbols.find(
"main");
2064 if(s_it==symbol_table.
symbols.end())
2065 throw "failed to find main symbol";
2067 const symbolt &symbol=s_it->second;
2095 convert(thread_body, body, mode);
2104 a->targets.push_back(c);
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void convert_atomic_begin(const codet &code, goto_programt &dest)
const irep_idt & get_statement() const
static bool is_empty(const goto_programt &goto_program)
The type of an expression.
irep_idt get_string_constant(const exprt &expr)
irep_idt name
The unique identifier.
void convert_skip(const codet &code, goto_programt &dest)
const codet & then_case() const
const exprt & return_value() const
const code_declt & to_code_decl(const codet &code)
std::vector< exception_list_entryt > exception_listt
void set_case_number(const irep_idt &number)
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest, const irep_idt &mode)
const std::string & id2string(const irep_idt &d)
void restore(targetst &targets)
pointer_typet pointer_type(const typet &subtype)
const exprt & init() const
bool is_skip(const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
Determine whether the instruction is semantically equivalent to a skip (no-op).
goto_programt::targett return_target
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const code_assumet & to_code_assume(const codet &code)
const exprt & cond() const
A continue for ‘for’ and ‘while’ loops.
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
struct goto_convertt::targetst targets
static void finish_catch_push_targets(goto_programt &dest)
Populate the CATCH instructions with the targets corresponding to their associated labels...
irep_idt mode
Language mode.
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
const exprt & cond() const
goto_program_instruction_typet type
What kind of instruction?
mp_integer::ullong_t integer2ulong(const mp_integer &n)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
const codet & body() const
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Deprecated expression utility functions.
goto_programt::targett break_target
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
source_locationt end_location() const
#define forall_expr(it, expr)
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void move_to_operands(exprt &expr)
Fresh auxiliary symbol creation.
void convert_atomic_end(const codet &code, goto_programt &dest)
const irep_idt & get_value() const
const code_breakt & to_code_break(const codet &code)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
exprt value
Initial value of symbol.
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
The trinary if-then-else operator.
void restore(targetst &targets)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void convert_end_thread(const codet &code, goto_programt &dest)
static const unsigned nil_target
Uniquely identify an invalid target or location.
static mstreamt & eom(mstreamt &m)
void convert_dowhile(const codet &code, goto_programt &dest, const irep_idt &mode)
code_expressiont & to_code_expression(codet &code)
void set_default(goto_programt::targett _default_target)
#define INVARIANT(CONDITION, REASON)
const exprt & case_op() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
targetst targets
The list of successor instructions.
mstreamt & warning() const
This class represents an instruction in the GOTO intermediate representation.
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
destructor_stackt destructor_stack
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
std::size_t continue_stack_size
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
const code_assignt & to_code_assign(const codet &code)
void convert_loop_invariant(const codet &code, goto_programt::targett loop, const irep_idt &mode)
const irep_idt & id() const
void convert_decl_type(const codet &code, goto_programt &dest)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
std::string tmp_symbol_prefix
instructionst::iterator targett
A declaration of a local variable.
static code_push_catcht & to_code_push_catch(codet &code)
void complete_goto(targett _target)
const source_locationt & find_source_location() const
const exprt & cond() const
source_locationt source_location
Operator to dereference a pointer.
const code_whilet & to_code_while(const codet &code)
void convert_init(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
goto_programt::targett default_target
exprt case_guard(const exprt &value, const caset &case_op)
const code_gotot & to_code_goto(const codet &code)
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
A label for branch targets.
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
#define PRECONDITION(CONDITION)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
targett insert_after(const_targett target)
Insertion after the given target.
const code_returnt & to_code_return(const codet &code)
bool has_prefix(const std::string &s, const std::string &prefix)
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
const code_switch_caset & to_code_switch_case(const codet &code)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
void convert_asm(const code_asmt &code, goto_programt &dest)
void finish_computed_gotos(goto_programt &dest)
Operator to return the address of an object.
void convert_cpp_delete(const codet &code, goto_programt &dest)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const codet & body() const
void generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
Generates the necessary goto-instructions to represent a thread-block.
const code_switcht & to_code_switch(const codet &code)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
bool has_return_value() const
std::vector< exprt > operandst
void swap(goto_programt &program)
Swap the goto program.
A generic container class for the GOTO intermediate representation of one function.
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
A non-fatal assertion, which checks a condition then permits execution to continue.
An assumption, which must hold in subsequent code.
exprt get_constant(const exprt &expr)
void set_continue(goto_programt::targett _continue_target)
const exprt & value() const
typet type
Type of symbol.
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
const code_continuet & to_code_continue(const codet &code)
static bool needs_cleaning(const exprt &expr)
goto_programt::targett continue_target
void optimize_guarded_gotos(goto_programt &dest)
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a bra...
mstreamt & result() const
void set_break(goto_programt::targett _break_target)
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
source_locationt source_location
The location of the instruction in the source file.
void set_statement(const irep_idt &statement)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
A break for ‘for’ and ‘while’ loops.
The symbol table base class interface.
const exprt & assumption() const
computed_gotost computed_gotos
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
bool empty() const
Is the program empty?
const exprt & iter() const
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
std::size_t break_stack_size
symbol_table_baset & symbol_table
A removal of a local variable.
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
#define Forall_operands(it, expr)
goto_programt & goto_program
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
source_locationt & add_source_location()
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
const code_fort & to_code_for(const codet &code)
Expression to hold a symbol (variable)
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
const code_blockt & to_code_block(const codet &code)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
code_function_callt get_destructor(const namespacet &ns, const typet &type)
const code_labelt & to_code_label(const codet &code)
bool is_start_thread() const
#define DATA_INVARIANT(CONDITION, REASON)
const code_assertt & to_code_assert(const codet &code)
void convert_start_thread(const codet &code, goto_programt &dest)
#define forall_goto_program_instructions(it, program)
const codet & else_case() const
exception_listt & exception_list()
const code_ifthenelset & to_code_ifthenelse(const codet &code)
void make_typecast(const typet &_type)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
static void replace_new_object(const exprt &object, exprt &dest)
const codet & body() const
const irept & find(const irep_namet &name) const
static bool has_and_or(const exprt &expr)
if(guard) goto target;
code_asmt & to_code_asm(codet &code)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void convert_goto(const code_gotot &code, goto_programt &dest)
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
const exprt & assertion() const
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) goto target_true; else goto target_false;