Skip to content

Improve automatic numbering of unnamed blocks #1

@iconmaster5326

Description

@iconmaster5326

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions