steps

docs/prover/diagnosis/index.md

@@ -38,11 +38,31 @@ inlined on the TAC source code level.
     callee's CFG. Intuitively, this set can be viewed as one CFG with nested 
     sub-CFGs for the calls.
 
-The upper-mid left part of a TAC report contains the source code box.
-
-
-
-### TAC source code box
+The upper-mid left part of a TAC report contains the TAC source code. The
+details the TAC language are outside the scope of this documentation. Generally
+speaking, TAC is generated by compiler-style transformations of the EVM bytecode
+together with the CVL specification. Many patterns from EVM bytecode are
+retained in TAC, however inlining of functions and various simplifications have
+already happenend. Especially since the source code in the TAC reports is taken
+from a stage directly before the SMT solving. The source code is useful because
+it "speaks the truth", i.e., it has all the summarizations and inlinings and
+optimizations already applied, it is very close to what the SMT solver sees.
+There are source code pointers in the TAC, too. These are the statements with a
+dotted underline; the source code location they have been translated from is
+revealed on hovering with the mouse over such a statement, as displayed in the
+image below.
+
+![Source pointer is shown on hover](source-pointer-on-hover-annotated.png)
+
+The call-based navigation on the mid-right side of the report lists all the
+calls. Each call is identified by a number. After the number there is a number
+of arrows, indicating the nesting depth of the call. After that the name of the
+called method is given. Each of these calls is clickable and will lead to the
+corresponding CFG.
+
+At the bottom of the TAC report are the successor and predecessor relations of
+the CFG on a per-block/per-node basis. These are usually not useful for the tool
+user, so we will ignore them in the remainder of this document.
 
 ## SAT TAC reports