70 b_it->address(),
a_it->address().type());
97 b_it->address(),
a_it->address().type());
169 if(
a_it->object_identifier() ==
"return_value")
171 else if(
a_it->object_identifier().starts_with(
"va_args::"))
173 else if(
a_it->object_identifier().starts_with(
"va_arg::"))
175 else if(
a_it->object_identifier().starts_with(
"va_arg_array::"))
177 else if(
a_it->object_identifier().starts_with(
"old::"))
180 auto &symbol =
ns.lookup(
a_it->object_expr());
188 :
static_cast<exprt>(*b_it);
250 std::cout <<
"OBJECT_SIZE1: " <<
format(equal) <<
'\n';
313 b_it->address(),
a_it->address().type());
332 if(
ns.lookup(
object.get_identifier(), symbol))
384 std::cout <<
"R " <<
format(s) <<
" --> " <<
format(src) <<
'\n';
633 const auto &state =
ok_expr.state();
634 const auto &pointer =
ok_expr.address();
635 const auto &size =
ok_expr.size();
753 constraint.visit_pre([
this](
const exprt &src) {
node(src); });
759 std::cout <<
"CONSTRAINT1: " <<
format(constraint) <<
"\n";
signedbv_typet signed_size_type()
bitvector_typet char_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void is_dynamic_object_fc()
std::set< address_of_exprt > address_of_exprs
std::set< state_ok_exprt > ok_exprs
std::unordered_map< exprt, symbol_exprt, irep_hash > replacement_map
std::set< object_address_exprt > object_address_exprs
std::set< state_live_object_exprt > live_object_exprs
std::set< evaluate_exprt > evaluate_exprs
std::set< state_is_dynamic_object_exprt > is_dynamic_object_exprs
std::set< state_is_sentinel_dll_exprt > is_sentinel_dll_exprs
std::set< initial_state_exprt > initial_state_exprs
std::set< state_writeable_object_exprt > writeable_object_exprs
std::map< irep_idt, std::size_t > counters
exprt translate(exprt) const
std::set< state_is_cstring_exprt > is_cstring_exprs
const std::unordered_set< symbol_exprt, irep_hash > & address_taken
decision_proceduret & dest
std::set< state_object_size_exprt > object_size_exprs
std::vector< exprt > constraints
void add(const state_ok_exprt &)
void writeable_object_fc()
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
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.
const std::string & id_string() const
const irep_idt & id() const
Operator to return the address of an object.
The plus expression Associativity is not specified.
The offset (in bytes) of a pointer relative to the object.
Expression to hold a symbol (variable)
An expression with three operands.
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.
Decision Procedure Interface.
static exprt implication(exprt lhs, exprt rhs)
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.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
std::optional< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
std::optional< 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.
Simplify State Expression.
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 reallocate_exprt & to_reallocate_expr(const exprt &expr)
Cast an exprt to a reallocate_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 deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_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 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.
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)