Pre-defined types. More...

#include "expr.h"
#include "expr_cast.h"
#include "invariant.h"
#include "mp_arith.h"
#include "validate.h"
#include <unordered_map>

Include dependency graph for std_types.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	bool_typet
	The Boolean type. More...

class	empty_typet
	The empty type. More...

class	struct_union_typet
	Base type for structs and unions. More...

class	struct_union_typet::componentt

class	struct_typet
	Structure type, corresponds to C style structs. More...

class	struct_typet::baset
	Base class or struct that a class or struct inherits from. More...

class	class_typet
	Class type. More...

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

class	struct_or_union_tag_typet
	A struct or union tag type. More...

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

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

class	code_typet
	Base type of functions. More...

class	code_typet::parametert

class	array_typet
	Arrays with given size. More...

class	bitvector_typet
	Base class of fixed-width bit-vector types. More...

class	string_typet
	String type. More...

class	range_typet
	A type for subranges of integers. More...

class	vector_typet
	The vector type. More...

class	complex_typet
	Complex numbers made of pair of given subtype. More...

Functions
bool	is_constant (const typet &type)
	This method tests, if the given typet is a constant. More...

template<>
bool	can_cast_type< bool_typet > (const typet &base)

template<>
bool	can_cast_type< struct_union_typet > (const typet &type)
	Check whether a reference to a typet is a struct_union_typet. More...

const struct_union_typet &	to_struct_union_type (const typet &type)
	Cast a typet to a struct_union_typet. More...

struct_union_typet &	to_struct_union_type (typet &type)
	Cast a typet to a struct_union_typet. More...

template<>
bool	can_cast_type< struct_typet > (const typet &type)
	Check whether a reference to a typet is a struct_typet. More...

const struct_typet &	to_struct_type (const typet &type)
	Cast a typet to a struct_typet. More...

struct_typet &	to_struct_type (typet &type)
	Cast a typet to a struct_typet. More...

template<>
bool	can_cast_type< class_typet > (const typet &type)
	Check whether a reference to a typet is a class_typet. More...

const class_typet &	to_class_type (const typet &type)
	Cast a typet to a class_typet. More...

class_typet &	to_class_type (typet &type)
	Cast a typet to a class_typet. More...

template<>
bool	can_cast_type< tag_typet > (const typet &type)
	Check whether a reference to a typet is a tag_typet. More...

const tag_typet &	to_tag_type (const typet &type)
	Cast a typet to a tag_typet. More...

tag_typet &	to_tag_type (typet &type)
	Cast a typet to a tag_typet. More...

template<>
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. More...

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

struct_or_union_tag_typet &	to_struct_or_union_tag_type (typet &type)
	Cast a typet to a struct_or_union_tag_typet. More...

template<>
bool	can_cast_type< struct_tag_typet > (const typet &type)
	Check whether a reference to a typet is a struct_tag_typet. More...

const struct_tag_typet &	to_struct_tag_type (const typet &type)
	Cast a typet to a struct_tag_typet. More...

struct_tag_typet &	to_struct_tag_type (typet &type)
	Cast a typet to a struct_tag_typet. More...

template<>
bool	can_cast_type< enumeration_typet > (const typet &type)
	Check whether a reference to a typet is a enumeration_typet. More...

const enumeration_typet &	to_enumeration_type (const typet &type)
	Cast a typet to a enumeration_typet. More...

enumeration_typet &	to_enumeration_type (typet &type)
	Cast a typet to a enumeration_typet. More...

template<>
bool	can_cast_type< code_typet > (const typet &type)
	Check whether a reference to a typet is a code_typet. More...

const code_typet &	to_code_type (const typet &type)
	Cast a typet to a code_typet. More...

code_typet &	to_code_type (typet &type)
	Cast a typet to a code_typet. More...

template<>
bool	can_cast_type< array_typet > (const typet &type)
	Check whether a reference to a typet is a array_typet. More...

const array_typet &	to_array_type (const typet &type)
	Cast a typet to an array_typet. More...

array_typet &	to_array_type (typet &type)
	Cast a typet to an array_typet. More...

template<>
bool	can_cast_type< bitvector_typet > (const typet &type)
	Check whether a reference to a typet is a bitvector_typet. More...

template<>
bool	can_cast_type< string_typet > (const typet &type)
	Check whether a reference to a typet is a string_typet. More...

const string_typet &	to_string_type (const typet &type)
	Cast a typet to a string_typet. More...

string_typet &	to_string_type (typet &type)
	Cast a typet to a string_typet. More...

template<>
bool	can_cast_type< range_typet > (const typet &type)
	Check whether a reference to a typet is a range_typet. More...

const range_typet &	to_range_type (const typet &type)
	Cast a typet to a range_typet. More...

