cprover
|
#include <jsil_typecheck.h>
Public Member Functions | |
jsil_typecheckt (symbol_tablet &_symbol_table, message_handlert &_message_handler) | |
virtual | ~jsil_typecheckt () |
virtual void | typecheck () |
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 () |
Protected Attributes | |
symbol_tablet & | symbol_table |
const namespacet | ns |
irep_idt | proc_name |
std::unordered_set< irep_idt, irep_id_hash > | already_typechecked |
Additional Inherited Members |
Definition at line 33 of file jsil_typecheck.h.
|
inline |
Definition at line 36 of file jsil_typecheck.h.
|
inlinevirtual |
Definition at line 46 of file jsil_typecheck.h.
Prefix parameters and variables with a procedure name.
Definition at line 32 of file jsil_typecheck.cpp.
References id2string(), and proc_name.
Referenced by typecheck_symbol_expr(), and typecheck_type().
|
protected |
Definition at line 59 of file jsil_typecheck.cpp.
References dstringt::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), irept::is_nil(), jsil_incompatible_types(), jsil_is_subtype(), jsil_union(), irept::pretty(), exprt::type(), and update_expr_type().
Referenced by typecheck_assign(), typecheck_expr_base(), typecheck_expr_binary_arith(), typecheck_expr_binary_boolean(), typecheck_expr_binary_compare(), typecheck_expr_concatenation(), typecheck_expr_delete(), typecheck_expr_field(), typecheck_expr_has_field(), typecheck_expr_index(), typecheck_expr_proto_field(), typecheck_expr_proto_obj(), typecheck_expr_ref(), typecheck_expr_subtype(), typecheck_expr_unary_boolean(), typecheck_expr_unary_num(), typecheck_expr_unary_string(), typecheck_function_call(), and typecheck_ifthenelse().
|
protectedvirtual |
Definition at line 21 of file jsil_typecheck.cpp.
References expr2jsil(), and ns.
|
protectedvirtual |
Definition at line 26 of file jsil_typecheck.cpp.
References ns, and type2jsil().
|
virtual |
Implements typecheckt.
Definition at line 883 of file jsil_typecheck.cpp.
References forall_symbols, symbolt::is_type, symbol_table, symbol_tablet::symbols, typecheck_non_type_symbol(), and typecheck_type_symbol().
|
protected |
Definition at line 840 of file jsil_typecheck.cpp.
References make_type_compatible(), exprt::op0(), exprt::op1(), exprt::type(), and typecheck_expr().
Referenced by typecheck_code().
|
protected |
Definition at line 702 of file jsil_typecheck.cpp.
References Forall_operands, to_code(), and typecheck_code().
Referenced by typecheck_code().
|
protected |
Definition at line 648 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), codet::get_statement(), exprt::op0(), exprt::operands(), to_code_assign(), to_code_function_call(), to_code_ifthenelse(), to_code_label(), to_code_return(), to_code_try_catch(), typecheck_assign(), typecheck_block(), typecheck_expr(), typecheck_function_call(), typecheck_ifthenelse(), typecheck_return(), and typecheck_try_catch().
Referenced by typecheck_block(), typecheck_ifthenelse(), typecheck_non_type_symbol(), and typecheck_try_catch().
|
protected |
Definition at line 496 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
virtual |
Definition at line 136 of file jsil_typecheck.cpp.
References typecheck_expr_main(), and typecheck_expr_operands().
Referenced by typecheck_assign(), typecheck_code(), typecheck_expr_operands(), typecheck_function_call(), typecheck_ifthenelse(), and typecheck_return().
|
protected |
Definition at line 386 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_reference_type(), jsil_value_type(), make_type_compatible(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 479 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 463 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 511 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 431 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 277 of file jsil_typecheck.cpp.
References irept::id(), jsil_empty_type(), jsil_null_type(), jsil_undefined_type(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 319 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_object_type(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 371 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_reference_type(), make_type_compatible(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 355 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_object_type(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 335 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_object_type(), jsil_value_type(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 151 of file jsil_typecheck.cpp.
References dstringt::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), irept::is_nil(), jsil_kind(), jsil_user_object_type(), irept::pretty(), to_side_effect_expr_throw(), to_symbol_expr(), exprt::type(), typecheck_exp_binary_equal(), typecheck_expr_base(), typecheck_expr_binary_arith(), typecheck_expr_binary_boolean(), typecheck_expr_binary_compare(), typecheck_expr_concatenation(), typecheck_expr_constant(), typecheck_expr_delete(), typecheck_expr_field(), typecheck_expr_has_field(), typecheck_expr_index(), typecheck_expr_proto_field(), typecheck_expr_proto_obj(), typecheck_expr_ref(), typecheck_expr_side_effect_throw(), typecheck_expr_subtype(), typecheck_expr_unary_boolean(), typecheck_expr_unary_num(), typecheck_expr_unary_string(), and typecheck_symbol_expr().
Referenced by typecheck_expr().
|
protected |
Definition at line 145 of file jsil_typecheck.cpp.
References Forall_operands, and typecheck_expr().
Referenced by typecheck_expr().
|
protected |
Definition at line 287 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_object_type(), jsil_value_or_empty_type(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 303 of file jsil_typecheck.cpp.
References typecheckt::err_location(), messaget::error(), irept::id(), jsil_object_type(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 401 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_kind(), jsil_member_reference_type(), jsil_value_type(), jsil_variable_reference_type(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 268 of file jsil_typecheck.cpp.
References irept::add(), irept::id(), and typecheck_symbol_expr().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 447 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), jsil_kind(), make_type_compatible(), exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 527 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 557 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), and exprt::operands().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 542 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), irept::id(), make_type_compatible(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by typecheck_expr_main().
|
protected |
Definition at line 726 of file jsil_typecheck.cpp.
References symbol_tablet::add(), code_function_callt::arguments(), dstringt::empty(), messaget::eom(), typecheckt::err_location(), messaget::error(), code_function_callt::function(), symbol_exprt::get_identifier(), symbol_tablet::has_symbol(), irept::id(), irept::is_not_nil(), symbolt::is_type, jsil_any_type(), jsil_undefined_type(), code_function_callt::lhs(), symbolt::location, symbol_tablet::lookup(), make_type_compatible(), symbolt::mode, symbolt::name, exprt::operands(), messaget::mstreamt::source_location, symbol_table, to_code_type(), to_symbol_expr(), symbolt::type, exprt::type(), typecheck_expr(), and symbolt::value.
Referenced by typecheck_code(), and typecheck_try_catch().
|
protected |
Definition at line 828 of file jsil_typecheck.cpp.
References code_ifthenelset::cond(), code_ifthenelset::else_case(), irept::is_nil(), make_type_compatible(), code_ifthenelset::then_case(), to_code(), typecheck_code(), and typecheck_expr().
Referenced by typecheck_code().
|
protected |
typechecking procedure declaration; any other symbols should have been typechecked during typechecking of procedure declaration
Definition at line 851 of file jsil_typecheck.cpp.
References messaget::eom(), messaget::error(), irept::id(), symbolt::is_extern, symbolt::is_type, symbolt::location, symbolt::name, irept::pretty(), proc_name, messaget::mstreamt::source_location, to_code(), symbolt::type, typecheck_code(), typecheck_type(), and symbolt::value.
Referenced by typecheck().
|
protected |
Definition at line 696 of file jsil_typecheck.cpp.
References code_returnt::has_return_value(), code_returnt::return_value(), and typecheck_expr().
Referenced by typecheck_code().
|
protected |
Definition at line 570 of file jsil_typecheck.cpp.
References symbol_tablet::add(), add_prefix(), symbolt::base_name, messaget::eom(), messaget::error(), symbol_exprt::get_identifier(), has_prefix(), irept::id(), id2string(), symbolt::is_extern, symbolt::is_lvalue, symbolt::is_type, symbolt::mode, symbolt::name, proc_name, symbol_exprt::set_identifier(), symbol_table, symbol_tablet::symbols, symbolt::type, and exprt::type().
Referenced by typecheck_expr_main(), and typecheck_expr_side_effect_throw().
|
protected |
Definition at line 708 of file jsil_typecheck.cpp.
References messaget::eom(), typecheckt::err_location(), messaget::error(), code_try_catcht::get_catch_code(), exprt::operands(), to_code_function_call(), code_try_catcht::try_code(), typecheck_code(), and typecheck_function_call().
Referenced by typecheck_code().
|
protected |
Definition at line 98 of file jsil_typecheck.cpp.
References symbol_tablet::add(), add_prefix(), symbolt::base_name, messaget::eom(), messaget::error(), irept::id(), symbolt::is_extern, is_jsil_builtin_code_type(), is_jsil_spec_code_type(), jsil_value_or_empty_type(), jsil_value_or_reference_type(), jsil_value_type(), symbolt::mode, symbolt::name, code_typet::parameters(), symbol_table, to_code_type(), and symbolt::type.
Referenced by typecheck_non_type_symbol().
|
inlineprotected |
Definition at line 59 of file jsil_typecheck.h.
Referenced by typecheck().
Definition at line 37 of file jsil_typecheck.cpp.
References dstringt::empty(), messaget::eom(), messaget::error(), symbol_exprt::get_identifier(), symbol_tablet::has_symbol(), irept::id(), irept::is_nil(), jsil_union(), symbol_tablet::lookup(), symbol_table, to_symbol_expr(), symbolt::type, and exprt::type().
Referenced by make_type_compatible().
|
protected |
Definition at line 97 of file jsil_typecheck.h.
|
protected |
Definition at line 53 of file jsil_typecheck.h.
Referenced by to_string().
|
protected |
Definition at line 55 of file jsil_typecheck.h.
Referenced by add_prefix(), typecheck_non_type_symbol(), and typecheck_symbol_expr().
|
protected |
Definition at line 52 of file jsil_typecheck.h.
Referenced by typecheck(), typecheck_function_call(), typecheck_symbol_expr(), typecheck_type(), and update_expr_type().