cprover
java_bytecode_convert_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
14 
15 #include <util/symbol_table.h>
16 #include <util/message.h>
17 
19 #include "java_bytecode_language.h"
21 
23  const java_bytecode_parse_treet &parse_tree,
24  symbol_tablet &symbol_table,
25  message_handlert &message_handler,
26  size_t max_array_length,
27  lazy_methodst &,
29  bool string_refinement_enabled,
30  const character_refine_preprocesst &character_preprocess);
31 
32 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
lazy_methods_modet
The symbol table.
Definition: symbol_table.h:52
std::map< irep_idt, lazy_method_valuet > lazy_methodst
Symbol table.
bool java_bytecode_convert_class(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, lazy_methodst &, lazy_methods_modet, bool string_refinement_enabled, const character_refine_preprocesst &character_preprocess)