CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.h File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Macros | Enumerations | Functions

java_bytecode_language.h File Reference

#include <util/json.h>
#include <util/prefix_filter.h>
#include <util/symbol.h>
#include <langapi/language.h>
#include "ci_lazy_methods.h"
#include "ci_lazy_methods_needed.h"
#include "code_with_references.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 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 "(jar):"

#define HELP_JAVA_JAR

#define OPT_JAVA_GOTO_BINARY "(gb):"

#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.

prefix_filtert get_context (const optionst &options)

Macro Definition Documentation

◆ HELP_JAVA_CLASS_NAME

#define HELP_JAVA_CLASS_NAME

Value:

" {uclass-name} \t " \

"name of class. The entry point is the method specified by --function, " \

"or otherwise, the public static void main(String[]) method of the given " \

"class.\n"

Definition at line 143 of file java_bytecode_language.h.

◆ HELP_JAVA_CLASSPATH

#define HELP_JAVA_CLASSPATH

Value:

" {y-classpath} {udirs/jars}, {y-cp} {udirs/jars}, " \

"{y--classpath} {udirs/jars} \t " \

"set class search path of directories and jar files to a " \

JAVA_CLASSPATH_SEPARATOR "-separated list of directories and JAR " \

"archives to search for class files\n" \

" {y--main-class} {uclass-name} \t set the name of the main class\n"

JAVA_CLASSPATH_SEPARATOR

#define JAVA_CLASSPATH_SEPARATOR

Definition java_bytecode_language.h:127

Definition at line 130 of file java_bytecode_language.h.

◆ HELP_JAVA_GOTO_BINARY

#define HELP_JAVA_GOTO_BINARY

Value:

" {y--gb} {ugoto-binary} \t " \

"goto-binary file to be checked. The entry point is the method specified " \

"by {y--function}, or otherwise, the public static void main(String[]) of " \

"the class specified by {y--main-class} (checked in this order).\n"

Definition at line 162 of file java_bytecode_language.h.

◆ HELP_JAVA_JAR

#define HELP_JAVA_JAR

Value:

" {y-jar} {ujarfile} \t " \

"JAR file to be checked. The entry point is the method specified by " \

"{y--function} or otherwise, the public static void main(String[]) method " \

"of the class specified by {y--main-class} or the main class specified in " \

"the JAR manifest (checked in this order).\n"

Definition at line 152 of file java_bytecode_language.h.

◆ HELP_JAVA_METHOD_NAME

#define HELP_JAVA_METHOD_NAME

Value:

" {umethod-name} \t " \

"fully qualified name of method used as entry point, e.g. " \

"mypackage.Myclass.foo:(I)Z\n"

Definition at line 138 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 32 of file java_bytecode_language.h.

◆ JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP

#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP

Definition at line 54 of file java_bytecode_language.h.

◆ JAVA_CLASS_MODEL_SUFFIX

#define JAVA_CLASS_MODEL_SUFFIX "@class_model"

Definition at line 257 of file java_bytecode_language.h.

◆ JAVA_CLASSPATH_SEPARATOR

#define JAVA_CLASSPATH_SEPARATOR ":"

Definition at line 127 of file java_bytecode_language.h.

◆ OPT_JAVA_GOTO_BINARY

#define OPT_JAVA_GOTO_BINARY "(gb):"

Definition at line 159 of file java_bytecode_language.h.

◆ OPT_JAVA_JAR

#define OPT_JAVA_JAR "(jar):"

Definition at line 149 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 169 of file java_bytecode_language.h.

Function Documentation

◆ get_context()

prefix_filtert get_context ( const optionst & options )

Definition at line 112 of file java_bytecode_language.cpp.

◆ new_java_bytecode_language()

std::unique_ptr< languaget > new_java_bytecode_language ( )

Definition at line 1532 of file java_bytecode_language.cpp.

◆ parse_java_language_options()

void parse_java_language_options ( const cmdlinet & cmd,

optionst & options

)

Parse options that are java bytecode specific.

Parameters: cmd Command line

[out] options The options object that will be updated.

Definition at line 51 of file java_bytecode_language.cpp.