java_entry_point.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
#define CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
 
#include <util/irep.h>
#include <util/symbol.h>
 
class code_blockt; // IWYU pragma: keep
class select_pointer_typet;
class symbol_table_baset;
struct java_object_factory_parameterst;
 
#define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'"
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'"
 
using build_argumentst =
  std::function<std::pair<code_blockt, std::vector<exprt>>(
    const symbolt &function,
    symbol_table_baset &symbol_table)>;
 
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);
 
struct main_function_resultt
{
  enum statust
  {
    Success,
    Error,
    NotFound
  } status;
  enum statust {…};
  symbolt main_function;
 
  // Implicit conversion doesn't lose information and allows return of status
  // NOLINTNEXTLINE(runtime/explicit)
  main_function_resultt(statust status) : status(status)
  {
  }
  main_function_resultt(statust status) : status(status) {…}
 
  // Implicit conversion doesn't lose information and allows return of symbol
  // NOLINTNEXTLINE(runtime/explicit)
  main_function_resultt(const symbolt &main_function)
    : status(Success), main_function(main_function)
  {
  }
  main_function_resultt(const symbolt &main_function) {…}
 
  bool is_success() const
  {
    return status == Success;
  }
  bool is_success() const {…}
  bool is_error() const
  {
    return status == Error;
  }
  bool is_error() const {…}
};
struct main_function_resultt {…};
 
irep_idt get_java_class_literal_initializer_signature();
 
main_function_resultt get_main_symbol(
  const symbol_table_baset &symbol_table,
  const irep_idt &main_class,
  message_handlert &);
 
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);
 
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);
 
void create_java_initialize(symbol_table_baset &symbol_table);
 
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);
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H