10 #ifndef CPROVER_UTIL_STD_CODE_H 11 #define CPROVER_UTIL_STD_CODE_H 37 set(ID_statement, statement);
42 return get(ID_statement);
55 template<
typename Tag>
58 if(
const auto ptr = expr_try_dynamic_cast<codet>(expr))
60 return ptr->get_statement() == tag;
69 return base.id()==ID_code;
77 assert(expr.
id()==ID_code);
78 return static_cast<const codet &
>(expr);
83 assert(expr.
id()==ID_code);
84 return static_cast<codet &
>(expr);
100 for(std::list<codet>::const_iterator
139 if(statement==ID_block &&
144 else if(statement==ID_label)
488 return static_cast<const codet &
>(
op1());
498 return static_cast<const codet &
>(
op2());
541 DEPRECATED(
"Use code_switcht(value, body) instead")
604 DEPRECATED(
"Use code_whilet(cond, body) instead")
667 DEPRECATED(
"Use code_dowhilet(cond, body) instead")
791 return static_cast<const code_fort &
>(code);
818 set(ID_destination, label);
823 return get(ID_destination);
865 op2().
id(ID_arguments);
1002 return get(ID_label);
1007 set(ID_label, label);
1012 return static_cast<codet &
>(
op0());
1017 return static_cast<const codet &
>(
op0());
1048 DEPRECATED(
"Use code_switch_caset(case_op, code) instead")
1067 return set(ID_default,
true);
1082 return static_cast<codet &
>(
op1());
1087 return static_cast<const codet &
>(
op1());
1189 return get(ID_flavor);
1215 return static_cast<const code_asmt &
>(code);
1223 DEPRECATED(
"Use code_expressiont(expr) instead")
1274 DEPRECATED(
"Use side_effect_exprt(statement, type, loc) instead")
1280 DEPRECATED(
"Use side_effect_exprt(statement, type, loc) instead")
1282 exprt(ID_side_effect, _type)
1294 return get(ID_statement);
1299 return set(ID_statement, statement);
1306 template<
typename Tag>
1309 if(
const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1311 return ptr->get_statement() == tag;
1320 return base.id()==ID_side_effect;
1328 assert(expr.
id()==ID_side_effect);
1334 assert(expr.
id()==ID_side_effect);
1343 DEPRECATED(
"Use side_effect_expr_nondett(statement, type, loc) instead")
1349 DEPRECATED(
"Use side_effect_expr_nondett(statement, type, loc) instead")
1360 set(ID_is_nondet_nullable, nullable);
1365 return get_bool(ID_is_nondet_nullable);
1381 assert(side_effect_expr_nondet.get_statement()==ID_nondet);
1389 assert(side_effect_expr_nondet.get_statement()==ID_nondet);
1399 "Use side_effect_expr_function_callt(" 1400 "function, arguments, type, loc) instead")
1405 op1().
id(ID_arguments);
1409 "Use side_effect_expr_function_callt(" 1410 "function, arguments, type, loc) instead")
1412 const
exprt &_function,
1417 op1().
id(ID_arguments);
1418 function() = _function;
1423 "Use side_effect_expr_function_callt(" 1424 "function, arguments, type, loc) instead")
1426 const
exprt &_function,
1432 op1().
id(ID_arguments);
1433 function() = _function;
1438 const exprt &_function,
1476 assert(expr.
id()==ID_side_effect);
1477 assert(expr.
get(ID_statement)==ID_function_call);
1484 assert(expr.
id()==ID_side_effect);
1485 assert(expr.
get(ID_statement)==ID_function_call);
1494 DEPRECATED(
"Use side_effect_expr_throwt(exception_list) instead")
1500 const irept &exception_list,
1505 set(ID_exception_list, exception_list);
1520 assert(expr.
id()==ID_side_effect);
1521 assert(expr.
get(ID_statement)==ID_throw);
1528 assert(expr.
id()==ID_side_effect);
1529 assert(expr.
get(ID_statement)==ID_throw);
1549 set(ID_exception_list,
irept(ID_exception_list));
1567 set(ID_label, label);
1581 set(ID_label, label);
1585 return get(ID_label);
1594 codet(ID_push_catch)
1596 set(ID_exception_list,
irept(ID_exception_list));
1671 codet(ID_exception_landingpad)
1717 return static_cast<codet &
>(
op0());
1722 return static_cast<const codet &
>(
op0());
1779 #endif // CPROVER_UTIL_STD_CODE_H
side_effect_expr_throwt(const irept &exception_list, const typet &type, const source_locationt &loc)
bool can_cast_expr< code_asmt >(const exprt &base)
const irep_idt & get_statement() const
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
The type of an expression.
const codet & then_case() const
code_dowhilet(const exprt &_cond, const codet &_body)
const exprt & return_value() const
const code_declt & to_code_decl(const codet &code)
side_effect_expr_function_callt()
std::vector< exception_list_entryt > exception_listt
side_effect_expr_nondett()
bool can_cast_expr< code_assertt >(const exprt &base)
bool can_cast_expr< code_push_catcht >(const exprt &base)
const exception_listt & exception_list() const
const irep_idt & get_identifier() const
const exprt & init() const
code_switcht(const exprt &_value, const codet &_body)
code_assignt(const exprt &lhs, const exprt &rhs)
void set_label(const irep_idt &label)
code_whilet(const exprt &_cond, const codet &_body)
code_gotot(const irep_idt &label)
codet & get_catch_code(unsigned i)
bool can_cast_expr< code_expressiont >(const exprt &base)
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)
bool can_cast_expr< code_whilet >(const exprt &base)
const irep_idt & get_tag() const
const exprt & cond() const
bool get_nullable() const
bool can_cast_expr< code_blockt >(const exprt &base)
const codet & body() const
bool can_cast_expr< code_landingpadt >(const exprt &base)
bool can_cast_expr< code_ifthenelset >(const exprt &base)
const codet & body() const
bool can_cast_expr< code_continuet >(const exprt &base)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
const argumentst & arguments() const
void copy_to_operands(const exprt &expr)
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
source_locationt end_location() const
code_returnt(const exprt &_op)
code_assertt(const exprt &expr)
void move_to_operands(exprt &expr)
void validate_expr(const code_assignt &x)
const code_breakt & to_code_break(const codet &code)
code_push_catcht(const irep_idt &tag, const irep_idt &label)
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
static code_pop_catcht & to_code_pop_catch(codet &code)
const exprt & symbol() const
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Pops an exception handler from the stack of active handlers (i.e.
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
void set_label(const irep_idt &label)
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &source_location)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
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)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const exprt & case_op() const
void set_flavor(const irep_idt &f)
side_effect_exprt & to_side_effect_expr(exprt &expr)
bool can_cast_expr< code_switch_caset >(const exprt &base)
void set_nullable(bool nullable)
Templated functions to cast to specific exprt-derived classes.
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()
bool can_cast_expr< code_labelt >(const exprt &base)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
A declaration of a local variable.
static code_push_catcht & to_code_push_catch(codet &code)
code_landingpadt(const exprt &catch_expr)
const exprt & cond() const
void add(codet code, const source_locationt &loc)
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)
bool can_cast_expr< code_breakt >(const exprt &base)
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
A label for branch targets.
void set_tag(const irep_idt &tag)
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)
exception_list_entryt(const irep_idt &tag)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
bool can_cast_expr< code_try_catcht >(const exprt &base)
bool can_cast_expr< code_declt >(const exprt &base)
Base class for tree-like data structures with sharing.
const codet & code() const
const exprt & rhs() const
bool has_else_case() const
const code_switch_caset & to_code_switch_case(const codet &code)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
codet & find_last_statement()
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
const codet & body() const
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
const code_switcht & to_code_switch(const codet &code)
bool has_return_value() const
bool can_cast_expr< code_switcht >(const exprt &base)
std::vector< exprt > operandst
const exprt & lhs() const
bool can_cast_expr< code_gotot >(const exprt &base)
A non-fatal assertion, which checks a condition then permits execution to continue.
A function call side effect.
An assumption, which must hold in subsequent code.
const exprt & symbol() const
const exprt & value() const
bool can_cast_expr< code_assumet >(const exprt &base)
const code_continuet & to_code_continue(const codet &code)
bool can_cast_expr< codet >(const exprt &base)
static code_landingpadt & to_code_landingpad(codet &code)
bool can_cast_expr< code_dowhilet >(const exprt &base)
void set_statement(const irep_idt &statement)
Base class for all expressions.
A break for ‘for’ and ‘while’ loops.
bool can_cast_expr< code_deadt >(const exprt &base)
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
const exprt & expression() const
bool can_cast_expr< code_pop_catcht >(const exprt &base)
exprt::operandst & arguments()
A removal of a local variable.
code_declt(const exprt &symbol)
code_declt & get_catch_decl(unsigned i)
source_locationt & add_source_location()
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 exprt & catch_expr() const
bool can_cast_expr< code_fort >(const exprt &base)
const code_blockt & to_code_block(const codet &code)
const exprt::operandst & arguments() const
const exprt & lhs() const
bool can_cast_expr< code_skipt >(const exprt &base)
const irep_idt & get_destination() const
A statement in a programming language.
void set_destination(const irep_idt &label)
const code_labelt & to_code_label(const codet &code)
const irep_idt & get_label() const
An expression containing a side effect.
const code_assertt & to_code_assert(const codet &code)
bool can_cast_expr< code_assignt >(const exprt &base)
const code_try_catcht & to_code_try_catch(const codet &code)
const exprt & cond() const
const codet & else_case() const
exception_listt & exception_list()
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
bool can_cast_expr< code_function_callt >(const exprt &base)
void add_catch(const code_declt &to_catch, const codet &code_catch)
code_asmt & to_code_asm(codet &code)
void reserve_operands(operandst::size_type n)
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
const irep_idt & get_statement() const
A statement that catches an exception, assigning the exception in flight to an expression (e...
const code_function_callt & to_code_function_call(const codet &code)
const exprt & assertion() const
bool can_cast_expr< code_returnt >(const exprt &base)
code_labelt(const irep_idt &_label, const codet &_code)