10 #ifndef CPROVER_UTIL_STD_CODE_H 11 #define CPROVER_UTIL_STD_CODE_H 53 set(ID_statement, statement);
58 return get(ID_statement);
116 template<
typename Tag>
119 if(
const auto ptr = expr_try_dynamic_cast<codet>(expr))
121 return ptr->get_statement() == tag;
130 return base.id()==ID_code;
139 return static_cast<const codet &
>(expr);
145 return static_cast<codet &
>(expr);
173 s.reserve(_list.size());
174 for(
const auto &c : _list)
181 operands()=(
const std::vector<exprt> &)_statements;
186 operands()=std::move((std::vector<exprt> &&)_statements);
294 vm, code.
operands().size() == 2,
"assignment must have two operands");
307 "lhs and rhs of assignment must have same type");
380 vm, code.
operands().size() == 1,
"declaration must have one operand");
383 code.
op0().
id() == ID_symbol,
384 "declaring a non-symbol: " +
405 code.
operands().size() >= 1,
"decls must have one or more operands");
407 code.
op0().
id() == ID_symbol,
"decls symbols must be a \"symbol\"");
418 code.
operands().size() >= 1,
"decls must have one or more operands");
454 "removal (code_deadt) must have one operand");
457 code.
op0().
id() == ID_symbol,
458 "removing a non-symbol: " +
477 code.
operands().size() == 1,
"dead statement must have one operand");
480 "dead statement must take symbol operand");
488 code.
operands().size() == 1,
"dead statement must have one operand");
491 "dead statement must take symbol operand");
617 DEPRECATED(
"use code_ifthenelset(condition, then_code[, else_code]) instead")
627 const exprt &condition,
628 const codet &then_code,
629 const codet &else_code)
630 :
codet(ID_ifthenelse)
637 :
codet(ID_ifthenelse)
654 return static_cast<const codet &
>(
op1());
664 return static_cast<const codet &
>(
op2());
692 code.
operands().size() == 3,
"if-then-else must have three operands");
700 code.
operands().size() == 3,
"if-then-else must have three operands");
708 DEPRECATED(
"use code_switcht(value, body) instead")
770 DEPRECATED(
"use code_whilet(cond, body) instead")
832 DEPRECATED(
"use code_dowhilet(cond, body) instead")
880 code.
operands().size() == 2,
"do-while must have two operands");
888 code.
operands().size() == 2,
"do-while must have two operands");
896 DEPRECATED(
"use code_fort(init, cond, iter, body) instead")
972 return static_cast<const code_fort &
>(code);
998 set(ID_destination, label);
1003 return get(ID_destination);
1021 return static_cast<const code_gotot &
>(code);
1039 DEPRECATED(
"Use code_function_callt(...) instead")
1044 op2().
id(ID_arguments);
1051 op2().
id(ID_arguments);
1052 function() = _function;
1059 const exprt &_function,
1069 const exprt &_function,
1126 "function calls must have three operands:\n1) expression to store the " 1127 "returned values\n2) the function being called\n3) the vector of " 1138 if(code.
op0().
id() == ID_nil)
1142 "void function should not return value");
1148 "function returns expression of wrong type");
1281 return get(ID_label);
1286 set(ID_label, label);
1291 return static_cast<codet &
>(
op0());
1296 return static_cast<const codet &
>(
op0());
1329 DEPRECATED(
"use code_switch_caset(case_op, code) instead")
1348 return set(ID_default,
true);
1363 return static_cast<codet &
>(
op1());
1368 return static_cast<const codet &
>(
op1());
1386 code.
operands().size() == 2,
"switch-case must have two operands");
1394 code.
operands().size() == 2,
"switch-case must have two operands");
1473 return get(ID_flavor);
1499 return static_cast<const code_asmt &
>(code);
1507 DEPRECATED(
"use code_expressiont(expr) instead")
1543 code.
operands().size() == 1,
"expression statement must have one operand");
1551 code.
operands().size() == 1,
"expression statement must have one operand");
1563 DEPRECATED(
"use side_effect_exprt(statement, type, loc) instead")
1569 DEPRECATED(
"use side_effect_exprt(statement, type, loc) instead")
1571 exprt(ID_side_effect, _type)
1580 :
exprt(ID_side_effect, _type)
1588 return get(ID_statement);
1593 return set(ID_statement, statement);
1600 template<
typename Tag>
1603 if(
const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1605 return ptr->get_statement() == tag;
1614 return base.id()==ID_side_effect;
1636 DEPRECATED(
"use side_effect_expr_nondett(statement, type, loc) instead")
1642 DEPRECATED(
"use side_effect_expr_nondett(statement, type, loc) instead")
1657 set(ID_is_nondet_nullable, nullable);
1662 return get_bool(ID_is_nondet_nullable);
1678 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1686 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1695 "use side_effect_expr_function_callt(" 1696 "function, arguments, type, loc) instead")
1701 op1().
id(ID_arguments);
1705 "use side_effect_expr_function_callt(" 1706 "function, arguments, type, loc) instead")
1708 const
exprt &_function,
1713 op1().
id(ID_arguments);
1714 function() = _function;
1719 "use side_effect_expr_function_callt(" 1720 "function, arguments, type, loc) instead")
1722 const
exprt &_function,
1728 op1().
id(ID_arguments);
1729 function() = _function;
1734 const exprt &_function,
1795 DEPRECATED(
"use side_effect_expr_throwt(exception_list) instead")
1801 const irept &exception_list,
1806 set(ID_exception_list, exception_list);
1850 set(ID_exception_list,
irept(ID_exception_list));
1868 set(ID_label, label);
1882 set(ID_label, label);
1886 return get(ID_label);
1895 codet(ID_push_catch)
1897 set(ID_exception_list,
irept(ID_exception_list));
1972 codet(ID_exception_landingpad)
2010 DEPRECATED(
"use code_try_catcht(try_code) instead")
2024 return static_cast<codet &
>(
op0());
2029 return static_cast<const codet &
>(
op0());
2076 code.
operands().size() >= 3,
"try-catch must have three or more operands");
2084 code.
operands().size() >= 3,
"try-catch must have three or more operands");
2088 #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, extends irept.
std::vector< codet > code_operandst
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)
std::vector< exception_list_entryt > exception_listt
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< code_assertt >(const exprt &base)
codet representing a switch statement.
bool can_cast_expr< code_push_catcht >(const exprt &base)
const std::string & id2string(const irep_idt &d)
const exception_listt & exception_list() 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)
const code_operandst & statements() const
codet representation of a try/catch block.
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
codet representation of a continue statement (within a for or while loop).
codet & find_last_statement()
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 base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
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)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
const argumentst & arguments() const
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
const irep_idt & get_identifier() const
source_locationt end_location() const
code_returnt(const exprt &_op)
code_operandst & statements()
code_assertt(const exprt &expr)
const irep_idt & get_identifier() const
side_effect_exprt(const irep_idt &statement, const typet &_type, const source_locationt &loc)
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)
code_blockt(std::vector< codet > &&_statements)
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
codet representation of a goto statement.
typet & type()
Return the type of the expression.
Pops an exception handler from the stack of active handlers (i.e.
exprt::operandst argumentst
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them...
const irep_idt & get_flavor() const
static code_blockt from_list(const std::list< codet > &_list)
bool get_bool(const irep_namet &name) const
void set_label(const irep_idt &label)
codet representation of an expression statement.
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_exprt representation of a side effect that throws an exception.
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
code_function_callt(const exprt &_function)
void add(const codet &code)
code_expressiont(const exprt &expr)
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements...
bool can_cast_expr< code_labelt >(const exprt &base)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
A codet representing the declaration of a local variable.
static code_push_catcht & to_code_push_catch(codet &code)
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
code_landingpadt(const exprt &catch_expr)
code_fort(const exprt &_init, const exprt &_cond, const exprt &_iter, const codet &_body)
A statement describing a for loop with initializer _init, loop condition _cond, increment _iter...
const exprt & cond() const
static void check(const codet &, const validation_modet)
Check that the code statement is well-formed (shallow checks only, i.e., enclosed statements...
static void validate_full(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed (full check, including checks of all subexpressions) ...
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_try_catcht(const codet &_try_code)
A statement representing try _try_code catch ...
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)
API to expression classes.
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get(const irep_namet &name) const
const codet & try_code() const
const codet & get_catch_code(unsigned i) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_ifthenelset(const exprt &condition, const codet &then_code, const codet &else_code)
An if condition then then_code else else_code statement.
codet representation of 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.
#define PRECONDITION(CONDITION)
A side_effect_exprt 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.
codet representation of a function call statement.
const codet & code() const
const exprt & rhs() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool has_else_case() const
codet representing a while statement.
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...
code_declt(const symbol_exprt &symbol)
code_ifthenelset(const exprt &condition, const codet &then_code)
An if condition then then_code statement (no "else" case).
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
const symbol_exprt & symbol() const
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 side_effect_exprt representation of a function call side effect.
An assumption, which must hold in subsequent code.
const exprt & value() const
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
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.
code_deadt(const symbol_exprt &symbol)
codet representation of a break statement (within a for or while loop).
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed, assuming that all its enclosed statements, subexpressions, etc.
bool can_cast_expr< code_deadt >(const exprt &base)
const exprt & assumption() const
codet representation of a do while statement.
codet representation of 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 codet representing the removal of a local variable going out of scope.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
code_declt & get_catch_decl(unsigned i)
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
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)
A codet representing a skip statement.
side_effect_expr_nondett(const typet &_type, const source_locationt &loc)
const code_fort & to_code_for(const codet &code)
codet representation of an if-then-else statement.
Expression to hold a symbol (variable)
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)
codet representation of a switch-case, i.e. a case statement within a switch.
const irep_idt & get_destination() const
Data structure for representing an arbitrary statement in a program.
codet representation of a "return from a function" statement.
void set_destination(const irep_idt &label)
codet representation of a for statement.
const code_labelt & to_code_label(const codet &code)
const irep_idt & get_label() const
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
An expression containing a side effect.
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const code_assertt & to_code_assert(const codet &code)
bool can_cast_expr< code_assignt >(const exprt &base)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const code_try_catcht & to_code_try_catch(const codet &code)
code_blockt(const std::vector< codet > &_statements)
code_function_callt(const exprt &_function, const argumentst &_arguments)
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)
side_effect_expr_function_callt(const exprt &_function, const exprt::operandst &_arguments, const typet &_type, const source_locationt &loc)
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)
const symbol_exprt & symbol() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const irep_idt & get_identifier() const
A codet representing an assignment in the program.
void reserve_operands(operandst::size_type n)
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
const irep_idt & get_statement() const
code_function_callt(const exprt &_function, argumentst &&_arguments)
code_function_callt(const exprt &_lhs, const exprt &_function, const argumentst &_arguments)
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
code_function_callt(const exprt &_lhs, const exprt &_function, argumentst &&_arguments)
bool can_cast_expr< code_returnt >(const exprt &base)
code_labelt(const irep_idt &_label, const codet &_code)