range_typet &	to_range_type (typet &type)
	Cast a typet to a range_typet. More...

template<>
bool	can_cast_type< vector_typet > (const typet &type)
	Check whether a reference to a typet is a vector_typet. More...

const vector_typet &	to_vector_type (const typet &type)
	Cast a typet to a vector_typet. More...

vector_typet &	to_vector_type (typet &type)
	Cast a typet to a vector_typet. More...

template<>
bool	can_cast_type< complex_typet > (const typet &type)
	Check whether a reference to a typet is a complex_typet. More...

const complex_typet &	to_complex_type (const typet &type)
	Cast a typet to a complex_typet. More...

complex_typet &	to_complex_type (typet &type)
	Cast a typet to a complex_typet. More...

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

Detailed Description

Pre-defined types.

Definition in file std_types.h.

Function Documentation

◆ can_cast_type< array_typet >()

template<>

bool can_cast_type< array_typet > ( const typet & type )

inline

Check whether a reference to a typet is a array_typet.

Parameters

type	Source type.

Returns: True if type is a array_typet.

Definition at line 875 of file std_types.h.

◆ can_cast_type< bitvector_typet >()

template<>

bool can_cast_type< bitvector_typet > ( const typet & type )

inline

Check whether a reference to a typet is a bitvector_typet.

Parameters

type	Source type.

Returns: True if type is a bitvector_typet.

Definition at line 952 of file std_types.h.

◆ can_cast_type< bool_typet >()

template<>

bool can_cast_type< bool_typet > ( const typet & base )

inline

Definition at line 44 of file std_types.h.

◆ can_cast_type< class_typet >()

template<>

bool can_cast_type< class_typet > ( const typet & type )

inline

Check whether a reference to a typet is a class_typet.

Parameters

type	Source type.

Returns: True if type is a class_typet.

Definition at line 368 of file std_types.h.

◆ can_cast_type< code_typet >()

template<>

bool can_cast_type< code_typet > ( const typet & type )

inline

Check whether a reference to a typet is a code_typet.

Parameters

type	Source type.

Returns: True if type is a code_typet.

Definition at line 775 of file std_types.h.

◆ can_cast_type< complex_typet >()

template<>

bool can_cast_type< complex_typet > ( const typet & type )

inline

Check whether a reference to a typet is a complex_typet.

Parameters

type	Source type.

Returns: True if type is a complex_typet.

Definition at line 1142 of file std_types.h.

◆ can_cast_type< enumeration_typet >()

template<>

bool can_cast_type< enumeration_typet > ( const typet & type )

inline

Check whether a reference to a typet is a enumeration_typet.

Parameters

type	Source type.

Returns: True if type is a enumeration_typet.

Definition at line 555 of file std_types.h.

◆ can_cast_type< range_typet >()

template<>

bool can_cast_type< range_typet > ( const typet & type )

inline

Check whether a reference to a typet is a range_typet.

Parameters

type	Source type.

Returns: True if type is a range_typet.

Definition at line 1024 of file std_types.h.

◆ can_cast_type< string_typet >()

template<>

bool can_cast_type< string_typet > ( const typet & type )

inline

Check whether a reference to a typet is a string_typet.

Parameters

type	Source type.

Returns: True if type is a string_typet.

Definition at line 977 of file std_types.h.

◆ can_cast_type< struct_or_union_tag_typet >()

template<>

bool can_cast_type< struct_or_union_tag_typet > ( const typet & type )

inline

Check whether a reference to a typet is a struct_or_union_tag_typet.

Parameters

type	Source type.

Returns: True if type is a struct_or_union_tag_typet.

Definition at line 464 of file std_types.h.

◆ can_cast_type< struct_tag_typet >()

template<>

bool can_cast_type< struct_tag_typet > ( const typet & type )

inline

Check whether a reference to a typet is a struct_tag_typet.

Parameters

type	Source type.

Returns: True if type is a struct_tag_typet.

Definition at line 505 of file std_types.h.

◆ can_cast_type< struct_typet >()

template<>

bool can_cast_type< struct_typet > ( const typet & type )

inline

Check whether a reference to a typet is a struct_typet.

Parameters

type	Source type.

Returns: True if type is a struct_typet.

Definition at line 295 of file std_types.h.

◆ can_cast_type< struct_union_typet >()

template<>

bool can_cast_type< struct_union_typet > ( const typet & type )

inline

Check whether a reference to a typet is a struct_union_typet.

Parameters

type	Source type.

Returns: True if type is a struct_union_typet.

Definition at line 201 of file std_types.h.

◆ can_cast_type< tag_typet >()

template<>

bool can_cast_type< tag_typet > ( const typet & type )

inline

Check whether a reference to a typet is a tag_typet.

Parameters

type	Source type.

Returns: True if type is a tag_typet.

Definition at line 420 of file std_types.h.

