10 #ifndef CPROVER_UTIL_STD_CODE_H
11 #define CPROVER_UTIL_STD_CODE_H
59 :
codet(statement, std::move(loc))
66 set(ID_statement, statement);
71 return get(ID_statement);
133 template<
typename Tag>
136 if(
const auto ptr = expr_try_dynamic_cast<codet>(expr))
138 return ptr->get_statement() == tag;
147 return base.
id()==ID_code;
156 return static_cast<const codet &
>(expr);
162 return static_cast<codet &
>(expr);
190 s.reserve(_list.size());
191 for(
const auto &c : _list)
197 :
codet(ID_block, (const std::vector<
exprt> &)_statements)
202 :
codet(ID_block, std::move((std::vector<
exprt> &&) _statements))
219 add(std::move(code));
237 for(
const auto &statement : code.
operands())
240 vm, code.
id() == ID_code,
"code block must be made up of codet");
301 :
codet(ID_assign, {std::move(
lhs), std::move(
rhs)})
306 :
codet(ID_assign, {std::move(
lhs), std::move(
rhs)}, std::move(loc))
335 vm, code.
operands().size() == 2,
"assignment must have two operands");
348 "lhs and rhs of assignment must have same type");
461 "declaration must have one or more operands");
464 code.
op0().
id() == ID_symbol,
465 "declaring a non-symbol: " +
525 "removal (code_deadt) must have one operand");
528 code.
op0().
id() == ID_symbol,
529 "removing a non-symbol: " +
id2string(code.
op0().
id()) +
"from scope");
681 std::vector<exprt> arguments,
728 std::vector<exprt> arguments,
782 {std::move(condition), std::move(then_code), std::move(else_code)})
790 {std::move(condition), std::move(then_code),
nil_exprt()})
806 return static_cast<const codet &
>(
op1());
816 return static_cast<const codet &
>(
op2());
867 :
codet(ID_switch, {std::move(_value), std::move(_body)})
929 :
codet(ID_while, {std::move(_cond), std::move(_body)})
991 :
codet(ID_dowhile, {std::move(_cond), std::move(_body)})
1012 return static_cast<codet &
>(
op1());
1102 return static_cast<codet &
>(
op3());
1166 set(ID_destination, label);
1171 return get(ID_destination);
1227 {std::move(_lhs), std::move(_function),
exprt(ID_arguments)})
1275 "function calls must have three operands:\n1) expression to store the "
1276 "returned values\n2) the function being called\n3) the vector of "
1287 if(code.
op0().
id() != ID_nil)
1291 "function returns expression of wrong type");
1408 :
codet(ID_label, {std::move(_code)})
1415 return get(ID_label);
1420 set(ID_label, label);
1425 return static_cast<codet &
>(
op0());
1430 return static_cast<const codet &
>(
op0());
1472 :
codet(ID_switch_case, {std::move(_case_op), std::move(_code)})
1483 return set(ID_default,
true);
1498 return static_cast<codet &
>(
op1());
1503 return static_cast<const codet &
>(
op1());
1547 ID_gcc_switch_case_range,
1548 {std::move(_lower), std::move(_upper), std::move(_code)})
1579 return static_cast<codet &
>(
op2());
1585 return static_cast<const codet &
>(
op2());
1711 return get(ID_flavor);
1737 return static_cast<const code_asmt &
>(code);
1843 :
codet(ID_expression, {std::move(expr)})
1903 :
exprt(ID_side_effect, std::move(_type), std::move(loc))
1913 :
exprt(ID_side_effect, std::move(_type), std::move(loc))
1920 return get(ID_statement);
1925 return set(ID_statement, statement);
1932 template<
typename Tag>
1935 if(
const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1937 return ptr->get_statement() == tag;
1946 return base.
id()==ID_side_effect;
1976 set(ID_is_nondet_nullable, nullable);
1981 return get_bool(ID_is_nondet_nullable);
1997 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
2005 PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
2031 {std::move(_lhs), std::move(_rhs)},
2067 PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2075 PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2089 ID_statement_expression,
2119 side_effect_expr_statement_expression.get_statement() ==
2120 ID_statement_expression);
2122 side_effect_expr_statement_expression);
2130 side_effect_expr_statement_expression.get_statement() ==
2131 ID_statement_expression);
2133 side_effect_expr_statement_expression);
2147 {std::move(_function),
2206 irept exception_list,
2211 set(ID_exception_list, std::move(exception_list));
2255 set(ID_exception_list,
irept(ID_exception_list));
2273 set(ID_label, label);
2287 set(ID_label, label);
2291 return get(ID_label);
2300 codet(ID_push_catch)
2302 set(ID_exception_list,
irept(ID_exception_list));
2436 :
codet(ID_try_catch, {std::move(_try_code)})
2442 return static_cast<codet &
>(
op0());
2447 return static_cast<const codet &
>(
op0());
2519 const std::vector<irep_idt> ¶meter_identifiers,
2521 :
codet(ID_function_body, {std::move(_block)})
2550 code.
operands().size() == 1,
"code_function_body must have one operand");
2558 code.
operands().size() == 1,
"code_function_body must have one operand");
codet representation of an inline assembler statement, for the gcc flavor.
const exprt & asm_text() const
const exprt & clobbers() const
const exprt & inputs() const
const exprt & labels() const
const exprt & outputs() 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
A codet representing an assignment in the program.
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const exprt & rhs() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & lhs() const
code_assignt(exprt lhs, exprt rhs, source_locationt loc)
code_assignt(exprt lhs, exprt rhs)
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
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)
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)
const code_operandst & statements() const
void add(const codet &code)
code_operandst & statements()
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
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).
A codet representing the removal of a local variable going out of scope.
code_deadt(symbol_exprt symbol)
const irep_idt & get_identifier() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const symbol_exprt & symbol() const
A codet representing the declaration of a local variable.
const irep_idt & get_identifier() const
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
optionalt< 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)
code_declt(symbol_exprt symbol)
const symbol_exprt & symbol() const
codet representation of a do while statement.
const exprt & cond() const
code_dowhilet(exprt _cond, codet _body)
const codet & body() const
codet representation of an expression statement.
code_expressiont(exprt expr)
const exprt & expression() const
codet representation of a for statement.
const exprt & init() const
const exprt & iter() 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 & cond() const
const codet & body() const
This class is used to interface between a language frontend and goto-convert – it communicates the id...
const code_blockt & block() const
code_function_bodyt(const std::vector< irep_idt > ¶meter_identifiers, code_blockt _block)
std::vector< irep_idt > get_parameter_identifiers() const
void set_parameter_identifiers(const std::vector< irep_idt > &)
codet representation of a function call statement.
const argumentst & arguments() const
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
code_function_callt(exprt _function)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & lhs() const
code_function_callt(exprt _function, argumentst _arguments)
code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
exprt::operandst argumentst
codet representation of a switch-case, i.e. a case statement within a switch.
codet & code()
the statement to be executed when the case applies
const exprt & lower() const
lower bound of range
exprt & upper()
upper bound of range
code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)
const codet & code() const
the statement to be executed when the case applies
const exprt & upper() const
upper bound of range
exprt & lower()
lower bound of range
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.
const codet & then_case() const
code_ifthenelset(exprt condition, codet then_code)
An if condition then then_code statement (no "else" case).
const exprt & cond() const
code_ifthenelset(exprt condition, codet then_code, codet else_code)
An if condition then then_code else else_code statement.
const codet & else_case() const
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)
A codet representing the declaration that an output of a particular description has a value which cor...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
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)
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
void set_label(const irep_idt &label)
const irep_idt & get_tag() const
const irep_idt & get_label() const
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
std::vector< exception_list_entryt > exception_listt
code_push_catcht(const irep_idt &tag, const irep_idt &label)
exception_listt & exception_list()
const exception_listt & exception_list() const
codet representation of a "return from a function" statement.
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & return_value() const
bool has_return_value() const
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
const codet & code() const
code_switch_caset(exprt _case_op, codet _code)
codet representing a switch statement.
code_switcht(exprt _value, codet _body)
const exprt & value() const
const codet & body() const
codet representation of a try/catch block.
codet & get_catch_code(unsigned i)
const codet & get_catch_code(unsigned i) const
code_try_catcht(codet _try_code)
A statement representing try _try_code catch ...
const code_declt & get_catch_decl(unsigned i) const
code_declt & get_catch_decl(unsigned i)
void add_catch(const code_declt &to_catch, const codet &code_catch)
const codet & try_code() const
const typet & return_type() const
codet representing a while statement.
const exprt & cond() const
code_whilet(exprt _cond, codet _body)
const codet & body() const
Data structure for representing an arbitrary statement in a program.
codet(const irep_idt &statement, source_locationt loc)
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)
codet(const irep_idt &statement)
codet(const irep_idt &statement, operandst op, source_locationt loc)
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
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,...
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
void set_statement(const irep_idt &statement)
const irep_idt & get_statement() const
static void check(const codet &, const validation_modet)
Check that the code statement is well-formed (shallow checks only, i.e., enclosed statements,...
codet(const irep_idt &statement, operandst _op)
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
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
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.
void set(const irep_namet &name, const irep_idt &value)
bool get_bool(const irep_namet &name) const
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
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 & lhs() const
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
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()
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.
Templated functions to cast to specific exprt-derived classes.
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)
nonstd::optional< T > optionalt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
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)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
bool can_cast_expr< code_switcht >(const exprt &base)
bool can_cast_expr< code_switch_caset >(const exprt &base)
bool can_cast_expr< code_asmt >(const exprt &base)
const code_returnt & to_code_return(const codet &code)
bool can_cast_expr< codet >(const exprt &base)
bool can_cast_expr< code_function_callt >(const exprt &base)
bool can_cast_expr< code_expressiont >(const exprt &base)
bool can_cast_expr< code_landingpadt >(const exprt &base)
static code_landingpadt & to_code_landingpad(codet &code)
static code_pop_catcht & to_code_pop_catch(codet &code)
bool can_cast_expr< code_inputt >(const exprt &base)
const code_gotot & to_code_goto(const codet &code)
const code_whilet & to_code_while(const codet &code)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
const code_continuet & to_code_continue(const codet &code)
const code_function_bodyt & to_code_function_body(const codet &code)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assumet & to_code_assume(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)
const code_switch_caset & to_code_switch_case(const codet &code)
bool can_cast_expr< code_try_catcht >(const exprt &base)
bool can_cast_expr< code_outputt >(const exprt &base)
const code_labelt & to_code_label(const codet &code)
bool can_cast_expr< code_assignt >(const exprt &base)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
bool can_cast_expr< code_declt >(const exprt &base)
const codet & to_code(const exprt &expr)
void validate_expr(const code_assignt &x)
bool can_cast_expr< code_assertt >(const exprt &base)
const code_dowhilet & to_code_dowhile(const codet &code)
bool can_cast_expr< code_skipt >(const exprt &base)
const code_switcht & to_code_switch(const codet &code)
const code_declt & to_code_decl(const codet &code)
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
bool can_cast_expr< code_returnt >(const exprt &base)
bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)
bool can_cast_expr< code_asm_gcct >(const exprt &base)
code_expressiont & to_code_expression(codet &code)
bool can_cast_expr< code_gotot >(const exprt &base)
const code_breakt & to_code_break(const codet &code)
bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)
static code_push_catcht & to_code_push_catch(codet &code)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
bool can_cast_expr< code_whilet >(const exprt &base)
bool can_cast_expr< code_continuet >(const exprt &base)
const code_blockt & to_code_block(const codet &code)
const code_deadt & to_code_dead(const codet &code)
const code_assertt & to_code_assert(const codet &code)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
bool can_cast_expr< code_push_catcht >(const exprt &base)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
bool can_cast_expr< code_fort >(const exprt &base)
bool can_cast_expr< code_deadt >(const exprt &base)
bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)
code_asm_gcct & to_code_asm_gcc(codet &code)
const code_fort & to_code_for(const codet &code)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
bool can_cast_expr< code_labelt >(const exprt &base)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
bool can_cast_expr< code_pop_catcht >(const exprt &base)
const code_function_callt & to_code_function_call(const codet &code)
const code_try_catcht & to_code_try_catch(const codet &code)
code_asmt & to_code_asm(codet &code)
const code_assignt & to_code_assign(const codet &code)
bool can_cast_expr< code_assumet >(const exprt &base)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
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...
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,...
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...