cprover
|
#include <util/language.h>
#include <util/cmdline.h>
#include "java_class_loader.h"
#include "character_refine_preprocess.h"
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 () |
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 |
Definition at line 19 of file java_bytecode_language.h.
typedef std::pair< const symbolt *, const java_bytecode_parse_treet::methodt *> lazy_method_valuet |
Definition at line 33 of file java_bytecode_language.h.
typedef std::map<irep_idt, lazy_method_valuet> lazy_methodst |
Definition at line 35 of file java_bytecode_language.h.
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.
languaget* new_java_bytecode_language | ( | ) |
Definition at line 658 of file java_bytecode_language.cpp.
References java_bytecode_languaget::java_bytecode_languaget().
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().