Currently, unnamed blocks are given Why3 block predicate names based on an internal counter. This does not correspond well to the order of the blocks in the actual LLVM code.
Blocks in LLVM are unordered- we have no guarantees about what blocks appear where in the block list. However, it may be good for usability if we attempt to reverse-engineer the original numbering of blocks, so Why3 block numbers map to the ones in the LLVM.
For instance, in this LLVM here:
define void @f() {
br label %1
br label %2
br label %3
ret void
}
the blocks could be named b_0, b_1, andb_3, and b_2 by WhyR, and that would be valid behavior. However, we would like them to be called b_0, b_1, etc. in ascending order, in the order they appeared in the function.
Currently, unnamed blocks are given Why3 block predicate names based on an internal counter. This does not correspond well to the order of the blocks in the actual LLVM code.
Blocks in LLVM are unordered- we have no guarantees about what blocks appear where in the block list. However, it may be good for usability if we attempt to reverse-engineer the original numbering of blocks, so Why3 block numbers map to the ones in the LLVM.
For instance, in this LLVM here:
the blocks could be named
b_0,b_1, andb_3, andb_2by WhyR, and that would be valid behavior. However, we would like them to be calledb_0,b_1, etc. in ascending order, in the order they appeared in the function.