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 
23  std::function<std::pair<code_blockt, std::vector<exprt>>(
24  const symbolt &function,
25  symbol_table_baset &symbol_table)>;
26 
75 bool java_entry_point(
76  class symbol_table_baset &symbol_table,
77  const irep_idt &main_class,
78  class message_handlert &message_handler,
79  bool assume_init_pointers_not_null,
80  bool assert_uncaught_exceptions,
81  const java_object_factory_parameterst &object_factory_parameters,
82  const select_pointer_typet &pointer_type_selector,
83  bool string_refinement_enabled,
84  const build_argumentst &build_arguments);
85 
87 {
88  enum statust
89  {
92  NotFound
93  } status;
95 
96  // Implicit conversion doesn't lose information and allows return of status
97  // NOLINTNEXTLINE(runtime/explicit)
99  {
100  }
101 
102  // Implicit conversion doesn't lose information and allows return of symbol
103  // NOLINTNEXTLINE(runtime/explicit)
106  {
107  }
108 
109  bool is_success() const
110  {
111  return status == Success;
112  }
113  bool is_error() const
114  {
115  return status == Error;
116  }
117 };
118 
136 
139  const symbol_table_baset &symbol_table,
140  const irep_idt &main_class,
141  message_handlert &);
142 
155  const symbolt &symbol,
156  class symbol_table_baset &symbol_table,
157  class message_handlert &message_handler,
158  bool assert_uncaught_exceptions,
159  const java_object_factory_parameterst &object_factory_parameters,
160  const select_pointer_typet &pointer_type_selector,
161  const build_argumentst &build_arguments);
162 
181 std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
182  const symbolt &function,
183  symbol_table_baset &symbol_table,
184  bool assume_init_pointers_not_null,
185  java_object_factory_parameterst object_factory_parameters,
186  const select_pointer_typet &pointer_type_selector,
187  message_handlert &message_handler);
188 
191 void create_java_initialize(symbol_table_baset &symbol_table);
192 
195  symbol_table_baset &symbol_table,
196  const source_locationt &source_location,
197  bool assume_init_pointers_not_null,
198  java_object_factory_parameterst object_factory_parameters,
199  const select_pointer_typet &pointer_type_selector,
200  bool string_refinement_enabled,
201  message_handlert &message_handler);
202 
203 #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:37
java_bytecode_language.h
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:94
build_argumentst
std::function< std::pair< code_blockt, std::vector< exprt > >(const symbolt &function, symbol_table_baset &symbol_table)> build_argumentst
Definition: java_entry_point.h:25
java_build_arguments
std::pair< code_blockt, std::vector< exprt > > java_build_arguments(const symbolt &function, symbol_table_baset &symbol_table, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Definition: java_entry_point.cpp:287
main_function_resultt::statust
statust
Definition: java_entry_point.h:89
main_function_resultt::NotFound
@ NotFound
Definition: java_entry_point.h:92
create_java_initialize
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
Definition: java_entry_point.cpp:44
main_function_resultt::is_error
bool is_error() const
Definition: java_entry_point.h:113
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:109
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:514
main_function_resultt::Success
@ Success
Definition: java_entry_point.h:90
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
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:75
select_pointer_typet
Definition: select_pointer_type.h:26
symbol.h
Symbol table entry.
message_handlert
Definition: message.h:28
main_function_resultt::main_function_resultt
main_function_resultt(statust status)
Definition: java_entry_point.h:98
main_function_resultt::status
enum main_function_resultt::statust status
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, const build_argumentst &build_arguments)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
Definition: java_entry_point.cpp:568
main_function_resultt
Definition: java_entry_point.h:87
main_function_resultt::main_function_resultt
main_function_resultt(const symbolt &main_function)
Definition: java_entry_point.h:104
source_locationt
Definition: source_location.h:20
generate_java_start_function
bool generate_java_start_function(const symbolt &symbol, class symbol_table_baset &symbol_table, class message_handlert &message_handler, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, const build_argumentst &build_arguments)
Generate a _start function for a specific function.
Definition: java_entry_point.cpp:603
symbolt
Symbol table entry.
Definition: symbol.h:28
main_function_resultt::Error
@ Error
Definition: java_entry_point.h:91
java_static_lifetime_init
void java_static_lifetime_init(symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Adds the body to __CPROVER_initialize.
Definition: java_entry_point.cpp:106
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
irep.h