◆ can_cast_type< vector_typet >()

template<>

bool can_cast_type< vector_typet > ( const typet & type )

inline

Check whether a reference to a typet is a vector_typet.

Parameters

type	Source type.

Returns: True if type is a vector_typet.

Definition at line 1100 of file std_types.h.

◆ is_constant()

bool is_constant ( const typet & type )

inline

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

Definition at line 29 of file std_types.h.

◆ is_constant_or_has_constant_components()

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.

Examples include:

const int a;
struct contains_constant_pointer { int x; int * const p; };
const int b[3];
Parameters

type The type we want to query constness of.

ns The namespace, needed for resolution of symbols.

Returns
Whether passed in type is const or not.

Definition at line 197 of file std_types.cpp.

◆ to_array_type() [1/2]

const array_typet& to_array_type ( const typet & type )

inline

Cast a typet to an array_typet.

This is an unchecked conversion. type must be known to be array_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type array_typet.

Definition at line 888 of file std_types.h.

◆ to_array_type() [2/2]

array_typet& to_array_type ( typet & type )

inline

Cast a typet to an array_typet.

This is an unchecked conversion. type must be known to be array_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type array_typet.

Definition at line 896 of file std_types.h.

◆ to_class_type() [1/2]

const class_typet& to_class_type ( const typet & type )

inline

Cast a typet to a class_typet.

This is an unchecked conversion. type must be known to be class_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type class_typet.

Definition at line 381 of file std_types.h.

◆ to_class_type() [2/2]

class_typet& to_class_type ( typet & type )

inline

Cast a typet to a class_typet.

This is an unchecked conversion. type must be known to be class_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type class_typet.

Definition at line 388 of file std_types.h.

◆ to_code_type() [1/2]

const code_typet& to_code_type ( const typet & type )

inline

Cast a typet to a code_typet.

This is an unchecked conversion. type must be known to be code_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type code_typet.

Definition at line 788 of file std_types.h.

◆ to_code_type() [2/2]

code_typet& to_code_type ( typet & type )

inline

Cast a typet to a code_typet.

This is an unchecked conversion. type must be known to be code_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type code_typet.

Definition at line 796 of file std_types.h.

◆ to_complex_type() [1/2]

const complex_typet& to_complex_type ( const typet & type )

inline

Cast a typet to a complex_typet.

This is an unchecked conversion. type must be known to be complex_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type complex_typet.

Definition at line 1155 of file std_types.h.

◆ to_complex_type() [2/2]

complex_typet& to_complex_type ( typet & type )

inline

Cast a typet to a complex_typet.

This is an unchecked conversion. type must be known to be complex_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type complex_typet.

Definition at line 1163 of file std_types.h.

◆ to_enumeration_type() [1/2]

const enumeration_typet& to_enumeration_type ( const typet & type )

inline

Cast a typet to a enumeration_typet.

This is an unchecked conversion. type must be known to be enumeration_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type enumeration_typet.

Definition at line 568 of file std_types.h.

◆ to_enumeration_type() [2/2]

enumeration_typet& to_enumeration_type ( typet & type )

inline

Cast a typet to a enumeration_typet.

This is an unchecked conversion. type must be known to be enumeration_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type enumeration_typet.

Definition at line 575 of file std_types.h.

◆ to_range_type() [1/2]

const range_typet& to_range_type ( const typet & type )

inline

Cast a typet to a range_typet.

This is an unchecked conversion. type must be known to be range_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type range_typet.

Definition at line 1037 of file std_types.h.

◆ to_range_type() [2/2]

range_typet& to_range_type ( typet & type )

inline

Cast a typet to a range_typet.

This is an unchecked conversion. type must be known to be range_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type range_typet.

Definition at line 1044 of file std_types.h.

◆ to_string_type() [1/2]

const string_typet& to_string_type ( const typet & type )

inline

Cast a typet to a string_typet.

This is an unchecked conversion. type must be known to be string_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type string_typet.

Definition at line 990 of file std_types.h.

◆ to_string_type() [2/2]

string_typet& to_string_type ( typet & type )

inline

Cast a typet to a string_typet.

This is an unchecked conversion. type must be known to be string_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type string_typet.

Definition at line 997 of file std_types.h.

◆ to_struct_or_union_tag_type() [1/2]

const struct_or_union_tag_typet& to_struct_or_union_tag_type ( const typet & type )

inline

Cast a typet to a struct_or_union_tag_typet.

This is an unchecked conversion. type must be known to be struct_or_union_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type struct_or_union_tag_typet

Definition at line 478 of file std_types.h.

◆ to_struct_or_union_tag_type() [2/2]

struct_or_union_tag_typet& to_struct_or_union_tag_type ( typet & type )

inline

Cast a typet to a struct_or_union_tag_typet.

