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

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 ()
 
signedbv_typet signed_short_int_type ()
 
unsignedbv_typet unsigned_int_type ()
 
unsignedbv_typet unsigned_short_int_type ()
 
unsignedbv_typet size_type ()
 
signedbv_typet signed_size_type ()
 
signedbv_typet signed_long_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 ()
 
bitvector_typet gcc_float128_type ()
 
signedbv_typet pointer_diff_type ()
 
pointer_typet pointer_type (const typet &subtype)
 
reference_typet reference_type (const typet &subtype)
 
typet void_type ()
 
unsignedbv_typet gcc_unsigned_int128_type ()
 
signedbv_typet gcc_signed_int128_type ()
 
std::string c_type_as_string (const irep_idt &c_type)
 

Function Documentation

§ c_bool_type()

§ c_type_as_string()

std::string c_type_as_string ( const irep_idt c_type)

Definition at line 325 of file c_types.cpp.

Referenced by expr2ct::convert_rec().

§ char16_t_type()

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().

§ char32_t_type()

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().

§ char_type()

§ double_type()

§ enum_constant_type()

bitvector_typet enum_constant_type ( )

return type of enum constants

Definition at line 22 of file c_types.cpp.

References signed_int_type().

§ float_type()

§ gcc_float128_type()

§ gcc_signed_int128_type()

signedbv_typet gcc_signed_int128_type ( )

§ gcc_unsigned_int128_type()

unsignedbv_typet gcc_unsigned_int128_type ( )

§ index_type()

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(), 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().

§ long_double_type()

§ pointer_diff_type()

§ pointer_type()

pointer_typet pointer_type ( const typet subtype)

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(), 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(), is_empty(), java_internal_additions(), java_object_factoryt::java_object_factoryt(), jsil_internal_additions(), make_vtable_function(), 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_type()

reference_typet reference_type ( const typet subtype)

Definition at line 301 of file c_types.cpp.

Referenced by java_reference_type(), and cpp_typecheckt::typecheck_expr_address_of().

§ 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 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(), guardt::as_expr(), 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(), aigt::empty(), 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(), lispexprt::make_nil(), 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().

§ unsigned_char_type()

§ unsigned_int_type()

§ unsigned_long_int_type()

§ unsigned_long_long_int_type()

§ unsigned_short_int_type()

§ void_type()

§ wchar_t_type()