32 !it->labels.empty() ||
43 goto_programt::instructiont &i=*target;
45 if(i.code.get_statement()==
"non-deterministic-goto")
47 const irept &destinations=i.code.
find(
"destinations");
53 labelst::const_iterator l_it=
59 str <<
"goto label `" << it->id_string() <<
"' not found";
64 i.targets.push_back(l_it->second);
67 else if(i.is_start_thread())
69 const irep_idt &goto_label=i.code.get(ID_destination);
71 labelst::const_iterator l_it=
77 str <<
"goto label `" << goto_label <<
"' not found";
82 i.targets.push_back(l_it->second);
84 else if(i.code.get_statement()==ID_goto)
86 const irep_idt &goto_label=i.code.get(ID_destination);
93 str <<
"goto label `" << goto_label <<
"' not found";
99 i.targets.push_back(l_it->second);
103 err_location(i.code);
104 error() <<
"finish_gotos: unexpected goto" <<
eom;
116 goto_programt::instructiont &i=*target;
119 assert(destination.
id()==ID_dereference);
120 assert(destination.
operands().size()==1);
132 label_expr.
set(ID_identifier, label.first);
142 t->make_goto(label.second);
143 t->source_location=i.source_location;
183 error() <<
"label statement expected to have one operand" <<
eom;
196 codet tmp_code(ID_start_thread);
207 targets.
labels.insert(std::pair<irep_idt, goto_programt::targett>
209 target->labels.push_front(label);
226 error() <<
"switch-case statement expected to have two operands" <<
eom;
260 case_op_dest.push_back(code.
case_op());
271 error() <<
"GCC's switch-case-range statement expected to have " 272 <<
"three operands" <<
eom;
293 case_op_dest.push_back(code.case_op());
304 if(statement==ID_block)
306 else if(statement==ID_decl)
308 else if(statement==ID_decl_type)
310 else if(statement==ID_expression)
312 else if(statement==ID_assign)
314 else if(statement==ID_init)
316 else if(statement==ID_assert)
318 else if(statement==ID_assume)
320 else if(statement==ID_function_call)
322 else if(statement==ID_label)
324 else if(statement==ID_gcc_local_label)
326 else if(statement==ID_switch_case)
328 else if(statement==ID_gcc_switch_case_range)
330 else if(statement==ID_for)
332 else if(statement==ID_while)
334 else if(statement==ID_dowhile)
336 else if(statement==ID_switch)
338 else if(statement==ID_break)
340 else if(statement==ID_return)
342 else if(statement==ID_continue)
344 else if(statement==ID_goto)
346 else if(statement==ID_gcc_computed_goto)
348 else if(statement==ID_skip)
350 else if(statement==
"non-deterministic-goto")
352 else if(statement==ID_ifthenelse)
354 else if(statement==ID_specc_notify)
356 else if(statement==ID_specc_wait)
358 else if(statement==ID_specc_par)
360 else if(statement==ID_start_thread)
362 else if(statement==ID_end_thread)
364 else if(statement==ID_atomic_begin)
366 else if(statement==ID_atomic_end)
368 else if(statement==ID_bp_enforce)
370 else if(statement==ID_bp_abortif)
372 else if(statement==ID_cpp_delete ||
373 statement==
"cpp_delete[]")
375 else if(statement==ID_msc_try_except)
377 else if(statement==ID_msc_try_finally)
379 else if(statement==ID_msc_leave)
381 else if(statement==ID_try_catch)
383 else if(statement==ID_CPROVER_try_catch)
385 else if(statement==ID_CPROVER_throw)
387 else if(statement==ID_CPROVER_try_finally)
389 else if(statement==ID_asm)
391 else if(statement==ID_static_assert)
397 if(assertion.is_false())
399 err_location(code.
op0());
400 str <<
"static assertion " 405 else if(assertion.is_true())
413 else if(statement==ID_dead)
415 else if(statement==ID_decl_block)
462 error() <<
"expression statement takes one operand" <<
eom;
504 if(op0.
id()!=ID_symbol)
507 error() <<
"decl statement expects symbol as first operand" <<
eom;
516 symbol.
type.
id()==ID_code)
529 initializer=code.
op1();
559 destructor.
arguments().push_back(this_expr);
581 if(rhs.id()==ID_side_effect &&
582 rhs.get(ID_statement)==ID_function_call)
584 if(rhs.operands().size()!=2)
587 error() <<
"function_call sideeffect takes two operands" <<
eom;
596 else if(rhs.id()==ID_side_effect &&
597 (rhs.get(ID_statement)==ID_cpp_new ||
598 rhs.get(ID_statement)==ID_cpp_new_array))
605 else if(rhs.id()==ID_side_effect &&
606 rhs.get(ID_statement)==ID_java_new)
613 else if(rhs.id()==ID_side_effect &&
614 rhs.get(ID_statement)==ID_java_new_array)
621 else if(rhs.id()==ID_side_effect &&
622 rhs.get(ID_statement)==ID_malloc)
629 new_assign.
lhs()=lhs;
630 new_assign.
rhs()=rhs;
638 if(lhs.
id()==ID_typecast)
652 new_assign.
lhs()=lhs;
653 new_assign.
rhs()=rhs;
666 error() <<
"init statement takes two operands" <<
eom;
671 codet assignment=code;
684 error() <<
"cpp_delete statement takes one operand" <<
eom;
693 const exprt &destructor=
694 static_cast<const exprt &
>(code.
find(ID_destructor));
699 delete_identifier=
"__delete_array";
701 delete_identifier=
"__delete";
726 exprt delete_symbol=
ns.
lookup(delete_identifier).symbol_expr();
734 delete_call.
function()=delete_symbol;
753 t->source_location.
set(ID_property, ID_assertion);
754 t->source_location.set(
"user-provided",
true);
804 break_continue_targetst old_targets(
targets);
891 break_continue_targetst old_targets(
targets);
897 z->source_location=source_location;
939 error() <<
"dowhile takes two operands" <<
eom;
959 break_continue_targetst old_targets(
targets);
1011 eq_expr.
lhs()=value;
1051 error() <<
"switch takes at least two operands" <<
eom;
1061 break_switch_targetst old_targets(
targets);
1095 const caset &case_ops=it->second;
1098 assert(it->first->is_goto());
1100 assert(!case_ops.empty());
1105 previous->set_target(it->first);
1106 it->first->guard=guard_expr;
1133 error() <<
"break without target" <<
eom;
1154 error() <<
"return without target" <<
eom;
1162 error() <<
"return takes none or one operand" <<
eom;
1170 bool result_is_used=
1186 err_location(new_code);
1187 error() <<
"function must return value" <<
eom;
1202 err_location(new_code);
1203 error() <<
"function must not return value" <<
eom;
1224 error() <<
"continue without target" <<
eom;
1290 std::set<irep_idt> &events)
1292 if(op.
id()==ID_or || op.
id()==ID_and)
1297 else if(op.
id()==ID_specc_event)
1302 event=std::string(
id2string(event), 7, std::string::npos);
1304 events.insert(event);
1309 error() <<
"convert_convert_event got " << op.
id() <<
eom;
1324 error() <<
"specc_wait expects one operand" <<
eom;
1331 t->or_semantics=
true;
1356 error() <<
"start_thread expects one operand" <<
eom;
1381 start_thread->targets.push_back(tmp.
instructions.begin());
1395 error() <<
"end_thread expects no operands" <<
eom;
1409 error() <<
"atomic_begin expects no operands" <<
eom;
1423 error() <<
"atomic_end expects no operands" <<
eom;
1437 str <<
"bp_enfroce expects two arguments";
1458 exprt constraint(op);
1465 assert(it->code.get(ID_statement)==ID_assign);
1468 codet constrain(ID_bp_constrain);
1469 constrain.reserve_operands(2);
1470 constrain.move_to_operands(it->code);
1471 constrain.copy_to_operands(constraint);
1472 it->code.swap(constrain);
1476 else if(it->is_other() &&
1477 it->code.get(ID_statement)==ID_bp_constrain)
1480 assert(it->code.operands().size()==2);
1497 error() <<
"bp_abortif expects one argument" <<
eom;
1520 error() <<
"ifthenelse takes three operands" <<
eom;
1533 if(code.
cond().
id()==ID_and &&
1567 std::list<exprt> &dest)
1571 dest.push_back(expr);
1638 boolean_negate(guard), false_case, true_case, source_location, dest);
1640 bool has_else=!
is_empty(false_case);
1664 z->source_location=source_location;
1671 tmp_y.
swap(false_case);
1682 tmp_w.
swap(true_case);
1687 x->source_location=tmp_w.
instructions.back().source_location;
1708 if(expr.
id()==ID_and || expr.
id()==ID_or)
1729 target_false->make_skip();
1730 target_false->source_location=source_location;
1733 guard, target_true, target_false, source_location, dest);
1745 g->make_goto(target_true);
1760 if(guard.
id()==ID_not)
1762 assert(guard.
operands().size()==1);
1765 guard.
op0(), target_false, target_true, source_location, dest);
1769 if(guard.
id()==ID_and)
1778 std::list<exprt> op;
1786 t_true->make_goto(target_true);
1788 t_true->source_location=source_location;
1792 else if(guard.
id()==ID_or)
1801 std::list<exprt> op;
1806 *it, target_true, source_location, dest);
1809 t_false->make_goto(target_false);
1820 t_true->make_goto(target_true);
1825 t_false->make_goto(target_false);
1827 t_false->source_location=source_location;
1833 if(expr.
id()==ID_typecast &&
1837 if(expr.
id()==ID_address_of &&
1839 expr.
op0().
id()==ID_index &&
1845 if(index_op.
id()==ID_string_constant)
1846 return index_op.
get(ID_value);
1847 else if(index_op.
id()==ID_array)
1851 if(it->is_constant())
1853 unsigned i=integer2long(
1857 result+=
static_cast<char>(i);
1864 if(expr.
id()==ID_string_constant)
1865 return expr.
get(ID_value);
1868 str <<
"expected string constant, but got: " 1877 if(expr.
id()==ID_symbol)
1882 return symbol.
value;
1884 else if(expr.
id()==ID_member)
1890 else if(expr.
id()==ID_index)
1903 const std::string &suffix,
1914 new_symbol.
type=type;
1915 new_symbol.
location=source_location;
1919 tmp_symbols.push_back(symbol_ptr->
name);
1930 const std::string &suffix,
1940 assignment.rhs()=expr;
1962 error() <<
"failed to find symbol " << identifier <<
eom;
1983 goto_convert.error_msg();
1986 catch(
const char *e)
1988 goto_convert.str << e;
1989 goto_convert.error_msg();
1992 catch(
const std::string &e)
1994 goto_convert.str << e;
1995 goto_convert.error_msg();
1998 if(goto_convert.get_error_found())
2008 const symbol_tablet::symbolst::const_iterator s_it=
2009 symbol_table.
symbols.find(
"main");
2011 if(s_it==symbol_table.
symbols.end())
2013 error() <<
"failed to find main symbol" <<
eom;
2017 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)
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'
pointer_typet pointer_type(const typet &subtype)
const exprt & init() const
symbol_tablet & symbol_table
goto_programt::targett return_target
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)
struct goto_convertt::targetst targets
const exprt & cond() const
const codet & body() const
instructionst instructions
The list of instructions in the goto program.
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)
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 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.
static bool has_and_or(const exprt &expr)
if(guard) goto target;
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
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
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
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)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
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...
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.
source_locationt location
Source code location of definition 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 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)
irep_idt base_name
Base (non-scoped) name.
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_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 &)
static bool is_empty(const goto_programt &goto_program)
unsigned temporary_counter
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
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
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)