12 #ifndef CPROVER_ANALYSES_GOTO_RW_H 13 #define CPROVER_ANALYSES_GOTO_RW_H 24 #define forall_rw_range_set_r_objects(it, rw_set) \ 25 for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \ 26 it!=(rw_set).get_r_set().end(); ++it) 28 #define forall_rw_range_set_w_objects(it, rw_set) \ 29 for(rw_range_sett::objectst::const_iterator it=(rw_set).get_w_set().begin(); \ 30 it!=(rw_set).get_w_set().end(); ++it) 65 assert(size.is_long());
67 assert(ll<=std::numeric_limits<range_spect>::max());
68 assert(ll>=std::numeric_limits<range_spect>::min());
75 typedef std::list<std::pair<range_spect, range_spect>>
sub_typet;
95 void push_back(sub_typet::value_type &&v) {
data.push_back(std::move(v)); }
112 typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>>
objectst;
114 typedef std::unordered_map<
137 PRECONDITION(dynamic_cast<range_domaint*>(it->second.get())!=
nullptr);
153 void output(std::ostream &out)
const;
294 typedef std::multimap<range_spect, std::pair<range_spect, exprt>>
sub_typet;
298 virtual void output(
const namespacet &ns, std::ostream &out)
const override;
315 return data.insert(v);
320 return data.insert(std::move(v));
337 dynamic_cast<guarded_range_domaint*>(it->second.get())!=
nullptr);
369 #endif // CPROVER_ANALYSES_GOTO_RW_H The type of an expression, extends irept.
goto_programt::const_targett target
sub_typet::const_iterator const_iterator
Semantic type conversion.
const guarded_range_domaint & get_ranges(objectst::const_iterator it) const
rw_range_sett(const namespacet &_ns)
const_iterator cbegin() const
sub_typet::const_iterator const_iterator
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
range_spect to_range_spect(const mp_integer &size)
const_iterator end() 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_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
The trinary if-then-else operator.
const_iterator end() const
std::list< std::pair< range_spect, range_spect > > sub_typet
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet
const_iterator cend() const
virtual void output(const namespacet &ns, std::ostream &out) const =0
const objectst & get_w_set() const
const_iterator cbegin() const
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
Imaginary part of the expression describing a complex number.
Extract member of struct or union.
void output(const namespacet &ns, std::ostream &out) const override
void goto_rw(goto_programt::const_targett target, rw_range_sett &rw_set)
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
iterator insert(const sub_typet::value_type &v)
The Boolean constant true.
virtual void get_objects_address_of(const exprt &object)
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
Real part of the expression describing a complex number.
Operator to dereference a pointer.
rw_guarded_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
sub_typet::iterator iterator
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
#define PRECONDITION(CONDITION)
const_iterator cend() const
virtual void get_objects_rec(goto_programt::const_targett, get_modet mode, const exprt &expr)
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, 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)
rw_range_set_value_sett(const namespacet &_ns, value_setst &_value_sets)
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
void push_back(const sub_typet::value_type &v)
A generic container class for the GOTO intermediate representation of one function.
const objectst & get_r_set() const
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_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
const_iterator begin() const
Base class for all expressions.
const_iterator begin() const
void push_back(sub_typet::value_type &&v)
virtual void output(const namespacet &ns, std::ostream &out) const override
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
range_domain_baset & operator=(const range_domain_baset &rhs)=delete
const range_domaint & get_ranges(objectst::const_iterator it) const
sub_typet::iterator iterator
virtual ~range_domain_baset()
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
range_domain_baset()=default
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
Struct constructor from list of elements.
iterator insert(sub_typet::value_type &&v)
std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hash > objectst
A base class for shift operators.
void output(std::ostream &out) const
Array constructor from list of elements.