24 "msc_try_finally expects two arguments",
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",
219 "CPROVER_try_finally expects two arguments",
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)
308 std::optional<codet> &destructor =
317 codet copied_instruction = *destructor;
319 convert(copied_instruction, dest, mode);
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 ....
std::vector< exception_list_entryt > exception_listt
exception_listt & exception_list()
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
source_locationt & add_source_location()
const source_locationt & source_location() const
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
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
void descend_tree()
Walks the current node down to its child.
void set_current_node(std::optional< node_indext > val)
Sets the current node.
std::optional< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
Expression to hold a symbol (variable)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
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.
void set_leave(goto_programt::targett _leave_target)
node_indext leave_stack_node
node_indext throw_stack_node
goto_programt::targett return_target
goto_programt::targett leave_target
void set_throw(goto_programt::targett _throw_target)
goto_programt::targett throw_target