/*******************************************************************\

Module: Synthetic methods map

Author: Chris Smowton, chris.smowton@diffblue.com

\*******************************************************************/

#ifndef CPROVER_JAVA_BYTECODE_SYNTHETIC_METHODS_MAP_H
#define CPROVER_JAVA_BYTECODE_SYNTHETIC_METHODS_MAP_H

/// \file
///   Synthetic methods are particular methods internally generated by the
///   Java frontend, including thunks to ensure static initializers are run once
///   and initializers created for unknown / stub types. Compare normal methods,
///   which are translated from Java bytecode. This file provides an
///   enumeration specifying the kind of a particular synthetic method and a
///   common type of a map giving a collection of synthetic methods.
///   Functions stubs and array.clone() functions are also generated by the Java
///   frontend but are not recorded using this framework, but may be in future.

/// Synthetic method kinds.
enum class synthetic_method_typet
{
  /// A static initializer wrapper
  /// (code of the form `if(!already_run) clinit(); already_run = true;`)
  /// These are generated for both user and stub types, to ensure the actual
  /// static initializer is only run once on any given path.
  STATIC_INITIALIZER_WRAPPER,
  /// A generated (synthetic) static initializer function for a stub type.
  /// Because we don't have the bytecode for a stub type (by definition), we
  /// generate a static initializer function to initialize its static fields.
  STUB_CLASS_STATIC_INITIALIZER
};

/// Maps method names on to a synthetic method kind.
typedef std::unordered_map<irep_idt, synthetic_method_typet>
  synthetic_methods_mapt;

#endif
