java_bytecode_language.h File Reference

#include <util/language.h>
#include <util/cmdline.h>
#include "java_class_loader.h"
#include "character_refine_preprocess.h"

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_valuet >	lazy_methodst

Enumerations
enum	lazy_methods_modet { LAZY_METHODS_MODE_EAGER, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, LAZY_METHODS_MODE_CONTEXT_SENSITIVE }

Functions
languaget *	new_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

typedef std::map<irep_idt, lazy_method_valuet> lazy_methodst

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

Definition at line 23 of file java_bytecode_language.h.

Function Documentation

new_java_bytecode_language()

languaget* new_java_bytecode_language

(

)

Definition at line 658 of file java_bytecode_language.cpp.

Referenced by symex_parse_optionst::doit(), goto_diff_languagest::register_languages(), goto_cc_modet::register_languages(), goto_analyzer_parse_optionst::register_languages(), cbmc_parse_optionst::register_languages(), and goto_instrument_parse_optionst::register_languages().