cprover
typet Class Reference

The type of an expression. More...

#include <type.h>

Inheritance diagram for typet:
[legend]
Collaboration diagram for typet:
[legend]

Public Types

typedef std::vector< typetsubtypest
 
- Public Types inherited from irept
typedef std::vector< ireptsubt
 
typedef std::map< irep_namet, ireptnamed_subt
 

Public Member Functions

 typet ()
 
 typet (const irep_idt &_id)
 
 typet (const irep_idt &_id, const typet &_subtype)
 
const typetsubtype () const
 
typetsubtype ()
 
subtypestsubtypes ()
 
const subtypestsubtypes () 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_locationtsource_location () const
 
source_locationtadd_source_location ()
 
typetadd_type (const irep_namet &name)
 
const typetfind_type (const irep_namet &name) const
 
- Public Member Functions inherited from irept
bool is_nil () const
 
bool is_not_nil () const
 
 irept (const irep_idt &_id)
 
 irept ()
 
 irept (const irept &irep)
 
 irept (irept &&irep)
 
ireptoperator= (const irept &irep)
 
ireptoperator= (irept &&irep)
 
 ~irept ()
 
const irep_idtid () const
 
const std::string & id_string () const
 
void id (const irep_idt &_data)
 
const ireptfind (const irep_namet &name) const
 
ireptadd (const irep_namet &name)
 
ireptadd (const irep_namet &name, const irept &irep)
 
const std::string & get_string (const irep_namet &name) const
 
