Document, overlay classes, overlay methods and ignored methods

Future improvements:
 - move this documentation to a better place
 - add tests for ignored methods

Author: Owen Jones

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -118,11 +118,43 @@ class java_bytecode_convert_classt:public messaget
   // see definition below for more info
   static void add_array_types(symbol_tablet &symbol_table);
 
+  /// Check if a method is an overlay method by searching for
+  /// `ID_overlay_method` in its list of annotations.
+  ///
+  /// An overlay method is a method with the annotation
+  /// \@OverlayMethodImplementation. They should only appear in
+  /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class). They
+  /// will be loaded by JBMC instead of the corresponding method in the
+  /// underlying class. It is an error if there is no corresponding
+  /// method in the underlying class. It is an error if a method in the overlay
+  /// class matches a method in the underlying class and it isn't marked as
+  /// an overlay method or an
+  /// [ignored method](\ref java_bytecode_convert_classt::is_ignored_method).
+  ///
+  /// \param method: a `methodt` object from a java bytecode parse tree
+  /// \return true if the method is an overlay method, else false
   static bool is_overlay_method(const methodt &method)
   {
     return method.has_annotation(ID_overlay_method);
   }
 
+  /// Check if a method is an ignored method by searching for
+  /// `ID_ignored_method` in its list of annotations.
+  ///
+  /// An ignored method is a method with the annotation
+  /// \@IgnoredMethodImplementation. They will be ignored by JBMC. They are
+  /// intended for use in
+  /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class), in
+  /// particular for methods which must exist in the overlay class so that
+  /// it will compile, e.g. default constructors, but which we do not want
+  /// to overlay the corresponding method in the
+  /// underlying class. It is an error if a method in the overlay class
+  /// matches a method in the underlying class and it isn't marked as
+  /// an [overlay method](\ref java_bytecode_convert_classt::is_overlay_method)
+  /// or an ignored method.
+  ///
+  /// \param method: a `methodt` object from a java bytecode parse tree
+  /// \return true if the method is an overlay method, else false
   static bool is_ignored_method(const methodt &method)
   {
     return method.has_annotation(ID_ignored_method);

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -69,9 +69,22 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
 }
 
 /// Check if class is an overlay class by searching for `ID_overlay_class` in
-/// its list of annotations. TODO(nathan) give a short explanation about what
-/// overlay classes are.
-/// \param c: a `classt` object from a java byte code parse tree
+/// its list of annotations.
+///
+/// An overlay class is a class with the annotation
+/// \@OverlayClassImplementation. They serve the following purpose. When the JVM
+/// searches the classpath for a particular class, it uses the first one
+/// that matches, and ignores any later matching ones. JBMC, however,
+/// will take account of other matching ones which are overlay classes. The
+/// overlay classes can change the methods of the first matching class in the
+/// following ways: adding a field (by having a new field), adding a method
+/// (by having a new method) or
+/// [changing the definition of a method](\ref java_bytecode_convert_classt::is_overlay_method).
+/// When there is a method which is required for the overlay class to compile
+/// but which should not be an overlay method then it should be marked as an
+/// [ignored method](\ref java_bytecode_convert_classt::is_ignored_method).
+///
+/// \param c: a `classt` object from a java bytecode parse tree
 /// \return true if parsed class is an overlay class, else false
 static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
 {