10 #ifndef CPROVER_UTIL_STD_CODE_H 11 #define CPROVER_UTIL_STD_CODE_H 34 set(ID_statement, statement);
39 return get(ID_statement);
51 assert(expr.
id()==ID_code);
52 return static_cast<const codet &
>(expr);
57 assert(expr.
id()==ID_code);
58 return static_cast<codet &
>(expr);
74 for(std::list<codet>::const_iterator
102 if(statement==ID_block &&
107 else if(statement==ID_label)
372 return static_cast<const codet &
>(
op1());
382 return static_cast<const codet &
>(
op2());
601 return static_cast<const code_fort &
>(code);
627 set(ID_destination, label);
632 return get(ID_destination);
664 op2().
id(ID_arguments);
784 return get(ID_label);
789 set(ID_label, label);
799 return static_cast<const codet &
>(
op0());
838 return set(ID_default,
true);
858 return static_cast<const codet &
>(
op1());
934 return get(ID_flavor);
952 return static_cast<const code_asmt &
>(code);
1001 exprt(ID_side_effect)
1007 exprt(ID_side_effect, _type)
1014 return get(ID_statement);
1019 return set(ID_statement, statement);
1025 assert(expr.
id()==ID_side_effect);
1031 assert(expr.
id()==ID_side_effect);
1058 op1().
id(ID_arguments);
1085 assert(expr.
id()==ID_side_effect);
1086 assert(expr.
get(ID_statement)==ID_function_call);
1093 assert(expr.
id()==ID_side_effect);
1094 assert(expr.
get(ID_statement)==ID_function_call);
1110 set(ID_exception_list, exception_list);
1116 assert(expr.
id()==ID_side_effect);
1117 assert(expr.
get(ID_statement)==ID_throw);
1124 assert(expr.
id()==ID_side_effect);
1125 assert(expr.
get(ID_statement)==ID_throw);
1139 set(ID_exception_list, exception_list);
1145 assert(expr.
id()==ID_side_effect);
1146 assert(expr.
get(ID_statement)==ID_push_catch);
1153 assert(expr.
id()==ID_side_effect);
1154 assert(expr.
get(ID_statement)==ID_push_catch);
1170 return static_cast<codet &
>(
op0());
1175 return static_cast<const codet &
>(
op0());
1222 #endif // CPROVER_UTIL_STD_CODE_H const irep_idt & get_statement() const
A side effect that pushes/pops a catch handler.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
The type of an expression.
const codet & then_case() const
const exprt & return_value() const
const code_declt & to_code_decl(const codet &code)
side_effect_expr_function_callt()
side_effect_expr_nondett()
const irep_idt & get_identifier() const
const exprt & init() const
code_assignt(const exprt &lhs, const exprt &rhs)
void set_label(const irep_idt &label)
code_gotot(const irep_idt &label)
codet & get_catch_code(unsigned i)
const code_assumet & to_code_assume(const codet &code)
const exprt & cond() const
A continue for ‘for’ and ‘while’ loops.
const code_deadt & to_code_dead(const codet &code)
const exprt & cond() const
const codet & body() const
const codet & body() const
const argumentst & arguments() const
void copy_to_operands(const exprt &expr)
source_locationt end_location() const
code_returnt(const exprt &_op)
code_assertt(const exprt &expr)
const code_breakt & to_code_break(const codet &code)
const exprt & symbol() const
exprt::operandst argumentst
codet & first_statement()
const irep_idt & get_flavor() const
code_blockt(const std::list< codet > &_list)
bool get_bool(const irep_namet &name) const
codet(const irep_idt &statement)
code_expressiont & to_code_expression(codet &code)
A side effect that throws an exception.
side_effect_exprt(const irep_idt &statement)
code_assumet(const exprt &expr)
const exprt & case_op() const
void set_flavor(const irep_idt &f)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void add(const codet &code)
code_expressiont(const exprt &expr)
class code_blockt & make_block()
A declaration of a local variable.
const exprt & cond() const
const code_declt & get_catch_decl(unsigned i) const
const code_dowhilet & to_code_dowhile(const codet &code)
code_deadt(const exprt &symbol)
const code_whilet & to_code_while(const codet &code)
const code_gotot & to_code_goto(const codet &code)
const irep_idt & get_identifier() const
const irep_idt & get(const irep_namet &name) const
const codet & try_code() const
const codet & get_catch_code(unsigned i) const
side_effect_exprt(const irep_idt &statement, const typet &_type)
A label for branch targets.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
A side effect that returns a non-deterministically chosen value.
const code_returnt & to_code_return(const codet &code)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Base class for tree-like data structures with sharing.
const codet & code() const
const exprt & rhs() const
bool has_else_case() const
static side_effect_expr_catcht & to_side_effect_expr_catch(exprt &expr)
side_effect_expr_catcht()
const code_switch_caset & to_code_switch_case(const codet &code)
codet & find_last_statement()
const codet & body() const
const code_switcht & to_code_switch(const codet &code)
bool has_return_value() const
std::vector< exprt > operandst
const exprt & lhs() const
A function call side effect.
const exprt & symbol() const
side_effect_expr_nondett(const typet &_type)
const exprt & value() const
const code_continuet & to_code_continue(const codet &code)
void set_statement(const irep_idt &statement)
Base class for all expressions.
A break for ‘for’ and ‘while’ loops.
const exprt & assumption() const
A ‘do while’ instruction.
An inline assembler statement.
const exprt & iter() const
code_labelt(const irep_idt &_label)
const codet & code() const
side_effect_expr_throwt()
const exprt & expression() const
exprt::operandst & arguments()
A removal of a local variable.
code_declt(const exprt &symbol)
code_declt & get_catch_decl(unsigned i)
code_switch_caset(const exprt &_case_op, const codet &_code)
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
code_asmt(const exprt &expr)
const code_fort & to_code_for(const codet &code)
const code_blockt & to_code_block(const codet &code)
const exprt::operandst & arguments() const
const exprt & lhs() const
const irep_idt & get_destination() const
A statement in a programming language.
side_effect_expr_catcht(const irept &exception_list)
void set_destination(const irep_idt &label)
const code_labelt & to_code_label(const codet &code)
An expression containing a side effect.
const code_assertt & to_code_assert(const codet &code)
const code_try_catcht & to_code_try_catch(const codet &code)
const exprt & cond() const
const codet & else_case() const
const code_ifthenelset & to_code_ifthenelse(const codet &code)
void set_statement(const irep_idt &statement)
const codet & body() const
const irept & find(const irep_namet &name) const
void add_catch(const code_declt &to_catch, const codet &code_catch)
code_asmt & to_code_asm(codet &code)
side_effect_expr_throwt(const irept &exception_list)
void reserve_operands(operandst::size_type n)
const irep_idt & get_statement() const
const code_function_callt & to_code_function_call(const codet &code)
const exprt & assertion() const
code_labelt(const irep_idt &_label, const codet &_code)