Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_GOTO_RW_H
13 #define CPROVER_ANALYSES_GOTO_RW_H
61 assert(size.is_long());
63 assert(ll<=std::numeric_limits<range_spect>::max());
64 assert(ll>=std::numeric_limits<range_spect>::min());
71 typedef std::list<std::pair<range_spect, range_spect>>
sub_typet;
91 void push_back(sub_typet::value_type &&v) {
data.push_back(std::move(v)); }
102 typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>>
objectst;
104 typedef std::unordered_map<
126 get_ranges(
const std::unique_ptr<range_domain_baset> &ranges)
const
151 void output(std::ostream &out)
const;
272 const exprt &expr)
override
274 function = _function;
283 const typet &type)
override
285 function = _function;
307 typedef std::multimap<range_spect, std::pair<range_spect, exprt>>
sub_typet;
311 virtual void output(
const namespacet &ns, std::ostream &out)
const override;
328 return data.insert(v);
333 return data.insert(std::move(v));
351 get_ranges(
const std::unique_ptr<range_domain_baset> &ranges)
const
362 const exprt &expr)
override
372 const typet &type)
override
396 #endif // CPROVER_ANALYSES_GOTO_RW_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const objectst & get_r_set() const
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_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
void goto_rw(const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
sub_typet::const_iterator const_iterator
virtual void get_objects_address_of(const exprt &object)
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
The type of an expression, extends irept.
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Operator to dereference a pointer.
guard_managert & guard_manager
const_iterator cbegin() const
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
The trinary if-then-else operator.
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
Real part of the expression describing a complex number.
void get_objects_rec(const irep_idt &function, goto_programt::const_targett target, const typet &type) override
Base class for all expressions.
const_iterator end() const
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
void output(const namespacet &ns, std::ostream &out) const override
range_domain_baset & operator=(range_domain_baset &&rhs)=delete
const_iterator cend() const
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
range_spect to_range_spect(const mp_integer &size)
const guarded_range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
iterator insert(const sub_typet::value_type &v)
const_iterator end() const
Struct constructor from list of elements.
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
This is unused by this implementation of guards, but can be used by other implementations of the same...
std::list< std::pair< range_spect, range_spect > > sub_typet
void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
range_domain_baset()=default
void get_objects_rec(const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
rw_range_sett(const namespacet &_ns)
#define PRECONDITION(CONDITION)
const_iterator begin() const
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
sub_typet::iterator iterator
sub_typet::iterator iterator
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
virtual void get_objects_complex_imag(get_modet mode, const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size)
range_domain_baset(const range_domain_baset &rhs)=delete
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual ~range_domain_baset()
void push_back(const sub_typet::value_type &v)
goto_programt::const_targett target
range_domain_baset(range_domain_baset &&rhs)=delete
const_iterator cbegin() const
void output(std::ostream &out) const
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
Extract member of struct or union.
A collection of goto functions.
A base class for shift and rotate operators.
const_iterator begin() const
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
Imaginary part of the expression describing a complex number.
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
A generic container class for the GOTO intermediate representation of one function.
virtual void output(const namespacet &ns, std::ostream &out) const =0
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
instructionst::const_iterator const_targett
virtual void output(const namespacet &ns, std::ostream &out) const override
void push_back(sub_typet::value_type &&v)
Semantic type conversion.
sub_typet::const_iterator const_iterator
The Boolean constant true.
void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
Array constructor from list of elements.
const objectst & get_w_set() const
iterator insert(sub_typet::value_type &&v)
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets, guard_managert &guard_manager)
const_iterator cend() const
range_domain_baset & operator=(const range_domain_baset &rhs)=delete