CBMC
c_types.h File Reference
#include "deprecate.h"
#include "pointer_expr.h"
+ Include dependency graph for c_types.h:

Go to the source code of this file.

Classes

class  c_bit_field_typet
 Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More...
 
class  c_bool_typet
 The C/C++ Booleans. More...
 
class  union_typet
 The union type. More...
 
class  union_tag_typet
 A union tag type, i.e., union_typet with an identifier. More...
 
class  c_enum_typet
 The type of C enums. More...
 
class  c_enum_typet::c_enum_membert
 
class  c_enum_tag_typet
 C enum tag type, i.e., c_enum_typet with an identifier. More...
 
class  code_with_contract_typet
 

Functions

template<>
bool can_cast_type< c_bit_field_typet > (const typet &type)
 Check whether a reference to a typet is a c_bit_field_typet. More...
 
const c_bit_field_typetto_c_bit_field_type (const typet &type)
 Cast a typet to a c_bit_field_typet. More...
 
c_bit_field_typetto_c_bit_field_type (typet &type)
 Cast a typet to a c_bit_field_typet. More...
 
template<>
bool can_cast_type< c_bool_typet > (const typet &type)
 Check whether a reference to a typet is a c_bool_typet. More...
 
const c_bool_typetto_c_bool_type (const typet &type)
 Cast a typet to a c_bool_typet. More...
 
c_bool_typetto_c_bool_type (typet &type)
 Cast a typet to a c_bool_typet. More...
 
template<>
bool can_cast_type< union_typet > (const typet &type)
 Check whether a reference to a typet is a union_typet. More...
 
const union_typetto_union_type (const typet &type)
 Cast a typet to a union_typet. More...
 
union_typetto_union_type (typet &type)
 Cast a typet to a union_typet. More...
 
template<>
bool can_cast_type< union_tag_typet > (const typet &type)
 Check whether a reference to a typet is a union_tag_typet. More...
 
const union_tag_typetto_union_tag_type (const typet &type)
 Cast a typet to a union_tag_typet. More...
 
union_tag_typetto_union_tag_type (typet &type)
 Cast a typet to a union_tag_typet. More...
 
template<>
bool can_cast_type< c_enum_typet > (const typet &type)
 Check whether a reference to a typet is a c_enum_typet. More...
 
const c_enum_typetto_c_enum_type (const typet &type)
 Cast a typet to a c_enum_typet. More...
 
c_enum_typetto_c_enum_type (typet &type)
 Cast a typet to a c_enum_typet. More...
 
template<>
bool can_cast_type< c_enum_tag_typet > (const typet &type)
 Check whether a reference to a typet is a c_enum_tag_typet. More...
 
const c_enum_tag_typetto_c_enum_tag_type (const typet &type)
 Cast a typet to a c_enum_tag_typet. More...
 
c_enum_tag_typetto_c_enum_tag_type (typet &type)
 Cast a typet to a c_enum_tag_typet. More...
 
template<>
bool can_cast_type< code_with_contract_typet > (const typet &type)
 Check whether a reference to a typet is a code_typet. More...
 
const code_with_contract_typetto_code_with_contract_type (const typet &type)
 Cast a typet to a code_with_contract_typet. More...
 
code_with_contract_typetto_code_with_contract_type (typet &type)
 Cast a typet to a code_typet. More...
 
bitvector_typet c_index_type ()
 
signedbv_typet signed_int_type ()
 
unsignedbv_typet unsigned_int_type ()
 
signedbv_typet signed_long_int_type ()
 
signedbv_typet signed_short_int_type ()
 
unsignedbv_typet unsigned_short_int_type ()
 
signedbv_typet signed_long_long_int_type ()
 
unsignedbv_typet unsigned_long_int_type ()
 
unsignedbv_typet unsigned_long_long_int_type ()
 
typet c_bool_type ()
 
bitvector_typet char_type ()
 
unsignedbv_typet unsigned_char_type ()
 
signedbv_typet signed_char_type ()
 
bitvector_typet wchar_t_type ()
 
unsignedbv_typet char16_t_type ()
 
unsignedbv_typet char32_t_type ()
 
floatbv_typet float_type ()
 
floatbv_typet double_type ()
 
floatbv_typet long_double_type ()
 
unsignedbv_typet size_type ()
 
signedbv_typet signed_size_type ()
 
signedbv_typet pointer_diff_type ()
 
pointer_typet pointer_type (const typet &)
 
empty_typet void_type ()
 
