|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Struct type. More...
#include <irep2_type.h>
Public Member Functions | |
| struct_type2t (const std::vector< type2tc > &_members, const std::vector< irep_idt > &memb_names, const std::vector< irep_idt > &memb_pretty_names, const irep_idt &_name, bool _packed=false, const std::vector< irep_idt > &memb_base_names={}, const BigInt &_alignment=0, const irep_idt &_python_aggregate=irep_idt(), bool _has_bases=false, const std::vector< irep_idt > &_bases={}) | |
| Primary constructor. | |
| struct_type2t (const struct_type2t &ref)=default | |
| unsigned int | get_width () const |
| Public Member Functions inherited from type2t | |
| virtual | ~type2t ()=default |
| unsigned int | get_width () const |
| Fetch bit width of this type. | |
| bool | operator== (const type2t &ref) const |
| bool | operator!= (const type2t &ref) const |
| bool | operator< (const type2t &ref) const |
| std::string | pretty (unsigned int indent=0) const |
| Produce a human-readable string representation of type. | |
| DUMP_METHOD void | dump () const |
| Dump object string representation to stdout. | |
| size_t | crc () const |
| Produce a checksum/hash of the current object. | |
| bool | cmp (const type2t &ref) const |
| Structural comparison. | |
| int | lt (const type2t &ref) const |
| Trinary structural ordering. | |
| list_of_memberst | tostring (unsigned int indent) const |
| Extract a list of members from type as strings. | |
| type2tc | clone () const |
| Clone method. | |
| template<typename T> | |
| void | foreach_subtype (T &&t) const |
| template<typename T> | |
| void | Foreach_subtype (T &&t) |
| Public Member Functions inherited from irep2t | |
| irep2t () noexcept | |
| irep2t (const irep2t &) noexcept | |
| irep2t & | operator= (const irep2t &)=delete |
| virtual | ~irep2t ()=default |
| void | mark_writer () const noexcept |
| void | clear_writer () const noexcept |
Public Attributes | |
| std::vector< type2tc > | members |
| std::vector< irep_idt > | member_names |
| std::vector< irep_idt > | member_pretty_names |
| std::vector< irep_idt > | member_base_names |
| The components' plain base_names – a different field from the #base_name that code_type2t::argument_base_names carries. | |
| irep_idt | name |
| bool | packed |
| bool | has_bases |
| Whether the legacy type had a bases list at all, which an empty one is not the same as: the key takes part in legacy type equality. | |
| BigInt | alignment |
| An explicit alignas, in bytes; zero when the record has none. | |
| irep_idt | python_aggregate |
| The Python model-aggregate kind ("tuple", "dict", "optional") that #python_aggregate records; empty for any other struct. | |
| std::vector< irep_idt > | bases |
| The class ids bases lists, as the C++ and Python frontends write it. | |
| Public Attributes inherited from type2t | |
| const type_ids | type_id |
| Instance of type_ids recording this types type. | |
| std::atomic< size_t > | crc_val |
| Public Attributes inherited from irep2t | |
| std::atomic< unsigned int > | refcount |
| std::atomic< std::uintptr_t > | writer_thread |
Static Public Attributes | |
| static constexpr auto | fields |
| static constexpr std::size_t | excluded_field_bytes |
| Covers the deliberately unreflected members: member_base_names (a member's spelling is no part of the struct's identity), alignment (two records differing only in alignas must still compare equal), python_aggregate, has_bases and bases. | |
| static std::string | field_names [esbmct::num_type_fields] |
Additional Inherited Members | |
| Public Types inherited from type2t | |
| enum | type_ids { end_type_id } |
| Enumeration identifying each sort of type. More... | |
| typedef esbmct::function_ref< void(const type2tc &)> | const_subtype_delegate |
| typedef esbmct::function_ref< void(type2tc &)> | subtype_delegate |
| typedef type2tc | container_type |
| typedef type2t | base_type |
| Static Public Member Functions inherited from irep2t | |
| static std::uintptr_t | current_thread_tag () noexcept |
| Protected Member Functions inherited from type2t | |
| type2t (type_ids id) | |
| Primary constructor. | |
| type2t (const type2t &ref) | |
| Copy constructor. | |
| void | foreach_subtype_impl_const (const_subtype_delegate &t) const |
| void | foreach_subtype_impl (subtype_delegate &t) |
Struct type.
Represents both C structs and the data in C++ classes. Contains a vector of types recording what type each member is, a vector of names recording what the member names are, and a name for the struct.
|
inline |
Primary constructor.
| members | Vector of types for the members in this struct. |
| memb_names | Vector of names for the members in this struct. |
| name | Name of this struct. |
|
default |
| unsigned int struct_type2t::get_width | ( | ) | const |
| BigInt struct_type2t::alignment |
An explicit alignas, in bytes; zero when the record has none.
IREP2 does not otherwise represent it, and add_padding reads it to decide a record's trailing padding – an over-aligned empty struct occupies its alignment, so without it the back-migrated type gets no pad member and a literal of it stays shorter than its own type (§7.4). Not reflected: two records that differ only here would otherwise stop comparing equal, which is a wider change than this repair.
| std::vector<irep_idt> struct_type2t::bases |
The class ids bases lists, as the C++ and Python frontends write it.
Unreflected, like alignment. Carried because exception dispatch (exception_typeid.cpp) and base_type.cpp read the class hierarchy from it (docs/roadmap/scope-python-irep2.md §15).
|
staticconstexpr |
Covers the deliberately unreflected members: member_base_names (a member's spelling is no part of the struct's identity), alignment (two records differing only in alignas must still compare equal), python_aggregate, has_bases and bases.
|
static |
|
staticconstexpr |
| bool struct_type2t::has_bases |
Whether the legacy type had a bases list at all, which an empty one is not the same as: the key takes part in legacy type equality.
| std::vector<irep_idt> struct_type2t::member_base_names |
The components' plain base_names – a different field from the #base_name that code_type2t::argument_base_names carries.
Unreflected: a member's spelling is no part of the struct's identity, so two otherwise identical structs must still compare equal (docs/roadmap/frontends-to-irep2.md §46).
| std::vector<irep_idt> struct_type2t::member_names |
| std::vector<irep_idt> struct_type2t::member_pretty_names |
| std::vector<type2tc> struct_type2t::members |
| irep_idt struct_type2t::name |
| bool struct_type2t::packed |
| irep_idt struct_type2t::python_aggregate |
The Python model-aggregate kind ("tuple", "dict", "optional") that #python_aggregate records; empty for any other struct.
Unreflected, like alignment: the tag already names the type. Carried because in and membership dispatch read it, and a user class may share a tuple's tag prefix (docs/roadmap/scope-python-irep2.md §10.4).