Add an overview of what lowerings are done

Author: thk123

jbmc/src/java_bytecode/README.md

@@ -6,6 +6,21 @@ This module provides a front end for Java.
 \section java-bytecode-conversion-section Overview of conversion from bytecode to codet
 
 To be documented.
+\subsection java-bytecode-lowering-to-goto Lowering to GOTO
+
+The Java language contains high level programming concepts like virtual functions and throw/catch semantics. We need to rewrite these in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering".
+
+The following lowering operations are done on java bytecode after converting into a basic codet representation.
+
+- \ref java-bytecode-runtime-exceptions "Add runtime exceptions"
+- \ref java-bytecode-remove-java-new "Remove new calls"
+- \ref java-bytecode-remove-exceptions "Remove thrown exceptions"
+- As well as other non-java specific transformations (see \ref goto-programs for details on these)
+
+These are performed in `process_goto_function` for example
+\ref jbmc_parse_optionst::process_goto_function
+
+Once these lowerings have been completed, you have a GOTO model that can be analysed.
 
 \section java-bytecode-object-factory Object Factory