cprover
java_entry_point.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
12 
13 #include <util/irep.h>
14 #include <util/symbol.h>
15 
16 bool java_entry_point(
17  class symbol_tablet &symbol_table,
18  const irep_idt &main_class,
19  class message_handlert &message_handler,
20  bool assume_init_pointers_not_null,
21  size_t max_nondet_array_length);
22 
23 typedef struct
24 {
29 
31  symbol_tablet &symbol_table,
32  const irep_idt &main_class,
34  bool allow_no_body=false);
35 
36 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
Symbol table entry.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
The symbol table.
Definition: symbol_table.h:52
main_function_resultt get_main_symbol(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &, bool allow_no_body=false)
bool java_entry_point(class symbol_tablet &symbol_table, const irep_idt &main_class, class message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length)
find entry point and create initialization code for function symbol_table main class message_handler ...