CBMC
load_java_class.h File Reference

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:

Go to the source code of 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_nameThe name of the class file to load. It should not include the .class extension.
class_pathThe path to load the class from. Should be relative to the unit directory.
mainThe name of the main function or "" to use the default behaviour to find a main function.
java_langThe language implementation to use for the loading, which will be destroyed by this function.
command_lineThe 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 = "" 
)

◆ 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)

Parameters
java_class_nameThe name of the class file to load. It should not include the .class extension.
class_pathThe path to load the class from. Should be relative to the unit directory.
mainThe name of the main function or "" to use the default behaviour to find a main function.
Returns
The symbol table that is generated by parsing this file.

Definition at line 34 of file load_java_class.cpp.