cprover
|
#include "ci_lazy_methods.h"
#include "ci_lazy_methods_needed.h"
#include "java_class_loader.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "object_factory_parameters.h"
#include "select_pointer_type.h"
#include "synthetic_methods_map.h"
#include <memory>
#include <util/cmdline.h>
#include <util/make_unique.h>
#include <langapi/language.h>
Go to the source code of this file.
Classes | |
class | java_bytecode_languaget |
Macros | |
#define | JAVA_BYTECODE_LANGUAGE_OPTIONS |
#define | JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP |
#define | JAVA_CLASS_MODEL_SUFFIX "@class_model" |
Enumerations | |
enum | lazy_methods_modet { LAZY_METHODS_MODE_EAGER, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, LAZY_METHODS_MODE_EXTERNAL_DRIVER } |
Functions | |
std::unique_ptr< languaget > | new_java_bytecode_language () |
#define JAVA_BYTECODE_LANGUAGE_OPTIONS |
Definition at line 30 of file java_bytecode_language.h.
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP |
Definition at line 48 of file java_bytecode_language.h.
Referenced by jdiff_parse_optionst::help(), jbmc_parse_optionst::help(), and janalyzer_parse_optionst::help().
#define JAVA_CLASS_MODEL_SUFFIX "@class_model" |
Definition at line 90 of file java_bytecode_language.h.
Referenced by get_class_literal_initializer(), get_or_create_class_literal_symbol(), java_static_lifetime_init(), and references_class_model().
enum lazy_methods_modet |
Enumerator | |
---|---|
LAZY_METHODS_MODE_EAGER | |
LAZY_METHODS_MODE_CONTEXT_INSENSITIVE | |
LAZY_METHODS_MODE_EXTERNAL_DRIVER |
Definition at line 83 of file java_bytecode_language.h.
std::unique_ptr<languaget> new_java_bytecode_language | ( | ) |
Definition at line 1116 of file java_bytecode_language.cpp.
Referenced by jbmc_parse_optionst::doit(), load_java_class(), load_java_class_lazy(), jdiff_languagest::register_languages(), and janalyzer_parse_optionst::register_languages().