Collaboration diagram for java_bytecode_convert_classt:

Public Types
typedef java_bytecode_parse_treet::classt	classt
typedef java_bytecode_parse_treet::fieldt	fieldt
typedef java_bytecode_parse_treet::methodt	methodt
typedef java_bytecode_parse_treet::annotationt	annotationt

Public Member Functions
	java_bytecode_convert_classt (symbol_table_baset &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, method_bytecodet &method_bytecode, java_string_library_preprocesst &_string_preprocess, const std::unordered_set< std::string > &no_load_classes)
void	operator() (const java_class_loadert::parse_tree_with_overlayst &parse_trees)
	Converts all the class parse trees into a class symbol and adds it to the symbol table.

Private Types
typedef std::list< std::reference_wrapper< const classt > >	overlay_classest

Private Member Functions
void	convert (const classt &c, const overlay_classest &overlay_classes)
	Convert a class, adding symbols to the symbol table for its members.
void	convert (symbolt &class_symbol, const fieldt &f)
	Convert a field, adding a symbol to teh symbol table for it.
bool	check_field_exists (const fieldt &field, const irep_idt &qualified_fieldname, const struct_union_typet::componentst &fields) const

Static Private Member Functions
static bool	is_overlay_method (const methodt &method)
	Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.
static bool	is_ignored_method (const irep_idt &class_name, const methodt &method)
	Check if a method is an ignored method, by one of two mechanisms:

Private Attributes
messaget	log
symbol_table_baset &	symbol_table
const size_t	max_array_length
method_bytecodet &	method_bytecode
java_string_library_preprocesst &	string_preprocess
std::unordered_set< std::string >	no_load_classes

Detailed Description

Definition at line 33 of file java_bytecode_convert_class.cpp.

Member Typedef Documentation

◆ annotationt

typedef java_bytecode_parse_treet::annotationt java_bytecode_convert_classt::annotationt

Definition at line 107 of file java_bytecode_convert_class.cpp.

◆ classt

typedef java_bytecode_parse_treet::classt java_bytecode_convert_classt::classt

Definition at line 104 of file java_bytecode_convert_class.cpp.

◆ fieldt

typedef java_bytecode_parse_treet::fieldt java_bytecode_convert_classt::fieldt

Definition at line 105 of file java_bytecode_convert_class.cpp.

◆ methodt

typedef java_bytecode_parse_treet::methodt java_bytecode_convert_classt::methodt

Definition at line 106 of file java_bytecode_convert_class.cpp.

◆ overlay_classest

typedef std::list<std::reference_wrapper<const classt> > java_bytecode_convert_classt::overlay_classest

private

Definition at line 117 of file java_bytecode_convert_class.cpp.

Constructor & Destructor Documentation

◆ java_bytecode_convert_classt()

java_bytecode_convert_classt::java_bytecode_convert_classt	(	symbol_table_baset &	_symbol_table,
		message_handlert &	_message_handler,
		size_t	_max_array_length,
		method_bytecodet &	method_bytecode,
		java_string_library_preprocesst &	_string_preprocess,
		const std::unordered_set< std::string > &	no_load_classes )

inline

Definition at line 36 of file java_bytecode_convert_class.cpp.

Member Function Documentation

◆ check_field_exists()

bool java_bytecode_convert_classt::check_field_exists	(	const fieldt &	field,
		const irep_idt &	qualified_fieldname,
		const struct_union_typet::componentst &	fields ) const

private

Definition at line 621 of file java_bytecode_convert_class.cpp.

◆ convert() [1/2]

void java_bytecode_convert_classt::convert	(	const classt &	c,
		const overlay_classest &	overlay_classes )

private

Convert a class, adding symbols to the symbol table for its members.

Parameters

c	Bytecode of the class to convert
overlay_classes	Bytecode of any overlays for the class to convert

Definition at line 270 of file java_bytecode_convert_class.cpp.

◆ convert() [2/2]

void java_bytecode_convert_classt::convert	(	symbolt &	class_symbol,
		const fieldt &	f )

private

Convert a field, adding a symbol to teh symbol table for it.

Parameters

class_symbol	The already added symbol for the containing class
f	The bytecode for the field to convert

this is for a free type variable, e.g., a field of the form T f;

this is for a field that holds a generic type, either with instantiated or with free type variables, e.g., List<T> l; or List<Integer> l;

