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=
true;
150 if(label_stack.size()>goto_stack.size())
151 stack_is_prefix=
false;
152 for(std::size_t i=0, ilim=label_stack.size();
153 i!=ilim && stack_is_prefix;
156 if(goto_stack[i]!=label_stack[i])
157 stack_is_prefix=
false;
163 debug() <<
"encountered goto `" << goto_label
164 <<
"' that enters one or more lexical blocks; " 165 <<
"omitting constructors and destructors" <<
eom;
169 auto unwind_to_size=label_stack.size();
170 if(unwind_to_size<goto_stack.size())
173 debug() <<
"adding goto-destructor code on jump to `" 174 << goto_label <<
"'" <<
eom;
191 error() <<
"finish_gotos: unexpected goto" <<
eom;
206 assert(destination.
id()==ID_dereference);
207 assert(destination.
operands().size()==1);
219 label_expr.
set(ID_identifier, label.first);
226 t->make_goto(label.second.first);
251 i.get_target()->target_number = (++cnt);
258 auto it_goto_y = std::next(it);
261 it_goto_y == dest.
instructions.end() || !it_goto_y->is_goto() ||
262 !it_goto_y->guard.is_true() || it_goto_y->is_target())
265 auto it_z = std::next(it_goto_y);
271 if(it->get_target()->target_number == it_z->target_number)
273 it->set_target(it_goto_y->get_target());
275 it_goto_y->make_skip();
319 error() <<
"label statement expected to have one operand" <<
eom;
336 "op0 in magic thread creation label is null");
353 target->labels.push_front(label);
392 case_op_dest.push_back(code.
case_op());
404 error() <<
"GCC's switch-case-range statement expected to have " 405 <<
"three operands" <<
eom;
412 if(!lb.has_value() || !ub.has_value())
415 error() <<
"GCC's switch-case-range statement requires constant bounds" 422 warning() <<
"GCC's switch-case-range statement with empty case range" 454 if(statement==ID_block)
456 else if(statement==ID_decl)
458 else if(statement==ID_decl_type)
460 else if(statement==ID_expression)
462 else if(statement==ID_assign)
464 else if(statement==ID_init)
466 else if(statement==ID_assert)
468 else if(statement==ID_assume)
470 else if(statement==ID_function_call)
472 else if(statement==ID_label)
474 else if(statement==ID_gcc_local_label)
476 else if(statement==ID_switch_case)
478 else if(statement==ID_gcc_switch_case_range)
480 else if(statement==ID_for)
482 else if(statement==ID_while)
484 else if(statement==ID_dowhile)
486 else if(statement==ID_switch)
488 else if(statement==ID_break)
490 else if(statement==ID_return)
492 else if(statement==ID_continue)
494 else if(statement==ID_goto)
496 else if(statement==ID_gcc_computed_goto)
498 else if(statement==ID_skip)
500 else if(statement==ID_ifthenelse)
502 else if(statement==ID_start_thread)
504 else if(statement==ID_end_thread)
506 else if(statement==ID_atomic_begin)
508 else if(statement==ID_atomic_end)
510 else if(statement==ID_cpp_delete ||
511 statement==
"cpp_delete[]")
513 else if(statement==ID_msc_try_except)
515 else if(statement==ID_msc_try_finally)
517 else if(statement==ID_msc_leave)
519 else if(statement==ID_try_catch)
521 else if(statement==ID_CPROVER_try_catch)
523 else if(statement==ID_CPROVER_throw)
525 else if(statement==ID_CPROVER_try_finally)
527 else if(statement==ID_asm)
529 else if(statement==ID_static_assert)
535 if(assertion.is_false())
538 error() <<
"static assertion " 542 else if(assertion.is_true())
550 else if(statement==ID_dead)
552 else if(statement==ID_decl_block)
557 else if(statement==ID_push_catch ||
558 statement==ID_pop_catch ||
559 statement==ID_exception_landingpad)
613 error() <<
"expression statement takes one operand" <<
eom;
656 if(op.
id() != ID_symbol)
659 error() <<
"decl statement expects symbol as operand" <<
eom;
668 symbol.
type.
id()==ID_code)
681 initializer=code.
op1();
711 destructor.
arguments().push_back(this_expr);
734 if(rhs.id()==ID_side_effect &&
735 rhs.get(ID_statement)==ID_function_call)
737 if(rhs.operands().size()!=2)
740 error() <<
"function_call sideeffect takes two operands" <<
eom;
749 else if(rhs.id()==ID_side_effect &&
750 (rhs.get(ID_statement)==ID_cpp_new ||
751 rhs.get(ID_statement)==ID_cpp_new_array))
760 rhs.id() == ID_side_effect &&
761 (rhs.get(ID_statement) == ID_assign ||
762 rhs.get(ID_statement) == ID_postincrement ||
763 rhs.get(ID_statement) == ID_preincrement ||
764 rhs.get(ID_statement) == ID_statement_expression))
769 if(lhs.
id() == ID_typecast)
772 lhs.
operands().size() == 1,
"Typecast must have one operand");
784 new_assign.
lhs() = lhs;
785 new_assign.
rhs() = rhs;
789 else if(rhs.id() == ID_side_effect)
797 new_assign.
lhs()=lhs;
798 new_assign.
rhs()=rhs;
807 if(lhs.
id()==ID_typecast)
821 new_assign.
lhs()=lhs;
822 new_assign.
rhs()=rhs;
836 error() <<
"init statement takes two operands" <<
eom;
841 codet assignment=code;
854 error() <<
"cpp_delete statement takes one operand" <<
eom;
863 const exprt &destructor=
864 static_cast<const exprt &
>(code.
find(ID_destructor));
869 delete_identifier=
"__delete_array";
871 delete_identifier=
"__delete";
888 convert(tmp_code, dest, ID_cpp);
895 exprt delete_symbol=
ns.
lookup(delete_identifier).symbol_expr();
903 delete_call.
function()=delete_symbol;
908 convert(delete_call, dest, ID_cpp);
923 t->source_location.
set(ID_property, ID_assertion);
924 t->source_location.set(
"user-provided",
true);
956 static_cast<const exprt&
>(code.
find(ID_C_spec_loop_invariant));
966 error() <<
"loop invariant is not side-effect free" <<
eom;
970 assert(loop->is_goto());
971 loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
1097 z->source_location=source_location;
1143 error() <<
"dowhile takes two operands" <<
eom;
1218 eq_expr.
lhs()=value;
1281 z->source_location=body_end_location;
1306 size_t case_number=1;
1309 const caset &case_ops=case_pair.second;
1311 assert(!case_ops.empty());
1318 guard_expr.add_source_location()=source_location;
1321 x->make_goto(case_pair.first);
1322 x->guard.
swap(guard_expr);
1323 x->source_location=source_location;
1349 error() <<
"break without target" <<
eom;
1371 error() <<
"return without target" <<
eom;
1379 error() <<
"return takes none or one operand" <<
eom;
1387 bool result_is_used=
1404 error() <<
"function must return value" <<
eom;
1420 error() <<
"function must not return value" <<
eom;
1442 error() <<
"continue without target" <<
eom;
1460 t->make_incomplete_goto(code);
1487 start_thread->code=code;
1501 error() <<
"end_thread expects no operands" <<
eom;
1515 error() <<
"atomic_begin expects no operands" <<
eom;
1529 error() <<
"atomic_end expects no operands" <<
eom;
1544 error() <<
"ifthenelse takes three operands" <<
eom;
1557 if(code.
cond().
id()==ID_and &&
1586 tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1592 std::list<exprt> &dest)
1596 dest.push_back(expr);
1632 v->make_goto(z, guard);
1633 v->source_location=source_location;
1701 bool has_else=!
is_empty(false_case);
1733 tmp_y.
swap(false_case);
1740 boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1744 tmp_w.
swap(true_case);
1749 x->source_location=tmp_w.
instructions.back().source_location;
1770 if(expr.
id()==ID_and || expr.
id()==ID_or)
1792 target_false->make_skip();
1793 target_false->source_location=source_location;
1796 guard, target_true, target_false, source_location, dest, mode);
1808 g->make_goto(target_true);
1824 if(guard.
id()==ID_not)
1826 assert(guard.
operands().size()==1);
1829 guard.
op0(), target_false, target_true, source_location, dest, mode);
1833 if(guard.
id()==ID_and)
1842 std::list<exprt> op;
1845 for(
const auto &expr : op)
1847 boolean_negate(expr), target_false, source_location, dest, mode);
1850 t_true->make_goto(target_true);
1852 t_true->source_location=source_location;
1856 else if(guard.
id()==ID_or)
1865 std::list<exprt> op;
1868 for(
const auto &expr : op)
1870 expr, target_true, source_location, dest, mode);
1873 t_false->make_goto(target_false);
1884 t_true->make_goto(target_true);
1889 t_false->make_goto(target_false);
1891 t_false->source_location=source_location;
1898 if(expr.
id()==ID_typecast &&
1902 if(expr.
id()==ID_address_of &&
1904 expr.
op0().
id()==ID_index &&
1910 if(index_op.
id()==ID_string_constant)
1911 return value=index_op.
get(ID_value),
false;
1912 else if(index_op.
id()==ID_array)
1916 if(it->is_constant())
1922 result+=
static_cast<char>(i);
1925 return value=
result,
false;
1929 if(expr.
id()==ID_string_constant)
1930 return value=expr.
get(ID_value),
false;
1942 error() <<
"expected string constant, but got: " 1953 if(expr.
id()==ID_symbol)
1958 return symbol.
value;
1960 else if(expr.
id()==ID_member)
1966 else if(expr.
id()==ID_index)
1979 const std::string &suffix,
1994 decl.
symbol()=new_symbol.symbol_expr();
2003 const std::string &suffix,
2014 assignment.rhs()=expr;
2017 convert(assignment, dest, mode);
2029 const std::size_t errors_before=
2044 catch(
const char *e)
2049 catch(
const std::string &e)
2064 const symbol_tablet::symbolst::const_iterator s_it=
2065 symbol_table.
symbols.find(
"main");
2067 if(s_it==symbol_table.
symbols.end())
2068 throw "failed to find main symbol";
2070 const symbolt &symbol=s_it->second;
2098 convert(thread_body, body, mode);
2107 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)
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;