Go to the documentation of this file.
23 "msc_try_finally expects two arguments",
60 "msc_try_except expects three arguments",
98 "try_catch expects at least two arguments",
103 catch_push_instruction->make_catch();
116 end_target->make_skip();
123 catch_pop_instruction->make_catch();
129 for(std::size_t i=1; i<code.
operands().size(); i++)
134 exception_list.push_back(
139 catch_push_instruction->targets.push_back(tmp.
instructions.begin());
146 catch_push_instruction->code=push_catch_code;
159 "CPROVER_try_catch expects two arguments",
231 "CPROVER_try_finally expects two arguments",
251 symbol_tablet::symbolst::const_iterator s_it=
271 std::size_t final_stack_size,
281 std::size_t final_stack_size,
291 while(destructor_stack.size()>final_stack_size)
293 codet d_code=destructor_stack.back();
297 destructor_stack.pop_back();
303 old_stack.swap(destructor_stack);
symbol_exprt exception_flag()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
goto_programt::targett leave_target
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
typet type
Type of symbol.
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
goto_programt::targett throw_target
irep_idt base_name
Base (non-scoped) name.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
destructor_stackt destructor_stack
std::vector< codet > destructor_stackt
Expression to hold a symbol (variable)
Pops an exception handler from the stack of active handlers (i.e.
codet representation of an if-then-else statement.
const codet & to_code(const exprt &expr)
void set_leave(goto_programt::targett _leave_target)
targett add_instruction()
Adds an instruction at the end.
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
exception_listt & exception_list()
void set_throw(goto_programt::targett _throw_target)
std::size_t throw_stack_size
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
struct goto_convertt::targetst targets
instructionst instructions
The list of instructions in the goto program.
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
const irep_idt & get(const irep_namet &name) const
std::vector< exception_list_entryt > exception_listt
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
A generic container class for the GOTO intermediate representation of one function.
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, 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
std::size_t leave_stack_size
source_locationt & add_source_location()
A codet representing an assignment in the program.
The Boolean constant true.
const source_locationt & source_location() const
irep_idt name
The unique identifier.
instructionst::iterator targett
Data structure for representing an arbitrary statement in a program.
goto_programt::targett return_target