Utility for loading and parsing a specified java class file, returning the symbol table generated by this. More...

#include <util/symbol_table.h>
#include <goto-programs/goto_model.h>
#include <memory>

Include dependency graph for load_java_class.h:

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

Functions
symbol_tablet	load_java_class (const std::string &java_class_name, const std::string &class_path, const std::string &main="")
	Returns the symbol table from load_goto_model_from_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main) // NOLINT. More...

symbol_tablet	load_java_class (const std::string &java_class_name, const std::string &class_path, const std::string &main, std::unique_ptr< languaget > &&java_lang)
	Returns the symbol table from load_goto_model_from_java_class with the command line set to be disabling lazy loading and string refinement. More...

symbol_tablet	load_java_class (const std::string &java_class_name, const std::string &class_path, const std::string &main, std::unique_ptr< languaget > &&java_lang, const cmdlinet &command_line)
	Returns the symbol table from load_goto_model_from_java_class. More...

goto_modelt	load_goto_model_from_java_class (const std::string &java_class_name, const std::string &class_path, const std::string &main, std::unique_ptr< languaget > &&java_lang, const cmdlinet &command_line)
	Go through the process of loading, type-checking and finalising a specific class file to build a goto model from it. More...

symbol_tablet	load_java_class_lazy (const std::string &java_class_name, const std::string &class_path, const std::string &main)
	Go through the process of loading, type-checking and finalising loading a specific class file to build the symbol table. More...

goto_modelt	load_goto_model_from_java_class (const std::string &java_class_name, const std::string &class_path, const std::vector< std::string > &command_line_flags, const std::unordered_map< std::string, std::string > &command_line_options, const std::string &main="")
	Overload of load_goto_model_from_java_class with configurable command-line options. More...

goto_modelt	load_goto_model_from_java_class (const std::string &java_class_name, const std::string &class_path, const std::string &main="")
	See load_goto_model_from_java_class With the command line configured to disable lazy loading and string refinement and the language set to be the default java_bytecode language. More...

Detailed Description

Utility for loading and parsing a specified java class file, returning the symbol table generated by this.

Definition in file load_java_class.h.

Function Documentation

◆ load_goto_model_from_java_class() [1/3]

goto_modelt load_goto_model_from_java_class	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::string &	main,
		std::unique_ptr< languaget > &&	java_lang,
		const cmdlinet &	command_line
	)

Go through the process of loading, type-checking and finalising a specific class file to build a goto model from it.

Parameters

java_class_name	The name of the class file to load. It should not include the .class extension.
class_path	The path to load the class from. Should be relative to the unit directory.
main	The name of the main function or "" to use the default behaviour to find a main function.
java_lang	The language implementation to use for the loading, which will be destroyed by this function.
command_line	The command line used to configure the provided language

Returns: The goto model containing both the functions and the symbol table from loading this class.

Definition at line 86 of file load_java_class.cpp.

◆ load_goto_model_from_java_class() [2/3]

goto_modelt load_goto_model_from_java_class	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::string &	main = `""`
	)

See load_goto_model_from_java_class With the command line configured to disable lazy loading and string refinement and the language set to be the default java_bytecode language.

Definition at line 199 of file load_java_class.cpp.

◆ load_goto_model_from_java_class() [3/3]

goto_modelt load_goto_model_from_java_class	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::vector< std::string > &	command_line_flags,
		const std::unordered_map< std::string, std::string > &	command_line_options,
		const std::string &	main = `""`
	)

Overload of load_goto_model_from_java_class with configurable command-line options.

Definition at line 177 of file load_java_class.cpp.

◆ load_java_class() [1/3]

symbol_tablet load_java_class	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::string &	main,
		std::unique_ptr< languaget > &&	java_lang
	)

Returns the symbol table from load_goto_model_from_java_class with the command line set to be disabling lazy loading and string refinement.

Definition at line 165 of file load_java_class.cpp.

◆ load_java_class() [2/3]

symbol_tablet load_java_class	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::string &	main,
		std::unique_ptr< languaget > &&	java_lang,
		const cmdlinet &	command_line
	)

Returns the symbol table from load_goto_model_from_java_class.

Definition at line 56 of file load_java_class.cpp.

◆ load_java_class() [3/3]

symbol_tablet load_java_class	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::string &	main = `""`
	)

Returns the symbol table from load_goto_model_from_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main) // NOLINT.

Definition at line 46 of file load_java_class.cpp.

◆ load_java_class_lazy()

symbol_tablet load_java_class_lazy	(	const std::string &	java_class_name,
		const std::string &	class_path,
		const std::string &	main
	)

Go through the process of loading, type-checking and finalising loading a specific class file to build the symbol table.

The functions are converted using ci_lazy_methods (equivalent to passing –lazy-methods to JBMC)