12 #ifndef CPROVER_ANALYSES_GOTO_RW_H
13 #define CPROVER_ANALYSES_GOTO_RW_H
89 ll > std::numeric_limits<range_spect::value_type>::max() ||
90 ll < std::numeric_limits<range_spect::value_type>::min())
176 typedef std::list<std::pair<range_spect, range_spect>>
sub_typet;
206 typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>>
objectst;
226 get_ranges(
const std::unique_ptr<range_domain_baset> &ranges)
const
257 void output(std::ostream &out)
const;
379 const exprt &expr)
override
381 function = _function;
390 const typet &type)
override
392 function = _function;
402 const exprt &pointer)
override
404 function = _function;
426 typedef std::multimap<range_spect, std::pair<range_spect, exprt>>
sub_typet;
430 virtual void output(
const namespacet &ns, std::ostream &out)
const override;
447 return data.insert(v);
452 return data.insert(std::move(v));
471 get_ranges(
const std::unique_ptr<range_domain_baset> &ranges)
const
482 const exprt &expr)
override
492 const typet &type)
override
Array constructor from list of elements.
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.
Base class for all expressions.
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
const_iterator cbegin() const
iterator insert(const sub_typet::value_type &v)
iterator insert(sub_typet::value_type &&v)
const_iterator begin() const
virtual void output(const namespacet &ns, std::ostream &out) const override
sub_typet::const_iterator const_iterator
sub_typet::iterator iterator
const_iterator cend() const
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
const_iterator end() const
The trinary if-then-else operator.
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual ~range_domain_baset()
range_domain_baset & operator=(range_domain_baset &&rhs)=delete
virtual void output(const namespacet &ns, std::ostream &out) const =0
range_domain_baset(range_domain_baset &&rhs)=delete
range_domain_baset()=default
range_domain_baset(const range_domain_baset &rhs)=delete
range_domain_baset & operator=(const range_domain_baset &rhs)=delete
sub_typet::iterator iterator
void output(const namespacet &ns, std::ostream &out) const override
std::list< std::pair< range_spect, range_spect > > sub_typet
sub_typet::const_iterator const_iterator
const_iterator cbegin() const
const_iterator cend() const
void push_back(sub_typet::value_type &&v)
void push_back(const sub_typet::value_type &v)
const_iterator end() const
const_iterator begin() const
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
bool operator>(const range_spect &other) const
static range_spect unknown()
range_spect operator*(const range_spect &other) const
friend std::ostream & operator<<(std::ostream &, const range_spect &)
range_spect & operator+=(const range_spect &other)
range_spect operator+(const range_spect &other) const
range_spect(value_type v)
static range_spect to_range_spect(const mp_integer &size)
bool operator<=(const range_spect &other) const
range_spect & operator-=(const range_spect &other)
bool operator==(const range_spect &other) const
bool operator>=(const range_spect &other) const
bool operator<(const range_spect &other) const
range_spect operator-(const range_spect &other) const
void get_objects_rec(const irep_idt &function, goto_programt::const_targett target, const typet &type) override
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, guard_managert &guard_manager, message_handlert &message_handler)
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
guard_managert & guard_manager
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
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
void get_array_objects(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &pointer) override
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, message_handlert &message_handler)
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override
goto_programt::const_targett target
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
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)
std::map< irep_idt, std::unique_ptr< range_domain_baset > > objectst
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
message_handlert & message_handler
const objectst & get_r_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)
rw_range_sett(const namespacet &_ns, message_handlert &message_handler)
virtual void get_array_objects(const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, const typet &type)
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
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)
const objectst & get_w_set() const
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.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
std::ostream & operator<<(std::ostream &os, const range_spect &r)
void goto_rw(const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
#define PRECONDITION(CONDITION)
This is unused by this implementation of guards, but can be used by other implementations of the same...