Currently, the assembly analyzer is not aware of the control flow from jumps to labels.

This issue keeps track of

• disabling labels first
• implement checks that control-flow sources and destinations have named stack elements at the same positions
• enabling labels

Since the Solidity compiler has enough information about the jump sources and jump destinations, the labels and jumps can be annotated with enough information that witnesses the stack layout of the sources and destinations are compatible. The assembly analyzer needs to check the annotations.