24 "msc_try_finally expects two arguments",
43 targets.scope_stack.set_current_node(old_stack_top);
62 "msc_try_except expects three arguments",
93 "try_catch expects at least two arguments",
122 for(std::size_t i = 1; i < code.
operands().size(); i++)
127 exception_list.push_back(
132 catch_push_instruction->targets.push_back(tmp.
instructions.begin());
139 catch_push_instruction->code_nonconst() = push_catch_code;
152 "CPROVER_try_catch expects two arguments",
169 targets.scope_stack.add(catch_code, {});
175 targets.scope_stack.set_current_node(old_stack_top);
219 "CPROVER_try_finally expects two arguments",
230 targets.scope_stack.set_current_node(old_stack_top);
240 symbol_table_baset::symbolst::const_iterator s_it =
246 new_symbol.
base_name =
"$exception_flag";
247 new_symbol.is_lvalue =
true;
248 new_symbol.is_thread_local =
true;
284 std::optional<node_indext> end_index,
285 std::optional<node_indext> starting_index)
298 starting_index.value_or(
targets.scope_stack.get_current_node());
300 targets.scope_stack.set_current_node(start_id);
304 while(
targets.scope_stack.get_current_node() > end_id)
308 std::optional<codet> &destructor =
309 targets.scope_stack.get_destructor(current_node);
313 targets.scope_stack.descend_tree();
317 codet copied_instruction = *destructor;
319 convert(copied_instruction, dest, mode);
324 targets.scope_stack.set_current_node(start_id);
codet representation of an if-then-else statement.
Pops an exception handler from the stack of active handlers (i.e.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
exception_listt & exception_list()
std::vector< exception_list_entryt > exception_listt
Data structure for representing an arbitrary statement in a program.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const source_locationt & source_location() const
source_locationt & add_source_location()
symbol_table_baset & symbol_table
void convert_CPROVER_throw(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)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
struct goto_convertt::targetst targets
symbol_exprt exception_flag(const irep_idt &mode)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
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.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
const irep_idt & get(const irep_idt &name) const
Expression to hold a symbol (variable)
irep_idt base_name
Base (non-scoped) name.
The Boolean constant true.
#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...
const codet & to_code(const exprt &expr)
API to expression classes.