cprover
|
The type of an expression. More...
#include <type.h>
Public Types | |
typedef std::vector< typet > | subtypest |
![]() | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_subt |
Public Member Functions | |
typet () | |
typet (const irep_idt &_id) | |
typet (const irep_idt &_id, const typet &_subtype) | |
const typet & | subtype () const |
typet & | subtype () |
subtypest & | subtypes () |
const subtypest & | subtypes () const |
bool | has_subtypes () const |
bool | has_subtype () const |
void | remove_subtype () |
void | move_to_subtypes (typet &type) |
void | copy_to_subtypes (const typet &type) |
const source_locationt & | source_location () const |
source_locationt & | add_source_location () |
typet & | add_type (const irep_namet &name) |
const typet & | find_type (const irep_namet &name) const |
![]() | |
bool | is_nil () const |
bool | is_not_nil () const |
irept (const irep_idt &_id) | |
irept () | |
irept (const irept &irep) | |
irept (irept &&irep) | |
irept & | operator= (const irept &irep) |
irept & | operator= (irept &&irep) |
~irept () | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_namet &name) const |
irept & | add (const irep_namet &name) |
irept & | add (const irep_namet &name, const irept &irep) |
const std::string & | get_string (const irep_namet &name) const |
const irep_idt & | get (const irep_namet &name) const |
bool | get_bool (const irep_namet &name) const |
signed int | get_int (const irep_namet &name) const |
unsigned int | get_unsigned_int (const irep_namet &name) const |
std::size_t | get_size_t (const irep_namet &name) const |
long long | get_long_long (const irep_namet &name) const |
void | set (const irep_namet &name, const irep_idt &value) |
void | set (const irep_namet &name, const irept &irep) |
void | set (const irep_namet &name, const long long value) |
void | remove (const irep_namet &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_namet &name, irept &irep) |
bool | operator== (const irept &other) const |
bool | operator!= (const irept &other) const |
void | swap (irept &irep) |
bool | operator< (const irept &other) const |
defines ordering on the internal representation More... | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation More... | |
int | compare (const irept &i) const |
defines ordering on the internal representation More... | |
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
named_subt & | get_comments () |
const named_subt & | get_comments () const |
std::size_t | hash () const |
std::size_t | full_hash () const |
bool | full_eq (const irept &other) const |
std::string | pretty (unsigned indent=0, unsigned max_indent=0) const |
const dt & | read () const |
dt & | write () |
Additional Inherited Members | |
![]() | |
void | detach () |
![]() | |
static bool | is_comment (const irep_namet &name) |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. More... | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
typedef std::vector<typet> typet::subtypest |
|
inline |
Definition at line 102 of file type.h.
References irept::add().
Referenced by c_typecheck_baset::adjust_function_parameter(), template_mapt::build_unassigned(), cpp_typecheckt::default_assignop(), goto_symext::dereference_rec(), cpp_typecheck_resolvet::disambiguate_template_classes(), cpp_typecheckt::instantiate_template(), Parser::merge_types(), Parser::rAttribute(), cpp_convert_typet::read_rec(), ansi_c_convert_typet::read_rec(), remove_complex(), goto_convertt::remove_gcc_conditional_expression(), remove_vector(), cpp_typecheck_resolvet::resolve_scope(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_explicit_constructor_call(), cpp_typecheckt::typecheck_template_parameters(), and ansi_c_convert_typet::write().
|
inline |
Definition at line 107 of file type.h.
References irept::add().
Referenced by code_typet::code_typet(), and code_typet::return_type().
void typet::copy_to_subtypes | ( | const typet & | type | ) |
Definition at line 13 of file type.cpp.
References subtypes().
|
inline |
Definition at line 112 of file type.h.
References irept::find().
Referenced by java_array_element_type(), print_struct_alignment_problems(), and code_typet::return_type().
|
inline |
Definition at line 79 of file type.h.
References irept::get_sub().
Referenced by check_renaming(), cpp_convert_auto(), find_symbols(), ansi_c_parsert::get_class(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), is_constant_or_has_constant_components(), c_storage_spect::read(), ansi_c_convert_typet::read_rec(), rename_symbolt::rename(), replace_symbolt::replace(), and type2name().
|
inline |
void typet::move_to_subtypes | ( | typet & | type | ) |
Definition at line 18 of file type.cpp.
References get_nil_irep(), and subtypes().
Referenced by Parser::merge_types().
|
inline |
Definition at line 86 of file type.h.
References irept::get_sub().
Referenced by cpp_convert_typet::read_function_type(), and c_typecheck_baset::typecheck_code_type().
|
inline |
Definition at line 97 of file type.h.
References irept::find().
Referenced by cpp_typecheckt::add_anonymous_members_to_scope(), cpp_typecheckt::add_base_components(), c_typecheck_baset::adjust_function_parameter(), ansi_c_declaratort::build(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::convert_class_template_specialization(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_template_function_or_member_specialization(), boolbvt::convert_with(), boolbvt::convert_with_array(), boolbvt::convert_with_struct(), boolbvt::convert_with_union(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), linkingt::detailed_conflict_report_rec(), goto_convertt::do_function_call_symbol(), cpp_typecheckt::dtor(), cpp_typecheckt::elaborate_class_template(), typecheckt::err_location(), Parser::merge_types(), ansi_c_convert_typet::read(), cpp_convert_typet::read_function_type(), cpp_convert_typet::read_rec(), ansi_c_convert_typet::read_rec(), remove_complex(), remove_vector(), Parser::rTemplateArgs(), type2name(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_symbol_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), and c_typecheck_baset::typecheck_typeof_type().
|
inline |
Definition at line 33 of file type.h.
References get_nil_irep(), and irept::get_sub().
Referenced by string_abstractiont::abstract_function_call(), c_typecheck_baset::add_argc_argv(), arrayst::add_array_Ackermann_constraints(), string_constraint_generatort::add_axioms_for_characters_in_integer_string(), string_constraint_generatort::add_axioms_for_code_point(), string_constraint_generatort::add_axioms_for_concat_code_point(), string_constraint_generatort::add_axioms_for_constant(), string_constraint_generatort::add_axioms_for_correct_number_format(), string_constraint_generatort::add_axioms_for_delete(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_fractional_part(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_insert_bool(), string_constraint_generatort::add_axioms_for_insert_char(), string_constraint_generatort::add_axioms_for_insert_double(), string_constraint_generatort::add_axioms_for_insert_int(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_for_trim(), string_constraint_generatort::add_axioms_from_bool(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), string_constraint_generatort::add_axioms_from_int_hex(), string_constraint_generatort::add_axioms_from_int_with_radix(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), goto_program2codet::add_local_types(), add_nondet_string_pointer_initialization(), goto_symext::address_arithmetic(), adjust_float_expressions(), c_typecheck_baset::adjust_function_parameter(), linkingt::adjust_object_type_rec(), alignment(), allocate_dynamic_object_with_decl(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), template_mapt::apply(), value_sett::apply_code_rec(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), value_set_fit::assign_rec(), base_type_rec(), simplify_exprt::bits2expr(), ansi_c_declaratort::build(), string_abstractiont::build(), string_abstractiont::build_abstraction_type_rec(), endianness_mapt::build_big_endian(), value_set_dereferencet::build_reference_to(), string_abstractiont::build_symbol(), string_abstractiont::build_wrap(), boolbvt::bv_get_rec(), boolbvt::bv_get_unbounded_array(), c_bit_field_replacement_type(), check_c_implicit_typecast(), cpp_typecheckt::check_fixed_size_array(), check_renaming(), value_set_analysis_fit::check_type(), value_set_analysis_fivrt::check_type(), value_set_analysis_fivrnst::check_type(), clean_deref(), dump_ct::cleanup_expr(), java_string_library_preprocesst::code_assign_components_to_java_string(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), compute_address_taken_functions(), compute_pointer_offset(), interpretert::concretize_type(), cpp_typecheckt::const_typecast(), cpp_declarator_convertert::convert(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), expr2ct::convert_allocate(), java_bytecode_convert_methodt::convert_aload(), boolbvt::convert_array_of(), expr2ct::convert_array_type(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), java_bytecode_convert_methodt::convert_astore(), bv_pointerst::convert_bitvector(), dump_ct::convert_compound(), expr2ct::convert_constant(), expr2cppt::convert_cpp_new(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), java_bytecode_convert_methodt::convert_getstatic(), cpp_typecheck_resolvet::convert_identifier(), boolbvt::convert_index(), smt2_convt::convert_index(), cpp_typecheckt::convert_initializer(), convert_integer_literal(), expr2javat::convert_java_new(), smt2_convt::convert_minus(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), bv_pointerst::convert_pointer_type(), expr2ct::convert_rec(), expr2cppt::convert_rec(), convert_string_literal(), smt2_convt::convert_type(), boolbvt::convert_unary_minus(), boolbvt::convert_with(), smt2_convt::convert_with(), expr2ct::convert_with_precedence(), copy_parent(), cpp_convert_auto(), cpp_typecheckt::cpp_destructor(), cpp_exception_list_rec(), cpp_typecheckt::cpp_is_pod(), goto_convertt::cpp_new_initializer(), cpp_type2name(), java_simple_method_stubst::create_method_stub_at(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), value_set_dereferencet::dereference(), dereferencet::dereference_plus(), goto_symext::dereference_rec(), value_set_dereferencet::dereference_type_compare(), c_typecheck_baset::designator_enter(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), c_typecastt::do_typecast(), does_remove_constt::does_type_preserve_const_correctness(), linkingt::duplicate_type_symbol(), cpp_typecheckt::dynamic_typecast(), equal_java_types(), string_transformation_builtin_functiont::eval(), string_insertion_builtin_functiont::eval(), interpretert::evaluate(), expr_initializert< nondet >::expr_initializer_rec(), character_refine_preprocesst::expr_of_to_chars(), array_poolt::find(), java_bytecode_parse_treet::find_annotation(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_superclass_with_type(), find_symbols(), smt2_convt::find_symbols_rec(), flatten_byte_extract(), flatten_byte_update(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_rec(), format_rec(), string_constantt::from_array_expr(), from_integer(), ansi_c_declarationt::full_type(), cpp_typecheckt::function_identifier(), function_to_call(), c_typecheck_baset::gcc_types_compatible_p(), c_typecheck_baset::gcc_vector_types_compatible(), java_object_factoryt::gen_nondet_array_init(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_pointer_target_init(), generate_ansi_c_start_function(), havoc_generate_function_bodiest::generate_function_body_impl(), string_refinementt::get(), get_array(), c_typecastt::get_c_type(), refined_string_typet::get_char_type(), ansi_c_parsert::get_class(), get_class_identifier_field(), java_bytecode_parsert::get_class_refs_rec(), get_dependencies_from_generic_parameters_rec(), get_destructor(), value_set_analysis_fit::get_entries_rec(), value_set_analysis_fivrt::get_entries_rec(), value_set_analysis_fivrnst::get_entries_rec(), boolbv_widtht::get_entry(), uncaught_exceptions_domaint::get_exception_type(), java_string_library_preprocesst::get_object_at_index(), rw_range_sett::get_objects_array(), rw_range_sett::get_objects_complex(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_rec(), goto_symex_statet::get_original_name(), java_string_library_preprocesst::get_primitive_value_of_object(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), interpretert::get_size(), interpretert::get_value(), value_set_fit::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), good_pointer_def(), cpp_typecheck_resolvet::guess_template_args(), have_to_adjust_float_expressions(), have_to_remove_complex(), have_to_remove_vector(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), c_typecastt::implicit_typecast_arithmetic(), c_typecastt::implicit_typecast_followed(), goto_symext::initialize_auto_object(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), string_instrumentationt::invalidate_buffer(), is_char_array_type(), is_char_pointer_type(), cpp_declarator_convertert::is_code_type(), c_typecheck_baset::is_complete_type(), remove_const_function_pointerst::is_const_type(), is_constant_or_has_constant_components(), 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(), string_abstractiont::is_ptr_string_struct(), string_instrumentationt::is_string_type(), is_void_pointer(), java_generic_symbol_typet::java_generic_symbol_typet(), java_type_from_string(), json(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), array_poolt::make_char_array_for_char_pointer(), make_clean_pointer_cast(), c_typecheck_baset::make_designator(), java_string_library_preprocesst::make_object_get_class_code(), cpp_typecheckt::make_ptr_typecast(), make_string(), java_string_library_preprocesst::make_string_length_code(), Parser::make_subtype(), string_abstractiont::make_val_or_dummy_rec(), value_set_dereferencet::memory_model_bytes(), cpp_declaratort::merge_type(), mutex_init_instrumentation(), linkingt::needs_renaming_type(), pointer_logict::object_rec(), dereferencet::operator()(), cpp_typecheckt::overloadable(), goto_inlinet::parameter_assignments(), smt2_convt::parse_array(), pointer_offset_bits(), goto_checkt::pointer_validity_check(), pretty_java_type(), print_struct_alignment_problems(), goto_symext::process_array_expr(), Parser::rConstructorDecl(), Parser::rDeclarator(), Parser::rDeclaratorWithInit(), c_storage_spect::read(), cpp_convert_typet::read_function_type(), dereferencet::read_object(), cpp_convert_typet::read_rec(), ansi_c_convert_typet::read_rec(), cpp_convert_typet::read_template(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_compatible(), cpp_typecheckt::reference_related(), remove_complex(), goto_program2codet::remove_const(), goto_convertt::remove_post(), remove_vector(), remove_virtual_functionst::remove_virtual_function(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), Parser::rEnumSpec(), replace_symbolt::replace(), java_string_library_preprocesst::replace_char_array(), require_java_generic_type_argument_expectation(), require_type::require_java_non_generic_type(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_index(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_typecast(), size_of_expr(), select_pointer_typet::specialize_generics(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_qualification(), cpp_typecheckt::standard_conversion_sequence(), cpp_typecheckt::static_typecast(), substitute_array_access(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_other(), template_subtype(), cpp_typecheckt::this_struct_type(), string_constantt::to_array_expr(), to_integer(), smt2_convt::type2id(), type2name(), boolbvt::type_conversion(), linkingt::type_to_string_verbose(), type_with_subtypet::type_with_subtypet(), c_typecheck_baset::typecheck_arithmetic_pointer(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), c_typecheck_baset::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), cpp_typecheckt::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_initializer(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_try_catch(), java_bytecode_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), typet(), interpretert::unbounded_size(), underlying_width(), smt2_convt::unflatten(), unpack_rec(), cpp_typecheckt::user_defined_conversion_sequence(), string_abstractiont::value_assignments(), ansi_c_convert_typet::write(), xml(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 44 of file type.h.
References irept::get_sub().
|
inline |
Definition at line 58 of file type.h.
References irept::get_sub().
Referenced by ansi_c_declaratort::build(), mathematical_function_typet::codomain(), copy_to_subtypes(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), mathematical_function_typet::domain(), ansi_c_declarationt::full_type(), cpp_typecheck_resolvet::guess_template_args(), has_subtype(), Parser::make_subtype(), mathematical_function_typet::mathematical_function_typet(), cpp_declaratort::merge_type(), Parser::merge_types(), move_to_subtypes(), and yyansi_cparse().
|
inline |
Definition at line 65 of file type.h.
References irept::get_sub().