java_bytecode_language.h File Reference
#include "ci_lazy_methods.h"#include "ci_lazy_methods_needed.h"#include "java_class_loader.h"#include "java_object_factory_parameters.h"#include "java_static_initializers.h"#include "java_string_library_preprocess.h"#include "select_pointer_type.h"#include "synthetic_methods_map.h"#include <memory>#include <util/json.h>#include <util/make_unique.h>#include <util/prefix_filter.h>#include <langapi/language.h>
Include dependency graph for java_bytecode_language.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | lazy_class_to_declared_symbols_mapt |
| Map classes to the symbols they declare but is only computed once it is needed and the map is then kept. More... | |
| struct | java_bytecode_language_optionst |
| class | java_bytecode_languaget |
Macros | |
| #define | JAVA_BYTECODE_LANGUAGE_OPTIONS |
| #define | JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP |
| #define | JAVA_CLASSPATH_SEPARATOR ":" |
| #define | HELP_JAVA_CLASSPATH |
| #define | HELP_JAVA_METHOD_NAME |
| #define | HELP_JAVA_CLASS_NAME |
| #define | OPT_JAVA_JAR |
| #define | HELP_JAVA_JAR |
| #define | OPT_JAVA_GOTO_BINARY |
| #define | HELP_JAVA_GOTO_BINARY |
| #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 () |
| void | parse_java_language_options (const cmdlinet &cmd, optionst &options) |
| Parse options that are java bytecode specific. More... | |
| prefix_filtert | get_context (const optionst &options) |
Macro Definition Documentation
◆ HELP_JAVA_CLASS_NAME
| #define HELP_JAVA_CLASS_NAME |
Value:
/* NOLINT(*) */ \
" class-name name of class\n" \
" The entry point is the method specified by\n" \
" --function, or otherwise, the\n" \
" public static void main(String[])\n" \
" method of the given class.\n"
Definition at line 151 of file java_bytecode_language.h.
◆ HELP_JAVA_CLASSPATH
| #define HELP_JAVA_CLASSPATH |
Value:
/* NOLINT(*) */ \
" -classpath dirs/jars\n" \
" -cp dirs/jars\n" \
" --classpath dirs/jars set class search path of directories and\n" \
" jar files\n" \
" A " JAVA_CLASSPATH_SEPARATOR \
" separated list of directories and JAR\n" \
" archives to search for class files.\n" \
" --main-class class-name set the name of the main class\n"
Definition at line 136 of file java_bytecode_language.h.
◆ HELP_JAVA_GOTO_BINARY
| #define HELP_JAVA_GOTO_BINARY |
Value:
/* NOLINT(*) */ \
" --gb goto-binary goto-binary file to be checked\n" \
" The entry point is the method specified by\n" \
" --function, or otherwise, the\n" \
" public static void main(String[])\n" \
" of the class specified by --main-class\n" \
" (checked in this order).\n"
Definition at line 173 of file java_bytecode_language.h.
◆ HELP_JAVA_JAR
| #define HELP_JAVA_JAR |
Value:
/* NOLINT(*) */ \
" -jar jarfile JAR file to be checked\n" \
" The entry point is the method specified by\n" \
" --function or otherwise, the\n" \
" public static void main(String[]) method\n" \
" of the class specified by --main-class or the main\n" /* NOLINT(*) */ \
" class specified in the JAR manifest\n" \
" (checked in this order).\n"
Definition at line 161 of file java_bytecode_language.h.
◆ HELP_JAVA_METHOD_NAME
| #define HELP_JAVA_METHOD_NAME |
Value:
/* NOLINT(*) */ \
" method-name fully qualified name of method\n" \
" used as entry point, e.g.\n" \
" mypackage.Myclass.foo:(I)Z\n"
Definition at line 146 of file java_bytecode_language.h.
◆ JAVA_BYTECODE_LANGUAGE_OPTIONS
| #define JAVA_BYTECODE_LANGUAGE_OPTIONS |
Value:
/*NOLINT*/ \
"(disable-uncaught-exception-check)" \
"(throw-assertion-error)" \
"(assert-no-exceptions-thrown)" \
"(java-assume-inputs-non-null)" \
"(java-assume-inputs-interval):" \
"(java-assume-inputs-integral)" \
"(throw-runtime-exceptions)" \
"(max-nondet-array-length):" \
"(max-nondet-tree-depth):" \
"(java-max-vla-length):" \
"(java-cp-include-files):" \
"(ignore-manifest-main-class)" \
"(context-include):" \
"(context-exclude):" \
"(no-lazy-methods)" \
"(lazy-methods-extra-entry-point):" \
"(java-load-class):" \
"(java-no-load-class):" \
"(static-values):" \
"(java-lift-clinit-calls)"
Definition at line 31 of file java_bytecode_language.h.
◆ JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
| #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP |
Definition at line 53 of file java_bytecode_language.h.
◆ JAVA_CLASS_MODEL_SUFFIX
| #define JAVA_CLASS_MODEL_SUFFIX "@class_model" |
Definition at line 272 of file java_bytecode_language.h.
◆ JAVA_CLASSPATH_SEPARATOR
| #define JAVA_CLASSPATH_SEPARATOR ":" |
Definition at line 133 of file java_bytecode_language.h.
◆ OPT_JAVA_GOTO_BINARY
| #define OPT_JAVA_GOTO_BINARY |
Value:
/* NOLINT(*) */ \
"(gb):"
Definition at line 170 of file java_bytecode_language.h.
◆ OPT_JAVA_JAR
| #define OPT_JAVA_JAR |
Value:
/* NOLINT(*) */ \
"(jar):"
Definition at line 158 of file java_bytecode_language.h.
Enumeration Type Documentation
◆ lazy_methods_modet
| enum lazy_methods_modet |
| Enumerator | |
|---|---|
| LAZY_METHODS_MODE_EAGER | |
| LAZY_METHODS_MODE_CONTEXT_INSENSITIVE | |
| LAZY_METHODS_MODE_EXTERNAL_DRIVER | |
Definition at line 184 of file java_bytecode_language.h.
Function Documentation
◆ get_context()
| prefix_filtert get_context | ( | const optionst & | options | ) |
Definition at line 116 of file java_bytecode_language.cpp.
◆ new_java_bytecode_language()
| std::unique_ptr<languaget> new_java_bytecode_language | ( | ) |
Definition at line 1524 of file java_bytecode_language.cpp.
◆ parse_java_language_options()
Parse options that are java bytecode specific.
- Parameters
-
cmd Command line [out] options The options object that will be updated.
Definition at line 55 of file java_bytecode_language.cpp.
