cprover
|
API to type classes. More...
#include "expr.h"
#include "mp_arith.h"
#include "invariant.h"
#include "expr_cast.h"
#include <unordered_map>
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 |
|
inline |
Definition at line 451 of file std_types.h.
References can_cast_type< struct_typet >().
Referenced by can_cast_type< java_class_typet >().
|
inline |
Definition at line 1470 of file std_types.h.
|
inline |
Definition at line 334 of file std_types.h.
Referenced by can_cast_type< class_typet >().
|
inline |
Definition at line 155 of file std_types.h.
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().
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().
|
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 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().
|
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 1054 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1150 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by float_bvt::add_sub(), polynomial_acceleratort::assert_for_values(), inv_object_storet::build_string(), c_bit_field_replacement_type(), smt2_convt::convert_expr(), smt2_convt::convert_rounding_mode_FPA(), smt2_convt::convert_type(), smt2_convt::convert_typecast(), value_set_dereferencet::dereference_type_compare(), interpretert::evaluate(), expr_initializert< nondet >::expr_initializer_rec(), 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(), max_printed_string_length(), mul_expr(), pointer_offset_bits(), float_bvt::sign_bit(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_typecast(), size_of_expr(), float_bvt::sticky_right_shift(), sum_expr(), c_typecheck_baset::typecheck_c_bit_field_type(), goto_checkt::undefined_shift_check(), underlying_width(), xml(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 1166 of file std_types.h.
References irept::id(), and PRECONDITION.
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 1203 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by 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 1212 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1402 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by add_padding(), add_padding_gcc(), add_padding_msvc(), dump_ct::cleanup_expr(), boolbvt::convert_byte_extract(), dump_ct::convert_compound(), expr2ct::convert_rec(), smt2_convt::convert_type(), smt2_convt::convert_typecast(), c_typecheck_baset::do_special_functions(), from_integer(), c_typecastt::get_c_type(), boolbv_widtht::get_entry(), json(), member_offset_expr(), c_typecastt::minimum_promotion(), member_offset_iterator::operator++(), size_of_expr(), 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 1418 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1552 of file std_types.h.
References irept::id(), and PRECONDITION.
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 1561 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 747 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by goto_program2codet::add_local_types(), alignment(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), c_bit_field_replacement_type(), dump_ct::convert_compound(), expr2ct::convert_constant(), smt2_convt::convert_floatbv_typecast(), expr2ct::convert_rec(), smt2_convt::convert_type(), smt2_convt::convert_typecast(), expr_initializert< nondet >::expr_initializer_rec(), find_symbols(), follow_tags_symbols(), c_typecheck_baset::gcc_types_compatible_p(), boolbv_widtht::get_entry(), has_subtype(), is_not_zero(), json(), smt2_convt::parse_literal(), pointer_offset_bits(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_typecast(), size_of_expr(), 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(), underlying_width(), and xml().
|
inline |
Definition at line 756 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 719 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 435 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by clinit_wrapper_do_recursive_calls(), infer_opaque_type_fields(), java_static_lifetime_init(), needs_clinit_wrapper(), java_syntactic_difft::operator()(), syntactic_difft::operator()(), class_hierarchy_grapht::populate(), require_type::require_complete_class(), require_type::require_incomplete_class(), require_type::require_java_generic_class(), require_type::require_java_implicitly_generic_class(), require_type::require_java_non_generic_class(), and cpp_typecheckt::typecheck_expr_main().
|
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 444 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 996 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 1709 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 649 of file std_types.h.
References irept::id(), and PRECONDITION.
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 658 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1334 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by smt2_convt::convert_constant(), smt2_convt::convert_div(), boolbvt::convert_div(), smt2_convt::convert_expr(), boolbvt::convert_mult(), smt2_convt::convert_mult(), expr2ct::convert_rec(), 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 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().
|
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 1085 of file std_types.h.
References irept::id(), and PRECONDITION.
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 1094 of file std_types.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic typet to a mathematical_function_typet.
This is an unchecked conversion. type must be known to be mathematical_function_typet.
type | Source type |
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().
|
inline |
Cast a generic typet to a mathematical_function_typet.
This is an unchecked conversion. type must be known to be mathematical_function_typet.
type | Source type |
Definition at line 1809 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 1461 of file std_types.h.
References irept::id(), PRECONDITION, and validate_type().
|
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 1621 of file std_types.h.
References irept::id(), and PRECONDITION.
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 1503 of file std_types.h.
References dstringt::empty(), irept::get(), irept::get_bool(), irept::id(), and PRECONDITION.
Referenced by add_generic_type_information().
|
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 1513 of file std_types.h.
References dstringt::empty(), irept::get(), irept::get_bool(), irept::id(), and PRECONDITION.
|
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 1287 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by smt2_parsert::cast_bv_to_unsigned(), goto_checkt::conversion_check(), float_bvt::convert(), dump_ct::convert_compound(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), float_bvt::denormalization_shift(), interpretert::evaluate(), from_integer(), float_bvt::from_signed_integer(), generate_ansi_c_start_function(), boolbv_widtht::get_entry(), goto_checkt::integer_overflow_check(), java_char_from_type(), json(), length_constraint_for_concat_substr(), max_value(), 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(), 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 1296 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1587 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 575 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 327 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 289 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 148 of file std_types.h.
References irept::id(), and PRECONDITION.
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 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().
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 536 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 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().
|
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 612 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 476 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by simplify_exprt::bits2expr(), boolbvt::bv_get_rec(), dump_ct::cleanup_expr(), expr2ct::convert_rec(), smt2_convt::convert_union(), boolbvt::convert_update_rec(), smt2_convt::convert_with(), boolbvt::convert_with(), c_typecheck_baset::designator_enter(), c_typecheck_baset::do_designated_initializer(), linkingt::duplicate_code_symbol(), expr_initializert< nondet >::expr_initializer_rec(), 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_typecheck_baset::typecheck_compound_body(), c_typecheck_baset::typecheck_expr_typecast(), and xml().
|
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 485 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1245 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by invariant_sett::add_type_bounds(), float_bvt::bias(), smt2_parsert::cast_bv_to_signed(), goto_checkt::conversion_check(), float_bvt::convert(), dump_ct::convert_compound(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), 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(), smt2_parsert::function_application(), generate_ansi_c_start_function(), boolbv_widtht::get_entry(), get_significand(), is_char_type(), json(), float_bvt::limit_distance(), max_value(), 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(), 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 1254 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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 1660 of file std_types.h.
References irept::id(), and PRECONDITION.
Referenced by goto_checkt::bounds_check(), endianness_mapt::build_big_endian(), boolbvt::bv_get_rec(), smt2_convt::convert_expr(), smt2_convt::convert_index(), smt2_convt::convert_minus(), smt2_convt::convert_plus(), expr2ct::convert_rec(), c_typecheck_baset::designator_enter(), expr_initializert< nondet >::expr_initializer_rec(), 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_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(), cpp_typecheckt::typecheck_type(), smt2_convt::unflatten(), and xml().
|
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 1669 of file std_types.h.
References irept::id(), and PRECONDITION.
|
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().