45 out <<
itr->first <<
":" <<
itr->second;
52 for(rw_range_sett::objectst::iterator it=
r_range_set.begin();
57 for(rw_range_sett::objectst::iterator it=
w_range_set.begin();
122 else if(
if_expr.cond().is_true())
284 if(!index.has_value())
455 else if(
object.
id()==
ID_if)
477 throw "rw_range_sett: address_of '" +
object.id_string() +
"' not handled";
486 objectst::iterator entry=
489 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
490 identifier,
nullptr))
493 if(entry->second==
nullptr)
571 add(mode, identifier, 0, -1);
594 throw "rw_range_sett: assignment to '" + expr.
id_string() +
"' not handled";
658 const namespacet &ns, std::ostream &out)
const
667 out <<
itr->first <<
":" <<
itr->second.first;
683 else if(
if_expr.cond().is_true())
697 guard = std::move(copy);
707 objectst::iterator entry=
710 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
711 identifier,
nullptr))
714 if(entry->second==
nullptr)
748 for(
const auto &
argument : arguments)
760 switch(target->type())
774 target->get_condition());
784 if(target->get_other().get_statement() ==
ID_printf)
786 for(
const auto &op : target->get_other().operands())
806 function, target, target->assign_lhs(), target->assign_rhs(),
rw_set);
815 rw_set.get_objects_rec(function, target, target->decl_symbol().type());
825 target->call_function(),
826 target->call_arguments(),
845 goto_functionst::function_mapt::const_iterator
f_it=
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Operator to return the address of an object.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
const array_typet & type() const
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void add(const exprt &expr)
virtual void output(const namespacet &ns, std::ostream &out) const override
sub_typet::const_iterator const_iterator
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual ~range_domain_baset()
void output(const namespacet &ns, std::ostream &out) const override
sub_typet::const_iterator const_iterator
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
goto_programt::const_targett target
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
void output(std::ostream &out) const
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
const objectst & get_w_set() const
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_complex_imag(get_modet mode, const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_address_of(const exprt &object)
const objectst & get_r_set() const
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
A base class for shift and rotate operators.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const typet & subtype() const
Semantic type conversion.
The type of an expression, extends irept.
#define forall_operands(it, expr)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
static void goto_rw_assign(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &rhs, rw_range_sett &rw_set)
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
range_spect to_range_spect(const mp_integer &size)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.