cprover
|
#include "std_types.h"
Go to the source code of this file.
typet c_bool_type | ( | ) |
Definition at line 107 of file c_types.cpp.
References configt::ansi_c, configt::ansi_ct::bool_width, and config.
Referenced by cpp_typecheckt::typecheck_expr_cpp_name(), and ansi_c_convert_typet::write().
std::string c_type_as_string | ( | const irep_idt & | ) |
Definition at line 325 of file c_types.cpp.
Referenced by expr2ct::convert_rec().
unsignedbv_typet char16_t_type | ( | ) |
Definition at line 164 of file c_types.cpp.
References irept::set().
Referenced by convert_string_literal(), and cpp_convert_typet::write().
unsignedbv_typet char32_t_type | ( | ) |
Definition at line 174 of file c_types.cpp.
References irept::set().
Referenced by convert_string_literal(), and cpp_convert_typet::write().
bitvector_typet char_type | ( | ) |
Definition at line 113 of file c_types.cpp.
References configt::ansi_c, configt::ansi_ct::char_is_unsigned, configt::ansi_ct::char_width, config, and irept::set().
Referenced by string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_to_lower_case(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_from_char_array(), string_constraint_generatort::add_axioms_from_float(), string_constraint_generatort::add_axioms_from_int(), string_constraint_generatort::add_axioms_from_int_hex(), goto_symext::address_arithmetic(), value_set_dereferencet::build_reference_to(), string_constraint_generatort::constant_char(), expr2ct::convert_array(), convert_character_literal(), expr2ct::convert_constant(), bv_pointerst::convert_pointer_type(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), string_instrumentationt::do_strerror(), character_refine_preprocesst::expr_of_to_chars(), function_to_call(), string_refinementt::get_array(), get_type(), value_sett::get_value_set_rec(), refined_string_typet::refined_string_typet(), string_constantt::set_value(), simplify_exprt::simplify_pointer_offset(), string_constantt::to_array_expr(), filedescriptor_streambuft::underflow(), cpp_convert_typet::write(), ansi_c_convert_typet::write(), and filedescriptor_streambuft::xsgetn().
bitvector_typet double_type | ( | ) |
Definition at line 203 of file c_types.cpp.
References configt::ansi_c, config, ieee_float_spect::double_precision(), configt::ansi_ct::double_width, irept::set(), fixedbv_typet::set_integer_bits(), bitvector_typet::set_width(), ieee_float_spect::to_type(), and configt::ansi_ct::use_fixed_for_float.
Referenced by expr2ct::convert_complex(), convert_float_literal(), goto_convertt::do_function_call_symbol(), get_type(), c_typecastt::implicit_typecast_arithmetic(), printf_formattert::process_format(), cpp_typecheckt::standard_conversion_floating_point_promotion(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
bitvector_typet enum_constant_type | ( | ) |
return type of enum constants
Definition at line 22 of file c_types.cpp.
References signed_int_type().
bitvector_typet float_type | ( | ) |
Definition at line 184 of file c_types.cpp.
References configt::ansi_c, config, irept::set(), fixedbv_typet::set_integer_bits(), bitvector_typet::set_width(), ieee_float_spect::single_precision(), configt::ansi_ct::single_width, ieee_float_spect::to_type(), and configt::ansi_ct::use_fixed_for_float.
Referenced by expr2ct::convert_complex(), expr2ct::convert_constant(), convert_float_literal(), goto_convertt::do_function_call_symbol(), get_type(), c_typecastt::implicit_typecast_arithmetic(), cpp_typecheckt::standard_conversion_floating_point_promotion(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
bitvector_typet gcc_float128_type | ( | ) |
Definition at line 260 of file c_types.cpp.
References configt::ansi_c, config, ieee_float_spect::quadruple_precision(), irept::set(), fixedbv_typet::set_integer_bits(), bitvector_typet::set_width(), ieee_float_spect::to_type(), and configt::ansi_ct::use_fixed_for_float.
Referenced by c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet gcc_signed_int128_type | ( | ) |
Definition at line 318 of file c_types.cpp.
References irept::set().
Referenced by c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
unsignedbv_typet gcc_unsigned_int128_type | ( | ) |
Definition at line 311 of file c_types.cpp.
References irept::set().
Referenced by c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
bitvector_typet index_type | ( | ) |
Definition at line 15 of file c_types.cpp.
References signed_size_type().
Referenced by string_abstractiont::abstract_function_call(), string_constraint_generatort::add_axioms_for_compare_to(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_hash_code(), string_constraint_generatort::add_axioms_for_if(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_index_of_string(), string_constraint_generatort::add_axioms_for_intern(), string_constraint_generatort::add_axioms_for_is_prefix(), string_constraint_generatort::add_axioms_for_is_suffix(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_last_index_of_string(), string_constraint_generatort::add_axioms_for_substring(), string_constraint_generatort::add_axioms_for_to_lower_case(), 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_char_array(), string_constraint_generatort::add_axioms_from_float(), string_constraint_generatort::add_axioms_from_int(), string_constraint_generatort::add_axioms_from_int_hex(), goto_symext::address_arithmetic(), ansi_c_entry_point(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), path_symext::assign_rec(), object_descriptor_exprt::build(), build_object_descriptor_rec(), c_nondet_symbol_factory(), string_refinementt::check_axioms(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), smt2_convt::convert_expr(), boolbvt::convert_extractbit(), boolbvt::convert_member(), smt2_convt::convert_minus(), smt2_convt::convert_plus(), convert_string_literal(), copy_array(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), string_refinementt::dec_solve(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), string_instrumentationt::do_format_string_read(), c_typecheck_baset::do_initializer_list(), goto_convertt::do_scanf(), string_instrumentationt::do_strerror(), c_typecastt::do_typecast(), function_to_call(), string_refinementt::get_array(), local_may_aliast::get_rec(), 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(), string_instrumentationt::invalidate_buffer(), java_build_arguments(), java_record_outputs(), c_typecheck_baset::make_index_type(), dereferencet::operator()(), goto_symext::parameter_assignments(), goto_symext::process_array_expr_rec(), record_function_outputs(), refined_string_typet::refined_string_typet(), goto_convertt::remove_post(), goto_convertt::remove_pre(), rewrite_union(), string_constantt::set_value(), simplify_exprt::simplify_address_of_arg(), cpp_typecheckt::standard_conversion_array_to_pointer(), string_refinementt::sum_over_map(), goto_symext::symex_cpp_new(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_other(), string_constantt::to_array_expr(), value_sett::to_expr(), value_set_fit::to_expr(), value_set_fivrnst::to_expr(), value_set_fivrt::to_expr(), c_typecheck_baset::typecheck_compound_body(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), unpack_rec(), and cpp_typecheckt::zero_initializer().
bitvector_typet long_double_type | ( | ) |
Definition at line 222 of file c_types.cpp.
References configt::ansi_c, config, ieee_float_spect::double_precision(), configt::ansi_ct::long_double_width, ieee_float_spect::quadruple_precision(), irept::set(), fixedbv_typet::set_integer_bits(), bitvector_typet::set_width(), ieee_float_spect::to_type(), and configt::ansi_ct::use_fixed_for_float.
Referenced by expr2ct::convert_complex(), expr2ct::convert_constant(), convert_float_literal(), c_typecheck_baset::do_special_functions(), get_type(), c_typecastt::implicit_typecast_arithmetic(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet pointer_diff_type | ( | ) |
Definition at line 281 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, configt::ansi_ct::pointer_width, signed_int_type(), signed_long_int_type(), and signed_long_long_int_type().
Referenced by pointer_logict::pointer_expr(), signed_size_type(), and c_typecheck_baset::typecheck_expr_pointer_arithmetic().
pointer_typet pointer_type | ( | const typet & | ) |
Definition at line 296 of file c_types.cpp.
Referenced by string_abstractiont::add_argument(), java_bytecode_convert_classt::add_array_types(), remove_exceptionst::add_exceptional_returns(), shared_bufferst::add_initialization(), java_bytecode_convert_classt::add_string_type(), cpp_typecheckt::add_this_to_method_type(), java_bytecode_vtable_factoryt::add_vtable_entry(), add_vtable_pointer_member(), goto_symext::address_arithmetic(), c_typecheck_baset::adjust_function_parameter(), java_object_factoryt::allocate_object(), ansi_c_entry_point(), string_abstractiont::build_abstraction_type_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), goto_program2codet::convert_assign_varargs(), goto_convertt::convert_decl(), java_bytecode_convert_methodt::convert_instructions(), goto_program2codet::convert_start_thread(), cpp_typecheckt::cpp_destructor(), goto_symext::dereference_rec(), dereferencet::dereference_typecast(), goto_convertt::do_function_call_symbol(), goto_convertt::do_scanf(), cpp_typecheckt::do_virtual_table(), function_to_call(), remove_asmt::gcc_asm_function_call(), 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(), get_class_identifier_field(), get_ref(), get_type(), good_pointer_def(), goto_symext::initialize_auto_object(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), java_internal_additions(), jsil_internal_additions(), make_vtable_function(), pointer_logict::object_rec(), shared_bufferst::operator()(), goto_checkt::pointer_validity_check(), cpp_convert_typet::read_function_type(), cpp_typecheckt::reference_binding(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), simplify_exprt::simplify_address_of_arg(), path_symext::symex_malloc(), goto_symext::symex_malloc(), thread_exit_instrumentation(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_symbol(), c_typecheck_baset::typecheck_function_call_arguments(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_type(), cpp_typecheckt::user_defined_conversion_sequence(), and shared_bufferst::cfg_visitort::weak_memory().
reference_typet reference_type | ( | const typet & | ) |
Definition at line 301 of file c_types.cpp.
Referenced by java_reference_type(), and cpp_typecheckt::typecheck_expr_address_of().
signedbv_typet signed_char_type | ( | ) |
Definition at line 141 of file c_types.cpp.
References configt::ansi_c, configt::ansi_ct::char_width, config, and irept::set().
Referenced by c_typecheck_baset::enum_underlying_type(), string_constantt::from_array_expr(), get_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet signed_int_type | ( | ) |
Definition at line 29 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, and irept::set().
Referenced by c_typecheck_baset::adjust_function_parameter(), convert_character_literal(), expr2ct::convert_constant(), enum_constant_type(), c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), get_type(), c_typecastt::implicit_typecast_arithmetic(), java_internal_additions(), jsil_internal_additions(), cpp_declarator_convertert::main_function_rules(), cpp_typecheck_resolvet::make_constructors(), pointer_diff_type(), printf_formattert::process_format(), goto_convertt::remove_post(), goto_convertt::remove_pre(), cpp_typecheckt::standard_conversion_integral_promotion(), c_typecheck_baset::typecheck_c_enum_tag_type(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_cpp_name(), c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet signed_long_int_type | ( | ) |
Definition at line 79 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::long_int_width, and irept::set().
Referenced by c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), get_type(), c_typecastt::implicit_typecast_arithmetic(), pointer_diff_type(), printf_formattert::process_format(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet signed_long_long_int_type | ( | ) |
Definition at line 86 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::long_long_int_width, and irept::set().
Referenced by c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), get_type(), c_typecastt::implicit_typecast_arithmetic(), pointer_diff_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet signed_short_int_type | ( | ) |
Definition at line 36 of file c_types.cpp.
References configt::ansi_c, config, irept::set(), and configt::ansi_ct::short_int_width.
Referenced by c_typecheck_baset::enum_underlying_type(), get_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
signedbv_typet signed_size_type | ( | ) |
Definition at line 73 of file c_types.cpp.
References pointer_diff_type().
Referenced by cpp_typecheck_resolvet::do_builtin(), index_type(), pointer_offset(), c_typecheck_baset::typecheck_type(), and c_typecheck_baset::typecheck_vector_type().
unsignedbv_typet size_type | ( | ) |
Definition at line 57 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, configt::ansi_ct::pointer_width, unsigned_int_type(), unsigned_long_int_type(), and unsigned_long_long_int_type().
Referenced by add_to_json(), assembler_name(), polynomial_acceleratort::assert_for_values(), simplify_exprt::bits2expr(), buffer_size(), resolution_prooft< clauset >::build_core(), build_sizeof_expr(), string_abstractiont::build_type(), c_sizeoft::c_offsetof(), clean_identifier(), goto_program2codet::cleanup_code_block(), irept::compare(), compiler_name(), aig_prop_solvert::convert_node(), compilet::convert_symbols(), cpp_typecheck_resolvet::do_builtin(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_strerror(), dott::escape(), simplify_exprt::expr2bits(), get_full_class_name(), aigt::get_terminals(), expr2ct::id_shorthand(), dump_ct::ignore(), symex_slice_by_tracet::implied_guards(), string_instrumentationt::invalidate_buffer(), java_bytecode_convert_methodt::is_constructor(), linker_name(), list_calls_and_arguments(), member_offset_expr(), value_set_dereferencet::memory_model_bytes(), object_size(), dump_ct::operator()(), aigt::output_dot(), lispexprt::parse(), symex_slice_by_tracet::parse_events(), parse_loop_ids(), gcc_cmdlinet::parse_specs_line(), pointer_object(), aigt::print(), event_grapht::critical_cyclet::print_name(), cvc_dect::read_assert(), dplib_dect::read_assert(), graphml_witnesst::remove_l0_l1(), set_virtual_name(), simplify_exprt::simplify_typecast(), size_of_expr(), c_sizeoft::sizeof_rec(), symex_slice_by_tracet::slice_by_trace(), split_string(), static_lifetime_init(), strip_string(), substitute(), c_typecheck_baset::typecheck_expr_alignof(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_type(), unpack_rec(), utf8_to_utf16(), yyansi_clex(), zero_initializert::zero_initializer_rec(), and zero_string_length().
unsignedbv_typet unsigned_char_type | ( | ) |
Definition at line 134 of file c_types.cpp.
References configt::ansi_c, configt::ansi_ct::char_width, config, and irept::set().
Referenced by c_typecheck_baset::enum_underlying_type(), string_constantt::from_array_expr(), get_type(), value_sett::get_value_set_rec(), value_sett::guard(), path_symext::symex_malloc(), goto_symext::symex_malloc(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
unsignedbv_typet unsigned_int_type | ( | ) |
Definition at line 43 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, and irept::set().
Referenced by c_typecheck_baset::add_rounding_mode(), expr2ct::convert_constant(), string_instrumentationt::do_format_string_write(), c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), get_type(), c_typecastt::implicit_typecast_arithmetic(), string_instrumentationt::invalidate_buffer(), printf_formattert::process_format(), size_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
unsignedbv_typet unsigned_long_int_type | ( | ) |
Definition at line 93 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::long_int_width, and irept::set().
Referenced by c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), get_type(), c_typecastt::implicit_typecast_arithmetic(), printf_formattert::process_format(), size_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
unsignedbv_typet unsigned_long_long_int_type | ( | ) |
Definition at line 100 of file c_types.cpp.
References configt::ansi_c, config, configt::ansi_ct::long_long_int_width, and irept::set().
Referenced by c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), get_type(), c_typecastt::implicit_typecast_arithmetic(), size_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
unsignedbv_typet unsigned_short_int_type | ( | ) |
Definition at line 50 of file c_types.cpp.
References configt::ansi_c, config, irept::set(), and configt::ansi_ct::short_int_width.
Referenced by c_typecheck_baset::enum_underlying_type(), get_type(), c_typecheck_baset::typecheck_type(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
typet void_type | ( | ) |
Definition at line 306 of file c_types.cpp.
Referenced by get_type(), c_typecheck_baset::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_function_call_arguments(), and c_typecheck_baset::typecheck_side_effect_function_call().
bitvector_typet wchar_t_type | ( | ) |
Definition at line 148 of file c_types.cpp.
References configt::ansi_c, config, irept::set(), configt::ansi_ct::wchar_t_is_unsigned, and configt::ansi_ct::wchar_t_width.
Referenced by c_preprocess_gcc_clang(), expr2ct::convert_array(), convert_character_literal(), convert_string_literal(), get_type(), and cpp_convert_typet::write().