java_bytecode_convert_method.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: JAVA Bytecode Language Conversion
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
 
#include "java_bytecode_convert_method_class.h"
#include "java_bytecode_parse_tree.h"
 
class class_hierarchyt;
class prefix_filtert;
 
void java_bytecode_initialize_parameter_names(
  symbolt &method_symbol,
  const java_bytecode_parse_treet::methodt::local_variable_tablet
    &local_variable_table,
  symbol_table_baset &symbol_table);
 
void java_bytecode_convert_method(
  const symbolt &class_symbol,
  const java_bytecode_parse_treet::methodt &,
  symbol_table_baset &symbol_table,
  message_handlert &message_handler,
  size_t max_array_length,
  bool throw_assertion_error,
  std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
  java_string_library_preprocesst &string_preprocess,
  const class_hierarchyt &class_hierarchy,
  bool threading_support,
  const std::optional<prefix_filtert> &method_context,
  bool assert_no_exceptions_thrown);
 
void create_method_stub_symbol(
  const irep_idt &identifier,
  const irep_idt &base_name,
  const irep_idt &pretty_name,
  const typet &type,
  const irep_idt &declaring_class,
  symbol_table_baset &symbol_table,
  message_handlert &message_handler);
 
void java_bytecode_convert_method_lazy(
  symbolt &class_symbol,
  const irep_idt &method_identifier,
  const java_bytecode_parse_treet::methodt &,
  symbol_table_baset &symbol_table,
  message_handlert &);
 
typedef expanding_vectort<std::vector<java_bytecode_convert_methodt::variablet>>
  variablest;
 
void create_parameter_names(
  const java_bytecode_parse_treet::methodt &m,
  const irep_idt &method_identifier,
  java_method_typet::parameterst &parameters,
  const java_bytecode_convert_methodt::method_offsett &slots_for_parameters);
 
void create_parameter_symbols(
  const java_method_typet::parameterst &parameters,
  variablest &variables,
  symbol_table_baset &symbol_table);
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H