cprover
|
#include <java_bytecode_typecheck.h>
Public Member Functions | |
java_bytecode_typecheckt (symbol_table_baset &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled) | |
virtual | ~java_bytecode_typecheckt () |
virtual void | typecheck () |
void | typecheck (const journalling_symbol_tablet::changesett &identifiers) |
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 Member Functions | |
void | typecheck_type_symbol (symbolt &) |
void | typecheck_non_type_symbol (symbolt &) |
void | typecheck_code (codet &) |
void | typecheck_type (typet &) |
void | typecheck_expr_symbol (symbol_exprt &) |
void | typecheck_expr_member (member_exprt &) |
void | typecheck_expr_java_new (side_effect_exprt &) |
void | typecheck_expr_java_new_array (side_effect_exprt &) |
virtual std::string | to_string (const exprt &expr) |
virtual std::string | to_string (const typet &type) |
Protected Attributes | |
symbol_table_baset & | symbol_table |
const namespacet | ns |
bool | string_refinement_enabled |
std::set< irep_idt > | already_typechecked |
Additional Inherited Members |
Definition at line 42 of file java_bytecode_typecheck.h.
|
inline |
Definition at line 45 of file java_bytecode_typecheck.h.
|
inlinevirtual |
Definition at line 56 of file java_bytecode_typecheck.h.
|
protectedvirtual |
Definition at line 20 of file java_bytecode_typecheck.cpp.
References expr2java(), and ns.
|
protectedvirtual |
Definition at line 25 of file java_bytecode_typecheck.cpp.
References ns, and type2java().
|
virtual |
Implements typecheckt.
Definition at line 37 of file java_bytecode_typecheck.cpp.
References symbol_table, and symbol_table_baset::symbols.
void java_bytecode_typecheckt::typecheck | ( | const journalling_symbol_tablet::changesett & | identifiers | ) |
Definition at line 48 of file java_bytecode_typecheck.cpp.
References symbol_table_baset::get_writeable(), symbolt::is_type, symbol_table, typecheck_non_type_symbol(), and typecheck_type_symbol().
|
protected |
Definition at line 14 of file java_bytecode_typecheck_code.cpp.
References code_function_callt::arguments(), code_labelt::code(), code_ifthenelset::cond(), code_ifthenelset::else_case(), Forall_operands, code_function_callt::function(), codet::get_statement(), irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), exprt::make_typecast(), exprt::op0(), exprt::operands(), code_assignt::rhs(), code_ifthenelset::then_case(), to_code(), to_code_assign(), to_code_function_call(), to_code_ifthenelse(), to_code_label(), to_code_switch(), exprt::type(), typecheck_expr(), and code_switcht::value().
Referenced by typecheck_expr().
|
virtual |
Definition at line 24 of file java_bytecode_typecheck_expr.cpp.
References Forall_operands, side_effect_exprt::get_statement(), irept::id(), INVARIANT, make_clean_pointer_cast(), ns, to_code(), to_member_expr(), to_pointer_type(), to_side_effect_expr(), to_symbol_expr(), exprt::type(), typecheck_code(), typecheck_expr_java_new(), typecheck_expr_java_new_array(), typecheck_expr_member(), and typecheck_expr_symbol().
Referenced by typecheck_code(), typecheck_non_type_symbol(), and typecheck_type().
|
protected |
Definition at line 59 of file java_bytecode_typecheck_expr.cpp.
References exprt::operands(), PRECONDITION, exprt::type(), and typecheck_type().
Referenced by typecheck_expr().
|
protected |
Definition at line 66 of file java_bytecode_typecheck_expr.cpp.
References exprt::operands(), PRECONDITION, exprt::type(), and typecheck_type().
Referenced by typecheck_expr().
|
protected |
Definition at line 124 of file java_bytecode_typecheck_expr.cpp.
References exprt::add_source_location(), base_type(), struct_union_typet::components(), messaget::eom(), namespace_baset::follow(), member_exprt::get_component_name(), struct_union_typet::componentt::get_name(), struct_union_typet::has_component(), ns, exprt::source_location(), messaget::mstreamt::source_location, member_exprt::struct_op(), irept::swap(), to_struct_type(), exprt::type(), and messaget::warning().
Referenced by typecheck_expr().
|
protected |
Definition at line 74 of file java_bytecode_typecheck_expr.cpp.
References symbol_table_baset::add(), symbolt::base_name, CPROVER_PREFIX, messaget::eom(), messaget::error(), irept::get(), symbol_exprt::get_identifier(), has_prefix(), irept::id(), id2string(), INVARIANT, symbolt::is_lvalue, symbolt::is_type, symbolt::mode, symbolt::name, PRECONDITION, symbolt::pretty_name, symbol_table, symbol_table_baset::symbols, symbolt::type, and exprt::type().
Referenced by typecheck_expr().
|
protected |
Definition at line 30 of file java_bytecode_typecheck.cpp.
References symbolt::is_type, symbolt::type, typecheck_expr(), typecheck_type(), and symbolt::value.
Referenced by typecheck().
|
protected |
Definition at line 17 of file java_bytecode_typecheck_type.cpp.
References DATA_INVARIANT, symbol_typet::get_identifier(), irept::id(), id2string(), symbol_table_baset::lookup(), code_typet::parameters(), code_typet::return_type(), typet::subtype(), symbol_table, to_array_type(), to_java_method_type(), to_symbol_type(), and typecheck_expr().
Referenced by typecheck_expr_java_new(), typecheck_expr_java_new_array(), typecheck_non_type_symbol(), and typecheck_type_symbol().
|
protected |
Definition at line 53 of file java_bytecode_typecheck_type.cpp.
References DATA_INVARIANT, id2string(), symbolt::is_type, symbolt::mode, symbolt::name, symbolt::type, and typecheck_type().
Referenced by typecheck().
|
protected |
Definition at line 80 of file java_bytecode_typecheck.h.
|
protected |
Definition at line 64 of file java_bytecode_typecheck.h.
Referenced by to_string(), typecheck_expr(), and typecheck_expr_member().
|
protected |
Definition at line 65 of file java_bytecode_typecheck.h.
|
protected |
Definition at line 63 of file java_bytecode_typecheck.h.
Referenced by typecheck(), typecheck_expr_symbol(), and typecheck_type().