Language.Boogie.BasicBlocks

Basic block transformation for imperative Boogie code

Documentation

toBasicBlocks :: Block -> [BasicBlock]

Transform procedure body into a sequence of basic blocks. A basic block starts with a label and contains no jump, if or while statements, except for the last statement, which can be a goto or return.

startLabel :: [Char]

Label of the first block in a procedure