ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
struct_type2t Class Reference

Struct type. More...

#include <irep2_type.h>

Inheritance diagram for struct_type2t:
[legend]

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)

Detailed Description

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.

Constructor & Destructor Documentation

◆ struct_type2t() [1/2]

struct_type2t::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 = {} )
inline

Primary constructor.

Parameters
membersVector of types for the members in this struct.
memb_namesVector of names for the members in this struct.
nameName of this struct.

◆ struct_type2t() [2/2]

struct_type2t::struct_type2t ( const struct_type2t & ref)
default

Member Function Documentation

◆ get_width()

unsigned int struct_type2t::get_width ( ) const

Member Data Documentation

◆ alignment

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.

◆ bases

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).

◆ excluded_field_bytes

std::size_t struct_type2t::excluded_field_bytes
staticconstexpr
Initial value:
=
2 * sizeof(std::vector<irep_idt>) + sizeof(BigInt) + sizeof(irep_idt) +
sizeof(bool)
Definition bigint.hh:58
Definition irep_idt.h:12

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.

◆ field_names

std::string struct_type2t::field_names
static
Initial value:
=
{"members", "member_names", "member_pretty_names", "typename", "packed", ""}

◆ fields

auto struct_type2t::fields
staticconstexpr
Initial value:
= std::make_tuple(
std::vector< irep_idt > member_names
Definition irep2_type.h:136
bool packed
Definition irep2_type.h:145
std::vector< type2tc > members
Definition irep2_type.h:135
irep_idt name
Definition irep2_type.h:144
std::vector< irep_idt > member_pretty_names
Definition irep2_type.h:137

◆ has_bases

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.

◆ member_base_names

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).

◆ member_names

std::vector<irep_idt> struct_type2t::member_names

◆ member_pretty_names

std::vector<irep_idt> struct_type2t::member_pretty_names

◆ members

std::vector<type2tc> struct_type2t::members

◆ name

irep_idt struct_type2t::name

◆ packed

bool struct_type2t::packed

◆ python_aggregate

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).


The documentation for this class was generated from the following files: