62{

63public:

67

139

141

146

151

156

161

163 const irep_idt &component_name) const;

164

167

170

176

183

189

195};

231{

232public:

236

241

243

249

258

259 typedef std::vector<baset> basest;

260

266

272

276

281

289};

309{

311 return static_cast<const struct_typet &>(type);

312}

325{

326public:

331

334

339

344

347

352

357

362};

382{

384 return static_cast<const class_typet &>(type);

385}

396{

397public:

404

409

414};

435{

437 return static_cast<const tag_typet &>(type);

438}

442{

444 return static_cast<tag_typet &>(type);

445}

534{

535public:

539

544

549};

583{

584public:

587

596

597

598

654

659

664

673

678

683

688

693

698

703

708

713

718

723

728

733

738

750

752

769};

789{

792 return static_cast<const code_typet &>(type);

793}

797{

800 return static_cast<code_typet &>(type);

801}

807{

808public:

814

817

825

831

837

838

839

844

845

846

851

856

861

862 static void check(

863 const typet &type,

865

866protected:

867

869};

889{

892 return static_cast<const array_typet &>(type);

893}

909{

910public:

914

919

924

929

930 std::size_t width() const;

931

936

938

946};

991{

993 return static_cast<const string_typet &>(type);

994}

1005{

1006public:

1012

1018

1021};

1041{

1043 return static_cast<const range_typet &>(type);

1044}

1048{

1050 return static_cast<range_typet &>(type);

1051}

1064{

1065public:

1067

1070

1078

1084

1090

1093

1094protected:

1095

1097};

1117{

1120 return static_cast<const vector_typet &>(type);

1121}

1159{

1162 return static_cast<const complex_typet &>(type);

1163}

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)

array_typet(typet _subtype, exprt _size)

bool is_incomplete() const

typet index_type() const

The type of the index expressions into any instance of this type.

const exprt & size() const

const typet & element_type() const

The type of the elements of the array.

const typet & subtype() const

typet & index_type_nonconst()

The type of the index expressions into any instance of this type.

typet & element_type()

The type of the elements of the array.

Base class of fixed-width bit-vector types.

void set_width(std::size_t width)

std::size_t get_width() const

std::size_t width() const

static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)

bitvector_typet(const irep_idt &_id, std::size_t width)

bitvector_typet(const irep_idt &_id, mp_integer _width)

bitvector_typet(const irep_idt &_id)

componentst static_memberst

static_memberst & static_members()

componentt static_membert

const methodst & methods() const

const static_memberst & static_members() const

parametert(const typet &type)

const irep_idt & get_base_name() const

const exprt & default_value() const

void set_base_name(const irep_idt &name)

const irep_idt & get_identifier() const

bool has_default_value() const

void set_identifier(const irep_idt &identifier)

code_typet(parameterst _parameters, typet _return_type)

Constructs a new code type, i.e., function type.

std::vector< parametert > parameterst

const irep_idt & get_access() const

void set_is_constructor()

void set_inlined(bool value)

const parameterst & parameters() const

const typet & return_type() const

parameterst & parameters()

void set_access(const irep_idt &access)

std::vector< irep_idt > parameter_identifiers() const

Produces the list of parameter identifiers.

std::unordered_map< irep_idt, std::size_t > parameter_indicest

bool get_is_constructor() const

bool has_ellipsis() const

const parametert * get_this() const

parameter_indicest parameter_indices() const

Get a map from parameter name to its index.

Complex numbers made of pair of given subtype.

complex_typet(typet _subtype)

A constant literal expression.

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

An enumeration type, i.e., a type with elements (not to be confused with C enums)

const irept::subt & elements() const

Base class for all expressions.

exprt & add_expr(const irep_idt &name)

typet & type()

Return the type of the expression.

const exprt & find_expr(const irep_idt &name) const

bool get_bool(const irep_idt &name) const

std::size_t get_size_t(const irep_idt &name) const

const irept & find(const irep_idt &name) const

const irep_idt & get(const irep_idt &name) const

void remove(const irep_idt &name)

void set(const irep_idt &name, const irep_idt &value)

void set_size_t(const irep_idt &name, const std::size_t value)

const irep_idt & id() const

irept & add(const irep_idt &name)

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

A type for subranges of integers.

void set_to(const mp_integer &to)

constant_exprt zero_expr() const

void set_from(const mp_integer &_from)

mp_integer get_to() const

range_typet(const mp_integer &_from, const mp_integer &_to)

bool includes(const mp_integer &) const

constant_exprt one_expr() const

mp_integer get_from() const

A struct or union tag type.

struct_or_union_tag_typet(const irep_idt &id, const irep_idt &identifier)

A struct tag type, i.e., struct_typet with an identifier.

struct_tag_typet(const irep_idt &identifier)

Base class or struct that a class or struct inherits from.

struct_tag_typet & type()

Structure type, corresponds to C style structs.

const basest & bases() const

Get the collection of base classes/structs.

std::optional< baset > get_base(const irep_idt &id) const

Return the base with the given name, if exists.

struct_typet(componentst _components)

bool has_base(const irep_idt &id) const

Test whether id is a base class/struct.

bool is_class() const

A struct may be a class, where members may have access restrictions.

basest & bases()

Get the collection of base classes/structs.

bool is_prefix_of(const struct_typet &other) const

Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...

