cprover
java_bytecode_convert_method.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_METHOD_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
14 
15 #include <util/symbol_table.h>
16 #include <util/message.h>
17 #include <util/safe_pointer.h>
19 
21 #include "ci_lazy_methods.h"
22 
23 class class_hierarchyt;
24 
26  const symbolt &class_symbol,
28  symbol_tablet &symbol_table,
29  message_handlert &message_handler,
30  size_t max_array_length,
31  safe_pointer<ci_lazy_methodst> lazy_methods,
32  const character_refine_preprocesst &character_refine);
33 
35  const symbolt &class_symbol,
37  symbol_tablet &symbol_table,
38  message_handlert &message_handler,
39  size_t max_array_length,
40  const character_refine_preprocesst &character_preprocess)
41 {
43  class_symbol,
44  method,
45  symbol_table,
46  message_handler,
47  max_array_length,
49  character_preprocess);
50 }
51 
53  const symbolt &class_symbol,
54  const irep_idt &method_identifier,
56  symbol_tablet &symbol_table);
57 
58 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Preprocess a goto-programs so that calls to the java Character library are replaced by simple express...
void java_bytecode_convert_method_lazy(const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table)
This creates a method symbol in the symtab, but doesn&#39;t actually perform method conversion just yet...
The symbol table.
Definition: symbol_table.h:52
Context-insensitive lazy methods container.
Symbol table.
Simple checked pointers.