cprover
std_types.h File Reference

API to type classes. More...

#include "expr.h"
#include "mp_arith.h"
#include "invariant.h"
#include "expr_cast.h"
#include <unordered_map>
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  class_typet::baset
 
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...
 
class  mathematical_function_typet
 A type for mathematical functions (do not confuse with functions/methods in code) More...
 
class  mathematical_function_typet::variablet
 

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...
 
template<>
bool can_cast_type< symbol_typet > (const typet &type)
 
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...
 
template<>
bool can_cast_type< struct_typet > (const typet &type)
 
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...
 
template<>
bool can_cast_type< class_typet > (const typet &type)
 
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...
 
template<>
bool can_cast_type< pointer_typet > (const typet &type)
 
void validate_type (const pointer_typet &type)
 
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...
 
const mathematical_function_typetto_mathematical_function_type (const typet &type)
 Cast a generic typet to a mathematical_function_typet. More...
 
mathematical_function_typetto_mathematical_function_type (typet &type)
 Cast a generic typet to a mathematical_function_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

◆ can_cast_type< class_typet >()

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

Definition at line 451 of file std_types.h.

References can_cast_type< struct_typet >().

Referenced by can_cast_type< java_class_typet >().

◆ can_cast_type< pointer_typet >()

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

Definition at line 1470 of file std_types.h.

◆ can_cast_type< struct_typet >()

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

Definition at line 334 of file std_types.h.

Referenced by can_cast_type< class_typet >().

◆ can_cast_type< symbol_typet >()

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

Definition at line 155 of file std_types.h.

◆ 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 add_generic_type_information(), 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(), pretty_java_type(), 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(), 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_BE_DOCUMENTED.

Definition at line 111 of file std_types.cpp.

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

Referenced by expr2cppt::convert_rec(), cpp_type2name(), and cpp_typecheck_resolvet::guess_template_args().

◆ to_array_type() [1/2]

const array_typet& to_array_type ( const typet type)
inline

Cast a generic typet to an array_typet.

This is an unchecked conversion. type must be known to be array_typet.

Parameters
typeSource type
Returns
Object of type array_typet

Definition at line 1045 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by string_abstractiont::add_dummy_symbol_and_value(), string_refinementt::add_lemma(), linkingt::adjust_object_type_rec(), base_type_eqt::base_type_eq_rec(), base_type_rec(), simplify_exprt::bits2expr(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), string_abstractiont::build_abstraction_type_rec(), string_abstractiont::build_array(), endianness_mapt::build_big_endian(), boolbvt::bv_get_unbounded_array(), interpretert::byte_offset_to_memory_offset(), cpp_typecheckt::check_fixed_size_array(), check_renaming(), goto_program2codet::cleanup_code(), dump_ct::cleanup_type(), arrayst::collect_arrays(), arrayst::collect_indices(), boolbvt::convert_array_of(), expr2ct::convert_array_type(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), dump_ct::convert_compound(), boolbvt::convert_index(), smt2_convt::convert_index(), boolbvt::convert_lambda(), smt2_convt::convert_type(), boolbvt::convert_update_rec(), smt2_convt::convert_with(), boolbvt::convert_with(), interpretert::count_type_leaves(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), string_refinementt::dec_solve(), cpp_typecheckt::default_assignop_value(), goto_symext::dereference_rec(), c_typecheck_baset::designator_enter(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_scanf(), linkingt::duplicate_type_symbol(), interpretert::evaluate(), expr_initializert< nondet >::expr_initializer_rec(), character_refine_preprocesst::expr_of_to_chars(), find_symbols(), smt2_convt::find_symbols(), smt2_convt::find_symbols_rec(), smt2_convt::flatten_array(), flatten_byte_extract(), flatten_byte_update(), format_rec(), boolbv_widtht::get_entry(), rw_range_sett::get_objects_array(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_rec(), goto_symex_statet::get_original_name(), get_subexpression_at_offset(), interpretert::get_value(), cpp_typecheck_resolvet::guess_template_args(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), havoc_generate_function_bodiest::havoc_expr_rec(), c_typecheck_baset::increment_designator(), c_typecheck_baset::is_complete_type(), boolbvt::is_unbounded_array(), array_string_exprt::length(), array_poolt::make_char_array_for_char_pointer(), c_typecheck_baset::make_designator(), string_abstractiont::make_val_or_dummy_rec(), interpretert::memory_offset_to_byte_offset(), linkingt::needs_renaming_type(), smt2_convt::parse_rec(), pointer_offset_bits(), print_struct_alignment_problems(), goto_symext::process_array_expr(), remove_vector(), rename_symbolt::rename(), goto_symex_statet::rename(), replace_symbolt::replace(), size_of_expr(), static_lifetime_init(), string_of_array(), goto_symext::symex_allocate(), goto_symext::symex_other(), type2name(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_expr_new(), cpp_typecheckt::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_redefinition_non_type(), java_bytecode_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), interpretert::unbounded_size(), unpack_rec(), string_abstractiont::value_assignments(), and cpp_typecheckt::zero_initializer().

◆ to_array_type() [2/2]

array_typet& to_array_type ( typet type)
inline

Cast a generic typet to an array_typet.

This is an unchecked conversion. type must be known to be array_typet.

Parameters
typeSource type
Returns
Object of type array_typet

Definition at line 1054 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_bitvector_type() [1/2]

◆ to_bitvector_type() [2/2]

bitvector_typet& to_bitvector_type ( typet type)
inline

Definition at line 1166 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_bv_type() [1/2]

const bv_typet& to_bv_type ( const typet type)
inline

Cast a generic typet to a bv_typet.

This is an unchecked conversion. type must be known to be bv_typet.

Parameters
typeSource type
Returns
Object of type bv_typet

Definition at line 1203 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by from_integer(), boolbv_widtht::get_entry(), json(), and xml().

◆ to_bv_type() [2/2]

bv_typet& to_bv_type ( typet type)
inline

Cast a generic typet to a bv_typet.

This is an unchecked conversion. type must be known to be bv_typet.

Parameters
typeSource type
Returns
Object of type bv_typet

Definition at line 1212 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_c_bit_field_type() [1/2]

◆ to_c_bit_field_type() [2/2]

c_bit_field_typet& to_c_bit_field_type ( typet type)
inline

Cast a generic typet to a c_bit_field_typet.

This is an unchecked conversion. type must be known to be c_bit_field_typet.

Parameters
typeSource type
Returns
Object of type c_bit_field_typet

Definition at line 1418 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_c_bool_type() [1/2]

const c_bool_typet& to_c_bool_type ( const typet type)
inline

Cast a generic typet to a c_bool_typet.

This is an unchecked conversion. type must be known to be c_bool_typet.

Parameters
typeSource type
Returns
Object of type c_bool_typet

Definition at line 1552 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by from_integer(), boolbv_widtht::get_entry(), and smt2_convt::type2id().

◆ to_c_bool_type() [2/2]

c_bool_typet& to_c_bool_type ( typet type)
inline

Cast a generic typet to a c_bool_typet.

This is an unchecked conversion. type must be known to be c_bool_typet.

Parameters
typeSource type
Returns
Object of type c_bool_typet

Definition at line 1561 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_c_enum_tag_type() [1/2]

◆ to_c_enum_tag_type() [2/2]

c_enum_tag_typet& to_c_enum_tag_type ( typet type)
inline

Definition at line 756 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_c_enum_type() [1/2]

const c_enum_typet& to_c_enum_type ( const typet type)
inline

Cast a generic typet to a c_enum_typet.

This is an unchecked conversion. type must be known to be c_enum_typet.

Parameters
typeSource type
Returns
Object of type c_enum_typet

Definition at line 710 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by dump_ct::convert_compound_enum(), expr2ct::convert_constant(), expr2ct::convert_rec(), linkingt::detailed_conflict_report_rec(), from_integer(), simplify_exprt::simplify_typecast(), to_integer(), type2name(), and cpp_typecheckt::typecheck_enum_body().

◆ to_c_enum_type() [2/2]

c_enum_typet& to_c_enum_type ( typet type)
inline

Cast a generic typet to a c_enum_typet.

This is an unchecked conversion. type must be known to be c_enum_typet.

Parameters
typeSource type
Returns
Object of type c_enum_typet

Definition at line 719 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_class_type() [1/2]

◆ to_class_type() [2/2]

class_typet& to_class_type ( typet type)
inline

Cast a generic typet to a class_typet.

This is an unchecked conversion. type must be known to be class_typet.

Parameters
typeSource type
Returns
Object of type class_typet

Definition at line 444 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_code_type() [1/2]

const code_typet& to_code_type ( const typet type)
inline

Cast a generic typet to a code_typet.

This is an unchecked conversion. type must be known to be code_typet.

Parameters
typeSource type
Returns
Object of type code_typet

Definition at line 987 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by string_abstractiont::abstract_function_call(), actuals_replace_map(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_str_arguments(), cpp_typecheckt::add_this_to_method_type(), c_typecheck_baset::apply_asm_label(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), base_type_eqt::base_type_eq_rec(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), dump_ct::cleanup_type(), java_string_library_preprocesst::code_for_function(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), cpp_declarator_convertert::convert(), java_bytecode_convert_methodt::convert(), expr2ct::convert_code_decl(), expr2javat::convert_code_function_call(), goto_convertt::convert_cpp_delete(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_invoke_dynamic(), expr2ct::convert_rec(), expr2cppt::convert_rec(), expr2javat::convert_rec(), java_bytecode_languaget::convert_single_method(), cpp_typecheckt::cpp_is_pod(), cpp_type2name(), compilet::cprover_macro_arities(), java_simple_method_stubst::create_method_stub(), create_static_function_call(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_cpp_new(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::do_function_call(), value_sett::do_function_call(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), interpretert::execute_function_call(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_symbols(), smt2_convt::find_symbols_rec(), remove_function_pointerst::fix_argument_types(), remove_function_pointerst::fix_return_type(), cpp_typecheckt::function_identifier(), function_to_call(), c_typecheck_baset::gcc_types_compatible_p(), java_object_factoryt::gen_nondet_struct_init(), generate_ansi_c_start_function(), generate_java_start_function(), languaget::generate_opaque_parameter_symbols(), java_bytecode_parsert::get_class_refs_rec(), get_dependencies_from_generic_parameters_rec(), get_destructor(), get_isr(), remove_returnst::get_or_create_return_value_symbol(), get_symbols_rec(), goto_checkt::goto_check(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), ci_lazy_methodst::initialize_instantiated_classes(), escape_analysist::insert_cleanup(), taint_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), is_java_main(), java_build_arguments(), java_bytecode_initialize_parameter_names(), java_record_outputs(), cpp_declarator_convertert::main_function_rules(), member_type_lazy(), mm_io(), model_argc_argv(), mutex_init_instrumentation(), dump_ct::operator()(), original_return_type(), read_bin_goto_object_v3(), record_function_outputs(), cpp_typecheckt::reference_binding(), remove_function_pointerst::remove_function_pointer(), remove_internal_symbols(), rename_symbolt::rename(), replace_symbolt::replace(), require_type::require_code(), ci_lazy_methodst::resolve_method_names(), goto_program2codet::scan_for_varargs(), cpp_typecheck_resolvet::show_identifiers(), cpp_typecheckt::standard_conversion_pointer_to_member(), static_lifetime_init(), jsil_declarationt::to_symbol(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), type2name(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_trinary(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_new_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), java_bytecode_typecheckt::typecheck_type(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), remove_returnst::undo_function_calls(), and ansi_c_convert_typet::write().

◆ to_code_type() [2/2]

code_typet& to_code_type ( typet type)
inline

Cast a generic typet to a code_typet.

This is an unchecked conversion. type must be known to be code_typet.

Parameters
typeSource type
Returns
Object of type code_typet

Definition at line 996 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_complex_type() [1/2]

const complex_typet& to_complex_type ( const typet type)
inline

Cast a generic typet to a complex_typet.

This is an unchecked conversion. type must be known to be complex_typet.

Parameters
typeSource type
Returns
Object of type complex_typet

Definition at line 1700 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by boolbvt::bv_get_rec(), expr_initializert< nondet >::expr_initializer_rec(), and goto_convertt::remove_post().

◆ to_complex_type() [2/2]

complex_typet& to_complex_type ( typet type)
inline

Cast a generic typet to a complex_typet.

This is an unchecked conversion. type must be known to be complex_typet.

Parameters
typeSource type
Returns
Object of type complex_typet

Definition at line 1709 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_enumeration_type() [1/2]

const enumeration_typet& to_enumeration_type ( const typet type)
inline

Cast a generic typet to a enumeration_typet.

This is an unchecked conversion. type must be known to be enumeration_typet.

Parameters
typeSource type
Returns
Object of type enumeration_typet

Definition at line 649 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by boolbvt::convert_constant(), and boolbv_widtht::get_entry().

◆ to_enumeration_type() [2/2]

enumeration_typet& to_enumeration_type ( typet type)
inline

Cast a generic typet to a enumeration_typet.

This is an unchecked conversion. type must be known to be enumeration_typet.

Parameters
typeSource type
Returns
Object of type enumeration_typet

Definition at line 658 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_fixedbv_type()

◆ to_floatbv_type()

const floatbv_typet& to_floatbv_type ( const typet type)
inline

Cast a generic typet to a floatbv_typet.

This is an unchecked conversion. type must be known to be floatbv_typet.

Parameters
typeSource type
Returns
Object of type floatbv_typet

Definition at line 1373 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by string_constraint_generatort::add_axioms_for_string_of_float(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), goto_checkt::conversion_check(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), boolbvt::convert_bitvector(), boolbvt::convert_bv_rel(), smt2_convt::convert_constant(), convert_float_literal(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), boolbvt::convert_ieee_float_rel(), expr2ct::convert_rec(), boolbvt::convert_rest(), smt2_convt::convert_type(), smt2_convt::convert_typecast(), boolbvt::convert_unary_minus(), c_typecheck_baset::do_special_functions(), interpretert::evaluate(), ieee_floatt::from_expr(), from_integer(), boolbv_widtht::get_entry(), float_bvt::get_spec(), interpretert::get_value(), float_bvt::is_zero(), java_char_from_type(), json(), java_string_library_preprocesst::make_float_to_string_code(), goto_checkt::nan_check(), smt2_convt::parse_literal(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_typecast(), cpp_typecheckt::standard_conversion_floating_point_promotion(), smt2_convt::type2id(), boolbvt::type_conversion(), and xml().

◆ to_incomplete_array_type() [1/2]

const incomplete_array_typet& to_incomplete_array_type ( const typet type)
inline

Cast a generic typet to an incomplete_array_typet.

This is an unchecked conversion. type must be known to be incomplete_array_typet.

Parameters
typeSource type
Returns
Object of type incomplete_array_typet

Definition at line 1085 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by base_type_eqt::base_type_eq_rec().

◆ to_incomplete_array_type() [2/2]

incomplete_array_typet& to_incomplete_array_type ( typet type)
inline

Cast a generic typet to an incomplete_array_typet.

This is an unchecked conversion. type must be known to be incomplete_array_typet.

Parameters
typeSource type
Returns
Object of type incomplete_array_typet

Definition at line 1094 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_mathematical_function_type() [1/2]

const mathematical_function_typet& to_mathematical_function_type ( const typet type)
inline

Cast a generic typet to a mathematical_function_typet.

This is an unchecked conversion. type must be known to be mathematical_function_typet.

Parameters
typeSource type
Returns
Object of type mathematical_function_typet

Definition at line 1799 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by smt2_solvert::expand_function_applications(), and smt2_parsert::function_application().

◆ to_mathematical_function_type() [2/2]

mathematical_function_typet& to_mathematical_function_type ( typet type)
inline

Cast a generic typet to a mathematical_function_typet.

This is an unchecked conversion. type must be known to be mathematical_function_typet.

Parameters
typeSource type
Returns
Object of type mathematical_function_typet

Definition at line 1809 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_pointer_type() [1/2]

const pointer_typet& to_pointer_type ( const typet type)
inline

Cast a generic typet to a pointer_typet.

This is an unchecked conversion. type must be known to be pointer_typet.

Parameters
typeSource type
Returns
Object of type pointer_typet

Definition at line 1450 of file std_types.h.

References irept::id(), PRECONDITION, and validate_type().

Referenced by allocate_dynamic_object(), value_sett::apply_code_rec(), base_type_eqt::base_type_eq_rec(), base_type_rec(), bv_pointerst::bv_get_rec(), java_bytecode_instrumentt::check_null_dereference(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), cpp_typecheckt::const_typecast(), smt2_convt::convert_expr(), java_bytecode_convert_methodt::convert_getstatic(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), java_simple_method_stubst::create_method_stub_at(), create_stub_global_symbol(), cpp_typecheckt::do_virtual_table(), require_goto_statements::find_pointer_assignments(), require_goto_statements::find_struct_component_assignments(), require_goto_statements::find_this_component_assignment(), from_integer(), ci_lazy_methods_neededt::gather_field_types(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), generate_ansi_c_start_function(), havoc_generate_function_bodiest::generate_function_body_impl(), generate_java_start_function(), invariant_sett::get_constant(), good_pointer_def(), goto_checkt::goto_check(), goto_symext::initialize_auto_object(), ci_lazy_methodst::initialize_instantiated_classes(), integer_address(), java_string_library_preprocesst::is_java_char_array_pointer_type(), java_string_library_preprocesst::is_java_char_sequence_pointer_type(), java_string_library_preprocesst::is_java_string_buffer_pointer_type(), java_string_library_preprocesst::is_java_string_builder_pointer_type(), java_string_library_preprocesst::is_java_string_pointer_type(), java_bytecode_instrument_uncaught_exceptions(), java_internal_additions(), remove_instanceoft::lower_instanceof(), java_string_library_preprocesst::make_argument_for_format(), null_object(), null_pointer(), smt2_convt::parse_rec(), goto_checkt::pointer_validity_check(), java_string_library_preprocesst::process_equals_function_operands(), require_type::require_pointer(), require_goto_statements::require_struct_array_component_assignment(), require_goto_statements::require_struct_component_assignment(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_typecast(), select_pointer_typet::specialize_generics(), goto_symext::symex_dead(), goto_symext::symex_decl(), and java_bytecode_typecheckt::typecheck_expr().

◆ to_pointer_type() [2/2]

pointer_typet& to_pointer_type ( typet type)
inline

Cast a generic typet to a pointer_typet.

This is an unchecked conversion. type must be known to be pointer_typet.

Parameters
typeSource type
Returns
Object of type pointer_typet

Definition at line 1461 of file std_types.h.

References irept::id(), PRECONDITION, and validate_type().

◆ to_range_type()

const range_typet& to_range_type ( const typet type)
inline

Cast a generic typet to a range_typet.

This is an unchecked conversion. type must be known to be range_typet.

Parameters
typeSource type
Returns
Object of type range_typet

Definition at line 1621 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by boolbvt::convert_constant(), and boolbvt::type_conversion().

◆ to_reference_type() [1/2]

const reference_typet& to_reference_type ( const typet type)
inline

Cast a generic typet to a reference_typet.

This is an unchecked conversion. type must be known to be reference_typet.

Parameters
typeSource type
Returns
Object of type reference_typet

Definition at line 1503 of file std_types.h.

References dstringt::empty(), irept::get(), irept::get_bool(), irept::id(), and PRECONDITION.

Referenced by add_generic_type_information().

◆ to_reference_type() [2/2]

reference_typet& to_reference_type ( typet type)
inline

Cast a generic typet to a reference_typet.

This is an unchecked conversion. type must be known to be reference_typet.

Parameters
typeSource type
Returns
Object of type reference_typet

Definition at line 1513 of file std_types.h.

References dstringt::empty(), irept::get(), irept::get_bool(), irept::id(), and PRECONDITION.

◆ to_signedbv_type() [1/2]

◆ to_signedbv_type() [2/2]

signedbv_typet& to_signedbv_type ( typet type)
inline

Cast a generic typet to a signedbv_typet.

This is an unchecked conversion. type must be known to be signedbv_typet.

Parameters
typeSource type
Returns
Object of type signedbv_typet

Definition at line 1296 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_string_type()

const string_typet& to_string_type ( const typet type)
inline

Cast a generic typet to a string_typet.

This is an unchecked conversion. type must be known to be string_typet.

Parameters
typeSource type
Returns
Object of type string_typet

Definition at line 1587 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_struct_tag_type() [1/2]

const struct_tag_typet& to_struct_tag_type ( const typet type)
inline

Cast a generic typet to a union_tag_typet.

This is an unchecked conversion. type must be known to be union_tag_typet.

Parameters
typeSource type
Returns
Object of type union_tag_typet

Definition at line 566 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by boolbvt::bv_get_rec(), expr2ct::convert_rec(), expr_initializert< nondet >::expr_initializer_rec(), find_symbols(), follow_tags_symbols(), and boolbv_widtht::get_entry().

◆ to_struct_tag_type() [2/2]

struct_tag_typet& to_struct_tag_type ( typet type)
inline

Cast a generic typet to a union_tag_typet.

This is an unchecked conversion. type must be known to be union_tag_typet.

Parameters
typeSource type
Returns
Object of type union_tag_typet

Definition at line 575 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_struct_type() [1/2]

const struct_typet& to_struct_type ( const typet type)
inline

Cast a generic typet to a struct_typet.

This is an unchecked conversion. type must be known to be struct_typet.

Parameters
typeSource type
Returns
Object of type struct_typet

Definition at line 318 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by cpp_typecheckt::add_base_components(), add_nondet_string_pointer_initialization(), add_string_equation_to_symbol_resolution(), cpp_typecheck_resolvet::apply_template_args(), value_set_fivrnst::assign(), value_set_fivrt::assign(), custom_bitvector_domaint::assign_struct_rec(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), build_class_identifier(), boolbvt::bv_get_rec(), interpretert::byte_offset_to_memory_offset(), cpp_typecheckt::check_component_access(), value_set_analysis_fivrt::check_type(), value_set_analysis_fivrnst::check_type(), dump_ct::cleanup_expr(), java_string_library_preprocesst::code_assign_components_to_java_string(), complex_member(), compute_pointer_offset(), cpp_declarator_convertert::convert(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), boolbvt::convert_member(), smt2_convt::convert_member(), cpp_typecheckt::convert_pmop(), expr2ct::convert_rec(), expr2javat::convert_struct(), expr2cppt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), expr2ct::convert_struct_type(), boolbvt::convert_update_rec(), smt2_convt::convert_with(), boolbvt::convert_with(), interpretert::count_type_leaves(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_typecheckt::cpp_is_pod(), cpp_typecheckt::default_cpctor(), value_set_dereferencet::dereference_type_compare(), c_typecheck_baset::designator_enter(), cpp_typecheck_resolvet::disambiguate_functions(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer_list(), cpp_typecheckt::do_virtual_table(), interpretert::evaluate_address(), expr_initializert< nondet >::expr_initializer_rec(), extract_strings_from_lhs(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_superclass_with_type(), smt2_convt::find_symbols_rec(), smt2_convt::flatten2bv(), flatten_byte_extract(), format_rec(), cpp_typecheckt::full_member_initialization(), ci_lazy_methods_neededt::gather_field_types(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_pointer_target_init(), generate_symbol_resolution_from_equations(), cpp_typecheckt::get_bases(), java_bytecode_parsert::get_class_refs_rec(), interpretert::get_component(), get_component_in_struct(), remove_const_function_pointerst::get_component_value(), get_data_type(), value_set_analysis_fivrt::get_entries_rec(), value_set_analysis_fivrnst::get_entries_rec(), boolbv_widtht::get_entry(), get_length_type(), rw_range_sett::get_objects_member(), invariant_propagationt::get_objects_rec(), rw_range_sett::get_objects_struct(), get_or_create_string_literal_symbol(), java_string_library_preprocesst::get_primitive_value_of_object(), interpretert::get_size(), get_subexpression_at_offset(), get_tag(), interpretert::get_value(), value_sett::get_value_set_rec(), cpp_typecheckt::get_virtual_bases(), c_typecheck_baset::increment_designator(), infer_opaque_type_fields(), goto_symext::initialize_auto_object(), initialize_nondet_string_struct(), cpp_typecheckt::instantiate_template(), is_refined_string_type(), java_add_components_to_class(), java_is_array_type(), java_root_class(), json(), boolbvt::literal(), remove_java_newt::lower_java_new_array(), cpp_typecheck_resolvet::make_constructors(), cpp_typecheckt::make_ptr_typecast(), member_offset_expr(), interpretert::memory_offset_to_byte_offset(), pointer_logict::object_rec(), class_hierarchyt::operator()(), cpp_typecheckt::operator_is_overloaded(), smt2_convt::parse_rec(), pointer_offset_bits(), print_struct_alignment_problems(), dereferencet::read_object(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_related(), require_goto_statements::require_struct_component_assignment(), set_class_identifier(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_member(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), size_of_expr(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::static_typecast(), invariant_sett::strengthen_rec(), string_data_type(), cpp_typecheckt::this_struct_type(), dereferencet::type_compatible(), boolbvt::type_conversion(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), java_bytecode_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_side_effect_function_call(), interpretert::unbounded_size(), smt2_convt::unflatten(), unpack_rec(), cpp_typecheckt::user_defined_conversion_sequence(), and xml().

◆ to_struct_type() [2/2]

struct_typet& to_struct_type ( typet type)
inline

Cast a generic typet to a struct_typet.

This is an unchecked conversion. type must be known to be struct_typet.

Parameters
typeSource type
Returns
Object of type struct_typet

Definition at line 327 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_struct_union_type() [1/2]

const struct_union_typet& to_struct_union_type ( const typet type)
inline

Cast a generic typet to a struct_union_typet.

This is an unchecked conversion. type must be known to be struct_union_typet.

Parameters
typeSource type
Returns
Object of type struct_union_typet

Definition at line 280 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by cpp_typecheckt::add_anonymous_members_to_scope(), goto_program2codet::add_local_types(), linkingt::adjust_object_type_rec(), alignment(), value_set_fit::assign(), value_sett::assign(), base_type_eqt::base_type_eq_rec(), base_type_rec(), string_abstractiont::build_abstraction_type_rec(), check_renaming(), value_set_analysis_fit::check_type(), cpp_typecheckt::clean_up(), compute_pointer_offset(), graphml_witnesst::convert_assign_rec(), dump_ct::convert_compound(), cpp_typecheck_resolvet::convert_identifier(), expr2ct::convert_member(), expr2ct::convert_with(), linkingt::detailed_conflict_report_rec(), cpp_typecheckt::dtor(), find_symbols(), cpp_typecheckt::get_component(), get_component_rec(), value_set_analysis_fit::get_entries_rec(), goto_symex_statet::get_original_name(), value_sett::get_value_set_rec(), has_component_rec(), has_subtype(), have_to_remove_complex(), have_to_remove_vector(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), havoc_generate_function_bodiest::havoc_expr_rec(), c_typecheck_baset::is_complete_type(), is_constant_or_has_constant_components(), c_typecheck_baset::make_designator(), value_sett::make_member(), string_abstractiont::make_val_or_dummy_rec(), remove_complex(), goto_program2codet::remove_const(), remove_vector(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), replace_symbolt::replace(), type2name(), linkingt::type_to_string_verbose(), cpp_typecheckt::typecheck_compound_body(), c_typecheck_baset::typecheck_compound_type(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), and string_abstractiont::value_assignments().

◆ to_struct_union_type() [2/2]

struct_union_typet& to_struct_union_type ( typet type)
inline

Cast a generic typet to a struct_union_typet.

This is an unchecked conversion. type must be known to be struct_union_typet.

Parameters
typeSource type
Returns
Object of type struct_union_typet

Definition at line 289 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_symbol_type() [1/2]

const symbol_typet& to_symbol_type ( const typet type)
inline

Cast a generic typet to a symbol_typet.

This is an unchecked conversion. type must be known to be symbol_typet.

Parameters
typeSource type
Returns
Object of type symbol_typet

Definition at line 139 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by goto_program2codet::add_local_types(), add_nondet_string_pointer_initialization(), template_mapt::apply(), base_type_rec(), clinit_wrapper_do_recursive_calls(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), dump_ct::collect_typedefs_rec(), dump_ct::convert_compound(), java_bytecode_convert_methodt::convert_getstatic(), cpp_typecheck_resolvet::convert_identifier(), java_bytecode_convert_methodt::convert_new(), java_bytecode_convert_methodt::convert_putstatic(), expr2ct::convert_rec(), expr2cppt::convert_rec(), cpp_typecheckt::cpp_is_pod(), cpp_typecheckt::elaborate_class_template(), equal_java_types(), cpp_typecheck_resolvet::filter_for_named_scopes(), java_bytecode_parse_treet::find_annotation(), find_symbols(), smt2_convt::find_symbols_rec(), namespace_baset::follow(), c_typecastt::follow_with_qualifiers(), format_rec(), ci_lazy_methods_neededt::gather_field_types(), java_object_factoryt::gen_nondet_init(), class_typet::get_base(), get_data_type(), get_dependencies_from_generic_parameters_rec(), uncaught_exceptions_domaint::get_exception_type(), get_length_type(), get_tag(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), infer_opaque_type_fields(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), is_volatile(), java_classname(), java_generic_symbol_typet::java_generic_symbol_typet(), java_generic_type_from_string(), java_static_lifetime_init(), java_type_from_string(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), needs_clinit_wrapper(), dump_ct::operator()(), class_hierarchy_grapht::populate(), pretty_java_type(), goto_program2codet::remove_const(), cpp_typecheck_resolvet::remove_duplicates(), rename_symbolt::rename(), goto_symex_statet::rename(), replace_symbolt::replace(), require_goto_statements::require_struct_array_component_assignment(), require_goto_statements::require_struct_component_assignment(), require_type::require_symbol(), java_bytecode_parsert::rmethod_attribute(), select_pointer_typet::specialize_generics(), type_eq(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_symbol_type(), and java_bytecode_typecheckt::typecheck_type().

◆ to_symbol_type() [2/2]

symbol_typet& to_symbol_type ( typet type)
inline

Cast a generic typet to a symbol_typet.

This is an unchecked conversion. type must be known to be symbol_typet.

Parameters
typeSource type
Returns
Object of type symbol_typet

Definition at line 148 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_tag_type() [1/2]

const tag_typet& to_tag_type ( const typet type)
inline

Cast a generic typet to a tag_typet.

This is an unchecked conversion. type must be known to be tag_typet.

Parameters
typeSource type
Returns
Object of type tag_typet

Definition at line 525 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by base_type_rec(), rename_symbolt::have_to_rename(), and rename_symbolt::rename().

◆ to_tag_type() [2/2]

tag_typet& to_tag_type ( typet type)
inline

Cast a generic typet to a tag_typet.

This is an unchecked conversion. type must be known to be tag_typet.

Parameters
typeSource type
Returns
Object of type tag_typet

Definition at line 536 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_union_tag_type() [1/2]

const union_tag_typet& to_union_tag_type ( const typet type)
inline

Cast a generic typet to a union_tag_typet.

This is an unchecked conversion. type must be known to be union_tag_typet.

Parameters
typeSource type
Returns
Object of type union_tag_typet

Definition at line 603 of file std_types.h.

References irept::id(), and PRECONDITION.

Referenced by boolbvt::bv_get_rec(), expr2ct::convert_rec(), expr_initializert< nondet >::expr_initializer_rec(), find_symbols(), follow_tags_symbols(), and boolbv_widtht::get_entry().

◆ to_union_tag_type() [2/2]

union_tag_typet& to_union_tag_type ( typet type)
inline

Cast a generic typet to a union_tag_typet.

This is an unchecked conversion. type must be known to be union_tag_typet.

Parameters
typeSource type
Returns
Object of type union_tag_typet

Definition at line 612 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_union_type() [1/2]

◆ to_union_type() [2/2]

union_typet& to_union_type ( typet type)
inline

Cast a generic typet to a union_typet.

This is an unchecked conversion. type must be known to be union_typet.

Parameters
typeSource type
Returns
Object of type union_typet

Definition at line 485 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_unsignedbv_type() [1/2]

◆ to_unsignedbv_type() [2/2]

unsignedbv_typet& to_unsignedbv_type ( typet type)
inline

Cast a generic typet to an unsignedbv_typet.

This is an unchecked conversion. type must be known to be unsignedbv_typet.

Parameters
typeSource type
Returns
Object of type unsignedbv_typet

Definition at line 1254 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ to_vector_type() [1/2]

◆ to_vector_type() [2/2]

vector_typet& to_vector_type ( typet type)
inline

Cast a generic typet to a vector_typet.

This is an unchecked conversion. type must be known to be vector_typet.

Parameters
typeSource type
Returns
Object of type vector_typet

Definition at line 1669 of file std_types.h.

References irept::id(), and PRECONDITION.

◆ validate_type()

void validate_type ( const pointer_typet type)
inline

Definition at line 1475 of file std_types.h.

References DATA_INVARIANT, dstringt::empty(), irept::get(), and bitvector_typet::get_width().

Referenced by to_pointer_type().