Definition at line 642 of file java_bytecode_convert_class.cpp.

◆ is_ignored_method()

bool java_bytecode_convert_classt::is_ignored_method	(	const irep_idt &	class_name,
		const methodt &	method )

inlinestaticprivate

Check if a method is an ignored method, by one of two mechanisms:

If the class under consideration is org.cprover.CProver, and the method is listed as ignored.
If it has the annotation@IgnoredMethodImplementation. This kind of ignord method is intended for use in overlay classes, in particular for methods which must exist in the overlay class so that it will compile, e.g. default constructors, but which we do not want to overlay the corresponding method in the underlying class. It is an error if a method in an overlay class has the same signature as a method in the underlying class and it isn't marked as an overlay method or an ignored method.

Parameters

class_name	class the method is declared on
method	a methodt object from a java bytecode parse tree

Returns: true if the method is an ignored method, else false

Definition at line 161 of file java_bytecode_convert_class.cpp.

◆ is_overlay_method()

bool java_bytecode_convert_classt::is_overlay_method ( const methodt & method )

inlinestaticprivate

Check if a method is an overlay method by searching for ID_overlay_method in its list of annotations.

An overlay method is a method with the annotation @OverlayMethodImplementation. They should only appear in overlay classes. They will be loaded by JBMC instead of the method with the same signature in the underlying class. It is an error if there is no method with the same signature in the underlying class. It is an error if a method in an overlay class has the same signature as a method in the underlying class and it isn't marked as an overlay method or an ignored method.

Parameters

method a methodt object from a java bytecode parse tree

Returns: true if the method is an overlay method, else false

Definition at line 136 of file java_bytecode_convert_class.cpp.

◆ operator()()

void java_bytecode_convert_classt::operator() ( const java_class_loadert::parse_tree_with_overlayst & parse_trees )

inline

Converts all the class parse trees into a class symbol and adds it to the symbol table.

Parameters

parse_trees The parse trees found for the class to be converted.

Remarks: Allows multiple definitions of the same class to appear on the classpath, so long as all but the first definition are marked with the attribute \@java::org.cprover.OverlayClassImplementation. Overlay class definitions can contain methods with the same signature as methods in the original class, so long as these are marked with the attribute \@java::org.cprover.OverlayMethodImplementation; such overlay methods are replaced in the original file with the version found in the last overlay on the classpath. Later definitions can also contain new supporting methods and fields that are merged in. This will allow insertion of Java methods into library classes to handle, for example, modelling dependency injection.

Definition at line 67 of file java_bytecode_convert_class.cpp.

Member Data Documentation

◆ log

messaget java_bytecode_convert_classt::log

private

Definition at line 110 of file java_bytecode_convert_class.cpp.

◆ max_array_length

const size_t java_bytecode_convert_classt::max_array_length

private

Definition at line 112 of file java_bytecode_convert_class.cpp.

◆ method_bytecode

method_bytecodet& java_bytecode_convert_classt::method_bytecode

private

Definition at line 113 of file java_bytecode_convert_class.cpp.

◆ no_load_classes

std::unordered_set<std::string> java_bytecode_convert_classt::no_load_classes

private

Definition at line 176 of file java_bytecode_convert_class.cpp.

◆ string_preprocess

java_string_library_preprocesst& java_bytecode_convert_classt::string_preprocess

private

Definition at line 114 of file java_bytecode_convert_class.cpp.

◆ symbol_table

symbol_table_baset& java_bytecode_convert_classt::symbol_table

private

Definition at line 111 of file java_bytecode_convert_class.cpp.

The documentation for this class was generated from the following file:

/builddir/build/BUILD/cbmc-6.9.0-build/cbmc-cbmc-6.9.0/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Public Types

Public Member Functions

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ annotationt

◆ classt

◆ fieldt

◆ methodt

◆ overlay_classest

Constructor & Destructor Documentation

◆ java_bytecode_convert_classt()

Member Function Documentation

◆ check_field_exists()

◆ convert() [1/2]

◆ convert() [2/2]

◆ is_ignored_method()

◆ is_overlay_method()

◆ operator()()

Member Data Documentation

◆ log

◆ max_array_length

◆ method_bytecode

◆ no_load_classes

◆ string_preprocess

◆ symbol_table