cprover
Conversion to specific types

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

Conversion to subclasses of typet

Function Documentation

§ 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 946 of file std_types.h.

References irept::id().

Referenced by string_constraint_generatort::add_axioms_from_char_array(), string_abstractiont::add_dummy_symbol_and_value(), linkingt::adjust_object_type_rec(), path_symex_statet::array_theory(), path_symext::assign_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(), smt1_convt::ce_value(), 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(), dplib_convt::convert_dplib_type(), smt1_convt::convert_index(), boolbvt::convert_index(), smt2_convt::convert_index(), boolbvt::convert_lambda(), cvc_convt::convert_type(), smt1_convt::convert_type(), smt2_convt::convert_type(), boolbvt::convert_update_rec(), smt1_convt::convert_with(), smt2_convt::convert_with(), boolbvt::convert_with(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), 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(), path_symex_statet::expand_structs_and_arrays(), character_refine_preprocesst::expr_of_to_chars(), dplib_convt::find_symbols(), cvc_convt::find_symbols(), find_symbols(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), smt1_convt::find_symbols_rec(), smt2_convt::find_symbols_rec(), smt1_convt::flatten_array(), smt2_convt::flatten_array(), flatten_byte_extract(), flatten_byte_update(), refined_string_typet::get_content_type(), 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(), cpp_typecheck_resolvet::guess_template_args(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), c_typecheck_baset::increment_designator(), c_typecheck_baset::is_complete_type(), boolbvt::is_unbounded_array(), c_typecheck_baset::make_designator(), string_abstractiont::make_val_or_dummy_rec(), linkingt::needs_renaming_type(), smt2_convt::parse_rec(), pointer_offset_bits(), print_struct_alignment_problems(), remove_vector(), rename_symbolt::rename(), goto_symex_statet::rename(), replace_symbolt::replace(), size_of_expr(), c_sizeoft::sizeof_rec(), static_lifetime_init(), path_symext::symex_malloc(), goto_symext::symex_malloc(), 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_redefinition_non_type(), java_bytecode_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), unpack_rec(), string_abstractiont::value_assignments(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

§ 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 955 of file std_types.h.

References irept::id().

§ to_bitvector_type()

§ 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 1108 of file std_types.h.

References irept::id().

Referenced by dplib_convt::convert_dplib_type(), 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 1117 of file std_types.h.

References irept::id().

§ 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 1335 of file std_types.h.

References irept::id().

§ 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 1473 of file std_types.h.

References irept::id().

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 1482 of file std_types.h.

References irept::id().

§ 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 726 of file std_types.h.

References irept::id().

§ 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 680 of file std_types.h.

References irept::id().

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 689 of file std_types.h.

References irept::id().

§ 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 416 of file std_types.h.

References irept::id().

§ 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 884 of file std_types.h.

References irept::id().

Referenced by string_abstractiont::abstract_function_call(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_str_arguments(), cpp_typecheckt::add_this_to_method_type(), ansi_c_entry_point(), 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(), 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(), expr2ct::convert_rec(), expr2javat::convert_rec(), expr2cppt::convert_rec(), cpp_typecheckt::cpp_is_pod(), cpp_type2name(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_cpp_new(), value_sett::do_function_call(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::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(), smt1_convt::find_symbols_rec(), 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_bytecode_parsert::get_class_refs_rec(), get_destructor(), get_isr(), get_symbols_rec(), goto_checkt::goto_check(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), initialize_needed_classes(), escape_analysist::insert_cleanup(), taint_analysist::instrument(), is_empty(), java_build_arguments(), java_bytecode_convert_method_lazy(), java_entry_point(), java_record_outputs(), cpp_declarator_convertert::main_function_rules(), mm_io(), model_argc_argv(), mutex_init_instrumentation(), dump_ct::operator()(), original_return_type(), read_bin_goto_object_v3(), read_goto_object(), record_function_outputs(), cpp_typecheckt::reference_binding(), remove_function_pointerst::remove_function_pointer(), remove_internal_symbols(), rename_symbolt::rename(), replace_symbolt::replace(), goto_program2codet::scan_for_varargs(), cpp_typecheck_resolvet::show_identifiers(), cpp_typecheckt::standard_conversion_pointer_to_member(), static_lifetime_init(), jsil_declarationt::to_symbol(), 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 893 of file std_types.h.

References irept::id().

§ 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 1629 of file std_types.h.

References irept::id().

Referenced by goto_convertt::remove_post(), and zero_initializert::zero_initializer_rec().

§ 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 1638 of file std_types.h.

References irept::id().

§ 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 619 of file std_types.h.

References irept::id().

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 628 of file std_types.h.

References irept::id().

§ to_fixedbv_type()

§ to_floatbv_type()

§ 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 986 of file std_types.h.

References irept::id().

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 995 of file std_types.h.

References irept::id().

§ to_pointer_type() [1/2]

§ 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 1386 of file std_types.h.

References irept::id().

§ 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 1546 of file std_types.h.

References irept::id().

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 1426 of file std_types.h.

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

Referenced by java_reference_type().

§ 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 1435 of file std_types.h.

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

§ 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 1209 of file std_types.h.

References irept::id().

§ 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 1508 of file std_types.h.

References irept::id().

§ 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 536 of file std_types.h.

References irept::id().

Referenced by boolbvt::bv_get_rec(), expr2ct::convert_rec(), find_symbols(), follow_tags_symbols(), boolbv_widtht::get_entry(), and zero_initializert::zero_initializer_rec().

§ 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 545 of file std_types.h.

References irept::id().

§ 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 317 of file std_types.h.

References irept::id().

Referenced by cpp_typecheckt::add_base_components(), add_vtable_pointer_member(), cpp_typecheck_resolvet::apply_template_args(), value_set_fivrnst::assign(), value_set_fivrt::assign(), path_symext::assign_rec(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), build_class_identifier(), boolbvt::bv_get_rec(), smt1_convt::ce_value(), cpp_typecheckt::check_component_access(), value_set_analysis_fivrt::check_type(), value_set_analysis_fivrnst::check_type(), dump_ct::cleanup_expr(), complex_member(), compute_pointer_offset(), cpp_declarator_convertert::convert(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), dplib_convt::convert_dplib_expr(), dplib_convt::convert_dplib_type(), smt1_convt::convert_member(), boolbvt::convert_member(), smt2_convt::convert_member(), cpp_typecheckt::convert_pmop(), expr2ct::convert_rec(), expr2javat::convert_struct(), expr2cppt::convert_struct(), smt1_convt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), cvc_convt::convert_struct_expr(), expr2ct::convert_struct_type(), cvc_convt::convert_type(), boolbvt::convert_update_rec(), smt1_convt::convert_with(), smt2_convt::convert_with(), boolbvt::convert_with(), 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(), goto_convertt::do_java_new_array(), cpp_typecheckt::do_virtual_table(), interpretert::evaluate_address(), path_symex_statet::expand_structs_and_arrays(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_superclass_with_type(), smt2_convt::find_symbols_rec(), smt2_convt::flatten2bv(), flatten_byte_extract(), cpp_typecheckt::full_member_initialization(), 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(), cpp_typecheckt::get_bases(), java_bytecode_parsert::get_class_refs_rec(), remove_const_function_pointerst::get_component_value(), value_set_analysis_fivrt::get_entries_rec(), value_set_analysis_fivrnst::get_entries_rec(), boolbv_widtht::get_entry(), rw_range_sett::get_objects_member(), invariant_propagationt::get_objects_rec(), rw_range_sett::get_objects_struct(), interpretert::get_size(), get_subexpression_at_offset(), value_sett::get_value_set_rec(), cpp_typecheckt::get_virtual_bases(), c_typecheck_baset::increment_designator(), goto_symext::initialize_auto_object(), cpp_typecheckt::instantiate_template(), refined_string_typet::is_c_string_type(), refined_string_typet::is_java_char_sequence_type(), refined_string_typet::is_java_string_builder_type(), refined_string_typet::is_java_string_type(), java_is_array_type(), java_root_class(), json(), boolbvt::literal(), cpp_typecheck_resolvet::make_constructors(), cpp_typecheckt::make_ptr_typecast(), member_offset_expr(), 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(), 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(), c_sizeoft::sizeof_rec(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::static_typecast(), invariant_sett::strengthen_rec(), smt1_dect::string_to_expr_z3(), 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_java_string_literal(), java_bytecode_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_side_effect_function_call(), smt2_convt::unflatten(), unpack_rec(), cpp_typecheckt::user_defined_conversion_sequence(), xml(), and zero_initializert::zero_initializer_rec().

§ 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 326 of file std_types.h.

References irept::id().

§ 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 277 of file std_types.h.

References irept::id().

Referenced by cpp_typecheckt::add_anonymous_members_to_scope(), goto_program2codet::add_local_types(), linkingt::adjust_object_type_rec(), alignment(), value_sett::assign(), value_set_fit::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(), 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(), smt1_convt::find_symbols_rec(), 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_vtable_info(), have_to_remove_complex(), have_to_remove_vector(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), c_typecheck_baset::is_complete_type(), 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(), fence_insertert::type_component(), 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 287 of file std_types.h.

References irept::id().

§ to_symbol_type() [1/2]

§ 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 151 of file std_types.h.

References irept::id().

§ 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 495 of file std_types.h.

References irept::id().

Referenced by 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 506 of file std_types.h.

References irept::id().

§ 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 573 of file std_types.h.

References irept::id().

Referenced by boolbvt::bv_get_rec(), expr2ct::convert_rec(), find_symbols(), follow_tags_symbols(), boolbv_widtht::get_entry(), and zero_initializert::zero_initializer_rec().

§ 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 582 of file std_types.h.

References irept::id().

§ 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 451 of file std_types.h.

References irept::id().

§ 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 1163 of file std_types.h.

References irept::id().

§ 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 1598 of file std_types.h.

References irept::id().