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 has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
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.
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__...
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
std::function< std::pair< code_blockt, std::vector< exprt > >(const symbolt &function, symbol_table_baset &symbol_table)> build_argumentst
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.
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.
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)
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
main_function_resultt(const symbolt &main_function)
enum main_function_resultt::statust status
main_function_resultt(statust status)
Symbol table entry.