Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_STD_CODE_H
11 #define CPROVER_UTIL_STD_CODE_H
61 :
codet(statement, std::move(loc))
68 set(ID_statement, statement);
73 return get(ID_statement);
135 template<
typename Tag>
138 if(
const auto ptr = expr_try_dynamic_cast<codet>(expr))
140 return ptr->get_statement() == tag;
149 return base.
id()==ID_code;
158 return static_cast<const codet &
>(expr);
164 return static_cast<codet &
>(expr);
192 s.reserve(_list.size());
193 for(
const auto &c : _list)
199 :
codet(ID_block, (const std::vector<
exprt> &)_statements)
204 :
codet(ID_block, std::move((std::vector<
exprt> &&) _statements))
221 add(std::move(code));
239 for(
const auto &statement : code.
operands())
242 vm, code.
id() == ID_code,
"code block must be made up of codet");
303 :
codet(ID_assign, {std::move(
lhs), std::move(
rhs)})
308 :
codet(ID_assign, {std::move(
lhs), std::move(
rhs)}, std::move(loc))
337 vm, code.
operands().size() == 2,
"assignment must have two operands");
350 "lhs and rhs of assignment must have same type");
431 "declaration must have one or more operands");
434 code.
op0().
id() == ID_symbol,
435 "declaring a non-symbol: " +
495 "removal (code_deadt) must have one operand");
498 code.
op0().
id() == ID_symbol,
499 "removing a non-symbol: " +
id2string(code.
op0().
id()) +
"from scope");
651 std::vector<exprt> arguments,
698 std::vector<exprt> arguments,
752 {std::move(condition), std::move(then_code), std::move(else_code)})
760 {std::move(condition), std::move(then_code),
nil_exprt()})
776 return static_cast<const codet &
>(
op1());
786 return static_cast<const codet &
>(
op2());
837 :
codet(ID_switch, {std::move(_value), std::move(_body)})
899 :
codet(ID_while, {std::move(_cond), std::move(_body)})
961 :
codet(ID_dowhile, {std::move(_cond), std::move(_body)})
1072 return static_cast<codet &
>(
op3());
1136 set(ID_destination, label);
1141 return get(ID_destination);
1197 {std::move(_lhs), std::move(_function),
exprt(ID_arguments)})
1245 "function calls must have three operands:\n1) expression to store the "
1246 "returned values\n2) the function being called\n3) the vector of "
1257 if(code.
op0().
id() != ID_nil)
1261 "function returns expression of wrong type");
1378 :
codet(ID_label, {std::move(_code)})
1385 return get(ID_label);
1390 set(ID_label, label);
1395 return static_cast<codet &
>(
op0());
1400 return static_cast<const codet &
>(
op0());
1442 :
codet(ID_switch_case, {std::move(_case_op), std::move(_code)})
1453 return set(ID_default,
true);
1468 return static_cast<codet &
>(
op1());
1473 return static_cast<const codet &
>(
op1());
1517 ID_gcc_switch_case_range,
1518 {std::move(_lower), std::move(_upper), std::move(_code)})
1549 return static_cast<codet &
>(
op2());
1555 return static_cast<const codet &
>(
op2());
1681 return get(ID_flavor);
1707 return static_cast<const code_asmt &
>(code);
1813 :
codet(ID_expression, {std::move(expr)})
1869 SINCE(2018, 8, 9,
"use side_effect_exprt(statement, type, loc) instead"))
1871 :
exprt(ID_side_effect, _type)
1882 :
exprt(ID_side_effect, std::move(_type), std::move(loc))
1892 :
exprt(ID_side_effect, std::move(_type), std::move(loc))
1899 return get(ID_statement);
1904 return set(ID_statement, statement);
1911 template<
typename Tag>
1914 if(
const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1916 return ptr->get_statement() == tag;
1925 return base.
id()==ID_side_effect;
1955 set(ID_is_nondet_nullable, nullable);
1960 return get_bool(ID_is_nondet_nullable);
1976 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1984 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
2010 {std::move(_lhs), std::move(_rhs)},
2046 PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2054 PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2068 ID_statement_expression,
2098 side_effect_expr_statement_expression.get_statement() ==
2099 ID_statement_expression);
2101 side_effect_expr_statement_expression);
2109 side_effect_expr_statement_expression.get_statement() ==
2110 ID_statement_expression);
2112 side_effect_expr_statement_expression);
2123 "use side_effect_expr_function_callt("
2124 "function, arguments, type, loc) instead"))
2126 const
exprt &_function,
2132 op1().
id(ID_arguments);
2133 function() = _function;
2144 {std::move(_function),
2203 irept exception_list,
2208 set(ID_exception_list, std::move(exception_list));
2252 set(ID_exception_list,
irept(ID_exception_list));
2270 set(ID_label, label);
2284 set(ID_label, label);
2288 return get(ID_label);
2297 codet(ID_push_catch)
2299 set(ID_exception_list,
irept(ID_exception_list));
2433 :
codet(ID_try_catch, {std::move(_try_code)})
2439 return static_cast<codet &
>(
op0());
2444 return static_cast<const codet &
>(
op0());
2516 const std::vector<irep_idt> ¶meter_identifiers,
2518 :
codet(ID_function_body, {std::move(_block)})
2547 code.
operands().size() == 1,
"code_function_body must have one operand");
2555 code.
operands().size() == 1,
"code_function_body must have one operand");
2559 #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.
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const exprt & case_op() const
side_effect_expr_assignt(const exprt &_lhs, const exprt &_rhs, const source_locationt &loc)
construct an assignment side-effect, given lhs and rhs The type is copied from lhs
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_switch_caset(exprt _case_op, codet _code)
void set_parameter_identifiers(const std::vector< irep_idt > &)
A base class for multi-ary expressions Associativity is not specified.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
codet representation of an inline assembler statement, for the gcc flavor.
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)
const exprt & lhs() const
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
bool can_cast_expr< code_inputt >(const exprt &base)
const exprt & clobbers() const
code_expressiont(exprt expr)
const exprt & cond() const
const symbol_exprt & symbol() const
codet representing a while statement.
const code_declt & to_code_decl(const codet &code)
code_function_callt(exprt _function, argumentst _arguments)
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
codet representation of an inline assembler statement.
code_try_catcht(codet _try_code)
A statement representing try _try_code catch ...
exprt & lower()
lower bound of range
side_effect_exprt(const irep_idt &statement, operandst _operands, typet _type, source_locationt loc)
constructor with operands
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)
std::size_t size() const
Amount of nodes this expression tree contains.
The type of an expression, extends irept.
const codet & then_case() const
code_assignt(exprt lhs, exprt rhs)
const exprt & upper() const
upper bound of range
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)
const code_function_bodyt & to_code_function_body(const codet &code)
const codet & code() const
A side_effect_exprt representation of a function call side effect.
codet & get_catch_code(unsigned i)
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
side_effect_expr_assignt(exprt _lhs, exprt _rhs, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
side_effect_expr_function_callt(exprt _function, exprt::operandst _arguments, typet _type, source_locationt loc)
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)
bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)
const exprt & assumption() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Base class for all expressions.
const exprt & iter() const
This class is used to interface between a language frontend and goto-convert – it communicates the id...
code_switcht(exprt _value, codet _body)
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)
const codet & statement() const
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)
codet representation of a switch-case, i.e. a case statement within a switch.
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 codet & code() const
the statement to be executed when the case applies
codet(const irep_idt &statement, operandst _op)
const irep_idt & get_identifier() const
bool can_cast_expr< code_deadt >(const exprt &base)
const code_fort & to_code_for(const codet &code)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
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 exprt & lower() const
lower bound of range
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)
side_effect_expr_statement_expressiont(codet _code, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
code_ifthenelset(exprt condition, codet then_code, codet else_code)
An if condition then then_code else else_code statement.
code_operandst & statements()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A codet representing the declaration that an output of a particular description has a value which cor...
code_deadt(symbol_exprt symbol)
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(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const codet & try_code() const
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.
const exprt & rhs() const
bool get_bool(const irep_namet &name) const
bool get_nullable() const
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
bool can_cast_expr< code_labelt >(const exprt &base)
bool can_cast_expr< code_continuet >(const exprt &base)
std::vector< irep_idt > get_parameter_identifiers() const
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
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
bool can_cast_expr< code_fort >(const exprt &base)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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
codet & code()
the statement to be executed when the case applies
const code_gotot & to_code_goto(const codet &code)
const codet & code() const
bool can_cast_expr< code_try_catcht >(const exprt &base)
bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)
codet representation of a goto statement.
const code_ifthenelset & to_code_ifthenelse(const codet &code)
codet representation of a label for branch targets.
#define PRECONDITION(CONDITION)
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
void add(codet code, source_locationt loc)
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)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
A side_effect_exprt that performs an assignment.
bool can_cast_expr< code_asm_gcct >(const exprt &base)
const code_dowhilet & to_code_dowhile(const codet &code)
exception_listt & exception_list()
const argumentst & arguments() const
bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const exprt & cond() const
const exprt & labels() const
const codet & body() const
const irep_idt & id() const
code_assignt(exprt lhs, exprt rhs, source_locationt loc)
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)
void add(const codet &code)
code_asm_gcct & to_code_asm_gcc(codet &code)
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)
code_labelt(const irep_idt &_label, codet _code)
codet(const irep_idt &statement, source_locationt loc)
A codet representing the removal of a local variable going out of scope.
code_dowhilet(exprt _cond, codet _body)
code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
#define SINCE(year, month, day, msg)
A side_effect_exprt that contains a statement.
nonstd::optional< T > optionalt
bool can_cast_expr< code_assumet >(const exprt &base)
const irep_idt & get_label() const
side_effect_expr_throwt(irept exception_list, typet type, source_locationt loc)
const codet & get_catch_code(unsigned i) const
bool has_else_case() const
code_ifthenelset(exprt condition, codet then_code)
An if condition then then_code statement (no "else" case).
const exprt & catch_expr() const
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
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)
code_function_callt(exprt _function)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_label() const
const exprt & inputs() 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)
bool has_return_value() const
bool can_cast_expr< code_skipt >(const exprt &base)
code_declt(symbol_exprt symbol)
static code_landingpadt & to_code_landingpad(codet &code)
bool can_cast_expr< code_outputt >(const exprt &base)
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
side_effect_exprt(const irep_idt &statement, typet _type, source_locationt loc)
bool can_cast_expr< code_declt >(const exprt &base)
const code_assignt & to_code_assign(const codet &code)
code_landingpadt(exprt catch_expr)
const irep_idt & get(const irep_namet &name) const
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
const exprt & asm_text() const
exprt::operandst & arguments()
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
const codet & body() const
void set_destination(const irep_idt &label)
code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)
A statement describing a for loop with initializer _init, loop condition _cond, increment _iter,...
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
const code_blockt & block() const
exprt & upper()
upper bound of range
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.
code_whilet(exprt _cond, codet _body)
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...
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
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.
const typet & return_type() const
const code_blockt & to_code_block(const codet &code)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
code_function_bodyt(const std::vector< irep_idt > ¶meter_identifiers, code_blockt _block)
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
source_locationt & add_source_location()
const irep_idt & get_flavor() const
const codet & body() const
const exprt & outputs() const
const exprt & return_value() const
A codet representing an assignment in the program.
const irep_idt & get_statement() const
const exprt & lhs() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< code_breakt >(const exprt &base)
API to expression classes.
const code_continuet & to_code_continue(const codet &code)
const exprt & rhs() const
code_declt & get_catch_decl(unsigned i)
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
codet(const irep_idt &statement, operandst op, source_locationt loc)
An expression containing a side effect.
source_locationt end_location() const
bool can_cast_expr< code_push_catcht >(const exprt &base)
codet representation of an expression statement.
side_effect_expr_nondett(typet _type, source_locationt loc)
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
static code_push_catcht & to_code_push_catch(codet &code)
Data structure for representing an arbitrary statement in a program.
bool can_cast_expr< code_dowhilet >(const exprt &base)