10#ifndef CPROVER_UTIL_STD_CODE_H
11#define CPROVER_UTIL_STD_CODE_H
66 vm, code.
operands().size() == 2,
"assignment must have two operands");
79 "lhs and rhs of assignment must have same type");
152 s.reserve(
_list.size());
153 for(
const auto &
c :
_list)
181 add(std::move(code));
409 "declaration must have one or more operands");
413 "declaring a non-symbol: " +
490 return static_cast<const codet &
>(
op1());
500 return static_cast<const codet &
>(
op2());
984 return static_cast<const codet &
>(
op0());
1052 return static_cast<codet &
>(
op1());
1057 return static_cast<const codet &
>(
op1());
1102 {std::move(
_lower), std::move(
_upper), std::move(_code)})
1133 return static_cast<codet &
>(
op2());
1139 return static_cast<const codet &
>(
op2());
1291 return static_cast<const code_asmt &
>(code);
1486template<
typename Tag>
1491 return ptr->get_statement() == tag;
1585 {std::move(
_lhs), std::move(
_rhs)},
1760 irept exception_list,
1996 return static_cast<codet &
>(
op0());
2001 return static_cast<const codet &
>(
op0());
2073 const std::vector<irep_idt> ¶meter_identifiers,
2104 code.
operands().size() == 1,
"code_function_body must have one operand");
2112 code.
operands().size() == 1,
"code_function_body must have one operand");
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
codet representation of an inline assembler statement, for the gcc flavor.
const exprt & asm_text() const
const exprt & labels() const
const exprt & outputs() const
const exprt & inputs() const
const exprt & clobbers() const
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
void set_flavor(const irep_idt &f)
A non-fatal assertion, which checks a condition then permits execution to continue.
const exprt & assertion() const
An assumption, which must hold in subsequent code.
const exprt & assumption() const
A codet representing sequential composition of program statements.
static code_blockt from_list(const std::list< codet > &_list)
code_operandst & statements()
source_locationt end_location() const
void add(codet code, source_locationt loc)
code_blockt(std::vector< codet > &&_statements)
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
code_blockt(const std::vector< codet > &_statements)
void add(const codet &code)
const code_operandst & statements() const
std::vector< codet > code_operandst
codet & find_last_statement()
codet representation of a break statement (within a for or while loop).
codet representation of a continue statement (within a for or while loop).
codet representation of a do while statement.
code_dowhilet(exprt _cond, codet _body)
const codet & body() const
const exprt & cond() const
codet representation of an expression statement.
code_expressiont(exprt expr)
const exprt & expression() const
codet representation of a for statement.
const exprt & cond() const
code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)
A statement describing a for loop with initializer _init, loop condition _cond, increment _iter,...
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 & iter() const
const codet & body() const
const exprt & init() const
A codet representing an assignment in the program.
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
code_frontend_assignt(exprt lhs, exprt rhs)
const exprt & lhs() const
const exprt & rhs() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_frontend_assignt(exprt lhs, exprt rhs, source_locationt loc)
A codet representing the declaration of a local variable.
code_frontend_declt(symbol_exprt symbol)
const symbol_exprt & symbol() const
void set_initial_value(std::optional< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
std::optional< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get_identifier() const
codet representation of a "return from a function" statement.
const exprt & return_value() const
bool has_return_value() const
code_frontend_returnt(exprt _op)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
This class is used to interface between a language frontend and goto-convert – it communicates the id...
code_function_bodyt(const std::vector< irep_idt > ¶meter_identifiers, code_blockt _block)
std::vector< irep_idt > get_parameter_identifiers() const
const code_blockt & block() const
void set_parameter_identifiers(const std::vector< irep_idt > &)
codet representation of a switch-case, i.e. a case statement within a switch.
const codet & code() const
the statement to be executed when the case applies
const exprt & upper() const
upper bound of range
code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)
const exprt & lower() const
lower bound of range
exprt & lower()
lower bound of range
exprt & upper()
upper bound of range
codet & code()
the statement to be executed when the case applies
codet representation of a goto statement.
const irep_idt & get_destination() const
code_gotot(const irep_idt &label)
void set_destination(const irep_idt &label)
codet representation of an if-then-else statement.
code_ifthenelset(exprt condition, codet then_code)
An if condition then then_code statement (no "else" case).
const exprt & cond() const
const codet & else_case() const
const codet & then_case() const
code_ifthenelset(exprt condition, codet then_code, codet else_code)
An if condition then then_code else else_code statement.
bool has_else_case() const
codet representation of a label for branch targets.
const irep_idt & get_label() const
code_labelt(const irep_idt &_label, codet _code)
const codet & code() const
void set_label(const irep_idt &label)
A statement that catches an exception, assigning the exception in flight to an expression (e....
const exprt & catch_expr() const
code_landingpadt(exprt catch_expr)
Pops an exception handler from the stack of active handlers (i.e.
void set_tag(const irep_idt &tag)
exception_list_entryt(const irep_idt &tag)
const irep_idt & get_label() const
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
const irep_idt & get_tag() const
void set_label(const irep_idt &label)
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
exception_listt & exception_list()
std::vector< exception_list_entryt > exception_listt
const exception_listt & exception_list() const
code_push_catcht(const irep_idt &tag, const irep_idt &label)
A codet representing a skip statement.
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & case_op() const
code_switch_caset(exprt _case_op, codet _code)
const codet & code() const
codet representing a switch statement.
code_switcht(exprt _value, codet _body)
const codet & body() const
const exprt & value() const
codet representation of a try/catch block.
const code_frontend_declt & get_catch_decl(unsigned i) const
const codet & try_code() const
code_frontend_declt & get_catch_decl(unsigned i)
code_try_catcht(codet _try_code)
A statement representing try _try_code catch ...
void add_catch(code_frontend_declt &&to_catch, codet &&code_catch)
codet & get_catch_code(unsigned i)
const codet & get_catch_code(unsigned i) const
codet representing a while statement.
code_whilet(exprt _cond, codet _body)
const exprt & cond() const
const codet & body() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
A base class for multi-ary expressions Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A side_effect_exprt that performs an assignment.
const exprt & rhs() const
side_effect_expr_assignt(exprt _lhs, exprt _rhs, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
const exprt & lhs() 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
A side_effect_exprt representation of a function call side effect.
side_effect_expr_function_callt(exprt _function, exprt::operandst _arguments, typet _type, source_locationt loc)
const exprt::operandst & arguments() const
exprt::operandst & arguments()
const exprt & function() const
A side_effect_exprt that returns a non-deterministically chosen value.
void set_nullable(bool nullable)
bool get_nullable() const
side_effect_expr_nondett(typet _type, source_locationt loc)
A side_effect_exprt that contains a statement.
const codet & statement() const
side_effect_expr_statement_expressiont(codet _code, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
A side_effect_exprt representation of a side effect that throws an exception.
side_effect_expr_throwt(irept exception_list, typet type, source_locationt loc)
An expression containing a side effect.
void set_statement(const irep_idt &statement)
const irep_idt & get_statement() const
side_effect_exprt(const irep_idt &statement, operandst _operands, typet _type, source_locationt loc)
side_effect_exprt(const irep_idt &statement, typet _type, source_locationt loc)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The type of an expression, extends irept.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const std::string & id2string(const irep_idt &d)
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
side_effect_exprt & to_side_effect_expr(exprt &expr)
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.
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
bool can_cast_expr< code_ifthenelset >(const exprt &base)
bool can_cast_expr< code_switcht >(const exprt &base)
const code_breakt & to_code_break(const codet &code)
const code_switch_caset & to_code_switch_case(const codet &code)
bool can_cast_expr< code_switch_caset >(const exprt &base)
bool can_cast_expr< code_asmt >(const exprt &base)
const code_function_bodyt & to_code_function_body(const codet &code)
bool can_cast_expr< code_expressiont >(const exprt &base)
bool can_cast_expr< code_landingpadt >(const exprt &base)
bool can_cast_expr< code_frontend_assignt >(const exprt &base)
const code_gotot & to_code_goto(const codet &code)
const code_assertt & to_code_assert(const codet &code)
bool can_cast_expr< code_blockt >(const exprt &base)
bool can_cast_expr< code_breakt >(const exprt &base)
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
bool can_cast_expr< code_dowhilet >(const exprt &base)
static code_push_catcht & to_code_push_catch(codet &code)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
bool can_cast_expr< code_try_catcht >(const exprt &base)
bool can_cast_expr< code_frontend_returnt >(const exprt &base)
code_asm_gcct & to_code_asm_gcc(codet &code)
static code_landingpadt & to_code_landingpad(codet &code)
const code_frontend_returnt & to_code_frontend_return(const codet &code)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const code_dowhilet & to_code_dowhile(const codet &code)
static code_pop_catcht & to_code_pop_catch(codet &code)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
const code_assumet & to_code_assume(const codet &code)
bool can_cast_expr< code_assertt >(const exprt &base)
const code_whilet & to_code_while(const codet &code)
bool can_cast_expr< code_skipt >(const exprt &base)
bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)
bool can_cast_expr< code_asm_gcct >(const exprt &base)
bool can_cast_expr< code_frontend_declt >(const exprt &base)
bool can_cast_expr< code_gotot >(const exprt &base)
bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)
const code_labelt & to_code_label(const codet &code)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
const code_blockt & to_code_block(const codet &code)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
void validate_expr(const code_frontend_assignt &x)
bool can_cast_expr< code_whilet >(const exprt &base)
bool can_cast_expr< code_continuet >(const exprt &base)
const code_frontend_assignt & to_code_frontend_assign(const codet &code)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
code_asmt & to_code_asm(codet &code)
bool can_cast_expr< code_push_catcht >(const exprt &base)
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
const code_fort & to_code_for(const codet &code)
bool can_cast_expr< code_fort >(const exprt &base)
const code_switcht & to_code_switch(const codet &code)
const code_try_catcht & to_code_try_catch(const codet &code)
bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)
const code_frontend_declt & to_code_frontend_decl(const codet &code)
code_expressiont & to_code_expression(codet &code)
bool can_cast_expr< code_labelt >(const exprt &base)
bool can_cast_expr< code_pop_catcht >(const exprt &base)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
const code_continuet & to_code_continue(const codet &code)
bool can_cast_expr< code_assumet >(const exprt &base)
const codet & to_code(const exprt &expr)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
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...