cprover
c_types.h File Reference
#include "std_types.h"
Include dependency graph for c_types.h:

Go to the source code of this file.

Functions

bitvector_typet index_type ()
 
bitvector_typet enum_constant_type ()
 return type of enum constants More...
 
signedbv_typet signed_int_type ()
 
unsignedbv_typet unsigned_int_type ()
 
signedbv_typet signed_long_int_type ()
 
signedbv_typet signed_short_int_type ()
 
unsignedbv_typet unsigned_short_int_type ()
 
signedbv_typet signed_long_long_int_type ()
 
unsignedbv_typet unsigned_long_int_type ()
 
unsignedbv_typet unsigned_long_long_int_type ()
 
typet c_bool_type ()
 
bitvector_typet char_type ()
 
unsignedbv_typet unsigned_char_type ()
 
signedbv_typet signed_char_type ()
 
bitvector_typet wchar_t_type ()
 
unsignedbv_typet char16_t_type ()
 
unsignedbv_typet char32_t_type ()
 
bitvector_typet float_type ()
 
bitvector_typet double_type ()
 
bitvector_typet long_double_type ()
 
unsignedbv_typet size_type ()
 
signedbv_typet signed_size_type ()
 
signedbv_typet pointer_diff_type ()
 
pointer_typet pointer_type (const typet &)
 
typet void_type ()
 
reference_typet reference_type (const typet &)
 
std::string c_type_as_string (const irep_idt &)
 

Function Documentation

◆ c_bool_type()

◆ c_type_as_string()

std::string c_type_as_string ( const irep_idt )

◆ char16_t_type()

unsignedbv_typet char16_t_type ( )

Definition at line 165 of file c_types.cpp.

References irept::set().

Referenced by convert_string_literal(), and cpp_convert_typet::write().

◆ char32_t_type()

unsignedbv_typet char32_t_type ( )

Definition at line 175 of file c_types.cpp.

References irept::set().

Referenced by convert_string_literal(), and cpp_convert_typet::write().

◆ char_type()

bitvector_typet char_type ( )

Definition at line 114 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_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_format_specifier(), 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_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_float_scientific_notation(), string_constraint_generatort::add_axioms_from_int_hex(), string_constraint_generatort::add_axioms_from_int_with_radix(), goto_symext::address_arithmetic(), string_constraint_generatort::constant_char(), expr2ct::convert_array(), convert_character_literal(), expr2ct::convert_constant(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), string_instrumentationt::do_strerror(), character_refine_preprocesst::expr_of_to_chars(), string_constraint_generatort::fresh_string(), function_to_call(), get_array(), get_numeric_value_from_character(), get_type(), value_sett::get_value_set_rec(), is_digit_with_radix(), linker_script_merget::ls_data2instructions(), make_string(), linker_script_merget::pointerize_linker_defined_symbols(), goto_symext::process_array_expr(), refined_string_typet::refined_string_typet(), string_constantt::set_value(), simplify_exprt::simplify_pointer_offset(), substitute_array_access(), substitute_array_lists(), goto_symext::symex_other(), string_constantt::to_array_expr(), c_typecheck_baset::typecheck_expr_sizeof(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().

◆ double_type()

◆ enum_constant_type()

bitvector_typet enum_constant_type ( )

return type of enum constants

Definition at line 23 of file c_types.cpp.

References signed_int_type().

◆ float_type()

◆ index_type()

bitvector_typet index_type ( )

Definition at line 16 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_concat_char(), string_constraint_generatort::add_axioms_for_concat_code_point(), string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_constant(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_copy(), string_constraint_generatort::add_axioms_for_correct_number_format(), string_constraint_generatort::add_axioms_for_delete(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_format_specifier(), string_constraint_generatort::add_axioms_for_fractional_part(), string_constraint_generatort::add_axioms_for_hash_code(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_index_of_string(), 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_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_set_length(), string_constraint_generatort::add_axioms_for_string_of_float(), 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_float_scientific_notation(), string_constraint_generatort::add_axioms_from_int_hex(), goto_symext::address_arithmetic(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), object_descriptor_exprt::build(), build_object_descriptor_rec(), c_nondet_symbol_factory(), interval_sparse_arrayt::concretize(), 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(), string_constraint_generatort::fresh_string(), function_to_call(), generate_ansi_c_start_function(), get_array(), local_may_aliast::get_rec(), 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(), 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(), 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(), sum_over_map(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_other(), string_constantt::to_array_expr(), value_set_fit::to_expr(), value_set_fivrt::to_expr(), value_set_fivrnst::to_expr(), value_sett::to_expr(), c_typecheck_baset::typecheck_compound_body(), c_typecheck_baset::typecheck_expr_dereference(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), unpack_rec(), and cpp_typecheckt::zero_initializer().

◆ long_double_type()

◆ pointer_diff_type()

◆ pointer_type()

pointer_typet pointer_type ( const typet )

Definition at line 243 of file c_types.cpp.

References configt::ansi_c, config, and configt::ansi_ct::pointer_width.

Referenced by ci_lazy_methods_neededt::add_all_needed_classes(), string_abstractiont::add_argument(), shared_bufferst::add_initialization(), java_string_library_preprocesst::add_string_type(), cpp_typecheckt::add_this_to_method_type(), goto_symext::address_arithmetic(), c_typecheck_baset::adjust_function_parameter(), allocate_dynamic_object(), string_abstractiont::build_abstraction_type_rec(), bv_pointerst::bv_pointerst(), java_bytecode_instrumentt::check_class_cast(), smt2_convt::convert_address_of_rec(), java_bytecode_convert_methodt::convert_aload(), goto_program2codet::convert_assign_varargs(), java_bytecode_convert_methodt::convert_astore(), goto_convertt::convert_decl(), java_bytecode_convert_methodt::convert_getstatic(), cpp_typecheck_resolvet::convert_identifier(), java_bytecode_convert_methodt::convert_instructions(), select_pointer_typet::convert_pointer_type(), java_bytecode_convert_methodt::convert_ret(), goto_program2codet::convert_start_thread(), copy_parent(), cpp_typecheckt::cpp_destructor(), java_string_library_preprocesst::decl_string_expr(), cpp_typecheckt::default_assignop(), goto_symext::dereference_rec(), 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(), generate_ansi_c_start_function(), get_class_identifier_field(), java_string_library_preprocesst::get_object_at_index(), java_string_library_preprocesst::get_primitive_value_of_object(), get_type(), good_pointer_def(), c_typecastt::implicit_typecast_arithmetic(), goto_symext::initialize_auto_object(), ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(), initialize_nondet_string_struct(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), java_internal_additions(), jsil_internal_additions(), remove_java_newt::lower_java_new_array(), linker_script_merget::ls_data2instructions(), pointer_logict::object_rec(), shared_bufferst::operator()(), goto_checkt::pointer_validity_check(), linker_script_merget::pointerize_linker_defined_symbols(), cpp_convert_typet::read_function_type(), cpp_typecheckt::reference_binding(), remove_function_pointerst::remove_function_pointer(), Parser::rPrimaryExpr(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_typecast(), select_pointer_typet::specialize_generics(), goto_symext::symex_allocate(), thread_exit_instrumentation(), java_bytecode_instrumentt::throw_exception(), 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_expr_trinary(), 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_type()

◆ signed_char_type()

◆ signed_int_type()

◆ signed_long_int_type()

◆ signed_long_long_int_type()

◆ signed_short_int_type()

◆ signed_size_type()

◆ size_type()

unsignedbv_typet size_type ( )

Definition at line 58 of file c_types.cpp.

References configt::ansi_c, config, configt::ansi_ct::int_width, INVARIANT, 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(), banner_string(), simplify_exprt::bits2expr(), buffer_size(), resolution_prooft< clauset >::build_core(), build_sizeof_expr(), string_abstractiont::build_type(), clean_identifier(), goto_program2codet::cleanup_code_block(), irept::compare(), compiler_name(), aig_prop_solvert::convert_node(), compilet::convert_symbols(), detect_file_type(), cpp_typecheck_resolvet::do_builtin(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_strerror(), dott::escape(), simplify_exprt::expr2bits(), expr_initializert< nondet >::expr_initializer_rec(), aigt::get_terminals(), expr2ct::id_shorthand(), symex_slice_by_tracet::implied_guards(), string_instrumentationt::invalidate_buffer(), system_library_symbolst::is_symbol_internal_symbol(), linker_name(), list_calls_and_arguments(), lazy_goto_modelt::load_all_functions(), linker_script_merget::ls_data2instructions(), 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(), graphml_witnesst::remove_l0_l1(), constant_propagator_domaint::valuest::set_to_top(), simplify_exprt::simplify_typecast(), size_of_expr(), symex_slice_by_tracet::slice_by_trace(), split_string(), static_lifetime_init(), strip_string(), trace_value_binary(), c_typecheck_baset::typecheck_declaration(), 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(), and zero_string_length().

◆ unsigned_char_type()

◆ unsigned_int_type()

◆ unsigned_long_int_type()

◆ unsigned_long_long_int_type()

◆ unsigned_short_int_type()

◆ void_type()

◆ wchar_t_type()