cprover
|
#include "java_bytecode_language.h"
#include <string>
#include <util/symbol_table.h>
#include <util/suffix.h>
#include <util/config.h>
#include <util/cmdline.h>
#include <util/string2int.h>
#include <json/json_parser.h>
#include <goto-programs/class_hierarchy.h>
#include "java_bytecode_convert_class.h"
#include "java_bytecode_convert_method.h"
#include "java_bytecode_internal_additions.h"
#include "java_bytecode_typecheck.h"
#include "java_entry_point.h"
#include "java_bytecode_parser.h"
#include "java_class_loader.h"
#include "expr2java.h"
Go to the source code of this file.
Functions | |
static irep_idt | get_virtual_method_target (const std::set< irep_idt > &needed_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table) |
Find a virtual callee, if one is defined and the callee type is known to exist. More... | |
static void | get_virtual_method_targets (const code_function_callt &c, const std::set< irep_idt > &needed_classes, std::vector< irep_idt > &needed_methods, symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy) |
Find possible callees, excluding types that are not known to be instantiated. More... | |
static void | gather_virtual_callsites (const exprt &e, std::vector< const code_function_callt *> &result) |
See output. More... | |
static void | gather_needed_globals (const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed) |
See output. More... | |
static void | gather_field_types (const typet &class_type, const namespacet &ns, ci_lazy_methodst &lazy_methods) |
See output. More... | |
static void | initialize_needed_classes (const std::vector< irep_idt > &entry_points, const namespacet &ns, const class_hierarchyt &ch, ci_lazy_methodst &lazy_methods) |
See output. More... | |
languaget * | new_java_bytecode_language () |
|
static |
See output.
ns
: global namespace lazy_methods
with all Java reference types reachable starting at class_type
. For example if class_type
is symbol_typet("java::A")
and A has a B field, then B
(but not A
) will noted as a needed class. Definition at line 323 of file java_bytecode_language.cpp.
References ci_lazy_methodst::add_needed_class(), namespace_baset::follow(), to_struct_type(), and to_symbol_type().
Referenced by initialize_needed_classes().
|
static |
See output.
symbol_table
: global symtab needed
with global variable symbols referenced from e
or its children. Definition at line 293 of file java_bytecode_language.cpp.
References symbol_tablet::add(), forall_operands, irept::id(), symbol_tablet::symbols, and to_symbol_expr().
Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().
|
static |
See output.
result
with pointers to each function call within e that calls a virtual function. Definition at line 273 of file java_bytecode_language.cpp.
References forall_operands, code_function_callt::function(), codet::get_statement(), irept::id(), to_code(), and to_code_function_call().
Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().
|
static |
Find a virtual callee, if one is defined and the callee type is known to exist.
call_basename
: unqualified function name with type signature (e.g. "f:(I)") classname
: class name that may define or override a function named call_basename
. symbol_table
: global symtab classname
's definition of call_basename
if found and classname
is present in needed_classes
, or irep_idt() otherwise. Definition at line 168 of file java_bytecode_language.cpp.
References symbol_tablet::has_symbol(), and id2string().
Referenced by get_virtual_method_targets().
|
static |
Find possible callees, excluding types that are not known to be instantiated.
needed_classes
: set of classes that can be instantiated. Any potential callee not in this set will be ignored. symbol_table
: global symtab class_hierarchy
: global class hierarchy needed_methods
with all possible c
callees, taking needed_classes
into account (virtual function overrides defined on classes that are not 'needed' are ignored) Definition at line 195 of file java_bytecode_language.cpp.
References symbol_tablet::add(), symbolt::base_name, class_hierarchyt::class_map, code_function_callt::function(), irept::get(), class_hierarchyt::get_children_trans(), get_virtual_method_target(), id2string(), irept::make_nil(), symbolt::mode, symbolt::name, symbolt::type, exprt::type(), and symbolt::value.
Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().
|
static |
See output.
ns
: global namespace ch
: global class hierarchy lazy_methods
with all Java reference types whose references may be passed, directly or indirectly, to any of the functions in entry_points
. Definition at line 354 of file java_bytecode_language.cpp.
References ci_lazy_methodst::add_needed_class(), gather_field_types(), class_hierarchyt::get_parents_trans(), namespacet::lookup(), to_code_type(), and to_symbol_type().
Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().
languaget* new_java_bytecode_language | ( | ) |
Definition at line 658 of file java_bytecode_language.cpp.
Referenced by symex_parse_optionst::doit(), goto_diff_languagest::register_languages(), goto_cc_modet::register_languages(), goto_analyzer_parse_optionst::register_languages(), cbmc_parse_optionst::register_languages(), and goto_instrument_parse_optionst::register_languages().