const irep_idtget (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 ()
 
subtget_sub ()
 
const subtget_sub () const
 
named_subtget_named_sub ()
 
const named_subtget_named_sub () const
 
named_subtget_comments ()
 
const named_subtget_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 dtread () const
 
dtwrite ()
 

Additional Inherited Members

- Protected Member Functions inherited from irept
void detach ()
 
- Static Protected Member Functions inherited from irept
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...
 
- Protected Attributes inherited from irept
dtdata
 
- Static Protected Attributes inherited from irept
static dt empty_d
 

Detailed Description

The type of an expression.

Definition at line 20 of file type.h.

Member Typedef Documentation

§ subtypest

typedef std::vector<typet> typet::subtypest

Definition at line 54 of file type.h.

Constructor & Destructor Documentation

§ typet() [1/3]

typet::typet ( )
inline

Definition at line 23 of file type.h.

§ typet() [2/3]

typet::typet ( const irep_idt _id)
inlineexplicit

Definition at line 25 of file type.h.

§ typet() [3/3]

typet::typet ( const irep_idt _id,
const typet _subtype 
)
inline

Definition at line 26 of file type.h.

References subtype().

Member Function Documentation

§ add_source_location()

§ add_type()

typet& typet::add_type ( const irep_namet name)
inline

Definition at line 105 of file type.h.

References irept::add().

Referenced by code_typet::return_type().

§ copy_to_subtypes()

void typet::copy_to_subtypes ( const typet type)

Definition at line 12 of file type.cpp.

References subtypes().

Referenced by Parser::merge_types(), remove_subtype(), and type_with_subtypest::type_with_subtypest().

§ find_type()

const typet& typet::find_type ( const irep_namet name) const
inline

Definition at line 110 of file type.h.

References irept::find().

Referenced by print_struct_alignment_problems(), and code_typet::return_type().

§ has_subtype()

§ has_subtypes()

bool typet::has_subtypes ( ) const
inline

Definition at line 70 of file type.h.

References irept::find(), irept::get_sub(), and irept::is_nil().

Referenced by fence_volatilet::is_volatile(), and type2name().

§ move_to_subtypes()

void typet::move_to_subtypes ( typet type)

§ remove_subtype()

void typet::remove_subtype ( )
inline

§ source_location()

const source_locationt& typet::source_location ( ) const
inline

Definition at line 95 of file type.h.

References irept::find().

Referenced by cpp_typecheckt::add_anonymous_members_to_scope(), cpp_typecheckt::add_base_components(), 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(), ansi_c_convert_typet::read(), cpp_convert_typet::read_function_type(), 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().

§ subtype() [1/2]

const typet& typet::subtype ( ) const
inline

Definition at line 31 of file type.h.

References irept::find(), 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_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), cpp_typecheckt::add_implicit_dereference(), goto_program2codet::add_local_types(), goto_symext::address_arithmetic(), adjust_float_expressions(), linkingt::adjust_object_type_rec(), alignment(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), ansi_c_entry_point(), template_mapt::apply(), value_sett::apply_code(), path_symex_statet::array_theory(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), path_symext::assign_rec(), 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(), bv_width(), c_bit_field_replacement_type(), smt1_convt::ce_value(), 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(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), compute_address_taken_functions(), cpp_typecheckt::const_typecast(), cpp_declarator_convertert::convert(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), boolbvt::convert_array_of(), expr2ct::convert_array_type(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), bv_pointerst::convert_bitvector(), dump_ct::convert_compound(), expr2ct::convert_constant(), goto_convertt::convert_cpp_delete(), expr2cppt::convert_cpp_new(), dplib_convt::convert_dplib_type(), convert_float_literal(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), cpp_typecheck_resolvet::convert_identifier(), smt1_convt::convert_index(), boolbvt::convert_index(), smt2_convt::convert_index(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), convert_integer_literal(), expr2javat::convert_java_new(), expr2ct::convert_malloc(), smt2_convt::convert_minus(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), bv_pointerst::convert_pointer_type(), expr2ct::convert_rec(), expr2cppt::convert_rec(), convert_string_literal(), cvc_convt::convert_type(), smt1_convt::convert_type(), smt2_convt::convert_type(), boolbvt::convert_unary_minus(), smt1_convt::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), expr2ct::convert_with_precedence(), copy_parent(), cpp_typecheckt::cpp_destructor(), cpp_exception_list_rec(), cpp_typecheckt::cpp_is_pod(), goto_convertt::cpp_new_initializer(), cpp_type2name(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), value_set_dereferencet::dereference(), dereferencet::dereference_plus(), goto_symext::dereference_rec(), c_typecheck_baset::designator_enter(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_array_equal(), 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_java_new(), goto_convertt::do_java_new_array(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_strerror(), c_typecastt::do_typecast(), does_remove_constt::does_type_preserve_const_correctness(), linkingt::duplicate_type_symbol(), cpp_typecheckt::dynamic_typecast(), path_symex_statet::expand_structs_and_arrays(), character_refine_preprocesst::expr_of_to_chars(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_superclass_with_type(), find_symbols(), smt1_convt::find_symbols_rec(), smt2_convt::find_symbols_rec(), smt1_convt::flatten_array(), flatten_byte_extract(), flatten_byte_update(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_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_pointer_init(), java_object_factoryt::gen_pointer_target_init(), string_refinementt::get_array(), c_typecastt::get_c_type(), ansi_c_parsert::get_class(), get_class_identifier_field(), java_bytecode_parsert::get_class_refs_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(), 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(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), interpretert::get_size(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), good_pointer_def(), goto_checkt::goto_check(), 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(), string_instrumentationt::invalidate_buffer(), cpp_declarator_convertert::is_code_type(), c_typecheck_baset::is_complete_type(), remove_const_function_pointerst::is_const_type(), is_empty(), refined_string_typet::is_java_char_sequence_type(), refined_string_typet::is_java_string_builder_type(), refined_string_typet::is_java_string_pointer_type(), string_abstractiont::is_ptr_string_struct(), string_instrumentationt::is_string_type(), is_void_pointer(), fence_volatilet::is_volatile(), java_type_from_string(), json(), c_typecheck_baset::make_already_typechecked(), make_clean_pointer_cast(), c_typecheck_baset::make_designator(), cpp_typecheckt::make_ptr_typecast(), 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(), print_struct_alignment_problems(), Parser::rConstructorDecl(), Parser::rDeclarator(), Parser::rDeclaratorWithInit(), c_storage_spect::read(), cpp_convert_typet::read_function_type(), dereferencet::read_object(), 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(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), Parser::rEnumSpec(), replace_symbolt::replace(), Parser::rNewDeclarator(), 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(), c_sizeoft::sizeof_rec(), 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(), smt1_dect::string_to_expr_z3(), goto_symext::symex_cpp_new(), path_symext::symex_malloc(), goto_symext::symex_malloc(), 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_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), cpp_typecheckt::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_expr_trinary(), 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(), smt2_convt::unflatten(), unpack_rec(), cpp_typecheckt::user_defined_conversion_sequence(), string_abstractiont::value_assignments(), ansi_c_convert_typet::write(), xml(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

§ subtype() [2/2]

typet& typet::subtype ( )
inline

Definition at line 42 of file type.h.

References irept::add(), and irept::get_sub().

§ subtypes() [1/2]

§ subtypes() [2/2]

const subtypest& typet::subtypes ( ) const
inline

Definition at line 63 of file type.h.

References irept::find(), and irept::get_sub().


The documentation for this class was generated from the following files: