Foundations: finish definitions

manuscrit/20_foundations/20_code_analyzers.tex

@@ -435,6 +435,8 @@ straight-line code linked to other basic blocks to reflect control flow. We
 define this notion here formally, to use it soundly in the following chapters
 of this manuscript.
 
+\newpage  % FIXME
+
 \begin{notation}
     For the purposes of this section,
     \begin{itemize}
@@ -459,7 +461,21 @@ of this manuscript.
 \end{notation}
 
 \begin{definition}[Basic block decomposition]
-    \todo{}
+    Consider a sequence of assembly code $A$. We note the $J_A$ the set of jump
+    sites of $A$, $F_A$ the set of flow-altering instructions of $A$. As each
+    element of those sets is the address of an instruction, we note $F^+_A$ the
+    set of addresses of instructions \emph{directly following} an instruction
+    from $F_A$ ---~note that, as instructions may be longer than one byte, it
+    is not sufficient to increase by 1 each address from $F_A$.
+
+    We note $S_A = J_A \cup F^+_A$. We split the instructions from $A$ into
+    $BB(A)$, the set of segments that begin either at the beginning of $A$, or
+    at instructions from $S_A$ ---~less formally, we split $A$ at each point
+    from $S_A$, including each boundary in the following segment.
+
+    The members of $BB(A)$ are the \emph{basic blocks} of $A$, and are segments
+    of code which, by construction, will always be executed as straight-line
+    code, and whose execution will always begin from their first instruction.
 \end{definition}
 
 \begin{remark}