12 #ifndef CPROVER_ANALYSES_GOTO_RW_H 13 #define CPROVER_ANALYSES_GOTO_RW_H 23 #define forall_rw_range_set_r_objects(it, rw_set) \ 24 for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \ 25 it!=(rw_set).get_r_set().end(); ++it) 27 #define forall_rw_range_set_w_objects(it, rw_set) \ 28 for(rw_range_sett::objectst::const_iterator it=(rw_set).get_w_set().begin(); \ 29 it!=(rw_set).get_w_set().end(); ++it) 56 assert(size.is_long());
57 mp_integer::llong_t ll=size.to_long();
58 assert(ll<=std::numeric_limits<range_spect>::max());
59 assert(ll>=std::numeric_limits<range_spect>::min());
66 public std::list<std::pair<range_spect, range_spect> >
86 typedef std::map<irep_idt, range_domain_baset*>
objectst;
88 typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash>
111 PRECONDITION(dynamic_cast<range_domaint*>(it->second)!=
nullptr);
127 void output(std::ostream &out)
const;
262 public std::multimap<range_spect, std::pair<range_spect, exprt> >
280 PRECONDITION(dynamic_cast<guarded_range_domaint*>(it->second)!=
nullptr);
312 #endif // CPROVER_ANALYSES_GOTO_RW_H virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
The type of an expression.
goto_programt::const_targett target
const guarded_range_domaint & get_ranges(objectst::const_iterator it) const
virtual void output(const namespacet &ns, std::ostream &out) const
rw_range_sett(const namespacet &_ns)
std::ostream & operator<<(std::ostream &out, const rw_range_sett &rw_set)
range_spect to_range_spect(const mp_integer &size)
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.
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_complex(get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void output(const namespacet &ns, std::ostream &out) const =0
const objectst & get_w_set() const
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
std::unordered_map< irep_idt, range_domain_baset *, string_hash > objectst
Extract member of struct or union.
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)
instructionst::const_iterator const_targett
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)
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)
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)
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)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
const objectst & get_r_set() const
virtual void output(const namespacet &ns, std::ostream &out) const
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)
Base class for all expressions.
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
const range_domaint & get_ranges(objectst::const_iterator it) const
virtual ~range_domain_baset()
virtual void get_objects_rec(goto_programt::const_targett _target, get_modet mode, const exprt &expr)
struct constructor from list of elements
A base class for shift operators.
void output(std::ostream &out) const
array constructor from list of elements