cprover
|
Conversion to subclasses of typet
|
inline |
Cast a generic typet to an array_typet.
This is an unchecked conversion. type must be known to be array_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to an array_typet.
This is an unchecked conversion. type must be known to be array_typet.
type | Source type |
Definition at line 955 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a bitvector_typet.
This is an unchecked conversion. type must be known to be bitvector_typet.
type | Source type |
Definition at line 1051 of file std_types.h.
References irept::id().
Referenced by string_constraint_generatort::add_axioms_from_float(), float_bvt::add_sub(), alignment(), polynomial_acceleratort::assert_for_values(), inv_object_storet::build_string(), c_bit_field_replacement_type(), smt2_convt::convert_rounding_mode_FPA(), smt2_convt::convert_type(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), value_set_dereferencet::dereference_type_compare(), polynomial_acceleratort::fit_polynomial_sliced(), c_typecheck_baset::gcc_vector_types_compatible(), string_abstractiont::is_char_type(), string_instrumentationt::is_string_type(), join_types(), json(), pointer_offset_bits(), float_bvt::sign_bit(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_typecast(), size_of_expr(), c_sizeoft::sizeof_rec(), float_bvt::sticky_right_shift(), c_typecheck_baset::typecheck_c_bit_field_type(), goto_checkt::undefined_shift_check(), xml(), and zero_initializert::zero_initializer_rec().
Cast a generic typet to a bv_typet.
This is an unchecked conversion. type must be known to be bv_typet.
type | Source type |
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().
Cast a generic typet to a bv_typet.
This is an unchecked conversion. type must be known to be bv_typet.
type | Source type |
Definition at line 1117 of file std_types.h.
References irept::id().
|
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.
type | Source type |
Definition at line 1319 of file std_types.h.
References irept::id().
Referenced by add_padding(), c_sizeoft::c_offsetof(), dump_ct::cleanup_expr(), boolbvt::convert_byte_extract(), dump_ct::convert_compound(), expr2ct::convert_rec(), smt2_convt::convert_type(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), from_integer(), c_typecastt::get_c_type(), boolbv_widtht::get_entry(), json(), member_offset_expr(), c_typecastt::minimum_promotion(), member_offset_iterator::operator++(), pointer_offset_bits(), size_of_expr(), c_sizeoft::sizeof_rec(), boolbvt::type_conversion(), c_typecheck_baset::typecheck_compound_body(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), and xml().
|
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.
type | Source type |
Definition at line 1335 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a c_bool_typet.
This is an unchecked conversion. type must be known to be c_bool_typet.
type | Source type |
Definition at line 1473 of file std_types.h.
References irept::id().
Referenced by from_integer(), boolbv_widtht::get_entry(), and smt2_convt::type2id().
|
inline |
Cast a generic typet to a c_bool_typet.
This is an unchecked conversion. type must be known to be c_bool_typet.
type | Source type |
Definition at line 1482 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a c_enum_tag_typet.
This is an unchecked conversion. type must be known to be c_enum_tag_typet.
type | Source type |
Definition at line 717 of file std_types.h.
References irept::id().
Referenced by goto_program2codet::add_local_types(), alignment(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), bv_width(), c_bit_field_replacement_type(), dump_ct::convert_compound(), expr2ct::convert_constant(), smt2_convt::convert_floatbv_typecast(), expr2ct::convert_rec(), smt1_convt::convert_type(), smt2_convt::convert_type(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), find_symbols(), follow_tags_symbols(), c_typecheck_baset::gcc_types_compatible_p(), boolbv_widtht::get_entry(), is_not_zero(), json(), smt2_convt::parse_literal(), pointer_offset_bits(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_typecast(), size_of_expr(), c_sizeoft::sizeof_rec(), smt2_convt::type2id(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_type(), xml(), and zero_initializert::zero_initializer_rec().
|
inline |
Definition at line 726 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a c_enum_typet.
This is an unchecked conversion. type must be known to be c_enum_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a c_enum_typet.
This is an unchecked conversion. type must be known to be c_enum_typet.
type | Source type |
Definition at line 689 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a class_typet.
This is an unchecked conversion. type must be known to be class_typet.
type | Source type |
Definition at line 407 of file std_types.h.
References irept::id().
Referenced by java_bytecode_vtable_factoryt::add_vtable_entry(), java_bytecode_convert_classt::convert(), java_bytecode_vtable_factoryt::get_class_type(), java_bytecode_vtable_factoryt::has_method(), java_bytecode_vtable_factoryt::is_class_with_vt(), java_bytecode_vtable_factoryt::operator()(), cpp_typecheckt::typecheck_expr_main(), and remove_static_init_loopst::unwind_enum_static().
|
inline |
Cast a generic typet to a class_typet.
This is an unchecked conversion. type must be known to be class_typet.
type | Source type |
Definition at line 416 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a code_typet.
This is an unchecked conversion. type must be known to be code_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a code_typet.
This is an unchecked conversion. type must be known to be code_typet.
type | Source type |
Definition at line 893 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a complex_typet.
This is an unchecked conversion. type must be known to be complex_typet.
type | Source type |
Definition at line 1629 of file std_types.h.
References irept::id().
Referenced by goto_convertt::remove_post(), and zero_initializert::zero_initializer_rec().
|
inline |
Cast a generic typet to a complex_typet.
This is an unchecked conversion. type must be known to be complex_typet.
type | Source type |
Definition at line 1638 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a enumeration_typet.
This is an unchecked conversion. type must be known to be enumeration_typet.
type | Source type |
Definition at line 619 of file std_types.h.
References irept::id().
Referenced by boolbvt::convert_constant(), and boolbv_widtht::get_entry().
|
inline |
Cast a generic typet to a enumeration_typet.
This is an unchecked conversion. type must be known to be enumeration_typet.
type | Source type |
Definition at line 628 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a fixedbv_typet.
This is an unchecked conversion. type must be known to be fixedbv_typet.
type | Source type |
Definition at line 1247 of file std_types.h.
References irept::id().
Referenced by smt1_convt::convert_constant(), smt2_convt::convert_constant(), smt1_convt::convert_div(), boolbvt::convert_div(), smt2_convt::convert_div(), smt2_convt::convert_expr(), smt1_convt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), expr2ct::convert_rec(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), interpretert::evaluate(), fixedbvt::from_expr(), from_integer(), boolbv_widtht::get_entry(), c_typecastt::implicit_typecast_arithmetic(), json(), simplify_exprt::simplify_typecast(), boolbvt::type_conversion(), and xml().
|
inline |
Cast a generic typet to a floatbv_typet.
This is an unchecked conversion. type must be known to be floatbv_typet.
type | Source type |
Definition at line 1286 of file std_types.h.
References irept::id().
Referenced by 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(), smt1_convt::convert_constant(), 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(), java_bytecode_convert_methodt::convert_instructions(), 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(), float_bvt::is_zero(), java_char_from_type(), json(), 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().
|
inline |
Cast a generic typet to an incomplete_array_typet.
This is an unchecked conversion. type must be known to be incomplete_array_typet.
type | Source type |
Definition at line 986 of file std_types.h.
References irept::id().
Referenced by base_type_eqt::base_type_eq_rec().
|
inline |
Cast a generic typet to an incomplete_array_typet.
This is an unchecked conversion. type must be known to be incomplete_array_typet.
type | Source type |
Definition at line 995 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a pointer_typet.
This is an unchecked conversion. type must be known to be pointer_typet.
type | Source type |
Definition at line 1377 of file std_types.h.
References irept::id().
Referenced by java_object_factoryt::allocate_object(), ansi_c_entry_point(), base_type_eqt::base_type_eq_rec(), base_type_rec(), cpp_typecheckt::const_typecast(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), java_bytecode_convert_methodt::convert_instructions(), cpp_typecheckt::do_virtual_table(), from_integer(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), good_pointer_def(), goto_checkt::goto_check(), goto_symext::initialize_auto_object(), integer_address(), refined_string_typet::is_java_char_sequence_type(), refined_string_typet::is_java_string_builder_type(), refined_string_typet::is_java_string_pointer_type(), null_object(), null_pointer(), goto_checkt::pointer_validity_check(), and simplify_exprt::simplify_typecast().
|
inline |
Cast a generic typet to a pointer_typet.
This is an unchecked conversion. type must be known to be pointer_typet.
type | Source type |
Definition at line 1386 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a range_typet.
This is an unchecked conversion. type must be known to be range_typet.
type | Source type |
Definition at line 1546 of file std_types.h.
References irept::id().
Referenced by boolbvt::convert_constant(), and boolbvt::type_conversion().
|
inline |
Cast a generic typet to a reference_typet.
This is an unchecked conversion. type must be known to be reference_typet.
type | Source type |
Definition at line 1426 of file std_types.h.
References irept::get_bool(), and irept::id().
Referenced by java_reference_type().
|
inline |
Cast a generic typet to a reference_typet.
This is an unchecked conversion. type must be known to be reference_typet.
type | Source type |
Definition at line 1435 of file std_types.h.
References irept::get_bool(), irept::id(), is_reference(), and is_rvalue_reference().
|
inline |
Cast a generic typet to a signedbv_typet.
This is an unchecked conversion. type must be known to be signedbv_typet.
type | Source type |
Definition at line 1200 of file std_types.h.
References irept::id().
Referenced by ansi_c_entry_point(), goto_checkt::conversion_check(), float_bvt::convert(), dump_ct::convert_compound(), dplib_convt::convert_dplib_type(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), cvc_convt::convert_type(), float_bvt::denormalization_shift(), interpretert::evaluate(), from_integer(), float_bvt::from_signed_integer(), boolbv_widtht::get_entry(), goto_checkt::integer_overflow_check(), java_char_from_type(), json(), float_bvt::normalization_shift(), overflow_instrumentert::overflow_expr(), float_bvt::round_exponent(), float_bvt::rounder(), cpp_typecheckt::standard_conversion_integral_promotion(), float_bvt::subtract_exponents(), smt2_convt::type2id(), type_max(), and xml().
|
inline |
Cast a generic typet to a signedbv_typet.
This is an unchecked conversion. type must be known to be signedbv_typet.
type | Source type |
Definition at line 1209 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a string_typet.
This is an unchecked conversion. type must be known to be string_typet.
type | Source type |
Definition at line 1508 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a union_tag_typet.
This is an unchecked conversion. type must be known to be union_tag_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a union_tag_typet.
This is an unchecked conversion. type must be known to be union_tag_typet.
type | Source type |
Definition at line 545 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a struct_typet.
This is an unchecked conversion. type must be known to be struct_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a struct_typet.
This is an unchecked conversion. type must be known to be struct_typet.
type | Source type |
Definition at line 326 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a struct_union_typet.
This is an unchecked conversion. type must be known to be struct_union_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a struct_union_typet.
This is an unchecked conversion. type must be known to be struct_union_typet.
type | Source type |
Definition at line 287 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a symbol_typet.
This is an unchecked conversion. type must be known to be symbol_typet.
type | Source type |
Definition at line 142 of file std_types.h.
References irept::id().
Referenced by java_bytecode_convert_classt::add_array_types(), goto_program2codet::add_local_types(), dump_ct::collect_typedefs_rec(), dump_ct::convert_compound(), java_bytecode_convert_methodt::convert_instructions(), expr2cppt::convert_rec(), goto_convertt::do_java_new(), cpp_typecheck_resolvet::filter_for_named_scopes(), smt1_convt::find_symbols_rec(), smt2_convt::find_symbols_rec(), gather_field_types(), java_bytecode_vtable_factoryt::get_class_type(), java_bytecode_vtable_factoryt::has_method(), initialize_needed_classes(), refined_string_typet::is_java_string_type(), is_volatile(), fence_volatilet::is_volatile(), java_classname(), remove_instanceoft::lower_instanceof(), dump_ct::operator()(), goto_program2codet::remove_const(), rename_symbolt::rename(), goto_symex_statet::rename(), java_bytecode_parsert::rmethod_attribute(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_symbol_type(), and java_bytecode_typecheckt::typecheck_type().
|
inline |
Cast a generic typet to a symbol_typet.
This is an unchecked conversion. type must be known to be symbol_typet.
type | Source type |
Definition at line 151 of file std_types.h.
References irept::id().
Cast a generic typet to a tag_typet.
This is an unchecked conversion. type must be known to be tag_typet.
type | Source type |
Definition at line 495 of file std_types.h.
References irept::id().
Referenced by rename_symbolt::have_to_rename(), and rename_symbolt::rename().
Cast a generic typet to a tag_typet.
This is an unchecked conversion. type must be known to be tag_typet.
type | Source type |
Definition at line 506 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a union_tag_typet.
This is an unchecked conversion. type must be known to be union_tag_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a union_tag_typet.
This is an unchecked conversion. type must be known to be union_tag_typet.
type | Source type |
Definition at line 582 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a union_typet.
This is an unchecked conversion. type must be known to be union_typet.
type | Source type |
Definition at line 442 of file std_types.h.
References irept::id().
Referenced by simplify_exprt::bits2expr(), boolbvt::bv_get_rec(), smt1_convt::ce_value(), dump_ct::cleanup_expr(), expr2ct::convert_rec(), smt1_convt::convert_union(), smt2_convt::convert_union(), boolbvt::convert_update_rec(), smt1_convt::convert_with(), smt2_convt::convert_with(), boolbvt::convert_with(), c_typecheck_baset::designator_enter(), c_typecheck_baset::do_designated_initializer(), linkingt::duplicate_code_symbol(), smt2_convt::find_symbols_rec(), boolbv_widtht::get_entry(), interpretert::get_size(), value_sett::get_value_set_rec(), c_typecastt::implicit_typecast_followed(), jsil_union_typet::jsil_union_typet(), json(), smt2_convt::parse_rec(), pointer_offset_bits(), size_of_expr(), c_sizeoft::sizeof_rec(), smt1_dect::string_to_expr_z3(), c_typecheck_baset::typecheck_compound_body(), c_typecheck_baset::typecheck_expr_typecast(), xml(), and zero_initializert::zero_initializer_rec().
|
inline |
Cast a generic typet to a union_typet.
This is an unchecked conversion. type must be known to be union_typet.
type | Source type |
Definition at line 451 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to an unsignedbv_typet.
This is an unchecked conversion. type must be known to be unsignedbv_typet.
type | Source type |
Definition at line 1154 of file std_types.h.
References irept::id().
Referenced by invariant_sett::add_type_bounds(), ansi_c_entry_point(), float_bvt::bias(), goto_checkt::conversion_check(), float_bvt::convert(), dump_ct::convert_compound(), dplib_convt::convert_dplib_type(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), cvc_convt::convert_type(), float_bvt::denormalization_shift(), float_bvt::div(), interpretert::evaluate(), float_bvt::exponent_all_ones(), float_bvt::exponent_all_zeros(), float_bvt::fraction_all_zeros(), float_bvt::fraction_rounding_decision(), from_integer(), float_bvt::from_unsigned_integer(), boolbv_widtht::get_entry(), json(), float_bvt::limit_distance(), float_bvt::normalization_shift(), float_bvt::pack(), float_bvt::round_exponent(), float_bvt::round_fraction(), cpp_typecheckt::standard_conversion_integral_promotion(), float_bvt::sticky_right_shift(), smt2_convt::type2id(), type_max(), and xml().
|
inline |
Cast a generic typet to an unsignedbv_typet.
This is an unchecked conversion. type must be known to be unsignedbv_typet.
type | Source type |
Definition at line 1163 of file std_types.h.
References irept::id().
|
inline |
Cast a generic typet to a vector_typet.
This is an unchecked conversion. type must be known to be vector_typet.
type | Source type |
Definition at line 1589 of file std_types.h.
References irept::id().
Referenced by goto_checkt::bounds_check(), endianness_mapt::build_big_endian(), smt2_convt::convert_expr(), smt2_convt::convert_index(), smt2_convt::convert_minus(), smt2_convt::convert_plus(), expr2ct::convert_rec(), c_typecheck_baset::designator_enter(), path_symex_statet::expand_structs_and_arrays(), smt2_convt::find_symbols_rec(), smt2_convt::flatten2bv(), boolbv_widtht::get_entry(), rw_range_sett::get_objects_index(), json(), pointer_offset_bits(), ansi_c_convert_typet::read_rec(), remove_vector(), size_of_expr(), c_sizeoft::sizeof_rec(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_type(), smt2_convt::unflatten(), xml(), and zero_initializert::zero_initializer_rec().
|
inline |
Cast a generic typet to a vector_typet.
This is an unchecked conversion. type must be known to be vector_typet.
type | Source type |
Definition at line 1598 of file std_types.h.
References irept::id().