cprover
|
Base type of functions. More...
#include <std_types.h>
Classes | |
class | parametert |
Public Types | |
typedef std::vector< parametert > | parameterst |
typedef std::unordered_map< irep_idt, std::size_t > | parameter_indicest |
![]() | |
typedef std::vector< typet > | subtypest |
![]() | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_subt |
Public Member Functions | |
code_typet (parameterst &&_parameters, typet &&_return_type) | |
Constructs a new code type, i.e. More... | |
code_typet (parameterst &&_parameters, const typet &_return_type) | |
Constructs a new code type, i.e. More... | |
code_typet () | |
bool | has_ellipsis () const |
bool | has_this () const |
const parametert * | get_this () const |
bool | is_KnR () const |
void | make_ellipsis () |
void | remove_ellipsis () |
const typet & | return_type () const |
typet & | return_type () |
const parameterst & | parameters () const |
parameterst & | parameters () |
bool | get_inlined () const |
void | set_inlined (bool value) |
const irep_idt & | get_access () const |
void | set_access (const irep_idt &access) |
bool | get_is_constructor () const |
void | set_is_constructor () |
std::vector< irep_idt > | parameter_identifiers () const |
parameter_indicest | parameter_indices () const |
Get a map from parameter name to its index. More... | |
![]() | |
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 |
Base type of functions.
Definition at line 764 of file std_types.h.
typedef std::unordered_map<irep_idt, std::size_t> code_typet::parameter_indicest |
Definition at line 957 of file std_types.h.
typedef std::vector<parametert> code_typet::parameterst |
Definition at line 767 of file std_types.h.
|
inline |
Constructs a new code type, i.e.
function type
_parameters | the vector of function parameters |
_return_type | the return type |
Definition at line 773 of file std_types.h.
References parameters(), return_type(), and irept::swap().
|
inline |
Constructs a new code type, i.e.
function type
_parameters | the vector of function parameters |
_return_type | the return type |
Definition at line 782 of file std_types.h.
References parameters(), and return_type().
|
inline |
Definition at line 791 of file std_types.h.
References irept::add(), and typet::add_type().
|
inline |
Definition at line 925 of file std_types.h.
|
inline |
Definition at line 915 of file std_types.h.
References irept::get_bool().
Referenced by cpp_declarator_convertert::combine_types(), expr2ct::convert_code_decl(), and linkingt::duplicate_code_symbol().
|
inline |
Definition at line 935 of file std_types.h.
References irept::get_bool().
Referenced by java_bytecode_convert_methodt::convert(), and java_simple_method_stubst::create_method_stub().
|
inline |
|
inline |
Definition at line 861 of file std_types.h.
References irept::find(), and irept::get_bool().
Referenced by expr2ct::convert_rec(), expr2javat::convert_rec(), expr2cppt::convert_rec(), linkingt::duplicate_code_symbol(), remove_function_pointerst::is_type_compatible(), cpp_typecheck_fargst::match(), goto_symext::parameter_assignments(), remove_function_pointerst::remove_function_pointer(), cpp_typecheck_resolvet::show_identifiers(), type2name(), c_typecheck_baset::typecheck_expr_trinary(), c_typecheck_baset::typecheck_function_call_arguments(), and c_typecheck_baset::typecheck_redefinition_non_type().
|
inline |
Definition at line 866 of file std_types.h.
References get_this().
Referenced by java_bytecode_convert_methodt::convert(), expr2javat::convert_code_function_call(), java_object_factoryt::gen_nondet_struct_init(), is_java_main(), and ci_lazy_methodst::resolve_method_names().
|
inline |
Definition at line 880 of file std_types.h.
References irept::get_bool().
Referenced by c_typecheck_baset::typecheck_function_call_arguments().
|
inline |
Definition at line 885 of file std_types.h.
References irept::add(), and irept::set().
Referenced by remove_asmt::gcc_asm_function_call(), Parser::rTypeNameOrFunctionType(), c_typecheck_baset::typecheck_code_type(), and cpp_typecheckt::typecheck_expr_cpp_name().
|
inline |
Definition at line 946 of file std_types.h.
References parameters().
|
inline |
Get a map from parameter name to its index.
Definition at line 960 of file std_types.h.
References irept::id(), and parameters().
|
inline |
Definition at line 905 of file std_types.h.
References irept::find(), and irept::get_sub().
Referenced by string_abstractiont::abstract_function_call(), c_typecheck_baset::add_argc_argv(), string_abstractiont::add_str_arguments(), cpp_typecheckt::add_this_to_method_type(), c_typecheck_baset::apply_asm_label(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), assign_parameter_names(), base_type_eqt::base_type_eq_rec(), localst::build(), local_may_aliast::build(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), dump_ct::cleanup_type(), code_typet(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_function(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_invoke_dynamic(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), cpp_typecheckt::convert_parameters(), expr2ct::convert_rec(), expr2cppt::convert_rec(), expr2javat::convert_rec(), cpp_type2name(), compilet::cprover_macro_arities(), java_simple_method_stubst::create_method_stub(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_cpp_new(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::do_function_call(), value_sett::do_function_call(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), interpretert::execute_function_call(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_symbols(), smt2_convt::find_symbols_rec(), remove_function_pointerst::fix_argument_types(), cpp_typecheckt::function_identifier(), function_to_call(), c_typecheck_baset::gcc_types_compatible_p(), generate_ansi_c_start_function(), languaget::generate_opaque_parameter_symbols(), java_bytecode_parsert::get_class_refs_rec(), get_dependencies_from_generic_parameters_rec(), get_destructor(), get_local_identifiers(), get_symbols_rec(), get_this(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), escape_analysist::insert_cleanup(), taint_analysist::instrument(), is_java_main(), remove_function_pointerst::is_type_compatible(), java_build_arguments(), java_bytecode_convert_method_lazy(), java_bytecode_initialize_parameter_names(), java_method_parameter_slots(), java_record_outputs(), jsil_internal_additions(), java_string_library_preprocesst::make_assign_and_return_function_from_call(), java_string_library_preprocesst::make_copy_constructor_code(), java_string_library_preprocesst::make_copy_string_code(), java_string_library_preprocesst::make_equals_function_code(), java_string_library_preprocesst::make_float_to_string_code(), java_string_library_preprocesst::make_function_from_call(), java_string_library_preprocesst::make_init_from_array_code(), java_string_library_preprocesst::make_init_function_from_call(), java_string_library_preprocesst::make_object_get_class_code(), java_string_library_preprocesst::make_string_format_code(), java_string_library_preprocesst::make_string_length_code(), java_string_library_preprocesst::make_string_returning_function_from_call(), cpp_typecheck_fargst::match(), member_type_lazy(), mm_io(), model_argc_argv(), mutex_init_instrumentation(), dump_ct::operator()(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), goto_inlinet::parameter_destruction(), parameter_identifiers(), parameter_indices(), pretty_signature(), cpp_typecheckt::reference_binding(), remove_function_pointerst::remove_function_pointer(), rename_symbolt::rename(), replace_symbolt::replace(), require_type::require_code(), require_type::require_parameter(), Parser::rTypeNameOrFunctionType(), goto_program2codet::scan_for_varargs(), cpp_typecheck_resolvet::show_identifiers(), cpp_typecheckt::standard_conversion_pointer_to_member(), static_lifetime_init(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), rd_range_domaint::transform_end_function(), type2name(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_trinary(), c_typecheck_baset::typecheck_function_body(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_new_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_function_call(), java_bytecode_typecheckt::typecheck_type(), jsil_typecheckt::typecheck_type(), cpp_typecheckt::typecheck_type(), and yyjsilparse().
|
inline |
Definition at line 910 of file std_types.h.
References irept::add(), and irept::get_sub().
|
inline |
Definition at line 890 of file std_types.h.
References irept::add(), and irept::remove().
Referenced by goto_convertt::do_function_call_symbol(), and remove_function_pointerst::remove_function_pointer().
|
inline |
Definition at line 895 of file std_types.h.
References typet::find_type().
Referenced by code_contractst::apply_contract(), base_type_eqt::base_type_eq_rec(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_type(), code_typet(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), cpp_declarator_convertert::convert(), java_bytecode_convert_methodt::convert(), cpp_typecheckt::convert_function(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_invoke_dynamic(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), expr2ct::convert_rec(), expr2javat::convert_rec(), expr2cppt::convert_rec(), java_bytecode_languaget::convert_single_method(), cpp_typecheckt::cpp_is_pod(), cpp_type2name(), java_simple_method_stubst::create_method_stub(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_cpp_new(), linkingt::duplicate_code_symbol(), find_symbols(), remove_function_pointerst::fix_return_type(), function_to_call(), c_typecheck_baset::gcc_types_compatible_p(), generate_ansi_c_start_function(), generate_java_start_function(), java_bytecode_parsert::get_class_refs_rec(), get_dependencies_from_generic_parameters_rec(), get_destructor(), remove_returnst::get_or_create_return_value_symbol(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), is_java_main(), remove_function_pointerst::is_type_compatible(), java_record_outputs(), cpp_declarator_convertert::main_function_rules(), java_string_library_preprocesst::make_copy_string_code(), java_string_library_preprocesst::make_equals_function_code(), java_string_library_preprocesst::make_float_to_string_code(), java_string_library_preprocesst::make_function_from_call(), java_string_library_preprocesst::make_string_format_code(), java_string_library_preprocesst::make_string_returning_function_from_call(), mm_io(), original_return_type(), record_function_outputs(), cpp_typecheckt::reference_binding(), remove_internal_symbols(), rename_symbolt::rename(), replace_symbolt::replace(), Parser::rTypeNameOrFunctionType(), cpp_typecheck_resolvet::show_identifiers(), static_lifetime_init(), type2name(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_declaration(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), c_typecheck_baset::typecheck_expr_trinary(), c_typecheck_baset::typecheck_function_body(), c_typecheck_baset::typecheck_side_effect_function_call(), java_bytecode_typecheckt::typecheck_type(), cpp_typecheckt::typecheck_type(), remove_returnst::undo_function_calls(), and ansi_c_convert_typet::write().
|
inline |
Definition at line 900 of file std_types.h.
References typet::add_type().
|
inline |
Definition at line 930 of file std_types.h.
Referenced by java_bytecode_convert_method_lazy().
|
inline |
Definition at line 920 of file std_types.h.
Referenced by cpp_declarator_convertert::combine_types().
|
inline |
Definition at line 940 of file std_types.h.
Referenced by java_bytecode_convert_methodt::convert_invoke(), and java_bytecode_convert_method_lazy().