Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve automatic numbering of unnamed blocks #1

Open
iconmaster5326 opened this issue Oct 21, 2016 · 0 comments
Open

Improve automatic numbering of unnamed blocks #1

iconmaster5326 opened this issue Oct 21, 2016 · 0 comments
Labels

Comments

@iconmaster5326
Copy link
Member

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant