cprover
|
#include <c_typecheck_base.h>
Public Member Functions | |
c_typecheck_baset (symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler) | |
c_typecheck_baset (symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler) | |
virtual | ~c_typecheck_baset () |
virtual void | typecheck ()=0 |
virtual void | typecheck_expr (exprt &expr) |
![]() | |
typecheckt (message_handlert &_message_handler) | |
virtual | ~typecheckt () |
void | err_location (const source_locationt &loc) |
void | err_location (const exprt &src) |
void | err_location (const typet &src) |
virtual bool | typecheck_main () |
![]() | |
namespacet (const symbol_tablet &_symbol_table) | |
namespacet (const symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2) | |
namespacet (const symbol_tablet *_symbol_table1, const symbol_tablet *_symbol_table2) | |
bool | lookup (const irep_idt &name, const symbolt *&symbol) const override |
See namespace_baset::lookup(). More... | |
std::size_t | smallest_unused_suffix (const std::string &prefix) const override |
See documentation for namespace_baset::smallest_unused_suffix(). More... | |
const symbol_tablet & | get_symbol_table () const |
const symbolt & | lookup (const irep_idt &name) const |
const symbolt & | lookup (const symbol_exprt &) const |
const symbolt & | lookup (const symbol_typet &) const |
const symbolt & | lookup (const tag_typet &) const |
virtual bool | lookup (const irep_idt &name, const symbolt *&symbol) const=0 |
Searches for a symbol named name . More... | |
![]() | |
const symbolt & | lookup (const irep_idt &name) const |
const symbolt & | lookup (const symbol_exprt &) const |
const symbolt & | lookup (const symbol_typet &) const |
const symbolt & | lookup (const tag_typet &) const |
virtual | ~namespace_baset () |
void | follow_macros (exprt &) const |
const typet & | follow (const typet &) const |
const typet & | follow_tag (const union_tag_typet &) const |
const typet & | follow_tag (const struct_tag_typet &) const |
const typet & | follow_tag (const c_enum_tag_typet &) const |
Protected Types | |
typedef std::unordered_map< irep_idt, typet > | id_type_mapt |
typedef std::unordered_map< irep_idt, irep_idt > | asm_label_mapt |
Static Protected Member Functions | |
static void | add_rounding_mode (exprt &) |
static bool | is_numeric_type (const typet &src) |
Protected Attributes | |
symbol_tablet & | symbol_table |
const irep_idt | module |
const irep_idt | mode |
symbolt | current_symbol |
id_type_mapt | parameter_map |
bool | break_is_allowed |
bool | continue_is_allowed |
bool | case_is_allowed |
typet | switch_op_type |
typet | return_type |
std::map< irep_idt, source_locationt > | labels_defined |
std::map< irep_idt, source_locationt > | labels_used |
std::list< codet > | clean_code |
asm_label_mapt | asm_label_map |
![]() | |
const symbol_tablet * | symbol_table1 |
const symbol_tablet * | symbol_table2 |
Additional Inherited Members |
Definition at line 25 of file c_typecheck_base.h.
|
protected |
Definition at line 273 of file c_typecheck_base.h.
|
protected |
Definition at line 72 of file c_typecheck_base.h.
|
inline |
Definition at line 30 of file c_typecheck_base.h.
|
inline |
Definition at line 45 of file c_typecheck_base.h.
|
inlinevirtual |
Definition at line 61 of file c_typecheck_base.h.
|
protected |
Definition at line 16 of file c_typecheck_argc_argv.cpp.
References irept::add(), symbolt::base_name, messaget::eom(), messaget::error(), from_integer(), irept::id(), symbolt::is_lvalue, symbolt::is_static_lifetime, symbolt::location, move_symbol(), symbolt::name, code_typet::parameters(), messaget::mstreamt::source_location, typet::subtype(), irept::swap(), symbolt::symbol_expr(), to_code_type(), to_string(), symbolt::type, and exprt::type().
Referenced by typecheck_function_body(), and cpp_typecheckt::typecheck_method_bodies().
|
staticprotected |
Definition at line 53 of file c_typecheck_expr.cpp.
References from_integer(), irept::id(), exprt::op2(), exprt::operands(), exprt::type(), UNREACHABLE, and unsigned_int_type().
Referenced by typecheck_array_type(), and typecheck_c_enum_type().
|
protectedvirtual |
Definition at line 1279 of file c_typecheck_expr.cpp.
References namespace_baset::follow(), irept::id(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_rel().
|
protectedvirtual |
Definition at line 1482 of file c_typecheck_type.cpp.
References typet::add_source_location(), irept::id(), pointer_type(), signed_int_type(), typet::source_location(), and typet::subtype().
Referenced by typecheck_code_type(), and typecheck_new_symbol().
Definition at line 575 of file c_typecheck_base.cpp.
References asm_label_map, symbolt::base_name, dstringt::empty(), messaget::eom(), messaget::error(), irept::id(), id2string(), symbolt::is_macro, irept::is_not_nil(), symbolt::is_static_lifetime, symbolt::is_type, symbolt::location, symbolt::name, code_typet::parameters(), messaget::mstreamt::source_location, to_code_type(), symbolt::type, and symbolt::value.
Referenced by typecheck_declaration().
|
protected |
Definition at line 254 of file c_typecheck_initializer.cpp.
References struct_union_typet::components(), designatort::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), designatort::entryt::index, integer2size_t(), irept::is_nil(), irept::make_nil(), designatort::push_entry(), designatort::entryt::size, array_typet::size(), vector_typet::size(), designatort::entryt::subtype, typet::subtype(), to_array_type(), to_integer(), to_string(), to_struct_type(), to_union_type(), to_vector_type(), UNREACHABLE, and designatort::entryt::vla_permitted.
Referenced by do_designated_initializer(), and do_initializer_list().
|
protectedvirtual |
pre:initialized | result, designator |
Definition at line 353 of file c_typecheck_initializer.cpp.
References exprt::add_source_location(), designatort::back(), struct_union_typet::components(), exprt::copy_to_operands(), DATA_INVARIANT, designator_enter(), do_initializer_rec(), designatort::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), irept::find(), exprt::find_source_location(), namespace_baset::follow(), irept::get(), messaget::get_message_handler(), struct_union_typet::componentt::get_name(), irept::id(), integer2size_t(), irept::is_nil(), exprt::is_zero(), make_designator(), unary_exprt::op(), exprt::op0(), exprt::operands(), messaget::result(), union_exprt::set_component_name(), designatort::size(), array_typet::size(), exprt::source_location(), messaget::mstreamt::source_location, designatort::entryt::subtype, typet::subtype(), to_array_type(), to_string(), to_struct_type(), to_union_type(), exprt::type(), UNREACHABLE, designatort::entryt::vla_permitted, messaget::warning(), and zero_initializer().
Referenced by do_initializer_list().
|
protectedvirtual |
Definition at line 26 of file c_typecheck_initializer.cpp.
References DATA_INVARIANT, do_initializer_rec(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), irept::is_not_nil(), messaget::result(), array_typet::size(), to_array_type(), and to_string().
Referenced by cpp_typecheckt::convert_initializer(), do_initializer(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_expr_explicit_typecast(), typecheck_expr_typecast(), typecheck_new_symbol(), and typecheck_redefinition_non_type().
|
protectedvirtual |
Definition at line 211 of file c_typecheck_initializer.cpp.
References CPROVER_PREFIX, do_initializer(), namespace_baset::follow(), has_prefix(), irept::id(), id2string(), symbolt::is_macro, irept::is_nil(), irept::is_not_nil(), symbolt::is_static_lifetime, symbolt::is_type, make_constant(), symbolt::name, array_typet::size(), exprt::source_location(), to_array_type(), symbolt::type, exprt::type(), typecheck_expr(), and symbolt::value.
|
protectedvirtual |
Definition at line 824 of file c_typecheck_initializer.cpp.
References char_type(), struct_union_typet::components(), designator_enter(), do_designated_initializer(), do_initializer_rec(), messaget::eom(), typecheckt::err_location(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), from_integer(), irept::get(), messaget::get_message_handler(), irept::id(), increment_designator(), index_type(), irept::is_nil(), exprt::op0(), exprt::operands(), messaget::result(), array_typet::size(), exprt::source_location(), messaget::mstreamt::source_location, to_array_type(), to_string(), to_struct_type(), messaget::warning(), and zero_initializer().
Referenced by do_initializer_rec().
|
protectedvirtual |
initialize something of type ‘type’ with given value ‘value’
Definition at line 54 of file c_typecheck_initializer.cpp.
References char_type(), do_initializer_list(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), Forall_operands, irept::get(), irept::get_bool(), messaget::get_message_handler(), irept::id(), implicit_typecast(), integer2size_t(), array_typet::is_complete(), irept::is_nil(), exprt::operands(), messaget::result(), array_typet::size(), exprt::source_location(), typet::subtype(), string_constantt::to_array_expr(), to_array_type(), to_integer(), to_string(), to_string_constant(), exprt::type(), and zero_initializer().
Referenced by do_designated_initializer(), do_initializer(), and do_initializer_list().
|
protectedvirtual |
Definition at line 2100 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), configt::ansi_c, side_effect_expr_function_callt::arguments(), base_type_eq(), configt::ansi_ct::CLANG, typecast_exprt::conditional_cast(), config, CPROVER_PREFIX, ieee_float_spect::double_precision(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), from_integer(), side_effect_expr_function_callt::function(), symbol_exprt::get_identifier(), irept::id(), invalid_pointer(), exprt::is_constant(), binary_relation_exprt::lhs(), long_double_type(), make_constant(), exprt::op0(), exprt::operands(), ieee_floatt::plus_infinity(), pointer_object(), pointer_offset(), configt::ansi_ct::preprocessor, binary_relation_exprt::rhs(), same_object(), irept::set(), simplify(), ieee_float_spect::single_precision(), size_type(), exprt::source_location(), typet::subtype(), to_c_bit_field_type(), ieee_floatt::to_expr(), to_floatbv_type(), to_integer(), to_string(), to_symbol_expr(), exprt::type(), typecheck_function_call_arguments(), and ieee_floatt::zero().
Referenced by typecheck_side_effect_function_call(), and cpp_typecheckt::typecheck_side_effect_function_call().
|
protected |
Definition at line 979 of file c_typecheck_type.cpp.
References configt::ansi_c, config, configt::ansi_ct::int_width, configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, max_value(), configt::ansi_ct::mode, signed_int_type(), signed_long_int_type(), signed_long_long_int_type(), unsigned_int_type(), unsigned_long_int_type(), unsigned_long_long_int_type(), and configt::ansi_ct::VISUAL_STUDIO.
Referenced by typecheck_c_enum_type().
|
protected |
Definition at line 1011 of file c_typecheck_type.cpp.
References configt::ansi_c, configt::ansi_ct::char_width, config, configt::ansi_ct::int_width, configt::ansi_ct::long_int_width, max_value(), configt::ansi_ct::mode, configt::ansi_ct::short_int_width, signed_char_type(), signed_int_type(), signed_long_int_type(), signed_long_long_int_type(), signed_short_int_type(), unsigned_char_type(), unsigned_int_type(), unsigned_long_int_type(), unsigned_long_long_int_type(), unsigned_short_int_type(), and configt::ansi_ct::VISUAL_STUDIO.
Referenced by typecheck_c_enum_type().
|
protectedvirtual |
Definition at line 87 of file c_typecheck_expr.cpp.
References namespace_baset::follow(), namespace_baset::follow_tag(), irept::get(), irept::id(), code_typet::parameters(), code_typet::return_type(), typet::subtype(), to_c_enum_tag_type(), and to_code_type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 2932 of file c_typecheck_expr.cpp.
References irept::id(), vector_typet::size(), typet::subtype(), to_bitvector_type(), and to_integer().
Referenced by typecheck_expr_binary_arithmetic(), and typecheck_side_effect_assignment().
Reimplemented in cpp_typecheckt.
Definition at line 13 of file c_typecheck_typecast.cpp.
References messaget::eom(), messaget::error(), c_typecastt::errors, exprt::find_source_location(), c_typecastt::implicit_typecast(), messaget::mstreamt::source_location, to_string(), exprt::type(), messaget::warning(), and c_typecastt::warnings.
Referenced by do_initializer_rec(), implicit_typecast_bool(), make_index_type(), typecheck_assign(), typecheck_expr_builtin_va_arg(), typecheck_expr_trinary(), typecheck_function_call_arguments(), typecheck_gcc_switch_case_range(), typecheck_return(), typecheck_side_effect_assignment(), typecheck_side_effect_statement_expression(), and typecheck_switch_case().
|
protectedvirtual |
Definition at line 61 of file c_typecheck_typecast.cpp.
References c_typecastt::implicit_typecast_arithmetic().
Referenced by typecheck_expr_binary_arithmetic(), typecheck_expr_rel(), typecheck_expr_shifts(), typecheck_expr_trinary(), typecheck_expr_unary_arithmetic(), typecheck_side_effect_assignment(), and typecheck_switch().
|
protectedvirtual |
Definition at line 53 of file c_typecheck_typecast.cpp.
References c_typecastt::implicit_typecast_arithmetic().
|
inlineprotectedvirtual |
Definition at line 117 of file c_typecheck_base.h.
References implicit_typecast().
Referenced by typecheck_dowhile(), typecheck_expr_binary_boolean(), typecheck_expr_trinary(), typecheck_expr_unary_boolean(), typecheck_for(), typecheck_ifthenelse(), typecheck_spec_expr(), and typecheck_while().
|
protected |
Definition at line 630 of file c_typecheck_initializer.cpp.
References struct_union_typet::components(), designatort::empty(), namespace_baset::follow(), irept::id(), designatort::entryt::index, irept::is_nil(), designatort::pop_entry(), designatort::entryt::size, designatort::size(), array_typet::size(), designatort::entryt::subtype, to_array_type(), to_struct_type(), and designatort::entryt::type.
Referenced by do_initializer_list().
|
protectedvirtual |
Definition at line 363 of file c_typecheck_code.cpp.
References struct_union_typet::components(), namespace_baset::follow(), irept::id(), irept::is_nil(), array_typet::size(), typet::subtype(), to_array_type(), and to_struct_union_type().
Referenced by typecheck_compound_body(), typecheck_decl(), and typecheck_expr_operands().
|
inlinestaticprotected |
Definition at line 258 of file c_typecheck_base.h.
References irept::id().
Referenced by typecheck_expr_side_effect(), and typecheck_expr_typecast().
|
inlineprotected |
Definition at line 229 of file c_typecheck_base.h.
References messaget::result().
Referenced by cpp_typecheckt::convert_non_template_declaration(), typecheck_compound_body(), cpp_typecheckt::typecheck_decl(), and typecheck_declaration().
|
protectedvirtual |
Definition at line 3452 of file c_typecheck_expr.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), irept::id(), exprt::is_constant(), make_constant_rec(), simplify(), messaget::mstreamt::source_location, and to_string().
Referenced by cpp_typecheckt::convert(), do_initializer(), do_special_functions(), make_constant_index(), cpp_typecheckt::template_suffix(), typecheck_compound_body(), cpp_typecheckt::typecheck_enum_body(), and typecheck_type().
|
protectedvirtual |
Definition at line 3467 of file c_typecheck_expr.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), irept::id(), exprt::is_constant(), make_constant(), make_index_type(), simplify(), and messaget::mstreamt::source_location.
Referenced by cpp_typecheckt::check_fixed_size_array(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), make_designator(), typecheck_c_bit_field_type(), typecheck_custom_type(), and typecheck_vector_type().
|
protectedvirtual |
Definition at line 3482 of file c_typecheck_expr.cpp.
Referenced by make_constant().
|
protected |
Definition at line 678 of file c_typecheck_initializer.cpp.
References struct_union_typet::component_number(), struct_union_typet::components(), designatort::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), forall_operands, irept::get(), struct_union_typet::has_component(), has_component_rec(), irept::id(), designatort::entryt::index, integer2size_t(), make_constant_index(), exprt::op0(), exprt::operands(), designatort::push_entry(), designatort::entryt::size, designatort::entryt::subtype, typet::subtype(), to_array_type(), to_integer(), to_string(), to_struct_union_type(), and designatort::entryt::type.
Referenced by do_designated_initializer().
|
protectedvirtual |
Definition at line 1211 of file c_typecheck_expr.cpp.
References implicit_typecast(), and index_type().
Referenced by make_constant_index(), typecheck_array_type(), typecheck_expr_index(), and typecheck_expr_pointer_arithmetic().
Definition at line 33 of file c_typecheck_base.cpp.
References messaget::eom(), messaget::error(), symbolt::location, symbolt::mode, mode, symbolt::module, module, symbol_tablet::move(), symbolt::name, messaget::mstreamt::source_location, and symbol_table.
Referenced by add_argc_argv(), move_symbol(), typecheck_c_enum_tag_type(), typecheck_c_enum_type(), typecheck_compound_type(), typecheck_function_body(), typecheck_side_effect_function_call(), and typecheck_symbol().
|
inlineprotected |
Definition at line 244 of file c_typecheck_base.h.
References move_symbol().
|
protectedvirtual |
Definition at line 19 of file c_typecheck_code.cpp.
References break_is_allowed, case_is_allowed, and continue_is_allowed.
Referenced by cpp_typecheckt::convert_function(), and ansi_c_typecheckt::typecheck().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 23 of file c_typecheck_base.cpp.
References expr2c().
Referenced by add_argc_argv(), designator_enter(), do_designated_initializer(), do_initializer(), do_initializer_list(), do_initializer_rec(), do_special_functions(), implicit_typecast(), make_constant(), make_designator(), typecheck_c_bit_field_type(), typecheck_expr_address_of(), typecheck_expr_binary_arithmetic(), typecheck_expr_builtin_offsetof(), typecheck_expr_dereference(), typecheck_expr_index(), typecheck_expr_main(), typecheck_expr_member(), typecheck_expr_pointer_arithmetic(), typecheck_expr_ptrmember(), typecheck_expr_rel(), typecheck_expr_rel_vector(), typecheck_expr_shifts(), typecheck_expr_side_effect(), typecheck_expr_sizeof(), typecheck_expr_trinary(), typecheck_expr_typecast(), typecheck_expr_unary_arithmetic(), typecheck_redefinition_non_type(), typecheck_redefinition_type(), typecheck_return(), typecheck_side_effect_assignment(), typecheck_side_effect_function_call(), typecheck_type(), and typecheck_vector_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 28 of file c_typecheck_base.cpp.
References type2c().
|
pure virtual |
Implements typecheckt.
Implemented in cpp_typecheckt, and ansi_c_typecheckt.
|
protectedvirtual |
Definition at line 3129 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), typet::subtype(), and exprt::type().
Referenced by typecheck_expr_index(), typecheck_expr_pointer_arithmetic(), and typecheck_expr_side_effect().
|
protectedvirtual |
Definition at line 480 of file c_typecheck_type.cpp.
References symbol_table_baset::add(), add_rounding_mode(), exprt::add_source_location(), symbolt::base_name, clean_code, current_symbol, dstringt::empty(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), irept::get_bool(), irept::id(), id2string(), exprt::is_constant(), irept::is_not_nil(), symbolt::is_static_lifetime, code_assignt::lhs(), symbolt::location, make_index_type(), symbolt::mode, mode, symbolt::name, PRECONDITION, irept::pretty(), symbolt::pretty_name, code_assignt::rhs(), irept::set(), symbol_exprt::set_identifier(), simplify(), array_typet::size(), typet::source_location(), messaget::mstreamt::source_location, typet::subtype(), symbol_table, symbol_table_baset::symbols, to_integer(), to_string(), symbolt::type, exprt::type(), typecheck_expr(), typecheck_type(), and symbolt::value.
Referenced by typecheck_type().
|
protectedvirtual |
Definition at line 135 of file c_typecheck_code.cpp.
References Forall_operands, code_asmt::get_flavor(), exprt::op0(), exprt::operands(), to_code_asm(), and typecheck_expr().
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 168 of file c_typecheck_code.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), implicit_typecast(), exprt::op0(), exprt::op1(), exprt::operands(), exprt::type(), and typecheck_expr().
Referenced by typecheck_code().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 184 of file c_typecheck_code.cpp.
References Forall_operands, codet::get_statement(), exprt::move_to_operands(), exprt::operands(), to_code(), and typecheck_code().
Referenced by cpp_typecheckt::typecheck_block(), and typecheck_code().
|
protectedvirtual |
Definition at line 223 of file c_typecheck_code.cpp.
References break_is_allowed, messaget::eom(), typecheckt::err_location(), and messaget::error().
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 1311 of file c_typecheck_type.cpp.
References irept::add(), messaget::eom(), messaget::error(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::get_int(), bitvector_typet::get_width(), irept::id(), integer2size_t(), make_constant_index(), irept::remove(), bitvector_typet::set_width(), typet::source_location(), messaget::mstreamt::source_location, typet::subtype(), to_bitvector_type(), to_c_enum_tag_type(), to_integer(), to_string(), typecheck_expr(), and typecheck_type().
Referenced by typecheck_type(), and cpp_typecheckt::typecheck_type().
|
protectedvirtual |
Definition at line 1252 of file c_typecheck_type.cpp.
References irept::add(), symbolt::base_name, messaget::eom(), messaget::error(), irept::find(), irept::get(), irept::id(), symbolt::is_file_local, irept::is_nil(), symbolt::is_type, symbolt::location, move_symbol(), symbolt::name, irept::remove(), tag_typet::set_identifier(), signed_int_type(), typet::source_location(), messaget::mstreamt::source_location, typet::subtype(), symbol_table, symbol_table_baset::symbols, and symbolt::type.
Referenced by typecheck_type().
|
protectedvirtual |
Definition at line 1069 of file c_typecheck_type.cpp.
References irept::add(), add_rounding_mode(), symbolt::base_name, ansi_c_declarationt::declarator(), dstringt::empty(), enum_constant_type(), enum_underlying_type(), messaget::eom(), messaget::error(), irept::find(), from_integer(), irept::get(), ansi_c_declaratort::get_base_name(), irept::get_bool(), ansi_c_declaratort::get_name(), irept::get_sub(), symbol_table_baset::get_writeable_ref(), irept::id(), id2string(), integer2string(), exprt::is_false(), symbolt::is_file_local, irept::is_nil(), irept::is_not_nil(), exprt::is_true(), symbolt::is_type, symbolt::location, max_value(), move_symbol(), symbolt::name, exprt::operands(), irept::remove(), irept::set(), c_enum_typet::c_enum_membert::set_base_name(), c_enum_typet::c_enum_membert::set_identifier(), c_enum_typet::c_enum_membert::set_value(), simplify(), typet::source_location(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), symbol_table, symbol_table_baset::symbols, to_ansi_c_declaration(), to_integer(), symbolt::type, exprt::type(), typecheck_declaration(), typecheck_expr(), and ansi_c_declaratort::value().
Referenced by typecheck_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 24 of file c_typecheck_code.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), codet::get_statement(), irept::id(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::pretty(), to_code(), to_code_dowhile(), to_code_goto(), to_code_ifthenelse(), to_code_label(), to_code_switch(), to_code_switch_case(), to_code_while(), exprt::type(), typecheck_asm(), typecheck_assign(), typecheck_block(), typecheck_break(), typecheck_continue(), typecheck_decl(), typecheck_dowhile(), typecheck_expr(), typecheck_expression(), typecheck_for(), typecheck_gcc_computed_goto(), typecheck_gcc_local_label(), typecheck_gcc_switch_case_range(), typecheck_goto(), typecheck_ifthenelse(), typecheck_label(), typecheck_return(), typecheck_start_thread(), typecheck_switch(), typecheck_switch_case(), and typecheck_while().
Referenced by typecheck_block(), cpp_typecheckt::typecheck_code(), typecheck_decl(), typecheck_dowhile(), typecheck_expr_operands(), typecheck_for(), typecheck_function_body(), typecheck_gcc_switch_case_range(), typecheck_ifthenelse(), typecheck_label(), typecheck_side_effect_function_call(), typecheck_start_thread(), typecheck_switch(), typecheck_switch_case(), and typecheck_while().
|
protectedvirtual |
Definition at line 381 of file c_typecheck_type.cpp.
References exprt::add_source_location(), adjust_function_parameter(), clean_code, ansi_c_declarationt::declarator(), dstringt::empty(), messaget::eom(), messaget::error(), namespace_baset::follow(), ansi_c_declarationt::full_type(), ansi_c_declaratort::get_base_name(), ansi_c_declaratort::get_name(), irept::id(), code_typet::make_ellipsis(), parameter_map, code_typet::parameters(), typet::remove_subtype(), return_type, code_typet::return_type(), code_typet::parametert::set_base_name(), typet::source_location(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), irept::swap(), to_ansi_c_declaration(), exprt::type(), and typecheck_type().
Referenced by typecheck_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 803 of file c_typecheck_type.cpp.
References add_padding(), exprt::add_source_location(), struct_union_typet::components(), messaget::eom(), messaget::error(), from_integer(), irept::id(), index_type(), is_complete_type(), array_typet::is_incomplete(), make_already_typechecked(), make_constant(), exprt::op0(), exprt::operands(), irept::set(), typet::source_location(), messaget::mstreamt::source_location, to_ansi_c_declaration(), to_array_type(), to_c_bit_field_type(), to_string(), to_struct_type(), to_union_type(), exprt::type(), typecheck_expr(), and typecheck_type().
Referenced by typecheck_compound_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 692 of file c_typecheck_type.cpp.
References typet::add_source_location(), symbolt::base_name, messaget::eom(), messaget::error(), irept::find(), irept::get(), symbol_table_baset::get_writeable_ref(), irept::id(), id2string(), irept::is_nil(), irept::is_not_nil(), symbolt::is_type, symbolt::location, move_symbol(), symbolt::name, symbolt::pretty_name, irept::remove(), irept::set(), typet::source_location(), messaget::mstreamt::source_location, irept::swap(), symbol_table, symbol_table_baset::symbols, to_struct_union_type(), symbolt::type, type2name(), typecheck_compound_body(), UNREACHABLE, and c_qualifierst::write().
Referenced by typecheck_type().
|
protectedvirtual |
Definition at line 233 of file c_typecheck_code.cpp.
References continue_is_allowed, messaget::eom(), typecheckt::err_location(), and messaget::error().
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 281 of file c_typecheck_type.cpp.
References messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), irept::id(), integer2string(), make_constant_index(), irept::remove(), irept::set(), exprt::source_location(), messaget::mstreamt::source_location, to_integer(), typecheck_expr(), and UNREACHABLE.
Referenced by typecheck_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 243 of file c_typecheck_code.cpp.
References exprt::add_source_location(), clean_code, ansi_c_declarationt::declarators(), messaget::eom(), typecheckt::err_location(), messaget::error(), ansi_c_declarationt::get_is_static_assert(), irept::id(), is_complete_type(), symbolt::is_extern, irept::is_not_nil(), symbolt::is_static_lifetime, symbolt::is_type, symbolt::location, exprt::op0(), exprt::op1(), exprt::operands(), codet::set_statement(), exprt::source_location(), messaget::mstreamt::source_location, irept::swap(), code_declt::symbol(), symbolt::symbol_expr(), symbol_table, symbol_table_baset::symbols, symbolt::type, typecheck_code(), typecheck_declaration(), and symbolt::value.
Referenced by typecheck_code().
|
protected |
Definition at line 643 of file c_typecheck_base.cpp.
References irept::add(), apply_asm_label(), asm_label_map, current_symbol, ansi_c_declarationt::declarators(), messaget::eom(), messaget::error(), irept::find(), ansi_c_declarationt::full_type(), ansi_c_declarationt::get_is_static_assert(), symbol_tablet::get_writeable(), irept::id(), id2string(), symbolt::is_macro, irept::is_not_nil(), symbolt::location, make_already_typechecked(), symbolt::name, exprt::op0(), exprt::op1(), exprt::operands(), parameter_map, code_typet::return_type(), ansi_c_declarationt::set_is_always_inline(), ansi_c_declarationt::set_is_extern(), ansi_c_declarationt::set_is_inline(), ansi_c_declarationt::set_is_register(), ansi_c_declarationt::set_is_static(), ansi_c_declarationt::set_is_thread_local(), ansi_c_declarationt::set_is_typedef(), ansi_c_declarationt::set_is_used(), ansi_c_declarationt::set_is_weak(), size_type(), messaget::mstreamt::source_location, irept::swap(), symbol_table, to_code_type(), ansi_c_declarationt::to_symbol(), symbolt::type, exprt::type(), typecheck_expr(), typecheck_spec_expr(), typecheck_symbol(), typecheck_type(), and symbolt::value.
Referenced by ansi_c_typecheckt::typecheck(), typecheck_c_enum_type(), typecheck_decl(), and typecheck_expr_operands().
|
protectedvirtual |
Definition at line 775 of file c_typecheck_code.cpp.
References exprt::add_source_location(), code_dowhilet::body(), break_is_allowed, code_dowhilet::cond(), continue_is_allowed, messaget::eom(), typecheckt::err_location(), messaget::error(), codet::get_statement(), implicit_typecast_bool(), exprt::move_to_operands(), exprt::operands(), exprt::source_location(), irept::swap(), typecheck_code(), typecheck_expr(), and typecheck_spec_expr().
Referenced by typecheck_code().
|
virtual |
Reimplemented in cpp_typecheckt.
Definition at line 35 of file c_typecheck_expr.cpp.
References irept::id(), exprt::op0(), exprt::operands(), irept::swap(), typecheck_expr_main(), and typecheck_expr_operands().
Referenced by do_initializer(), typecheck_array_type(), typecheck_asm(), typecheck_assign(), typecheck_c_bit_field_type(), typecheck_c_enum_type(), typecheck_code(), typecheck_compound_body(), typecheck_custom_type(), typecheck_declaration(), typecheck_dowhile(), cpp_typecheckt::typecheck_expr(), typecheck_expr_builtin_offsetof(), typecheck_expr_main(), typecheck_expr_operands(), typecheck_expr_symbol(), typecheck_expression(), typecheck_for(), typecheck_gcc_computed_goto(), typecheck_gcc_switch_case_range(), typecheck_ifthenelse(), typecheck_return(), typecheck_side_effect_function_call(), typecheck_spec_expr(), typecheck_switch(), typecheck_switch_case(), typecheck_type(), typecheck_typeof_type(), typecheck_vector_type(), and typecheck_while().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1684 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::get(), irept::get_bool(), irept::id(), labels_used, exprt::op0(), exprt::operands(), pointer_type(), irept::set(), exprt::source_location(), irept::swap(), to_string(), exprt::type(), and void_type().
Referenced by cpp_typecheckt::typecheck_expr_address_of(), and typecheck_expr_main().
|
protectedvirtual |
Definition at line 990 of file c_typecheck_expr.cpp.
References irept::add(), exprt::add_source_location(), alignment(), from_integer(), exprt::op0(), exprt::operands(), size_type(), exprt::source_location(), irept::swap(), exprt::type(), and typecheck_type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 2959 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), gcc_vector_types_compatible(), irept::id(), implicit_typecast_arithmetic(), is_number(), exprt::make_typecast(), exprt::op0(), exprt::op1(), exprt::operands(), typet::subtype(), to_string(), to_vector_type(), exprt::type(), typecheck_expr_pointer_arithmetic(), and UNREACHABLE.
Referenced by cpp_typecheckt::typecheck_expr_binary_arithmetic(), and typecheck_expr_main().
|
protectedvirtual |
Definition at line 3237 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), implicit_typecast_bool(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Definition at line 507 of file c_typecheck_expr.cpp.
References irept::add(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), forall_operands, from_integer(), has_component_rec(), irept::id(), irept::is_nil(), exprt::make_typecast(), member_offset_expr(), exprt::op0(), exprt::operands(), messaget::result(), simplify(), size_of_expr(), size_type(), exprt::source_location(), typet::subtype(), irept::swap(), to_string(), to_struct_type(), to_struct_union_type(), exprt::type(), typecheck_expr(), and typecheck_type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Definition at line 447 of file c_typecheck_expr.cpp.
References symbolt::base_name, implicit_typecast(), symbol_tablet::insert(), symbolt::name, exprt::op0(), exprt::operands(), pointer_type(), messaget::result(), code_typet::return_type(), exprt::source_location(), irept::swap(), symbol_table, symbolt::type, exprt::type(), typecheck_type(), and void_type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 431 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::get_bool(), exprt::op1(), exprt::operands(), irept::set(), and exprt::type().
Referenced by cpp_typecheckt::typecheck_expr_comma(), and typecheck_expr_main().
|
protectedvirtual |
Definition at line 2866 of file c_typecheck_expr.cpp.
Referenced by typecheck_expr_main().
|
protectedvirtual |
Definition at line 490 of file c_typecheck_expr.cpp.
References irept::add(), signed_int_type(), exprt::type(), and typecheck_type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1754 of file c_typecheck_expr.cpp.
References exprt::copy_to_operands(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), from_integer(), irept::id(), index_type(), exprt::op0(), exprt::operands(), irept::set(), typet::subtype(), to_string(), exprt::type(), and typecheck_expr_function_identifier().
Referenced by cpp_typecheckt::typecheck_expr_dereference(), typecheck_expr_main(), and typecheck_expr_ptrmember().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1797 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), irept::id(), pointer_type(), irept::set(), exprt::source_location(), and exprt::type().
Referenced by typecheck_expr_dereference(), and cpp_typecheckt::typecheck_expr_function_identifier().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1216 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::get_bool(), irept::id(), make_index_type(), exprt::move_to_operands(), exprt::op0(), exprt::op1(), exprt::operands(), irept::set(), typet::subtype(), to_string(), exprt::type(), and typecheck_arithmetic_pointer().
Referenced by cpp_typecheckt::typecheck_expr_index(), and typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 169 of file c_typecheck_expr.cpp.
References irept::add(), exprt::add_source_location(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), forall_irep, Forall_irep, Forall_operands, gcc_types_compatible_p(), irept::get(), irept::get_bool(), irept::get_sub(), irept::id(), irept::is_nil(), irept::is_not_nil(), is_number(), exprt::make_bool(), exprt::make_typecast(), exprt::op0(), exprt::operands(), irept::pretty(), irept::remove(), irept::set(), signed_int_type(), exprt::source_location(), typet::subtype(), irept::swap(), to_binary_relation_expr(), to_if_expr(), to_shift_expr(), to_side_effect_expr(), to_string(), to_symbol_expr(), exprt::type(), typecheck_expr(), typecheck_expr_address_of(), typecheck_expr_alignof(), typecheck_expr_binary_arithmetic(), typecheck_expr_binary_boolean(), typecheck_expr_builtin_offsetof(), typecheck_expr_builtin_va_arg(), typecheck_expr_comma(), typecheck_expr_constant(), typecheck_expr_cw_va_arg_typeof(), typecheck_expr_dereference(), typecheck_expr_index(), typecheck_expr_member(), typecheck_expr_ptrmember(), typecheck_expr_rel(), typecheck_expr_shifts(), typecheck_expr_side_effect(), typecheck_expr_sizeof(), typecheck_expr_symbol(), typecheck_expr_trinary(), typecheck_expr_typecast(), typecheck_expr_unary_arithmetic(), typecheck_expr_unary_boolean(), typecheck_type(), and void_type().
Referenced by typecheck_expr(), and cpp_typecheckt::typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1465 of file c_typecheck_expr.cpp.
References dstringt::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::get(), struct_union_typet::componentt::get_access(), irept::get_bool(), struct_union_typet::get_component(), get_component_rec(), irept::id(), irept::is_nil(), exprt::op0(), exprt::operands(), irept::set(), irept::swap(), to_string(), to_struct_union_type(), and exprt::type().
Referenced by typecheck_expr_main(), and typecheck_expr_ptrmember().
|
protectedvirtual |
Definition at line 671 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), messaget::eom(), typecheckt::err_location(), messaget::error(), Forall_operands, irept::get(), irept::id(), is_complete_type(), symbolt::is_extern, symbolt::is_static_lifetime, symbolt::is_type, exprt::op0(), exprt::op1(), exprt::operands(), code_declt::symbol(), symbolt::symbol_expr(), symbol_table, symbol_table_baset::symbols, to_ansi_c_declaration(), to_code(), symbolt::type, typecheck_code(), typecheck_declaration(), and typecheck_expr().
Referenced by typecheck_expr(), and cpp_typecheckt::typecheck_function_expr().
|
protectedvirtual |
Definition at line 3147 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::get(), side_effect_exprt::get_statement(), irept::id(), make_index_type(), exprt::op0(), exprt::op1(), exprt::operands(), pointer_diff_type(), to_side_effect_expr(), to_string(), exprt::type(), typecheck_arithmetic_pointer(), and UNREACHABLE.
Referenced by typecheck_expr_binary_arithmetic(), and typecheck_side_effect_assignment().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1425 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), from_integer(), irept::id(), index_type(), exprt::op0(), exprt::operands(), irept::set(), exprt::source_location(), typet::subtype(), irept::swap(), to_string(), exprt::type(), typecheck_expr_dereference(), and typecheck_expr_member().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1293 of file c_typecheck_expr.cpp.
References adjust_float_rel(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), implicit_typecast_arithmetic(), is_number(), exprt::is_zero(), exprt::make_typecast(), exprt::op0(), exprt::op1(), simplify_expr(), to_string(), exprt::type(), and typecheck_expr_rel_vector().
Referenced by typecheck_expr_main(), and cpp_typecheckt::typecheck_expr_rel().
|
protectedvirtual |
Definition at line 1399 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), exprt::op0(), exprt::op1(), signed_int_type(), typet::subtype(), to_string(), to_vector_type(), and exprt::type().
Referenced by typecheck_expr_rel().
|
protectedvirtual |
Definition at line 3060 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), implicit_typecast_arithmetic(), is_number(), exprt::op0(), exprt::op1(), typet::subtype(), to_string(), and exprt::type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1808 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::get_bool(), side_effect_exprt::get_statement(), has_prefix(), irept::id(), id2string(), is_numeric_type(), exprt::make_typecast(), exprt::op0(), exprt::operands(), typet::subtype(), to_c_bit_field_type(), to_c_enum_tag_type(), to_side_effect_expr_function_call(), to_string(), exprt::type(), typecheck_arithmetic_pointer(), typecheck_side_effect_assignment(), typecheck_side_effect_function_call(), typecheck_side_effect_gcc_conditional_expression(), and typecheck_side_effect_statement_expression().
Referenced by typecheck_expr_main(), cpp_typecheckt::typecheck_expr_side_effect(), and cpp_typecheckt::typecheck_side_effect_inc_dec().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 918 of file c_typecheck_expr.cpp.
References irept::add(), char_type(), clean_code, exprt::copy_to_operands(), messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), irept::is_nil(), exprt::op0(), exprt::operands(), codet::set_statement(), size_of_expr(), irept::swap(), to_string(), exprt::type(), typecheck_type(), and void_type().
Referenced by typecheck_expr_main(), and cpp_typecheckt::typecheck_expr_sizeof().
|
protectedvirtual |
Definition at line 742 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), asm_label_map, CPROVER_PREFIX, symbolt::display_name(), dstringt::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow_macros(), irept::get(), source_locationt::get_function(), symbol_exprt::get_identifier(), has_prefix(), irept::id(), id2string(), symbolt::is_lvalue, symbolt::is_macro, symbolt::is_type, namespacet::lookup(), parameter_map, pointer_type(), irept::set(), symbol_exprt::set_identifier(), exprt::source_location(), irept::swap(), symbolt::symbol_expr(), to_symbol_expr(), symbolt::type, exprt::type(), and typecheck_expr().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1561 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), constant_exprt::get_value(), code_typet::has_ellipsis(), implicit_typecast(), implicit_typecast_arithmetic(), implicit_typecast_bool(), exprt::is_constant(), exprt::operands(), code_typet::parameters(), pointer_type(), code_typet::return_type(), irept::set(), simplify_expr(), to_code_type(), to_constant_expr(), to_string(), exprt::type(), and void_type().
Referenced by typecheck_expr_main(), and typecheck_side_effect_gcc_conditional_expression().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1012 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), index_exprt::array(), base_type_eq(), clean_code, struct_union_typet::components(), exprt::copy_to_operands(), do_initializer(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), from_integer(), irept::get_bool(), irept::id(), index_exprt::index(), index_type(), irept::is_nil(), is_numeric_type(), exprt::make_typecast(), exprt::op0(), exprt::operands(), pointer_offset_bits(), irept::set(), codet::set_statement(), signed_int_type(), exprt::source_location(), typet::subtype(), irept::swap(), to_array_type(), to_string(), to_union_type(), to_vector_type(), exprt::type(), typecheck_type(), and void_type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Definition at line 2871 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), implicit_typecast_arithmetic(), is_number(), exprt::op0(), exprt::operands(), typet::subtype(), to_string(), and exprt::type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Definition at line 2910 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), implicit_typecast_bool(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protectedvirtual |
Definition at line 393 of file c_typecheck_code.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), exprt::op0(), exprt::operands(), and typecheck_expr().
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 407 of file c_typecheck_code.cpp.
References exprt::add_source_location(), configt::ansi_c, break_is_allowed, config, continue_is_allowed, code_blockt::end_location(), messaget::eom(), typecheckt::err_location(), messaget::error(), configt::ansi_ct::for_has_scope, implicit_typecast_bool(), irept::is_nil(), irept::is_not_nil(), irept::make_nil(), exprt::move_to_operands(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::op3(), exprt::operands(), exprt::reserve_operands(), irept::set(), exprt::source_location(), irept::swap(), to_code(), to_code_block(), typecheck_code(), typecheck_expr(), and typecheck_spec_expr().
Referenced by typecheck_code().
|
protected |
Definition at line 505 of file c_typecheck_base.cpp.
References add_argc_argv(), symbolt::base_name, messaget::eom(), messaget::error(), id2string(), irept::is_not_nil(), labels_defined, labels_used, symbolt::location, move_symbol(), symbolt::name, code_typet::parameters(), return_type, code_typet::return_type(), messaget::mstreamt::source_location, to_code(), to_code_type(), to_string(), symbolt::type, exprt::type(), typecheck_code(), and symbolt::value.
Referenced by typecheck_new_symbol(), and typecheck_redefinition_non_type().
|
protectedvirtual |
type:checked | arguments, type-checked function |
Reimplemented in cpp_typecheckt.
Definition at line 2784 of file c_typecheck_expr.cpp.
References side_effect_expr_function_callt::arguments(), messaget::eom(), typecheckt::err_location(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), side_effect_expr_function_callt::function(), irept::get(), irept::get_bool(), code_typet::has_ellipsis(), irept::id(), implicit_typecast(), code_typet::is_KnR(), irept::is_nil(), code_typet::parameters(), pointer_type(), irept::set(), messaget::mstreamt::source_location, typet::subtype(), to_code_type(), exprt::type(), void_type(), and messaget::warning().
Referenced by do_special_functions(), cpp_typecheckt::typecheck_function_call_arguments(), and typecheck_side_effect_function_call().
|
protectedvirtual |
Definition at line 578 of file c_typecheck_code.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), exprt::op0(), exprt::operands(), exprt::type(), and typecheck_expr().
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 566 of file c_typecheck_code.cpp.
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 541 of file c_typecheck_code.cpp.
References case_is_allowed, messaget::eom(), typecheckt::err_location(), messaget::error(), implicit_typecast(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), switch_op_type, to_code(), typecheck_code(), and typecheck_expr().
Referenced by typecheck_code().
|
protectedvirtual |
Definition at line 572 of file c_typecheck_code.cpp.
References code_gotot::get_destination(), labels_used, and exprt::source_location().
Referenced by typecheck_code().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 603 of file c_typecheck_code.cpp.
References exprt::add_source_location(), code_ifthenelset::cond(), code_ifthenelset::else_case(), messaget::eom(), typecheckt::err_location(), messaget::error(), irept::get(), irept::id(), implicit_typecast_bool(), irept::is_nil(), exprt::move_to_operands(), exprt::operands(), exprt::source_location(), irept::swap(), code_ifthenelset::then_case(), to_code(), typecheck_code(), typecheck_expr(), and messaget::warning().
Referenced by typecheck_code(), and cpp_typecheckt::typecheck_ifthenelse().
|
protectedvirtual |
Definition at line 498 of file c_typecheck_code.cpp.
References code_labelt::code(), code_labelt::get_label(), labels_defined, exprt::source_location(), and typecheck_code().
Referenced by typecheck_code().
|
protected |
Definition at line 132 of file c_typecheck_base.cpp.
References adjust_function_parameter(), do_initializer(), irept::id(), symbolt::is_macro, irept::is_not_nil(), symbolt::is_parameter, code_typet::parameters(), to_code_type(), symbolt::type, typecheck_function_body(), and symbolt::value.
Referenced by typecheck_symbol().
|
protected |
Definition at line 245 of file c_typecheck_base.cpp.
References configt::ansi_c, configt::ansi_ct::APPLE, configt::ansi_ct::ARM, config, symbolt::display_name(), do_initializer(), messaget::eom(), symbol_tablet::erase(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), configt::ansi_ct::GCC, irept::get(), irept::get_bool(), code_typet::has_ellipsis(), irept::id(), exprt::is_constant(), symbolt::is_extern, symbolt::is_file_local, symbolt::is_macro, irept::is_nil(), irept::is_not_nil(), symbolt::is_weak, symbolt::location, configt::ansi_ct::mode, code_typet::parameters(), PRECONDITION, irept::set(), array_typet::size(), messaget::mstreamt::source_location, typet::subtype(), irept::swap(), symbol_table, symbol_table_baset::symbols, to_array_type(), to_code_type(), to_string(), symbolt::type, typecheck_function_body(), symbolt::value, and messaget::warning().
Referenced by typecheck_symbol().
|
protected |
Definition at line 162 of file c_typecheck_base.cpp.
References configt::ansi_c, config, symbolt::display_name(), messaget::eom(), messaget::error(), namespace_baset::follow(), irept::id(), irept::id_string(), symbolt::location, configt::ansi_ct::os, configt::ansi_ct::OS_WIN, messaget::mstreamt::source_location, typet::subtype(), irept::swap(), to_string(), and symbolt::type.
Referenced by typecheck_symbol().
|
protectedvirtual |
Definition at line 664 of file c_typecheck_code.cpp.
References exprt::copy_to_operands(), messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow(), irept::id(), implicit_typecast(), exprt::make_typecast(), exprt::op0(), exprt::operands(), return_type, exprt::source_location(), messaget::mstreamt::source_location, to_string(), exprt::type(), typecheck_expr(), and messaget::warning().
Referenced by typecheck_code().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 3258 of file c_typecheck_expr.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), namespace_baset::follow_tag(), gcc_vector_types_compatible(), irept::get_bool(), side_effect_exprt::get_statement(), irept::id(), implicit_typecast(), implicit_typecast_arithmetic(), is_number(), exprt::make_typecast(), exprt::op0(), exprt::op1(), exprt::operands(), irept::set(), typet::subtype(), to_c_enum_tag_type(), to_string(), to_vector_type(), exprt::type(), and typecheck_expr_pointer_arithmetic().
Referenced by typecheck_expr_side_effect(), and cpp_typecheckt::typecheck_side_effect_assignment().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 1899 of file c_typecheck_expr.cpp.
References irept::add(), side_effect_expr_function_callt::arguments(), asm_label_map, symbolt::base_name, builtin_factory(), do_special_functions(), dstringt::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), code_blockt::find_last_statement(), exprt::find_source_location(), namespace_baset::follow(), side_effect_expr_function_callt::function(), irept::get_bool(), symbol_exprt::get_identifier(), messaget::get_message_handler(), codet::get_statement(), has_subexpr(), irept::id(), id2string(), replace_symbolt::insert(), irept::is_not_nil(), symbolt::location, codet::make_block(), move_symbol(), symbolt::name, exprt::op0(), exprt::operands(), code_typet::parameters(), pointer_type(), return_type, code_typet::return_type(), irept::set(), codet::set_statement(), signed_int_type(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), irept::swap(), symbol_table, symbol_table_baset::symbols, to_code(), to_code_block(), to_code_type(), to_string(), to_symbol_expr(), symbolt::type, exprt::type(), typecheck_code(), typecheck_expr(), typecheck_function_call_arguments(), typecheck_side_effect_statement_expression(), symbolt::value, void_type(), and messaget::warning().
Referenced by typecheck_expr_side_effect().
|
protectedvirtual |
Definition at line 1653 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), if_exprt::cond(), messaget::eom(), typecheckt::err_location(), messaget::error(), if_exprt::false_case(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), exprt::source_location(), if_exprt::true_case(), exprt::type(), and typecheck_expr_trinary().
Referenced by typecheck_expr_side_effect().
|
protectedvirtual |
Definition at line 846 of file c_typecheck_expr.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), side_effect_expr_function_callt::arguments(), messaget::eom(), typecheckt::err_location(), messaget::error(), irept::find(), code_blockt::find_last_statement(), code_function_callt::function(), side_effect_expr_function_callt::function(), implicit_typecast(), irept::is_nil(), code_function_callt::lhs(), exprt::op0(), exprt::operands(), pointer_type(), exprt::source_location(), irept::swap(), to_code(), to_code_block(), to_code_function_call(), exprt::type(), and UNREACHABLE.
Referenced by typecheck_expr_side_effect(), and typecheck_side_effect_function_call().
|
protectedvirtual |
Definition at line 810 of file c_typecheck_code.cpp.
References irept::add(), irept::find(), implicit_typecast_bool(), irept::is_not_nil(), and typecheck_expr().
Referenced by typecheck_declaration(), typecheck_dowhile(), typecheck_for(), and typecheck_while().
|
protectedvirtual |
Definition at line 652 of file c_typecheck_code.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), exprt::op0(), exprt::operands(), to_code(), and typecheck_code().
Referenced by typecheck_code().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 709 of file c_typecheck_code.cpp.
References code_switcht::body(), break_is_allowed, case_is_allowed, messaget::eom(), typecheckt::err_location(), messaget::error(), implicit_typecast_arithmetic(), exprt::operands(), switch_op_type, exprt::type(), typecheck_code(), typecheck_expr(), and code_switcht::value().
Referenced by typecheck_code(), and cpp_typecheckt::typecheck_switch().
|
protectedvirtual |
Definition at line 506 of file c_typecheck_code.cpp.
References case_is_allowed, code_switch_caset::case_op(), code_switch_caset::code(), messaget::eom(), typecheckt::err_location(), messaget::error(), implicit_typecast(), code_switch_caset::is_default(), exprt::operands(), switch_op_type, typecheck_code(), and typecheck_expr().
Referenced by typecheck_code().
|
protected |
Definition at line 47 of file c_typecheck_base.cpp.
References symbolt::base_name, symbolt::display_name(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), symbol_tablet::get_writeable(), irept::id(), id2string(), symbolt::is_extern, symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_macro, symbolt::is_static_lifetime, symbolt::is_type, symbolt::location, move_symbol(), symbolt::name, symbolt::pretty_name, messaget::mstreamt::source_location, symbol_table, symbol_table_baset::symbols, symbolt::type, typecheck_new_symbol(), typecheck_redefinition_non_type(), typecheck_redefinition_type(), and symbolt::value.
Referenced by typecheck_declaration().
|
protectedvirtual |
Definition at line 1428 of file c_typecheck_type.cpp.
References alignment(), symbolt::base_name, messaget::eom(), messaget::error(), irept::find(), irept::get_bool(), symbol_typet::get_identifier(), symbolt::is_macro, symbolt::is_type, irept::set(), typet::source_location(), messaget::mstreamt::source_location, symbol_table, symbol_table_baset::symbols, to_symbol_type(), symbolt::type, and c_qualifierst::write().
Referenced by typecheck_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 28 of file c_typecheck_type.cpp.
References irept::add(), alignment(), configt::ansi_c, config, double_type(), dstringt::empty(), messaget::eom(), messaget::error(), irept::find(), float_type(), namespace_baset::follow_tag(), from_integer(), gcc_float128_type(), gcc_signed_int128_type(), gcc_unsigned_int128_type(), irept::get(), irept::get_bool(), messaget::get_message_handler(), symbol_table_baset::get_writeable_ref(), irept::id(), INVARIANT, irept::is_not_nil(), is_signed(), configt::ansi_ct::long_int_width, configt::ansi_ct::long_long_int_width, make_constant(), mode, ansi_c_convert_typet::read(), messaget::result(), irept::set(), signed_char_type(), signed_int_type(), signed_long_int_type(), signed_long_long_int_type(), signed_short_int_type(), signed_size_type(), size_type(), typet::source_location(), messaget::mstreamt::source_location, typet::subtype(), symbol_table, to_array_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_code_type(), to_string(), to_struct_union_type(), to_vector_type(), symbolt::type, typecheck_array_type(), typecheck_c_bit_field_type(), typecheck_c_enum_tag_type(), typecheck_c_enum_type(), typecheck_code_type(), typecheck_compound_type(), typecheck_custom_type(), typecheck_expr(), typecheck_symbol_type(), typecheck_typeof_type(), typecheck_vector_type(), unsigned_char_type(), unsigned_int_type(), unsigned_long_int_type(), unsigned_long_long_int_type(), unsigned_short_int_type(), ansi_c_convert_typet::write(), and c_qualifierst::write().
Referenced by typecheck_array_type(), typecheck_c_bit_field_type(), typecheck_code_type(), typecheck_compound_body(), typecheck_declaration(), typecheck_expr_alignof(), typecheck_expr_builtin_offsetof(), typecheck_expr_builtin_va_arg(), typecheck_expr_cw_va_arg_typeof(), typecheck_expr_main(), typecheck_expr_sizeof(), typecheck_expr_typecast(), cpp_typecheckt::typecheck_type(), typecheck_typeof_type(), and typecheck_vector_type().
|
protectedvirtual |
Definition at line 1391 of file c_typecheck_type.cpp.
References exprt::add_source_location(), irept::find(), irept::get_bool(), irept::id(), exprt::op0(), exprt::operands(), c_qualifierst::read(), typet::source_location(), irept::swap(), exprt::type(), typecheck_expr(), typecheck_type(), and c_qualifierst::write().
Referenced by typecheck_type().
|
protectedvirtual |
Definition at line 611 of file c_typecheck_type.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), from_integer(), irept::id(), make_constant_index(), irept::pretty(), signed_size_type(), simplify(), vector_typet::size(), size_of_expr(), messaget::mstreamt::source_location, typet::subtype(), to_integer(), to_string(), typecheck_expr(), and typecheck_type().
Referenced by typecheck_type(), and cpp_typecheckt::typecheck_type().
|
protectedvirtual |
Reimplemented in cpp_typecheckt.
Definition at line 740 of file c_typecheck_code.cpp.
References exprt::add_source_location(), code_whilet::body(), break_is_allowed, code_whilet::cond(), continue_is_allowed, messaget::eom(), typecheckt::err_location(), messaget::error(), codet::get_statement(), implicit_typecast_bool(), exprt::move_to_operands(), exprt::operands(), exprt::source_location(), irept::swap(), typecheck_code(), typecheck_expr(), and typecheck_spec_expr().
Referenced by typecheck_code(), and cpp_typecheckt::typecheck_while().
|
protected |
Definition at line 274 of file c_typecheck_base.h.
Referenced by apply_asm_label(), typecheck_declaration(), typecheck_expr_symbol(), and typecheck_side_effect_function_call().
|
protected |
Definition at line 148 of file c_typecheck_base.h.
Referenced by start_typecheck_code(), typecheck_break(), typecheck_dowhile(), typecheck_for(), typecheck_switch(), and typecheck_while().
|
protected |
Definition at line 150 of file c_typecheck_base.h.
Referenced by start_typecheck_code(), typecheck_gcc_switch_case_range(), typecheck_switch(), and typecheck_switch_case().
|
protected |
Definition at line 237 of file c_typecheck_base.h.
Referenced by typecheck_array_type(), typecheck_code_type(), typecheck_decl(), typecheck_expr_sizeof(), and typecheck_expr_typecast().
|
protected |
Definition at line 149 of file c_typecheck_base.h.
Referenced by start_typecheck_code(), typecheck_continue(), typecheck_dowhile(), typecheck_for(), and typecheck_while().
|
protected |
Definition at line 70 of file c_typecheck_base.h.
Referenced by typecheck_array_type(), and typecheck_declaration().
|
protected |
Definition at line 155 of file c_typecheck_base.h.
Referenced by typecheck_function_body(), and typecheck_label().
|
protected |
Definition at line 155 of file c_typecheck_base.h.
Referenced by typecheck_expr_address_of(), typecheck_function_body(), and typecheck_goto().
|
protected |
Definition at line 69 of file c_typecheck_base.h.
Referenced by cpp_typecheckt::convert_parameter(), cpp_typecheckt::convert_parameters(), move_symbol(), typecheck_array_type(), and typecheck_type().
|
protected |
Definition at line 68 of file c_typecheck_base.h.
Referenced by cpp_typecheckt::convert(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), cpp_typecheckt::do_virtual_table(), move_symbol(), cpp_typecheckt::static_and_dynamic_initialization(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_function_template(), and cpp_typecheckt::typecheck_member_function().
|
protected |
Definition at line 73 of file c_typecheck_base.h.
Referenced by typecheck_code_type(), typecheck_declaration(), and typecheck_expr_symbol().
|
protected |
Definition at line 152 of file c_typecheck_base.h.
Referenced by cpp_typecheckt::convert_function(), cpp_typecheckt::cpp_is_pod(), cpp_typecheckt::find_cpctor(), typecheck_code_type(), cpp_typecheckt::typecheck_compound_declarator(), typecheck_function_body(), typecheck_return(), typecheck_side_effect_function_call(), and cpp_typecheckt::typecheck_side_effect_function_call().
|
protected |
Definition at line 151 of file c_typecheck_base.h.
Referenced by typecheck_gcc_switch_case_range(), typecheck_switch(), and typecheck_switch_case().
|
protected |
Definition at line 67 of file c_typecheck_base.h.
Referenced by cpp_typecheckt::builtin_factory(), cpp_typecheckt::class_template_symbol(), cpp_typecheckt::clean_up(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::convert_class_template_specialization(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_parameter(), cpp_typecheckt::do_not_typechecked(), cpp_typecheckt::do_virtual_table(), cpp_declarator_convertert::get_final_identifier(), cpp_typecheckt::instantiate_template(), move_symbol(), cpp_typecheckt::static_and_dynamic_initialization(), typecheck_array_type(), typecheck_c_enum_tag_type(), typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_compound_declarator(), typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), typecheck_decl(), typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_member(), typecheck_expr_operands(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_method_application(), typecheck_redefinition_non_type(), typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), typecheck_symbol(), typecheck_symbol_type(), and typecheck_type().