34 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
49 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
60 std::cout <<
"E: " <<
format(evaluate_expr.
address()) <<
"\n";
61 std::cout <<
"T: " <<
format(evaluate_expr.
address().type()) <<
"\n";
71 std::cout <<
"M: ?\n";
203 return std::move(src);
222 auto symbol_expr =
symbol_exprt(identifier, object_type);
225 return std::move(evaluate_expr);
234 return std::move(evaluate_expr);
312 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
315 const auto &pointer = src.
address();
326 else if(identifier ==
"return_value")
336 const auto &symbol = ns.
lookup(identifier);
337 if(symbol.is_static_lifetime)
423 return std::move(src);
430 const auto &pointer = src.
address();
447 const auto &symbol = ns.
lookup(identifier);
457 return std::move(src);
460 return std::move(src);
465 const auto &pointer = src.
address();
494 return std::move(src);
501 const auto &pointer = src.
address();
512 return std::move(src);
522 return std::move(src);
527 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
530 auto &state = src.
state();
532 auto &size = src.
size();
582 return std::move(src);
623 return std::move(src);
627static bool is_one(
const exprt &src)
661 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
665 const auto &state = src.
state();
666 const auto &pointer = src.
address();
754 return std::move(src);
759 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
762 const auto &state = src.
state();
763 const auto &pointer = src.
address();
833 return std::move(src);
838 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
842 const auto &state = src.
state();
843 const auto &head = src.
head();
844 const auto &tail = src.
tail();
869 if(update_type != src.
head().type())
891 return std::move(src);
896 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
921 return std::move(
sum);
942 return std::move(src);
947 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
955 return std::move(src);
960 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
1086 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
unsignedbv_typet size_type()
bitvector_typet char_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
allocate_exprt with_state(exprt state) const
const exprt & state() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Operator to return the address of an array element relative to a base address.
const exprt & address() const
const exprt & state() const
evaluate_exprt with_state(exprt state) const
Base class for all expressions.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
The trinary if-then-else operator.
const irep_idt & id() const
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Operator to return the address of an object.
The plus expression Associativity is not specified.
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
const exprt & state() const
state_cstrlen_exprt with_state(exprt state) const
const exprt & address() const
const exprt & address() const
const exprt & state() const
state_is_cstring_exprt with_state(exprt state) const
const exprt & state() const
const exprt & address() const
state_is_dynamic_object_exprt with_state(exprt state) const
const exprt & head() const
const exprt & state() const
state_is_sentinel_dll_exprt with_state(exprt state) const
const exprt & tail() const
const exprt & address() const
const exprt & state() const
state_live_object_exprt with_state(exprt state) const
const exprt & state() const
state_object_size_exprt with_state(exprt state) const
const exprt & address() const
state_ok_exprt with_state(exprt state) const
const exprt & size() const
const exprt & address() const
const exprt & state() const
const exprt & address() const
const exprt & state() const
Expression to hold a symbol (variable)
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
bool has_prefix(const std::string &s, const std::string &prefix)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
static exprt implication(exprt lhs, exprt rhs)
const std::string & id2string(const irep_idt &d)
optionalt< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt may_be_same_object(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
optionalt< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
optionalt< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr(const exprt &expr)
Cast an exprt to a state_is_sentinel_dll_exprt.
exprt simplify_expr(exprt src, const namespacet &ns)
exprt simplify_evaluate_enter_scope_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_allocate(allocate_exprt src)
exprt simplify_is_dynamic_object_expr(state_is_dynamic_object_exprt src)
exprt simplify_object_expression_rec(exprt src)
static bool is_zero_char(const exprt &src, const namespacet &ns)
exprt simplify_live_object_expr(state_live_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_is_sentinel_dll_expr(state_is_sentinel_dll_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_exit_scope_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_ok_expr(state_ok_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_is_cstring_expr(state_is_cstring_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_update(evaluate_exprt evaluate_expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_cstrlen_expr(state_cstrlen_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
std::size_t allocate_counter
exprt simplify_pointer_offset_expr(pointer_offset_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
static bool is_a_char_type(const typet &type)
exprt simplify_evaluate_deallocate_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_object_expression(exprt src)
exprt simplify_object_size_expr(state_object_size_exprt src, const namespacet &ns)
exprt simplify_state_expr(exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_writeable_object_expr(state_writeable_object_exprt src, const namespacet &ns)
exprt simplify_pointer_object_expr(pointer_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_allocate_state(evaluate_exprt evaluate_expr, const namespacet &ns)
static bool types_are_compatible(const typet &a, const typet &b)
Simplify State Expression.
#define PRECONDITION(CONDITION)
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
const state_cstrlen_exprt & to_state_cstrlen_expr(const exprt &expr)
Cast an exprt to a state_cstrlen_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_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
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 state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.