This is an unchecked conversion. type must be known to be struct_or_union_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type struct_or_union_tag_typet

Definition at line 485 of file std_types.h.

◆ to_struct_tag_type() [1/2]

const struct_tag_typet& to_struct_tag_type ( const typet & type )

inline

Cast a typet to a struct_tag_typet.

This is an unchecked conversion. type must be known to be struct_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type struct_tag_typet

Definition at line 518 of file std_types.h.

◆ to_struct_tag_type() [2/2]

struct_tag_typet& to_struct_tag_type ( typet & type )

inline

Cast a typet to a struct_tag_typet.

This is an unchecked conversion. type must be known to be struct_tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type struct_tag_typet

Definition at line 525 of file std_types.h.

◆ to_struct_type() [1/2]

const struct_typet& to_struct_type ( const typet & type )

inline

Cast a typet to a struct_typet.

This is an unchecked conversion. type must be known to be struct_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type struct_typet.

Definition at line 308 of file std_types.h.

◆ to_struct_type() [2/2]

struct_typet& to_struct_type ( typet & type )

inline

Cast a typet to a struct_typet.

This is an unchecked conversion. type must be known to be struct_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type struct_typet.

Definition at line 315 of file std_types.h.

◆ to_struct_union_type() [1/2]

const struct_union_typet& to_struct_union_type ( const typet & type )

inline

Cast a typet to a struct_union_typet.

This is an unchecked conversion. type must be known to be struct_union_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type

Returns: Object of type struct_union_typet

Definition at line 214 of file std_types.h.

◆ to_struct_union_type() [2/2]

struct_union_typet& to_struct_union_type ( typet & type )

inline

Cast a typet to a struct_union_typet.

This is an unchecked conversion. type must be known to be struct_union_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type

Returns: Object of type struct_union_typet

Definition at line 221 of file std_types.h.

◆ to_tag_type() [1/2]

const tag_typet& to_tag_type ( const typet & type )

inline

Cast a typet to a tag_typet.

This is an unchecked conversion. type must be known to be tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type tag_typet.

Definition at line 434 of file std_types.h.

◆ to_tag_type() [2/2]

tag_typet& to_tag_type ( typet & type )

inline

Cast a typet to a tag_typet.

This is an unchecked conversion. type must be known to be tag_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type tag_typet.

Definition at line 441 of file std_types.h.

◆ to_vector_type() [1/2]

const vector_typet& to_vector_type ( const typet & type )

inline

Cast a typet to a vector_typet.

This is an unchecked conversion. type must be known to be vector_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type vector_typet.

Definition at line 1113 of file std_types.h.

◆ to_vector_type() [2/2]

vector_typet& to_vector_type ( typet & type )

inline

Cast a typet to a vector_typet.

This is an unchecked conversion. type must be known to be vector_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type vector_typet.

Definition at line 1121 of file std_types.h.

type	The type we want to query constness of.
ns	The namespace, needed for resolution of symbols.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_type< array_typet >()

◆ can_cast_type< bitvector_typet >()

◆ can_cast_type< bool_typet >()

◆ can_cast_type< class_typet >()

◆ can_cast_type< code_typet >()

◆ can_cast_type< complex_typet >()

◆ can_cast_type< enumeration_typet >()

◆ can_cast_type< range_typet >()

◆ can_cast_type< string_typet >()

◆ can_cast_type< struct_or_union_tag_typet >()

◆ can_cast_type< struct_tag_typet >()

◆ can_cast_type< struct_typet >()

◆ can_cast_type< struct_union_typet >()

◆ can_cast_type< tag_typet >()

◆ can_cast_type< vector_typet >()

◆ is_constant()

◆ is_constant_or_has_constant_components()

◆ to_array_type() [1/2]

◆ to_array_type() [2/2]

◆ to_class_type() [1/2]

◆ to_class_type() [2/2]

◆ to_code_type() [1/2]

◆ to_code_type() [2/2]

◆ to_complex_type() [1/2]

◆ to_complex_type() [2/2]

◆ to_enumeration_type() [1/2]

◆ to_enumeration_type() [2/2]

◆ to_range_type() [1/2]

◆ to_range_type() [2/2]

◆ to_string_type() [1/2]

◆ to_string_type() [2/2]

◆ to_struct_or_union_tag_type() [1/2]

◆ to_struct_or_union_tag_type() [2/2]

◆ to_struct_tag_type() [1/2]

◆ to_struct_tag_type() [2/2]

◆ to_struct_type() [1/2]

◆ to_struct_type() [2/2]

◆ to_struct_union_type() [1/2]

◆ to_struct_union_type() [2/2]

◆ to_tag_type() [1/2]

◆ to_tag_type() [2/2]

◆ to_vector_type() [1/2]

◆ to_vector_type() [2/2]