rw_range_set_value_sett Class Reference
#include <goto_rw.h>
Inheritance diagram for rw_range_set_value_sett: Collaboration diagram for rw_range_set_value_sett:Public Member Functions | |
| 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, get_modet mode, const exprt &expr) override |
| void | get_objects_rec (const irep_idt &_function, goto_programt::const_targett _target, const typet &type) override |
| void | get_array_objects (const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &pointer) override |
| Public Member Functions inherited from rw_range_sett | |
| virtual | ~rw_range_sett () |
| rw_range_sett (const namespacet &_ns, message_handlert &message_handler) | |
| const objectst & | get_r_set () const |
| const objectst & | get_w_set () const |
| const range_domaint & | get_ranges (const std::unique_ptr< range_domain_baset > &ranges) const |
| void | output (std::ostream &out) const |
Protected Member Functions | |
| 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) |
| virtual void | get_objects_rec (const irep_idt &, goto_programt::const_targett, const typet &type) |
| virtual void | get_objects_rec (get_modet mode, const exprt &expr) |
| virtual void | get_objects_rec (const typet &type) |
| virtual void | get_objects_rec (get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size) |
| Protected Member Functions inherited from rw_range_sett | |
| virtual void | get_objects_rec (get_modet mode, const exprt &expr) |
| virtual void | get_objects_rec (const typet &type) |
| virtual void | get_objects_complex_real (get_modet mode, const complex_real_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_byte_extract (get_modet mode, const byte_extract_exprt &be, 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) |
| virtual void | get_objects_member (get_modet mode, const member_exprt &expr, 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_array (get_modet mode, const array_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_typecast (get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size) |
| virtual void | get_objects_address_of (const exprt &object) |
| virtual void | get_objects_rec (get_modet mode, const 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) |
Protected Attributes | |
| value_setst & | value_sets |
| irep_idt | function |
| goto_programt::const_targett | target |
| Protected Attributes inherited from rw_range_sett | |
| const namespacet & | ns |
| message_handlert & | message_handler |
| objectst | r_range_set |
| objectst | w_range_set |
Additional Inherited Members | |
| Public Types inherited from rw_range_sett | |
| enum class | get_modet { LHS_W , READ } |
| typedef std::map< irep_idt, std::unique_ptr< range_domain_baset > > | objectst |
Detailed Description
Constructor & Destructor Documentation
◆ rw_range_set_value_sett()
|
inline |
Member Function Documentation
◆ get_array_objects()
|
inlineoverridevirtual |
Reimplemented from rw_range_sett.
◆ get_objects_dereference()
|
overrideprotectedvirtual |
Reimplemented from rw_range_sett.
Definition at line 672 of file goto_rw.cpp.
◆ get_objects_rec() [1/7]
|
inlineprotected |
◆ get_objects_rec() [2/7]
|
inlineprotected |
◆ get_objects_rec() [3/7]
|
inlineoverridevirtual |
Reimplemented from rw_range_sett.
Reimplemented in rw_guarded_range_set_value_sett.
◆ get_objects_rec() [4/7]
|
inlineoverridevirtual |
Reimplemented from rw_range_sett.
Reimplemented in rw_guarded_range_set_value_sett.
◆ get_objects_rec() [5/7]
|
protected |
Definition at line 269 of file goto_rw.cpp.
◆ get_objects_rec() [6/7]
|
protected |
Definition at line 265 of file goto_rw.cpp.
◆ get_objects_rec() [7/7]
|
protected |
Definition at line 341 of file goto_rw.cpp.
Member Data Documentation
◆ function
◆ target
|
protected |
◆ value_sets
|
protected |
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.h
- /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.cpp
