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 "java_bytecode_language.h"
14 #include "select_pointer_type.h"
15 
16 #include <util/irep.h>
17 #include <util/symbol.h>
18 
19 #define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'"
20 #define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'"
21 
22 bool java_entry_point(
23  class symbol_table_baset &symbol_table,
24  const irep_idt &main_class,
25  class message_handlert &message_handler,
26  bool assume_init_pointers_not_null,
27  bool assert_uncaught_exceptions,
28  const java_object_factory_parameterst &object_factory_parameters,
29  const select_pointer_typet &pointer_type_selector,
30  bool string_refinement_enabled);
31 
33 {
34  enum statust
35  {
39  } status;
41 
42  // Implicit conversion doesn't lose information and allows return of status
43  // NOLINTNEXTLINE(runtime/explicit)
45  {
46  }
47 
48  // Implicit conversion doesn't lose information and allows return of symbol
49  // NOLINTNEXTLINE(runtime/explicit)
52  {
53  }
54 
55  bool is_success() const
56  {
57  return status == Success;
58  }
59  bool is_error() const
60  {
61  return status == Error;
62  }
63 };
64 
66 
69  const symbol_table_baset &symbol_table,
70  const irep_idt &main_class,
72 
74  const symbolt &symbol,
75  class symbol_table_baset &symbol_table,
76  class message_handlert &message_handler,
77  bool assume_init_pointers_not_null,
78  bool assert_uncaught_exceptions,
79  const java_object_factory_parameterst &object_factory_parameters,
80  const select_pointer_typet &pointer_type_selector);
81 
82 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
java_bytecode_language.h
select_pointer_type.h
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:40
main_function_resultt::statust
statust
Definition: java_entry_point.h:34
main_function_resultt::NotFound
Definition: java_entry_point.h:38
main_function_resultt::is_error
bool is_error() const
Definition: java_entry_point.h:59
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:55
main_function_resultt::status
enum main_function_resultt::statust status
get_main_symbol
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &)
Figures out the entry point of the code to verify.
Definition: java_entry_point.cpp:516
main_function_resultt::Success
Definition: java_entry_point.h:36
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
get_java_class_literal_initializer_signature
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
Definition: java_entry_point.cpp:90
select_pointer_typet
Definition: select_pointer_type.h:28
symbol.h
Symbol table entry.
message_handlert
Definition: message.h:24
main_function_resultt::main_function_resultt
main_function_resultt(statust status)
Definition: java_entry_point.h:44
main_function_resultt
Definition: java_entry_point.h:32
java_entry_point
bool java_entry_point(class symbol_table_baset &symbol_table, const irep_idt &main_class, class message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
Definition: java_entry_point.cpp:610
main_function_resultt::main_function_resultt
main_function_resultt(const symbolt &main_function)
Definition: java_entry_point.h:50
generate_java_start_function
bool generate_java_start_function(const symbolt &symbol, class symbol_table_baset &symbol_table, class message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Generate a _start function for a specific function.
Definition: java_entry_point.cpp:666
symbolt
Symbol table entry.
Definition: symbol.h:27
main_function_resultt::Error
Definition: java_entry_point.h:37
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:14
irep.h