void add_base(const struct_tag_typet &base)

Add a base class/struct.

std::vector< baset > basest

const irep_idt & get_pretty_name() const

bool get_anonymous() const

void set_pretty_name(const irep_idt &name)

void set_anonymous(bool anonymous)

void set_base_name(const irep_idt &base_name)

const irep_idt & get_access() const

void set_is_padding(bool is_padding)

const irep_idt & get_base_name() const

bool get_is_padding() const

void set_access(const irep_idt &access)

const irep_idt & get_name() const

void set_name(const irep_idt &name)

componentt(const irep_idt &_name, typet _type)

Base type for structs and unions.

const typet & component_type(const irep_idt &component_name) const

void set_tag(const irep_idt &tag)

bool is_class() const

A struct may be a class, where members may have access restrictions.

irep_idt default_access() const

Return the access specification for members where access has not been modified.

const componentst & components() const

struct_union_typet(const irep_idt &_id)

const componentt & get_component(const irep_idt &component_name) const

Get the reference to a component with given name.

struct_union_typet(const irep_idt &_id, componentst _components)

bool has_component(const irep_idt &component_name) const

bool is_incomplete() const

A struct/union may be incomplete.

void make_incomplete()

A struct/union may be incomplete.

componentst & components()

std::size_t component_number(const irep_idt &component_name) const

Return the sequence number of the component with given name.

std::vector< componentt > componentst

A tag-based type, i.e., typet with an identifier.

const irep_idt & get_identifier() const

tag_typet(const irep_idt &_id, const irep_idt &identifier)

void set_identifier(const irep_idt &identifier)

Type with a single subtype.

static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)

const typet & subtype() const

The type of an expression, extends irept.

typet & add_type(const irep_idt &name)

const typet & find_type(const irep_idt &name) const

static void check(const typet &, const validation_modet=validation_modet::INVARIANT)

Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)

const constant_exprt & size() const

typet & element_type()

The type of the elements of the vector.

const typet & subtype() const

typet & index_type_nonconst()

The type of any index expression into an instance of this type.

typet index_type() const

The type of any index expression into an instance of this type.

const typet & element_type() const

The type of the elements of the vector.

Templated functions to cast to specific exprt-derived classes.

#define PRECONDITION(CONDITION)

const range_typet & to_range_type(const typet &type)

Cast a typet to a range_typet.

bool can_cast_type< class_typet >(const typet &type)

Check whether a reference to a typet is a class_typet.

bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)

Identify whether a given type is constant itself or contains constant components.

bool can_cast_type< bool_typet >(const typet &base)

bool can_cast_type< complex_typet >(const typet &type)

Check whether a reference to a typet is a complex_typet.

const vector_typet & to_vector_type(const typet &type)

Cast a typet to a vector_typet.

const code_typet & to_code_type(const typet &type)

Cast a typet to a code_typet.

bool can_cast_type< array_typet >(const typet &type)

Check whether a reference to a typet is a array_typet.

bool can_cast_type< vector_typet >(const typet &type)

Check whether a reference to a typet is a vector_typet.

bool can_cast_type< struct_or_union_tag_typet >(const typet &type)

Check whether a reference to a typet is a struct_or_union_tag_typet.

const string_typet & to_string_type(const typet &type)

Cast a typet to a string_typet.

bool is_constant(const typet &type)

This method tests, if the given typet is a constant.

bool can_cast_type< struct_tag_typet >(const typet &type)

Check whether a reference to a typet is a struct_tag_typet.

const struct_typet & to_struct_type(const typet &type)

Cast a typet to a struct_typet.

const enumeration_typet & to_enumeration_type(const typet &type)

Cast a typet to a enumeration_typet.

const struct_tag_typet & to_struct_tag_type(const typet &type)

Cast a typet to a struct_tag_typet.

bool can_cast_type< code_typet >(const typet &type)

Check whether a reference to a typet is a code_typet.

const complex_typet & to_complex_type(const typet &type)

Cast a typet to a complex_typet.

const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)

Cast a typet to a struct_or_union_tag_typet.

bool can_cast_type< range_typet >(const typet &type)

Check whether a reference to a typet is a range_typet.

const array_typet & to_array_type(const typet &type)

Cast a typet to an array_typet.

bool can_cast_type< tag_typet >(const typet &type)

Check whether a reference to a typet is a tag_typet.

const struct_union_typet & to_struct_union_type(const typet &type)

Cast a typet to a struct_union_typet.

bool can_cast_type< enumeration_typet >(const typet &type)

Check whether a reference to a typet is a enumeration_typet.

bool can_cast_type< bitvector_typet >(const typet &type)

Check whether a reference to a typet is a bitvector_typet.

bool can_cast_type< struct_union_typet >(const typet &type)

Check whether a reference to a typet is a struct_union_typet.

bool can_cast_type< string_typet >(const typet &type)

Check whether a reference to a typet is a string_typet.

bool can_cast_type< struct_typet >(const typet &type)

Check whether a reference to a typet is a struct_typet.

const class_typet & to_class_type(const typet &type)

Cast a typet to a class_typet.

const tag_typet & to_tag_type(const typet &type)

Cast a typet to a tag_typet.

#define DATA_CHECK(vm, condition, message)

This macro takes a condition which denotes a well-formedness criterion on goto programs,...