java_bytecode_convert_method.h File Reference

JAVA Bytecode Language Conversion. More...

#include "ci_lazy_methods_needed.h"
#include "java_bytecode_parse_tree.h"
#include "java_string_library_preprocess.h"
#include <util/message.h>
#include <util/symbol_table.h>

Include dependency graph for java_bytecode_convert_method.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	java_bytecode_initialize_parameter_names (symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
	This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode. More...
void	java_bytecode_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
void	java_bytecode_convert_method_lazy (const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, message_handlert &)
	This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet. More...

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_method.h.

Function Documentation

java_bytecode_convert_method()

void java_bytecode_convert_method	(	const symbolt &	class_symbol,
		const java_bytecode_parse_treet::methodt &	,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		size_t	max_array_length,
		bool	throw_assertion_error,
		optionalt< ci_lazy_methods_neededt >	needed_lazy_methods,
		java_string_library_preprocesst &	string_preprocess,
		const class_hierarchyt &	class_hierarchy,
		bool	threading_support
	)

Definition at line 3096 of file java_bytecode_convert_method.cpp.

References cprover_methods_to_ignore, id2string(), java_bytecode_convert_method(), message_handler, symbolt::name, and java_bytecode_parse_treet::membert::name.

Referenced by java_bytecode_languaget::convert_single_method(), and java_bytecode_convert_method().

java_bytecode_convert_method_lazy()

void java_bytecode_convert_method_lazy	(	const symbolt &	class_symbol,
		const irep_idt &	method_identifier,
		const java_bytecode_parse_treet::methodt &	m,
		symbol_tablet &	symbol_table,
		message_handlert &	message_handler
	)

This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.

The caller should call java_bytecode_convert_method later to give the symbol/method a body.

parameters: class_symbol: class this method belongs to

method_identifier: fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)") m: parsed method object to convert symbol_table: global symbol table (will be modified) message_handler: message handler to collect warnings

Definition at line 340 of file java_bytecode_convert_method.cpp.

References symbol_table_baset::add(), java_bytecode_parse_treet::membert::annotations, symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, convert_annotations(), java_bytecode_parse_treet::membert::descriptor, java_bytecode_parse_treet::find_annotation(), id2string(), java_bytecode_parse_treet::methodt::is_abstract, java_bytecode_parse_treet::methodt::is_bridge, is_constructor(), java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_bytecode_parse_treet::methodt::is_synchronized, java_reference_type(), symbolt::location, member_type_lazy(), message_handler, symbolt::mode, symbolt::name, code_typet::parameters(), symbolt::pretty_name, pretty_signature(), irept::set(), code_typet::set_access(), source_locationt::set_function(), code_typet::set_is_constructor(), code_typet::parametert::set_this(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, symbolt::type, and exprt::type().

java_bytecode_initialize_parameter_names()

void java_bytecode_initialize_parameter_names	(	symbolt &	method_symbol,
		const java_bytecode_parse_treet::methodt::local_variable_tablet &	local_variable_table,
		symbol_table_baset &	symbol_table
	)

This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode.

Remarks

This is useful for pre-initialization for methods generated by the string solver

Parameters

method_symbol	The symbol for the method for which to initialize the parameters
local_variable_table	The local variable table containing the bytecode for the parameters
symbol_table	The symbol table into which to insert symbols for the parameters

Definition at line 3018 of file java_bytecode_convert_method.cpp.

References symbolt::base_name, id2string(), symbol_table_baset::insert(), java_char_from_type(), java_local_variable_slots(), java_method_parameter_slots(), symbolt::mode, symbolt::name, code_typet::parameters(), to_java_method_type(), to_string(), and symbolt::type.

Referenced by java_bytecode_languaget::convert_single_method().