reference_typet reference_type (const typet &)
 
std::string c_type_as_string (const irep_idt &)
 

Function Documentation

◆ c_bool_type()

typet c_bool_type ( )

Definition at line 100 of file c_types.cpp.

◆ c_index_type()

bitvector_typet c_index_type ( )

Definition at line 16 of file c_types.cpp.

◆ c_type_as_string()

std::string c_type_as_string ( const irep_idt c_type)

Definition at line 251 of file c_types.cpp.

◆ can_cast_type< c_bit_field_typet >()

template<>
bool can_cast_type< c_bit_field_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_bit_field_typet.

Parameters
typeSource type.
Returns
True if type is a c_bit_field_typet.

Definition at line 67 of file c_types.h.

◆ can_cast_type< c_bool_typet >()

template<>
bool can_cast_type< c_bool_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_bool_typet.

Parameters
typeSource type.
Returns
True if type is a c_bool_typet.

Definition at line 115 of file c_types.h.

◆ can_cast_type< c_enum_tag_typet >()

template<>
bool can_cast_type< c_enum_tag_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_enum_tag_typet.

Parameters
typeSource type.
Returns
True if type is a c_enum_tag_typet.

Definition at line 364 of file c_types.h.

◆ can_cast_type< c_enum_typet >()

template<>
bool can_cast_type< c_enum_typet > ( const typet type)
inline

Check whether a reference to a typet is a c_enum_typet.

Parameters
typeSource type.
Returns
True if type is a c_enum_typet.

Definition at line 322 of file c_types.h.

◆ can_cast_type< code_with_contract_typet >()

template<>
bool can_cast_type< code_with_contract_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 453 of file c_types.h.

◆ can_cast_type< union_tag_typet >()

template<>
bool can_cast_type< union_tag_typet > ( const typet type)
inline

Check whether a reference to a typet is a union_tag_typet.

Parameters
typeSource type.
Returns
True if type is a union_tag_typet.

Definition at line 211 of file c_types.h.

◆ can_cast_type< union_typet >()

template<>
bool can_cast_type< union_typet > ( const typet type)
inline

Check whether a reference to a typet is a union_typet.

Parameters
typeSource type.
Returns
True if type is a union_typet.

Definition at line 171 of file c_types.h.

◆ char16_t_type()

unsignedbv_typet char16_t_type ( )

Definition at line 157 of file c_types.cpp.

◆ char32_t_type()

unsignedbv_typet char32_t_type ( )

Definition at line 167 of file c_types.cpp.

◆ char_type()

bitvector_typet char_type ( )

Definition at line 106 of file c_types.cpp.

◆ double_type()

floatbv_typet double_type ( )

Definition at line 185 of file c_types.cpp.

◆ float_type()

floatbv_typet float_type ( )

Definition at line 177 of file c_types.cpp.

◆ long_double_type()

floatbv_typet long_double_type ( )

Definition at line 193 of file c_types.cpp.

◆ pointer_diff_type()

signedbv_typet pointer_diff_type ( )

Definition at line 220 of file c_types.cpp.

◆ pointer_type()

pointer_typet pointer_type ( const typet subtype)

Definition at line 235 of file c_types.cpp.

◆ reference_type()

reference_typet reference_type ( const typet subtype)

Definition at line 240 of file c_types.cpp.

◆ signed_char_type()

signedbv_typet signed_char_type ( )

Definition at line 134 of file c_types.cpp.

◆ signed_int_type()

signedbv_typet signed_int_type ( )

Definition at line 22 of file c_types.cpp.

◆ signed_long_int_type()

signedbv_typet signed_long_int_type ( )

Definition at line 72 of file c_types.cpp.

◆ signed_long_long_int_type()

signedbv_typet signed_long_long_int_type ( )

Definition at line 79 of file c_types.cpp.

◆ signed_short_int_type()

signedbv_typet signed_short_int_type ( )

Definition at line 29 of file c_types.cpp.

◆ signed_size_type()

signedbv_typet signed_size_type ( )

Definition at line 66 of file c_types.cpp.

◆ size_type()

unsignedbv_typet size_type ( )

Definition at line 50 of file c_types.cpp.

◆ to_c_bit_field_type() [1/2]

const c_bit_field_typet& to_c_bit_field_type ( const typet type)
inline

Cast a typet to a c_bit_field_typet.

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

Parameters
typeSource type.
Returns
Object of type c_bit_field_typet.

