24 error() <<
"msc_try_finally expects two arguments" <<
eom;
63 error() <<
"msc_try_except expects three arguments" <<
eom;
80 error() <<
"leave without target" <<
eom;
108 catch_push_instruction->make_catch();
121 end_target->make_skip();
128 catch_pop_instruction->make_catch();
134 for(std::size_t i=1; i<code.
operands().size(); i++)
139 exception_list.push_back(
144 catch_push_instruction->targets.push_back(tmp.
instructions.begin());
151 catch_push_instruction->code=push_catch_code;
165 error() <<
"CPROVER_try_catch expects two arguments" <<
eom;
241 error() <<
"CPROVER_try_finally expects two arguments" <<
eom;
262 symbol_tablet::symbolst::const_iterator s_it=
282 std::size_t final_stack_size,
292 std::size_t final_stack_size,
302 while(destructor_stack.size()>final_stack_size)
304 codet d_code=destructor_stack.back();
308 destructor_stack.pop_back();
314 old_stack.swap(destructor_stack);
irep_idt name
The unique identifier.
const codet & then_case() const
std::vector< exception_list_entryt > exception_listt
goto_programt::targett return_target
struct goto_convertt::targetst targets
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
const exprt & cond() const
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
Pops an exception handler from the stack of active handlers (i.e.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
goto_programt::targett throw_target
destructor_stackt destructor_stack
The boolean constant true.
instructionst::iterator targett
symbol_exprt exception_flag()
goto_programt::targett leave_target
const source_locationt & find_source_location() const
source_locationt source_location
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
std::size_t throw_stack_size
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
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)
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
std::vector< codet > destructor_stackt
targett add_instruction()
Adds an instruction at the end.
void set_leave(goto_programt::targett _leave_target)
irep_idt base_name
Base (non-scoped) name.
void set_throw(goto_programt::targett _throw_target)
std::size_t leave_stack_size
const source_locationt & source_location() const
void convert_msc_try_except(const codet &code, goto_programt &dest, 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)
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbol_table_baset & symbol_table
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
A statement in a programming language.
exception_listt & exception_list()