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 ()
 
void parse_java_language_options (const cmdlinet &cmd, optionst &options)
 Parse options that are java bytecode specific. More...
 

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)" \
"(throw-runtime-exceptions)" \
"(max-nondet-array-length):" \
"(max-nondet-tree-depth):" \
"(java-max-vla-length):" \
"(java-cp-include-files):" \
"(no-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

Definition at line 44 of file java_bytecode_language.h.

◆ JAVA_CLASS_MODEL_SUFFIX

#define JAVA_CLASS_MODEL_SUFFIX   "@class_model"

Definition at line 86 of file java_bytecode_language.h.

Enumeration Type Documentation

◆ lazy_methods_modet

Enumerator
LAZY_METHODS_MODE_EAGER 
LAZY_METHODS_MODE_CONTEXT_INSENSITIVE 
LAZY_METHODS_MODE_EXTERNAL_DRIVER 

Definition at line 79 of file java_bytecode_language.h.

Function Documentation

◆ new_java_bytecode_language()

std::unique_ptr<languaget> new_java_bytecode_language ( )

Definition at line 1172 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
cmdCommand line
[out]optionsThe options object that will be updated.

Definition at line 47 of file java_bytecode_language.cpp.