Definition at line 80 of file c_types.h.

◆ to_c_bit_field_type() [2/2]

c_bit_field_typet& to_c_bit_field_type ( typet type)
inline

Cast a typet to a c_bit_field_typet.

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

Parameters
typeSource type.
Returns
Object of type c_bit_field_typet.

Definition at line 88 of file c_types.h.

◆ to_c_bool_type() [1/2]

const c_bool_typet& to_c_bool_type ( const typet type)
inline

Cast a typet to a c_bool_typet.

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

Parameters
typeSource type.
Returns
Object of type c_bool_typet.

Definition at line 128 of file c_types.h.

◆ to_c_bool_type() [2/2]

c_bool_typet& to_c_bool_type ( typet type)
inline

Cast a typet to a c_bool_typet.

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

Parameters
typeSource type.
Returns
Object of type c_bool_typet.

Definition at line 136 of file c_types.h.

◆ to_c_enum_tag_type() [1/2]

const c_enum_tag_typet& to_c_enum_tag_type ( const typet type)
inline

Cast a typet to a c_enum_tag_typet.

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

Parameters
typeSource type.
Returns
Object of type c_enum_tag_typet.

Definition at line 377 of file c_types.h.

◆ to_c_enum_tag_type() [2/2]

c_enum_tag_typet& to_c_enum_tag_type ( typet type)
inline

Cast a typet to a c_enum_tag_typet.

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

Parameters
typeSource type.
Returns
Object of type c_enum_tag_typet.

Definition at line 384 of file c_types.h.

◆ to_c_enum_type() [1/2]

const c_enum_typet& to_c_enum_type ( const typet type)
inline

Cast a typet to a c_enum_typet.

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

Parameters
typeSource type.
Returns
Object of type c_enum_typet.

Definition at line 335 of file c_types.h.

◆ to_c_enum_type() [2/2]

c_enum_typet& to_c_enum_type ( typet type)
inline

Cast a typet to a c_enum_typet.

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

Parameters
typeSource type.
Returns
Object of type c_enum_typet.

Definition at line 343 of file c_types.h.

◆ to_code_with_contract_type() [1/2]

const code_with_contract_typet& to_code_with_contract_type ( const typet type)
inline

Cast a typet to a code_with_contract_typet.

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

Parameters
typeSource type.
Returns
Object of type code_with_contract_typet.

Definition at line 467 of file c_types.h.

◆ to_code_with_contract_type() [2/2]

code_with_contract_typet& to_code_with_contract_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 475 of file c_types.h.

◆ to_union_tag_type() [1/2]

const union_tag_typet& to_union_tag_type ( const typet type)
inline

Cast a typet to a union_tag_typet.

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

Parameters
typeSource type.
Returns
Object of type union_tag_typet.

Definition at line 224 of file c_types.h.

◆ to_union_tag_type() [2/2]

union_tag_typet& to_union_tag_type ( typet type)
inline

Cast a typet to a union_tag_typet.

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

Parameters
typeSource type.
Returns
Object of type union_tag_typet.

Definition at line 231 of file c_types.h.

◆ to_union_type() [1/2]

const union_typet& to_union_type ( const typet type)
inline

Cast a typet to a union_typet.

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

Parameters
typeSource type.
Returns
Object of type union_typet

Definition at line 184 of file c_types.h.

◆ to_union_type() [2/2]

union_typet& to_union_type ( typet type)
inline

Cast a typet to a union_typet.

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

Parameters
typeSource type.
Returns
Object of type union_typet

Definition at line 191 of file c_types.h.

◆ unsigned_char_type()

unsignedbv_typet unsigned_char_type ( )

Definition at line 127 of file c_types.cpp.

◆ unsigned_int_type()

unsignedbv_typet unsigned_int_type ( )

Definition at line 36 of file c_types.cpp.

◆ unsigned_long_int_type()

unsignedbv_typet unsigned_long_int_type ( )

Definition at line 86 of file c_types.cpp.

◆ unsigned_long_long_int_type()

unsignedbv_typet unsigned_long_long_int_type ( )

Definition at line 93 of file c_types.cpp.

◆ unsigned_short_int_type()

unsignedbv_typet unsigned_short_int_type ( )

Definition at line 43 of file c_types.cpp.

◆ void_type()

empty_typet void_type ( )

Definition at line 245 of file c_types.cpp.

◆ wchar_t_type()

bitvector_typet wchar_t_type ( )

Definition at line 141 of file c_types.cpp.