cprover
java_bytecode_language.h File Reference
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  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< languagetnew_java_bytecode_language ()
 

Macro Definition Documentation

◆ JAVA_BYTECODE_LANGUAGE_OPTIONS

#define JAVA_BYTECODE_LANGUAGE_OPTIONS
Value:
/*NOLINT*/ \
"(disable-uncaught-exception-check)" \
"(throw-assertion-error)" \
"(java-assume-inputs-non-null)" \
"(java-throw-runtime-exceptions)" \
"(java-max-input-array-length):" \
"(java-max-input-tree-depth):" \
"(java-max-vla-length):" \
"(java-cp-include-files):" \
"(lazy-methods)" \
"(lazy-methods-extra-entry-point):" \
"(java-load-class):" \
"(java-no-load-class):"

Definition at line 30 of file java_bytecode_language.h.

◆ JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP

#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Value:
/*NOLINT*/ \
" --disable-uncaught-exception-check" \
" ignore uncaught exceptions and errors\n" \
" --throw-assertion-error throw java.lang.AssertionError on violated\n" /* NOLINT(*) */ \
" assert statements instead of failing\n" \
" at the location of the assert statement\n" /* NOLINT(*) */ \
" --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \
" entry point with null\n" /* NOLINT(*) */ \
" --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \
" --java-max-input-array-length N limit input array size to <= N\n" /* NOLINT(*) */ \
" --java-max-input-tree-depth N object references are (deterministically) set to null in\n" /* NOLINT(*) */ \
" the object\n" /* NOLINT(*) */ \
" --java-max-vla-length limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
" --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" /* NOLINT(*) */ \
" --lazy-methods only translate methods that appear to be reachable from\n" /* NOLINT(*) */ \
" the --function entry point or main class\n" /* NOLINT(*) */ \
" Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
" will be restricted to loaded methods in this case\n" /* NOLINT(*) */ \
" --lazy-methods-extra-entry-point METHODNAME\n" /* NOLINT(*) */ \
" treat METHODNAME as a possible program entry point for\n" /* NOLINT(*) */ \
" the purpose of lazy method loading\n" /* NOLINT(*) */ \
" A '.*' wildcard is allowed to specify all class members\n"

Definition at line 44 of file java_bytecode_language.h.

Referenced by jdiff_parse_optionst::help(), jbmc_parse_optionst::help(), and janalyzer_parse_optionst::help().

◆ JAVA_CLASS_MODEL_SUFFIX

#define JAVA_CLASS_MODEL_SUFFIX   "@class_model"

Enumeration Type Documentation

◆ lazy_methods_modet

Enumerator
LAZY_METHODS_MODE_EAGER 
LAZY_METHODS_MODE_CONTEXT_INSENSITIVE 
LAZY_METHODS_MODE_EXTERNAL_DRIVER 

Definition at line 70 of file java_bytecode_language.h.

Function Documentation

◆ new_java_bytecode_language()