cprover
std_types.h File Reference

API to type classes. More...

#include <cassert>
#include "expr.h"
#include "mp_arith.h"
Include dependency graph for std_types.h:

Go to the source code of this file.

Classes

class  bool_typet
 The proper Booleans. More...
 
class  nil_typet
 The NIL type. More...
 
class  empty_typet
 The empty type. More...
 
class  void_typet
 The void type. More...
 
class  integer_typet
 Unbounded, signed integers. More...
 
class  natural_typet
 Natural numbers (which include zero) More...
 
class  rational_typet
 Unbounded, signed rational numbers. More...
 
class  real_typet
 Unbounded, signed real numbers. More...
 
class  symbol_typet
 A reference into the symbol table. More...
 
class  struct_union_typet
 Base type of C structs and unions, and C++ classes. More...
 
class  struct_union_typet::componentt
 
class  struct_typet
 Structure type. More...
 
class  class_typet
 C++ class type. More...
 
class  union_typet
 The union type. More...
 
class  tag_typet
 A generic tag-based type. More...
 
class  struct_tag_typet
 A struct tag type. More...
 
class  union_tag_typet
 A union tag type. More...
 
class  enumeration_typet
 A generic enumeration type (not to be confused with C enums) More...
 
class  c_enum_typet
 The type of C enums. More...
 
class  c_enum_typet::c_enum_membert
 
class  c_enum_tag_typet
 An enum tag type. More...
 
class  code_typet
 Base type of functions. More...
 
class  code_typet::parametert
 
class  array_typet
 arrays with given size More...
 
class  incomplete_array_typet
 arrays without size More...
 
class  bitvector_typet
 Base class of bitvector types. More...
 
class  bv_typet
 fixed-width bit-vector without numerical interpretation More...
 
class  unsignedbv_typet
 Fixed-width bit-vector with unsigned binary interpretation. More...
 
class  signedbv_typet
 Fixed-width bit-vector with two's complement interpretation. More...
 
class  fixedbv_typet
 Fixed-width bit-vector with signed fixed-point interpretation. More...
 
class  floatbv_typet
 Fixed-width bit-vector with IEEE floating-point interpretation. More...
 
class  c_bit_field_typet
 Type for c bit fields. More...
 
class  pointer_typet
 The pointer type. More...
 
class  reference_typet
 The reference type. More...
 
class  c_bool_typet
 The C/C++ Booleans. More...
 
class  string_typet
 TO_BE_DOCUMENTED. More...
 
class  range_typet
 A type for subranges of integers. More...
 
class  vector_typet
 A constant-size array type. More...
 
class  complex_typet
 Complex numbers made of pair of given subtype. More...
 

Functions

const symbol_typetto_symbol_type (const typet &type)
 Cast a generic typet to a symbol_typet. More...
 
symbol_typetto_symbol_type (typet &type)
 Cast a generic typet to a symbol_typet. More...
 
const struct_union_typetto_struct_union_type (const typet &type)
 Cast a generic typet to a struct_union_typet. More...
 
struct_union_typetto_struct_union_type (typet &type)
 Cast a generic typet to a struct_union_typet. More...
 
const struct_typetto_struct_type (const typet &type)
 Cast a generic typet to a struct_typet. More...
 
struct_typetto_struct_type (typet &type)
 Cast a generic typet to a struct_typet. More...
 
const class_typetto_class_type (const typet &type)
 Cast a generic typet to a class_typet. More...
 
class_typetto_class_type (typet &type)
 Cast a generic typet to a class_typet. More...
 
const union_typetto_union_type (const typet &type)
 Cast a generic typet to a union_typet. More...
 
union_typetto_union_type (typet &type)
 Cast a generic typet to a union_typet. More...
 
const tag_typetto_tag_type (const typet &type)
 Cast a generic typet to a tag_typet. More...
 
tag_typetto_tag_type (typet &type)
 Cast a generic typet to a tag_typet. More...
 
const struct_tag_typetto_struct_tag_type (const typet &type)
 Cast a generic typet to a union_tag_typet. More...
 
struct_tag_typetto_struct_tag_type (typet &type)
 Cast a generic typet to a union_tag_typet. More...
 
const union_tag_typetto_union_tag_type (const typet &type)
 Cast a generic typet to a union_tag_typet. More...
 
union_tag_typetto_union_tag_type (typet &type)
 Cast a generic typet to a union_tag_typet. More...
 
const enumeration_typetto_enumeration_type (const typet &type)
 Cast a generic typet to a enumeration_typet. More...
 
enumeration_typetto_enumeration_type (typet &type)
 Cast a generic typet to a enumeration_typet. More...
 
const c_enum_typetto_c_enum_type (const typet &type)
 Cast a generic typet to a c_enum_typet. More...
 
c_enum_typetto_c_enum_type (typet &type)
 Cast a generic typet to a c_enum_typet. More...
 
const c_enum_tag_typetto_c_enum_tag_type (const typet &type)
 Cast a generic typet to a c_enum_tag_typet. More...
 
c_enum_tag_typetto_c_enum_tag_type (typet &type)
 
const code_typetto_code_type (const typet &type)
 Cast a generic typet to a code_typet. More...
 
