CBMC
std_types.h File Reference

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_typetto_struct_union_type (const typet &type)
 Cast a typet to a struct_union_typet. More...
 
struct_union_typetto_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_typetto_struct_type (const typet &type)
 Cast a typet to a struct_typet. More...
 
struct_typetto_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_typetto_class_type (const typet &type)
 Cast a typet to a class_typet. More...
 
class_typetto_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_typetto_tag_type (const typet &type)
 Cast a typet to a tag_typet. More...
 
tag_typetto_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_typetto_struct_or_union_tag_type (const typet &type)
 Cast a typet to a struct_or_union_tag_typet. More...
 
struct_or_union_tag_typetto_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_typetto_struct_tag_type (const typet &type)
 Cast a typet to a struct_tag_typet. More...
 
struct_tag_typetto_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_typetto_enumeration_type (const typet &type)
 Cast a typet to a enumeration_typet. More...
 
enumeration_typetto_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_typetto_code_type (const typet &type)
 Cast a typet to a code_typet. More...
 
code_typetto_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_typetto_array_type (const typet &type)
 Cast a typet to an array_typet. More...
 
array_typetto_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_typetto_string_type (const typet &type)
 Cast a typet to a string_typet. More...
 
string_typetto_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_typetto_range_type (const typet &type)
 Cast a typet to a range_typet. More...
 
range_typetto_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_typetto_vector_type (const typet &type)
 Cast a typet to a vector_typet. More...
 
vector_typetto_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_typetto_complex_type (const typet &type)
 Cast a typet to a complex_typet. More...
 
complex_typetto_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
typeSource 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
typeSource type.
Returns
True if type is a bitvector_typet.

Definition at line 943 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
typeSource 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
typeSource 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
typeSource type.
Returns
True if type is a complex_typet.

Definition at line 1133 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
typeSource 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
typeSource type.
Returns
True if type is a range_typet.

Definition at line 1015 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
typeSource type.
Returns
True if type is a string_typet.

Definition at line 968 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource type.
Returns
True if type is a vector_typet.

Definition at line 1091 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
    typeThe type we want to query constness of.
    nsThe namespace, needed for resolution of symbols.
    Returns
    Whether passed in type is const or not.

Definition at line 186 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource type.
Returns
Object of type complex_typet.

Definition at line 1146 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
typeSource type.
Returns
Object of type complex_typet.

Definition at line 1154 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
typeSource 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
typeSource 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
typeSource type.
Returns
Object of type range_typet.

Definition at line 1028 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
typeSource type.
Returns
Object of type range_typet.

Definition at line 1035 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
typeSource type.
Returns
Object of type string_typet.

Definition at line 981 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
typeSource type.
Returns
Object of type string_typet.

Definition at line 988 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource 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
typeSource type.
Returns
Object of type vector_typet.

Definition at line 1104 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
typeSource type.
Returns
Object of type vector_typet.

Definition at line 1112 of file std_types.h.