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. More...
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"

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.