cprover
load_java_class.cpp File Reference
#include "load_java_class.h"
#include <iostream>
#include <testing-utils/catch.hpp>
#include <testing-utils/free_form_cmdline.h>
#include <testing-utils/message.h>
#include <util/config.h>
#include <util/suffix.h>
#include <goto-programs/lazy_goto_model.h>
#include <langapi/mode.h>
#include <java_bytecode/java_bytecode_language.h>
#include <util/file_util.h>
Include dependency graph for load_java_class.cpp:

Go to the source code of this file.

Functions

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...
 
symbol_tablet load_java_class (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...
 
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)
 Go through the process of loading, type-checking and finalising loading a specific class file to build the symbol table. 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)
 

Function Documentation

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

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

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 56 of file load_java_class.cpp.

References free_form_cmdlinet::add_flag(), get_language_from_mode(), load_java_class(), main(), new_java_bytecode_language(), and register_language().

Referenced by load_java_class(), and load_java_class_lazy().

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

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

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.
Returns
The symbol table that is generated by parsing this file.

Definition at line 86 of file load_java_class.cpp.

References configt::javat::classpath, config, languaget::final(), languaget::generate_support_functions(), irept::get_bool(), get_current_working_directory(), languaget::get_language_options(), has_suffix(), symbol_table_baset::has_symbol(), irept::id(), INVARIANT, configt::java, language_filet::language, symbol_table_baset::lookup(), main(), configt::main, null_message_handler, languaget::parse(), PRECONDITION, lazy_goto_modelt::process_whole_model_and_freeze(), messaget::set_message_handler(), goto_modelt::symbol_table, and languaget::typecheck().

◆ 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,
std::unique_ptr< languaget > &&  java_lang 
)

◆ 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 36 of file load_java_class.cpp.

References get_language_from_mode(), load_java_class(), main(), new_java_bytecode_language(), and register_language().