9 #ifndef CPROVER_CPROVER_STATE_H
10 #define CPROVER_CPROVER_STATE_H
461 ID_state_live_object,
523 ID_state_writeable_object,
701 ID_state_is_dynamic_object,
765 ID_state_object_size,
885 expr.
id() == ID_state_r_ok || expr.
id() == ID_state_w_ok ||
886 expr.
id() == ID_state_rw_ok);
896 expr.
id() == ID_state_r_ok || expr.
id() == ID_state_w_ok ||
897 expr.
id() == ID_state_rw_ok);
909 ID_state_type_compatible,
983 ID_enter_scope_state,
1023 const exprt &size()
const
1066 ID_exit_scope_state,
1101 const exprt &size()
const
void validate_expr(const shuffle_vector_exprt &value)
allocate_exprt(exprt state, exprt size, pointer_typet type)
allocate_exprt with_state(exprt state) const
const exprt & state() const
const exprt & size() const
allocate_state_exprt(exprt state, exprt size)
const exprt & state() const
const exprt & size() const
A base class for binary expressions.
const exprt & op2() const =delete
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
const exprt & address() const
deallocate_state_exprt(exprt state, exprt address)
const exprt & state() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const exprt & address() const
typet object_type() const
const exprt & state() const
symbol_exprt symbol() const
enter_scope_state_exprt(exprt state, exprt address)
const exprt & state() const
evaluate_exprt(exprt state, exprt address)
evaluate_exprt with_state(exprt state) const
const exprt & address() const
evaluate_exprt(exprt state, exprt address, typet type)
exit_scope_state_exprt(exprt state, exprt address)
const exprt & state() const
symbol_exprt symbol() const
const exprt & address() const
Base class for all expressions.
typet & type()
Return the type of the expression.
initial_state_exprt(exprt state)
const exprt & state() const
const irep_idt & id() const
A type for mathematical functions (do not confuse with functions/methods in code)
symbol_exprt object_expr() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const exprt & address() const
const exprt & state() const
const exprt & size() const
reallocate_exprt(exprt state, exprt address, exprt size, pointer_typet type)
const exprt & size() const
const exprt & address() const
reallocate_state_exprt(exprt state, exprt address, exprt size)
const exprt & state() const
const exprt & address() const
const exprt & state() const
state_cstrlen_exprt(exprt state, exprt address, typet type)
state_cstrlen_exprt with_state(exprt state) const
const exprt & address() const
const exprt & state() const
state_is_cstring_exprt(exprt state, exprt address)
state_is_cstring_exprt with_state(exprt state) const
const exprt & address() const
state_is_dynamic_object_exprt(exprt state, exprt address)
state_is_dynamic_object_exprt with_state(exprt state) const
const exprt & state() const
state_live_object_exprt(exprt state, exprt address)
const exprt & state() const
const exprt & address() const
state_live_object_exprt with_state(exprt state) const
const exprt & address() const
state_object_size_exprt with_state(exprt state) const
state_object_size_exprt(exprt state, exprt address, typet type)
const exprt & state() const
const exprt & address() const
state_ok_exprt with_state(exprt state) const
const exprt & state() const
const exprt & size() const
state_ok_exprt(irep_idt id, exprt state, exprt address, exprt size)
const exprt & address() const
state_type_compatible_exprt with_state(exprt state) const
const exprt & state() const
state_type_compatible_exprt(exprt state, exprt address)
const typet & access_type() const
const exprt & state() const
const exprt & address() const
state_writeable_object_exprt(exprt state, exprt address)
Expression to hold a symbol (variable)
An expression with three operands.
The type of an expression, extends irept.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
update_state_exprt with_state(exprt state) const
const exprt & state() const
update_state_exprt(exprt state, exprt address, exprt new_value)
const exprt & new_value() const
const exprt & address() const
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
#define PRECONDITION(CONDITION)
const state_type_compatible_exprt & to_state_type_compatible_expr(const exprt &expr)
Cast an exprt to a state_type_compatible_exprt.
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
const state_cstrlen_exprt & to_state_cstrlen_expr(const exprt &expr)
Cast an exprt to a state_cstrlen_exprt.
const reallocate_exprt & to_reallocate_expr(const exprt &expr)
Cast an exprt to a reallocate_exprt.
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
static symbol_exprt state_expr()
const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr(const exprt &expr)
Cast an exprt to a state_is_dynamic_object_exprt.
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
const state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
const initial_state_exprt & to_initial_state_expr(const exprt &expr)
Cast an exprt to a initial_state_exprt.
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
const reallocate_state_exprt & to_reallocate_state_expr(const exprt &expr)
Cast an exprt to a reallocate_state_exprt.
const state_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
const exit_scope_state_exprt & to_exit_scope_state_expr(const exprt &expr)
Cast an exprt to a exit_scope_state_exprt.
const enter_scope_state_exprt & to_enter_scope_state_expr(const exprt &expr)
Cast an exprt to a enter_scope_state_exprt.
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
const allocate_state_exprt & to_allocate_state_expr(const exprt &expr)
Cast an exprt to a allocate_state_exprt.
static mathematical_function_typet state_predicate_type()