Document synthetic methods generated by the Java frontend

src/java_bytecode/java_bytecode_language.h

@@ -172,6 +172,10 @@ class java_bytecode_languaget:public languaget
 
 private:
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
+
+  /// Maps synthetic method names on to the particular type of synthetic method
+  /// (static initializer, initializer wrapper, etc). For full documentation see
+  /// synthetic_method_map.h
   synthetic_methods_mapt synthetic_methods;
   stub_global_initializer_factoryt stub_global_initializer_factory;
   class_hierarchyt class_hierarchy;

src/java_bytecode/synthetic_methods_map.h

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Java Static Initializers
+Module: Synthetic methods map
 
 Author: Chris Smowton, [email protected]
 
@@ -9,12 +9,31 @@ Author: Chris Smowton, [email protected]
 #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, irep_id_hash>
   synthetic_methods_mapt;