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

Unsigned integer type. More...

#include <irep2_type.h>

Inheritance diagram for unsignedbv_type2t:
[legend]

Public Member Functions

 unsignedbv_type2t (unsigned int w, bool qualified=false, const irep_idt &cpp=irep_idt())
 Primary constructor.
 unsignedbv_type2t (const unsignedbv_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

unsigned int width
irep_idt cpp_type
 The source language's own spelling of this type, as #cpp_type records it.
bool constant_qualified
 Whether the source qualified this const, as #constant records 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 = std::make_tuple(&unsignedbv_type2t::width)
static constexpr std::size_t excluded_field_bytes
static std::string field_names [esbmct::num_type_fields]
 cpp_type pushes constant_qualified into a fresh slot, so this class now carries four bytes of trailing padding and fields_cover_class has no margin left: a further unreflected field would fit in the hole unnoticed.

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

Unsigned integer type.

Represents any form of unsigned integer; the size of this integer is recorded in the width field.

Constructor & Destructor Documentation

◆ unsignedbv_type2t() [1/2]

unsignedbv_type2t::unsignedbv_type2t ( unsigned int w,
bool qualified = false,
const irep_idt & cpp = irep_idt() )
inline

Primary constructor.

Parameters
widthWidth of represented integer

◆ unsignedbv_type2t() [2/2]

unsignedbv_type2t::unsignedbv_type2t ( const unsignedbv_type2t & ref)
default

Member Function Documentation

◆ get_width()

unsigned int unsignedbv_type2t::get_width ( ) const

Member Data Documentation

◆ constant_qualified

bool unsignedbv_type2t::constant_qualified

Whether the source qualified this const, as #constant records it.

Unreflected: c_expr2string prints it and nothing else reads it, so two integers of the same width are the same type whether or not one was qualified (docs/roadmap/scope-clang-c-irep2.md §158).

◆ cpp_type

irep_idt unsignedbv_type2t::cpp_type

The source language's own spelling of this type, as #cpp_type records it.

Unreflected: a spelling is no part of the type's identity, so two bitvectors of the same width are the same type however they were spelled. Carried because a consumer reads it back – python_converter:: get_python_type_category distinguishes a 1-char string element from an 8-bit int by it (docs/roadmap/scope-python-irep2.md §9).

◆ excluded_field_bytes

std::size_t unsignedbv_type2t::excluded_field_bytes
staticconstexpr
Initial value:
=
sizeof(irep_idt) + sizeof(bool)
Definition irep_idt.h:12

◆ field_names

std::string unsignedbv_type2t::field_names
static
Initial value:
=
{"width", "", "", "", ""}

cpp_type pushes constant_qualified into a fresh slot, so this class now carries four bytes of trailing padding and fields_cover_class has no margin left: a further unreflected field would fit in the hole unnoticed.

Pin the size so the next one has to come here first.

◆ fields

auto unsignedbv_type2t::fields = std::make_tuple(&unsignedbv_type2t::width)
staticconstexpr

◆ width

unsigned int unsignedbv_type2t::width

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