Go to the documentation of this file.
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);
210 return static_cast<const source_locationt &>(
find(ID_C_end_location));
227 return static_cast<const code_blockt &>(code);
233 return static_cast<code_blockt &>(code);
294 vm, code.
operands().size() == 2,
"assignment must have two operands");
307 "lhs and rhs of assignment must have same type");
338 return static_cast<const code_assignt &>(code);
345 return static_cast<code_assignt &>(code);
362 return static_cast<symbol_exprt &>(
op0());
367 return static_cast<const symbol_exprt &>(
op0());
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\"");
409 return static_cast<const code_declt &>(code);
418 code.
operands().size() >= 1,
"decls must have one or more operands");
419 return static_cast<code_declt &>(code);
434 return static_cast<symbol_exprt &>(
op0());
439 return static_cast<const symbol_exprt &>(
op0());
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");
481 return static_cast<const code_deadt &>(code);
488 code.
operands().size() == 1,
"dead statement must have one operand");
491 "dead statement must take symbol operand");
492 return static_cast<code_deadt &>(code);
532 return static_cast<const code_assumet &>(code);
538 return static_cast<code_assumet &>(code);
584 return static_cast<const code_assertt &>(code);
590 return static_cast<code_assertt &>(code);
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());
669 return static_cast<codet &>(
op1());
674 return static_cast<codet &>(
op2());
692 code.
operands().size() == 3,
"if-then-else must have three operands");
693 return static_cast<const code_ifthenelset &>(code);
700 code.
operands().size() == 3,
"if-then-else must have three operands");
701 return static_cast<code_ifthenelset &>(code);
708 DEPRECATED(
"use code_switcht(value, body) instead")
738 return static_cast<codet &>(
op1());
756 return static_cast<const code_switcht &>(code);
763 return static_cast<code_switcht &>(code);
770 DEPRECATED(
"use code_whilet(cond, body) instead")
800 return static_cast<codet &>(
op1());
818 return static_cast<const code_whilet &>(code);
825 return static_cast<code_whilet &>(code);
832 DEPRECATED(
"use code_dowhilet(cond, body) instead")
862 return static_cast<codet &>(
op1());
880 code.
operands().size() == 2,
"do-while must have two operands");
881 return static_cast<const code_dowhilet &>(code);
888 code.
operands().size() == 2,
"do-while must have two operands");
889 return static_cast<code_dowhilet &>(code);
896 DEPRECATED(
"use code_fort(init, cond, iter, body) instead")
954 return static_cast<codet &>(
op3());
972 return static_cast<const code_fort &>(code);
979 return static_cast<code_fort &>(code);
998 set(ID_destination, label);
1003 return get(ID_destination);
1021 return static_cast<const code_gotot &>(code);
1028 return static_cast<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");
1176 return static_cast<const code_function_callt &>(code);
1182 return static_cast<code_function_callt &>(code);
1241 return static_cast<const code_returnt &>(code);
1247 return static_cast<code_returnt &>(code);
1281 return get(ID_label);
1286 set(ID_label, label);
1291 return static_cast<codet &>(
op0());
1296 return static_cast<const codet &>(
op0());
1314 return static_cast<const code_labelt &>(code);
1321 return static_cast<code_labelt &>(code);
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");
1387 return static_cast<const code_switch_caset &>(code);
1394 code.
operands().size() == 2,
"switch-case must have two operands");
1395 return static_cast<code_switch_caset &>(code);
1419 return static_cast<const code_breakt &>(code);
1425 return static_cast<code_breakt &>(code);
1449 return static_cast<const code_continuet &>(code);
1455 return static_cast<code_continuet &>(code);
1473 return get(ID_flavor);
1493 return static_cast<code_asmt &>(code);
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");
1544 return static_cast<code_expressiont &>(code);
1551 code.
operands().size() == 1,
"expression statement must have one operand");
1552 return static_cast<const code_expressiont &>(code);
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;
1623 return static_cast<side_effect_exprt &>(expr);
1629 return static_cast<const side_effect_exprt &>(expr);
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);
1679 return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
1686 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1687 return static_cast<const side_effect_expr_nondett &>(side_effect_expr_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,
1779 return static_cast<side_effect_expr_function_callt &>(expr);
1787 return static_cast<const side_effect_expr_function_callt &>(expr);
1795 DEPRECATED(
"use side_effect_expr_throwt(exception_list) instead")
1801 const irept &exception_list,
1806 set(ID_exception_list, exception_list);
1823 return static_cast<side_effect_expr_throwt &>(expr);
1831 return static_cast<const side_effect_expr_throwt &>(expr);
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));
1921 return static_cast<code_push_catcht &>(code);
1927 return static_cast<const code_push_catcht &>(code);
1952 return static_cast<code_pop_catcht &>(code);
1958 return static_cast<const code_pop_catcht &>(code);
1972 codet(ID_exception_landingpad)
1997 return static_cast<code_landingpadt &>(code);
2003 return static_cast<const code_landingpadt &>(code);
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");
2077 return static_cast<const code_try_catcht &>(code);
2084 code.
operands().size() >= 3,
"try-catch must have three or more operands");
2085 return static_cast<code_try_catcht &>(code);
2088 #endif // CPROVER_UTIL_STD_CODE_H
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const exprt & case_op() const
const exprt::operandst & arguments() const
A codet representing sequential composition of program statements.
void add_catch(const code_declt &to_catch, const codet &code_catch)
code_labelt(const irep_idt &_label, const codet &_code)
#define PRECONDITION(CONDITION)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
code_expressiont & to_code_expression(codet &code)
codet representation of a switch-case, i.e. a case statement within a switch.
static code_blockt from_list(const std::list< codet > &_list)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
const exprt & cond() const
const symbol_exprt & symbol() const
codet representing a while statement.
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,...
side_effect_expr_function_callt(const exprt &_function, const exprt::operandst &_arguments, const typet &_type, const source_locationt &loc)
const code_declt & to_code_decl(const codet &code)
code_asmt(const exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
codet representation of an inline assembler statement.
codet representation of a for statement.
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
The type of an expression, extends irept.
const codet & then_case() const
void validate_expr(const code_assignt &x)
const exprt & lhs() const
codet representation of a try/catch block.
const code_breakt & to_code_break(const codet &code)
code_function_callt(const exprt &_function, const argumentst &_arguments)
const codet & code() const
A side_effect_exprt representation of a function call side effect.
codet & get_catch_code(unsigned i)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_function_callt(const exprt &_lhs, const exprt &_function, const argumentst &_arguments)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
const irept & find(const irep_namet &name) const
codet(const irep_idt &statement)
A codet representing the declaration of a local variable.
A non-fatal assertion, which checks a condition then permits execution to continue.
code_gotot(const irep_idt &label)
const exprt & assumption() const
Base class for all expressions.
const exprt & iter() const
code_returnt(const exprt &_op)
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
exception_list_entryt(const irep_idt &tag)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
bool can_cast_expr< code_function_callt >(const exprt &base)
codet representation of a continue statement (within a for or while loop).
const code_whilet & to_code_while(const codet &code)
code_expressiont(const exprt &expr)
const exprt & cond() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
Expression to hold a symbol (variable)
Pops an exception handler from the stack of active handlers (i.e.
const irep_idt & get_identifier() const
bool can_cast_expr< code_deadt >(const exprt &base)
const code_fort & to_code_for(const codet &code)
codet representation of an if-then-else statement.
bool can_cast_expr< code_expressiont >(const exprt &base)
bool can_cast_expr< code_pop_catcht >(const exprt &base)
bool can_cast_expr< codet >(const exprt &base)
bool can_cast_expr< code_returnt >(const exprt &base)
const code_declt & get_catch_decl(unsigned i) const
const codet & to_code(const exprt &expr)
code_blockt(const std::vector< codet > &_statements)
const irep_idt & get_tag() const
const code_switch_caset & to_code_switch_case(const codet &code)
bool can_cast_expr< code_switcht >(const exprt &base)
code_operandst & statements()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static void check(const codet &, const validation_modet)
Check that the code statement is well-formed (shallow checks only, i.e., enclosed statements,...
const codet & try_code() const
code_function_callt(const exprt &_lhs, const exprt &_function, argumentst &&_arguments)
typet & type()
Return the type of the expression.
const code_assumet & to_code_assume(const codet &code)
const code_assertt & to_code_assert(const codet &code)
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
code_assignt(const exprt &lhs, const exprt &rhs)
bool get_nullable() const
bool can_cast_expr< code_labelt >(const exprt &base)
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.
const exprt & assertion() const
codet representation of a do while statement.
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
const exprt & init() const
code_labelt(const irep_idt &_label)
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
code_ifthenelset(const exprt &condition, const codet &then_code, const codet &else_code)
An if condition then then_code else else_code statement.
bool can_cast_expr< code_fort >(const exprt &base)
code_landingpadt(const exprt &catch_expr)
void set_flavor(const irep_idt &f)
codet representation of a break statement (within a for or while loop).
const std::string & id2string(const irep_idt &d)
std::vector< codet > code_operandst
const code_gotot & to_code_goto(const codet &code)
const codet & code() const
bool can_cast_expr< code_try_catcht >(const exprt &base)
codet representation of a goto statement.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
code_declt(const symbol_exprt &symbol)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
codet representation of a label for branch targets.
code_push_catcht(const irep_idt &tag, const irep_idt &label)
void set_tag(const irep_idt &tag)
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
code_assumet(const exprt &expr)
An assumption, which must hold in subsequent code.
void set_nullable(bool nullable)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const code_labelt & to_code_label(const codet &code)
bool can_cast_expr< code_asmt >(const exprt &base)
const code_operandst & statements() const
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
bool can_cast_expr< code_ifthenelset >(const exprt &base)
static code_pop_catcht & to_code_pop_catch(codet &code)
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)
code_ifthenelset(const exprt &condition, const codet &then_code)
An if condition then then_code statement (no "else" case).
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
const code_dowhilet & to_code_dowhile(const codet &code)
exception_listt & exception_list()
const argumentst & arguments() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const exprt & cond() const
const codet & body() const
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
std::vector< exprt > operandst
exprt::operandst argumentst
const code_returnt & to_code_return(const codet &code)
code_switch_caset(const exprt &_case_op, const codet &_code)
void add(const codet &code)
code_try_catcht(const codet &_try_code)
A statement representing try _try_code catch ...
void set_label(const irep_idt &label)
void set_label(const irep_idt &label)
void set_statement(const irep_idt &statement)
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,...
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
A codet representing the removal of a local variable going out of scope.
bool can_cast_expr< code_assumet >(const exprt &base)
const irep_idt & get_label() const
const codet & get_catch_code(unsigned i) const
code_deadt(const symbol_exprt &symbol)
bool has_else_case() const
const exprt & catch_expr() const
const exception_listt & exception_list() const
const code_try_catcht & to_code_try_catch(const codet &code)
const irep_idt & get_statement() const
bool can_cast_expr< code_blockt >(const exprt &base)
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_label() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_asmt & to_code_asm(codet &code)
const exprt & value() const
bool can_cast_expr< code_whilet >(const exprt &base)
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
bool has_return_value() const
bool can_cast_expr< code_skipt >(const exprt &base)
side_effect_exprt(const irep_idt &statement, const typet &_type, const source_locationt &loc)
static code_landingpadt & to_code_landingpad(codet &code)
A codet representing a skip statement.
bool can_cast_expr< code_assignt >(const exprt &base)
codet representation of a "return from a function" statement.
A statement that catches an exception, assigning the exception in flight to an expression (e....
const symbol_exprt & symbol() const
bool can_cast_expr< code_declt >(const exprt &base)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & get(const irep_namet &name) const
code_function_callt(const exprt &_function, argumentst &&_arguments)
code_assertt(const exprt &expr)
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,...
std::vector< exception_list_entryt > exception_listt
codet representing a switch statement.
void set(const irep_namet &name, const irep_idt &value)
const codet & body() const
exprt::operandst & arguments()
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
code_switcht(const exprt &_value, const codet &_body)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
const codet & body() const
void set_destination(const irep_idt &label)
const codet & else_case() const
Templated functions to cast to specific exprt-derived classes.
bool can_cast_expr< code_switch_caset >(const exprt &base)
code_blockt(std::vector< codet > &&_statements)
const code_switcht & to_code_switch(const codet &code)
const irep_idt & get_destination() const
bool can_cast_expr< code_gotot >(const exprt &base)
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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...
const exprt & cond() const
bool can_cast_expr< code_landingpadt >(const exprt &base)
A side_effect_exprt representation of a side effect that throws an exception.
void add(codet code, const source_locationt &loc)
const code_blockt & to_code_block(const codet &code)
Base class for tree-like data structures with sharing.
bool can_cast_expr< code_assertt >(const exprt &base)
const exprt & expression() const
codet & find_last_statement()
void set_statement(const irep_idt &statement)
const irep_idt & get_identifier() const
code_whilet(const exprt &_cond, const codet &_body)
source_locationt & add_source_location()
const irep_idt & get_flavor() const
const codet & body() const
const exprt & return_value() const
A codet representing an assignment in the program.
const irep_idt & get_statement() const
const exprt & lhs() const
void reserve_operands(operandst::size_type n)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< code_breakt >(const exprt &base)
const code_continuet & to_code_continue(const codet &code)
const exprt & rhs() const
code_declt & get_catch_decl(unsigned i)
code_function_callt(const exprt &_function)
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
An expression containing a side effect.
code_dowhilet(const exprt &_cond, const codet &_body)
source_locationt end_location() const
side_effect_expr_nondett(const typet &_type, const source_locationt &loc)
bool can_cast_expr< code_push_catcht >(const exprt &base)
codet representation of an expression statement.
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
static code_push_catcht & to_code_push_catch(codet &code)
side_effect_expr_throwt(const irept &exception_list, const typet &type, const source_locationt &loc)
Data structure for representing an arbitrary statement in a program.
bool can_cast_expr< code_dowhilet >(const exprt &base)