34 !it->labels.empty() ||
45 std::map<irep_idt, goto_programt::targett> label_targets;
50 if(!it->labels.empty())
52 for(
auto label : it->labels)
54 label_targets.insert(std::make_pair(label, it));
63 bool handler_added=
true;
64 irept exceptions=it->code.
find(ID_exception_list);
67 it->code.has_operands())
68 exceptions=it->code.op0().
find(ID_exception_list);
72 if(!exception_list.empty())
77 it->code.has_operands())
78 handlers=it->code.op0().
find(ID_label);
83 for(
const auto &handler : handler_list)
85 if(label_targets.find(handler.id())==label_targets.end())
95 for(
const auto &handler : handler_list)
99 label_targets.find(handler.id());
100 assert(handler_it!=label_targets.end());
102 it->targets.push_back(handler_it->second);
125 goto_programt::instructiont &i=*(g_it.first);
127 if(i.code.get_statement()==
"non-deterministic-goto")
129 const irept &destinations=i.code.
find(
"destinations");
135 labelst::const_iterator l_it=
141 error() <<
"goto label `" << it->id() <<
"' not found" <<
eom;
145 i.targets.push_back(l_it->second.first);
148 else if(i.is_start_thread())
150 const irep_idt &goto_label=i.code.get(ID_destination);
152 labelst::const_iterator l_it=
158 error() <<
"goto label `" << goto_label <<
"' not found" <<
eom;
162 i.targets.push_back(l_it->second.first);
164 else if(i.code.get_statement()==ID_goto)
166 const irep_idt &goto_label=i.code.get(ID_destination);
168 labelst::const_iterator l_it=
targets.
labels.find(goto_label);
173 error() <<
"goto label `" << goto_label <<
"' not found" <<
eom;
178 i.targets.push_back(l_it->second.first);
184 auto goto_stack=g_it.second;
185 const auto &label_stack=l_it->second.second;
186 bool stack_is_prefix=
true;
187 if(label_stack.size()>goto_stack.size())
188 stack_is_prefix=
false;
189 for(
unsigned i=0, ilim=label_stack.size();
190 i!=ilim && stack_is_prefix;
193 if(goto_stack[i]!=label_stack[i])
194 stack_is_prefix=
false;
200 debug() <<
"encountered goto `" << goto_label
201 <<
"' that enters one or more lexical blocks; " 202 <<
"omitting constructors and destructors" <<
eom;
206 auto unwind_to_size=label_stack.size();
207 if(unwind_to_size<goto_stack.size())
210 debug() <<
"adding goto-destructor code on jump to `" 211 << goto_label <<
"'" <<
eom;
214 i.code.add_source_location(),
227 error() <<
"finish_gotos: unexpected goto" <<
eom;
239 goto_programt::instructiont &i=*g_it;
242 assert(destination.
id()==ID_dereference);
243 assert(destination.
operands().size()==1);
255 label_expr.
set(ID_identifier, label.first);
265 t->make_goto(label.second.first);
266 t->source_location=i.source_location;
282 bool destructor_present=
false;
283 for(
auto it=gg.ifiter;
284 it!=gg.gotoiter && !destructor_present;
287 if(!(it->is_goto() || it->is_skip()))
288 destructor_present=
true;
292 if(destructor_present)
297 gg.gotoiter->guard=gg.guard;
301 for(
auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it)
340 error() <<
"label statement expected to have one operand" <<
eom;
353 codet tmp_code(ID_start_thread);
365 target->labels.push_front(label);
382 error() <<
"switch-case statement expected to have two operands" 410 case_op_dest.push_back(code.
case_op());
421 error() <<
"GCC's switch-case-range statement expected to have " 422 <<
"three operands" <<
eom;
443 case_op_dest.push_back(code.case_op());
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==
"non-deterministic-goto")
502 else if(statement==ID_ifthenelse)
504 else if(statement==ID_specc_notify)
506 else if(statement==ID_specc_wait)
508 else if(statement==ID_specc_par)
510 else if(statement==ID_start_thread)
512 else if(statement==ID_end_thread)
514 else if(statement==ID_atomic_begin)
516 else if(statement==ID_atomic_end)
518 else if(statement==ID_bp_enforce)
520 else if(statement==ID_bp_abortif)
522 else if(statement==ID_cpp_delete ||
523 statement==
"cpp_delete[]")
525 else if(statement==ID_msc_try_except)
527 else if(statement==ID_msc_try_finally)
529 else if(statement==ID_msc_leave)
531 else if(statement==ID_try_catch)
533 else if(statement==ID_CPROVER_try_catch)
535 else if(statement==ID_CPROVER_throw)
537 else if(statement==ID_CPROVER_try_finally)
539 else if(statement==ID_asm)
541 else if(statement==ID_static_assert)
547 if(assertion.is_false())
550 error() <<
"static assertion " 554 else if(assertion.is_true())
562 else if(statement==ID_dead)
564 else if(statement==ID_decl_block)
619 error() <<
"expression statement takes one operand" <<
eom;
661 if(op0.
id()!=ID_symbol)
664 error() <<
"decl statement expects symbol as first operand" <<
eom;
673 symbol.
type.
id()==ID_code)
686 initializer=code.
op1();
716 destructor.
arguments().push_back(this_expr);
738 if(rhs.id()==ID_side_effect &&
739 rhs.get(ID_statement)==ID_function_call)
741 if(rhs.operands().size()!=2)
744 error() <<
"function_call sideeffect takes two operands" <<
eom;
753 else if(rhs.id()==ID_side_effect &&
754 (rhs.get(ID_statement)==ID_cpp_new ||
755 rhs.get(ID_statement)==ID_cpp_new_array))
762 else if(rhs.id()==ID_side_effect &&
763 rhs.get(ID_statement)==ID_java_new)
770 else if(rhs.id()==ID_side_effect &&
771 rhs.get(ID_statement)==ID_java_new_array)
778 else if(rhs.id()==ID_side_effect &&
779 rhs.get(ID_statement)==ID_malloc)
786 new_assign.
lhs()=lhs;
787 new_assign.
rhs()=rhs;
795 if(lhs.
id()==ID_typecast)
809 new_assign.
lhs()=lhs;
810 new_assign.
rhs()=rhs;
823 error() <<
"init statement takes two operands" <<
eom;
828 codet assignment=code;
841 error() <<
"cpp_delete statement takes one operand" <<
eom;
850 const exprt &destructor=
851 static_cast<const exprt &
>(code.
find(ID_destructor));
856 delete_identifier=
"__delete_array";
858 delete_identifier=
"__delete";
883 exprt delete_symbol=
ns.
lookup(delete_identifier).symbol_expr();
891 delete_call.
function()=delete_symbol;
910 t->source_location.
set(ID_property, ID_assertion);
911 t->source_location.set(
"user-provided",
true);
941 static_cast<const exprt&
>(code.
find(ID_C_spec_loop_invariant));
951 error() <<
"loop invariant is not side-effect free" <<
eom;
955 assert(loop->is_goto());
956 loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
1080 z->source_location=source_location;
1125 error() <<
"dowhile takes two operands" <<
eom;
1200 eq_expr.
lhs()=value;
1239 error() <<
"switch takes at least two operands" <<
eom;
1273 const caset &case_ops=case_pair.second;
1275 assert(!case_ops.empty());
1280 x->make_goto(case_pair.first);
1281 x->guard.swap(guard_expr);
1282 x->source_location=case_ops.front().find_source_location();
1307 error() <<
"break without target" <<
eom;
1328 error() <<
"return without target" <<
eom;
1336 error() <<
"return takes none or one operand" <<
eom;
1344 bool result_is_used=
1361 error() <<
"function must return value" <<
eom;
1377 error() <<
"function must not return value" <<
eom;
1398 error() <<
"continue without target" <<
eom;
1464 std::set<irep_idt> &events)
1466 if(op.
id()==ID_or || op.
id()==ID_and)
1471 else if(op.
id()==ID_specc_event)
1476 event=std::string(
id2string(event), 7, std::string::npos);
1478 events.insert(event);
1483 error() <<
"convert_convert_event got " << op.
id() <<
eom;
1498 error() <<
"specc_wait expects one operand" <<
eom;
1505 t->or_semantics=
true;
1530 error() <<
"start_thread expects one operand" <<
eom;
1555 start_thread->targets.push_back(tmp.
instructions.begin());
1569 error() <<
"end_thread expects no operands" <<
eom;
1583 error() <<
"atomic_begin expects no operands" <<
eom;
1597 error() <<
"atomic_end expects no operands" <<
eom;
1611 error() <<
"bp_enfroce expects two arguments" <<
eom;
1631 exprt constraint(op);
1638 assert(it->code.get(ID_statement)==ID_assign);
1641 codet constrain(ID_bp_constrain);
1642 constrain.reserve_operands(2);
1643 constrain.move_to_operands(it->code);
1644 constrain.copy_to_operands(constraint);
1645 it->code.swap(constrain);
1649 else if(it->is_other() &&
1650 it->code.get(ID_statement)==ID_bp_constrain)
1653 assert(it->code.operands().size()==2);
1670 error() <<
"bp_abortif expects one argument" <<
eom;
1693 error() <<
"ifthenelse takes three operands" <<
eom;
1706 if(code.
cond().
id()==ID_and &&
1740 std::list<exprt> &dest)
1744 dest.push_back(expr);
1779 v->make_goto(z, guard);
1780 v->source_location=source_location;
1785 bool is_guarded_goto=
false;
1799 is_guarded_goto=
true;
1831 boolean_negate(guard), false_case, true_case, source_location, dest);
1833 bool has_else=!
is_empty(false_case);
1865 tmp_y.
swap(false_case);
1876 tmp_w.
swap(true_case);
1881 x->source_location=tmp_w.
instructions.back().source_location;
1911 if(expr.
id()==ID_and || expr.
id()==ID_or)
1932 target_false->make_skip();
1933 target_false->source_location=source_location;
1936 guard, target_true, target_false, source_location, dest);
1948 g->make_goto(target_true);
1963 if(guard.
id()==ID_not)
1965 assert(guard.
operands().size()==1);
1968 guard.
op0(), target_false, target_true, source_location, dest);
1972 if(guard.
id()==ID_and)
1981 std::list<exprt> op;
1989 t_true->make_goto(target_true);
1991 t_true->source_location=source_location;
1995 else if(guard.
id()==ID_or)
2004 std::list<exprt> op;
2009 *it, target_true, source_location, dest);
2012 t_false->make_goto(target_false);
2023 t_true->make_goto(target_true);
2028 t_false->make_goto(target_false);
2030 t_false->source_location=source_location;
2037 if(expr.
id()==ID_typecast &&
2041 if(expr.
id()==ID_address_of &&
2043 expr.
op0().
id()==ID_index &&
2049 if(index_op.
id()==ID_string_constant)
2050 return value=index_op.
get(ID_value),
false;
2051 else if(index_op.
id()==ID_array)
2055 if(it->is_constant())
2061 result+=
static_cast<char>(i);
2064 return value=
result,
false;
2068 if(expr.
id()==ID_string_constant)
2069 return value=expr.
get(ID_value),
false;
2081 error() <<
"expected string constant, but got: " 2092 if(expr.
id()==ID_symbol)
2097 return symbol.
value;
2099 else if(expr.
id()==ID_member)
2105 else if(expr.
id()==ID_index)
2118 const std::string &suffix,
2141 const std::string &suffix,
2151 assignment.rhs()=expr;
2173 error() <<
"failed to find symbol " << identifier <<
eom;
2185 const unsigned errors_before=
2197 goto_convert.
error();
2200 catch(
const char *e)
2205 catch(
const std::string &e)
2220 const symbol_tablet::symbolst::const_iterator s_it=
2221 symbol_table.
symbols.find(
"main");
2223 if(s_it==symbol_table.
symbols.end())
2224 throw "failed to find main symbol";
2226 const symbolt &symbol=s_it->second;
void convert_atomic_begin(const codet &code, goto_programt &dest)
const irep_idt & get_statement() const
void convert_specc_event(const exprt &op, std::set< irep_idt > &events)
static bool is_empty(const goto_programt &goto_program)
The type of an expression.
irep_idt name
The unique identifier.
void convert_skip(const codet &code, goto_programt &dest)
const codet & then_case() const
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest)
const exprt & return_value() const
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const code_declt & to_code_decl(const codet &code)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
targett add_instruction()
Adds an instruction at the end.
A `switch' instruction.
const std::string & id2string(const irep_idt &d)
void convert(const codet &code, goto_programt &dest)
converts 'code' and appends the result to 'dest'
void restore(targetst &targets)
pointer_typet pointer_type(const typet &subtype)
const exprt & init() const
symbol_tablet & symbol_table
goto_programt::targett return_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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest)
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_ifthenelse(const code_ifthenelset &code, goto_programt &dest)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::vector< irept > subt
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...
const exprt & cond() const
mp_integer::ullong_t integer2ulong(const mp_integer &n)
guarded_gotost guarded_gotos
const codet & body() const
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
goto_programt::targett break_target
void copy_to_operands(const exprt &expr)
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)
void convert_assign(const code_assignt &code, goto_programt &dest)
void convert_dowhile(const codet &code, goto_programt &dest)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
exprt value
Initial value of symbol.
void convert_init(const codet &code, goto_programt &dest)
The trinary if-then-else operator.
void restore(targetst &targets)
bool empty() const
Is the program empty?
void convert_goto(const codet &code, goto_programt &dest)
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 mstreamt & eom(mstreamt &m)
code_expressiont & to_code_expression(codet &code)
void set_default(goto_programt::targett _default_target)
const exprt & case_op() const
void convert_specc_wait(const codet &code, goto_programt &dest)
side_effect_exprt & to_side_effect_expr(exprt &expr)
destructor_stackt destructor_stack
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
std::size_t continue_stack_size
const code_assignt & to_code_assign(const codet &code)
void goto_convert(const codet &code, goto_programt &dest)
const irep_idt & id() const
void convert_switch(const code_switcht &code, goto_programt &dest)
void convert_decl_type(const codet &code, goto_programt &dest)
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
irep_idt get_string_constant(const exprt &expr)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void make_next_state(exprt &expr)
void convert_bp_abortif(const codet &code, goto_programt &dest)
void convert_for(const code_fort &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_msc_try_finally(const codet &code, goto_programt &dest)
A declaration of a local variable.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void convert_label(const code_labelt &code, goto_programt &dest)
const source_locationt & find_source_location() const
const exprt & cond() const
source_locationt source_location
const code_whilet & to_code_while(const codet &code)
goto_programt::targett default_target
exprt case_guard(const exprt &value, const caset &case_op)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void convert_specc_notify(const codet &code, goto_programt &dest)
void convert_continue(const code_continuet &code, goto_programt &dest)
void convert_while(const code_whilet &code, goto_programt &dest)
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest)
A label for branch targets.
const code_returnt & to_code_return(const codet &code)
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
void convert_msc_leave(const codet &code, goto_programt &dest)
A `while' instruction.
const code_switch_caset & to_code_switch_case(const codet &code)
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void convert_asm(const code_asmt &code, goto_programt &dest)
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_specc_par(const codet &code, goto_programt &dest)
void finish_computed_gotos(goto_programt &dest)
Operator to return the address of an object.
void convert_return(const code_returnt &code, goto_programt &dest)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
#define forall_expr_list(it, expr)
void goto_convert_rec(const codet &code, goto_programt &dest)
const code_switcht & to_code_switch(const codet &code)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
bool has_return_value() const
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
void convert_function_call(const code_function_callt &code, goto_programt &dest)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
void convert_assert(const code_assertt &code, goto_programt &dest)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest)
exprt get_constant(const exprt &expr)
void set_continue(goto_programt::targett _continue_target)
const exprt & value() const
typet type
Type of symbol.
const code_continuet & to_code_continue(const codet &code)
static bool needs_cleaning(const exprt &expr)
goto_programt::targett continue_target
void convert_decl(const code_declt &code, goto_programt &dest)
void new_name(symbolt &symbol)
void convert_try_catch(const codet &code, goto_programt &dest)
void finish_guarded_gotos(goto_programt &dest)
For each if(x) goto z; goto y; z: emitted, see if any destructor statements were inserted between got...
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest)
if(guard) goto target_true; else goto target_false;
void set_break(goto_programt::targett _break_target)
void set_statement(const irep_idt &statement)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
const symbolt & lookup(const irep_idt &identifier)
A break for `for' and `while' loops.
void finish_gotos(goto_programt &dest)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void convert_break(const code_breakt &code, goto_programt &dest)
void convert_loop_invariant(const codet &code, goto_programt::targett loop)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest)
const exprt & assumption() const
computed_gotost computed_gotos
const source_locationt & source_location() const
const exprt & iter() const
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &)
void convert_assume(const code_assumet &code, goto_programt &dest)
std::size_t break_stack_size
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void convert_block(const code_blockt &code, goto_programt &dest)
A removal of a local variable.
#define Forall_operands(it, expr)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
const code_fort & to_code_for(const codet &code)
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A statement in a programming language.
void convert_msc_try_except(const codet &code, goto_programt &dest)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
code_function_callt get_destructor(const namespacet &ns, const typet &type)
const code_labelt & to_code_label(const codet &code)
void convert_bp_enforce(const codet &code, goto_programt &dest)
const typet & subtype() const
const code_assertt & to_code_assert(const codet &code)
void convert_expression(const code_expressiont &code, goto_programt &dest)
void convert_start_thread(const codet &code, goto_programt &dest)
#define forall_goto_program_instructions(it, program)
const codet & else_case() const
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
message_handlert * message_handler
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)
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
void swap(goto_program_templatet< codeT, guardT > &program)
Swap the goto program.
const code_function_callt & to_code_function_call(const codet &code)
void convert_CPROVER_throw(const codet &code, goto_programt &dest)
bool simplify(exprt &expr, const namespacet &ns)
const exprt & assertion() const
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest)
if(guard) true_case; else false_case;
instructionst::iterator targett
void convert_non_deterministic_goto(const codet &code, goto_programt &dest)
#define forall_irep(it, irep)
unsigned get_message_count(unsigned level) const