code_typetto_code_type (typet &type)
 Cast a generic typet to a code_typet. More...
 
const array_typetto_array_type (const typet &type)
 Cast a generic typet to an array_typet. More...
 
array_typetto_array_type (typet &type)
 Cast a generic typet to an array_typet. More...
 
const incomplete_array_typetto_incomplete_array_type (const typet &type)
 Cast a generic typet to an incomplete_array_typet. More...
 
incomplete_array_typetto_incomplete_array_type (typet &type)
 Cast a generic typet to an incomplete_array_typet. More...
 
const bitvector_typetto_bitvector_type (const typet &type)
 Cast a generic typet to a bitvector_typet. More...
 
bitvector_typetto_bitvector_type (typet &type)
 
const bv_typetto_bv_type (const typet &type)
 Cast a generic typet to a bv_typet. More...
 
bv_typetto_bv_type (typet &type)
 Cast a generic typet to a bv_typet. More...
 
const unsignedbv_typetto_unsignedbv_type (const typet &type)
 Cast a generic typet to an unsignedbv_typet. More...
 
unsignedbv_typetto_unsignedbv_type (typet &type)
 Cast a generic typet to an unsignedbv_typet. More...
 
const signedbv_typetto_signedbv_type (const typet &type)
 Cast a generic typet to a signedbv_typet. More...
 
signedbv_typetto_signedbv_type (typet &type)
 Cast a generic typet to a signedbv_typet. More...
 
const fixedbv_typetto_fixedbv_type (const typet &type)
 Cast a generic typet to a fixedbv_typet. More...
 
const floatbv_typetto_floatbv_type (const typet &type)
 Cast a generic typet to a floatbv_typet. More...
 
const c_bit_field_typetto_c_bit_field_type (const typet &type)
 Cast a generic typet to a c_bit_field_typet. More...
 
c_bit_field_typetto_c_bit_field_type (typet &type)
 Cast a generic typet to a c_bit_field_typet. More...
 
const pointer_typetto_pointer_type (const typet &type)
 Cast a generic typet to a pointer_typet. More...
 
pointer_typetto_pointer_type (typet &type)
 Cast a generic typet to a pointer_typet. More...
 
const reference_typetto_reference_type (const typet &type)
 Cast a generic typet to a reference_typet. More...
 
reference_typetto_reference_type (typet &type)
 Cast a generic typet to a reference_typet. More...
 
bool is_reference (const typet &type)
 TO_BE_DOCUMENTED. More...
 
bool is_rvalue_reference (const typet &type)
 TO_BE_DOCUMENTED. More...
 
const c_bool_typetto_c_bool_type (const typet &type)
 Cast a generic typet to a c_bool_typet. More...
 
c_bool_typetto_c_bool_type (typet &type)
 Cast a generic typet to a c_bool_typet. More...
 
const string_typetto_string_type (const typet &type)
 Cast a generic typet to a string_typet. More...
 
const range_typetto_range_type (const typet &type)
 Cast a generic typet to a range_typet. More...
 
const vector_typetto_vector_type (const typet &type)
 Cast a generic typet to a vector_typet. More...
 
vector_typetto_vector_type (typet &type)
 Cast a generic typet to a vector_typet. More...
 
const complex_typetto_complex_type (const typet &type)
 Cast a generic typet to a complex_typet. More...
 
complex_typetto_complex_type (typet &type)
 Cast a generic typet to a complex_typet. More...
 

Detailed Description

API to type classes.

Author
Daniel Kroening kroen.nosp@m.ing@.nosp@m.kroen.nosp@m.ing..nosp@m.com
Date
Sun Jul 31 21:54:44 BST 2011

Definition in file std_types.h.

Function Documentation

§ is_reference()

bool is_reference ( const typet type)

TO_BE_DOCUMENTED.

Definition at line 105 of file std_types.cpp.

References irept::get_bool(), and irept::id().

Referenced by cpp_typecheckt::add_implicit_dereference(), cpp_typecheckt::cast_away_constness(), cpp_typecheckt::const_typecast(), cpp_typecheckt::convert_initializer(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), expr2cppt::convert_rec(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_typecheckt::cpp_is_pod(), cpp_type2name(), cpp_typecheck_resolvet::disambiguate_functions(), cpp_typecheckt::dtor(), cpp_typecheckt::dynamic_typecast(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), cpp_typecheck_resolvet::guess_template_args(), cpp_typecheckt::implicit_conversion_sequence(), irep2name(), cpp_typecheck_fargst::match(), cpp_typecheckt::overloadable(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_compatible(), cpp_typecheckt::reference_initializer(), cpp_typecheckt::reference_related(), cpp_typecheckt::reinterpret_typecast(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_qualification(), cpp_typecheckt::standard_conversion_sequence(), to_reference_type(), cpp_typecheckt::typecheck_expr_address_of(), cpp_typecheckt::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_try_catch(), and cpp_typecheckt::user_defined_conversion_sequence().

§ is_rvalue_reference()

bool is_rvalue_reference ( const typet type)

§ to_bitvector_type()

bitvector_typet& to_bitvector_type ( typet type)
inline

Definition at line 1067 of file std_types.h.

References irept::id().