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,
26  bool assume_init_pointers_not_null,
27  bool assert_uncaught_exceptions,
28  const 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,
77  bool assume_init_pointers_not_null,
78  bool assert_uncaught_exceptions,
79  const object_factory_parameterst &object_factory_parameters,
80  const select_pointer_typet &pointer_type_selector);
81 
82 #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:30
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 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__...
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.
main_function_resultt(const symbolt &main_function)
main_function_resultt(statust status)
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class&#39; initializer method.
enum main_function_resultt::statust status
The symbol table base class interface.
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 object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Generate a _start function for a specific function.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...