cprover
|
#include "java_entry_point.h"
#include <algorithm>
#include <set>
#include <iostream>
#include <util/arith_tools.h>
#include <util/prefix.h>
#include <util/std_types.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/cprover_prefix.h>
#include <util/message.h>
#include <util/config.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/suffix.h>
#include <util/c_types.h>
#include <ansi-c/string_constant.h>
#include <goto-programs/remove_exceptions.h>
#include "java_object_factory.h"
#include "java_types.h"
Go to the source code of this file.
Macros | |
#define | INITIALIZE CPROVER_PREFIX "initialize" |
Functions | |
static void | create_initialize (symbol_tablet &symbol_table) |
static bool | should_init_symbol (const symbolt &sym) |
void | java_static_lifetime_init (symbol_tablet &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, unsigned max_nondet_array_length) |
exprt::operandst | java_build_arguments (const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table, bool assume_init_pointers_not_null, unsigned max_nondet_array_length) |
void | java_record_outputs (const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_tablet &symbol_table) |
main_function_resultt | get_main_symbol (symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool allow_no_body) |
bool | java_entry_point (symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length) |
find entry point and create initialization code for function symbol_table main class message_handler More... | |
#define INITIALIZE CPROVER_PREFIX "initialize" |
Definition at line 35 of file java_entry_point.cpp.
Referenced by create_initialize(), java_entry_point(), and java_static_lifetime_init().
|
static |
Definition at line 37 of file java_entry_point.cpp.
References symbol_tablet::add(), code_blockt::add(), symbolt::base_name, CPROVER_PREFIX, from_integer(), INITIALIZE, namespacet::lookup(), symbolt::mode, symbolt::name, code_typet::return_type(), symbolt::type, exprt::type(), and symbolt::value.
Referenced by java_entry_point().
main_function_resultt get_main_symbol | ( | symbol_tablet & | symbol_table, |
const irep_idt & | main_class, | ||
message_handlert & | message_handler, | ||
bool | allow_no_body | ||
) |
Definition at line 298 of file java_entry_point.cpp.
References config, dstringt::empty(), messaget::eom(), messaget::error(), main_function_resultt::error_found, has_prefix(), irept::id(), id2string(), irept::is_nil(), configt::main, main_function_resultt::main_function, main_function_resultt::stop_convert, symbol_tablet::symbols, symbolt::type, and symbolt::value.
Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion(), java_bytecode_languaget::final(), and java_entry_point().
exprt::operandst java_build_arguments | ( | const symbolt & | function, |
code_blockt & | init_code, | ||
symbol_tablet & | symbol_table, | ||
bool | assume_init_pointers_not_null, | ||
unsigned | max_nondet_array_length | ||
) |
Definition at line 154 of file java_entry_point.cpp.
References config, dstringt::empty(), from_integer(), code_typet::parametert::get_base_name(), has_suffix(), code_typet::has_this(), irept::id(), index_type(), java_type_from_string(), configt::main, object_factory(), code_typet::parameters(), code_typet::return_type(), dstringt::size(), to_code_type(), and exprt::type().
Referenced by java_entry_point().
bool java_entry_point | ( | symbol_tablet & | symbol_table, |
const irep_idt & | main_class, | ||
message_handlert & | message_handler, | ||
bool | assume_init_pointers_not_null, | ||
size_t | max_nondet_array_length | ||
) |
find entry point and create initialization code for function symbol_table main class message_handler
assume_init_pointers_not_null | allow pointers in initialization code to be null max_nondet_array_length |
Definition at line 476 of file java_entry_point.cpp.
References symbol_tablet::add(), exprt::add_source_location(), code_function_callt::arguments(), symbolt::base_name, create_initialize(), goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), messaget::error(), EXC_SUFFIX, code_function_callt::function(), get_main_symbol(), irept::id(), id2string(), INITIALIZE, irept::is_nil(), symbolt::is_static_lifetime, java_build_arguments(), java_record_outputs(), java_reference_type(), java_static_lifetime_init(), code_function_callt::lhs(), loc, symbolt::location, main_function_resultt::main_function, irept::make_nil(), symbolt::mode, symbol_tablet::move(), exprt::move_to_operands(), symbolt::name, code_typet::return_type(), main_function_resultt::stop_convert, irept::swap(), symbolt::symbol_expr(), symbol_tablet::symbols, to_code_type(), symbolt::type, and symbolt::value.
Referenced by java_bytecode_languaget::final().
void java_record_outputs | ( | const symbolt & | function, |
const exprt::operandst & | main_arguments, | ||
code_blockt & | init_code, | ||
symbol_tablet & | symbol_table | ||
) |
Definition at line 221 of file java_entry_point.cpp.
References exprt::add_source_location(), symbolt::base_name, EXC_SUFFIX, from_integer(), symbol_tablet::has_symbol(), irept::id(), id2string(), index_type(), symbol_tablet::lookup(), exprt::move_to_operands(), exprt::op0(), exprt::op1(), exprt::operands(), code_typet::parameters(), code_typet::return_type(), symbolt::symbol_expr(), to_code_type(), and symbolt::type.
Referenced by java_entry_point().
void java_static_lifetime_init | ( | symbol_tablet & | symbol_table, |
const source_locationt & | source_location, | ||
bool | assume_init_pointers_not_null, | ||
unsigned | max_nondet_array_length | ||
) |
Definition at line 77 of file java_entry_point.cpp.
References code_blockt::add(), exprt::add_source_location(), code_function_callt::function(), symbol_exprt::get_identifier(), has_prefix(), has_suffix(), id2string(), INITIALIZE, irept::is_nil(), irept::is_not_nil(), code_function_callt::lhs(), symbol_tablet::lookup(), object_factory(), should_init_symbol(), symbolt::symbol_expr(), symbol_tablet::symbols, to_code(), to_code_block(), symbolt::type, and symbolt::value.
Referenced by java_entry_point().
|
static |
Definition at line 65 of file java_entry_point.cpp.
References has_prefix(), irept::id(), id2string(), symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, symbolt::mode, symbolt::name, and symbolt::type.
Referenced by java_static_lifetime_init().