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 MAX_NONDET_ARRAY_LENGTH_DEFAULT   5
 

Typedefs

typedef std::pair< const symbolt *, const java_bytecode_parse_treet::methodt * > lazy_method_valuet
 
typedef std::map< irep_idt, lazy_method_valuetlazy_methodst
 

Enumerations

enum  lazy_methods_modet { LAZY_METHODS_MODE_EAGER, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, LAZY_METHODS_MODE_CONTEXT_SENSITIVE }
 

Functions

languagetnew_java_bytecode_language ()
 

Macro Definition Documentation

§ MAX_NONDET_ARRAY_LENGTH_DEFAULT

#define MAX_NONDET_ARRAY_LENGTH_DEFAULT   5

Definition at line 19 of file java_bytecode_language.h.

Typedef Documentation

§ lazy_method_valuet

typedef std::pair< const symbolt *, const java_bytecode_parse_treet::methodt *> lazy_method_valuet

Definition at line 33 of file java_bytecode_language.h.

§ lazy_methodst

Definition at line 35 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_CONTEXT_SENSITIVE 

Definition at line 23 of file java_bytecode_language.h.

Function Documentation

§ new_java_bytecode_language()