-
Notifications
You must be signed in to change notification settings - Fork 36
-
Notifications
You must be signed in to change notification settings - Fork 36
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
Nested Bytecode Blocks #190
Comments
We can also simplify the issue of handling source annotations by using attribute maps? |
DavePearce
added a commit
that referenced
this issue
May 25, 2014
DavePearce
added a commit
that referenced
this issue
Aug 21, 2014
The purpose of this bytecode is as a stepping stone towards bytecode blocks (#190). Furthermore, to remove the e.g. assertge bytecodes, and replace them with fail bytecodes. This should reduce the number of path generated during verification condition generation.
Basically, done. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
An important issue is how to handle nested byte code blocks. After some thought, I've concluded this is primarily a UI issue. We want an API which doesn't have LoopEnd labels, and allows easy access to the contents of a nested block. There are two obvious approaches:
In thinking about this, I'm also wondering about labels for branches. Use of labels gives rise to the relabelling problem. That is, importing one block into another (e.g. inline pre-/post-conditions) means we have to relabel the incoming blocks to avoid name clashes. Perhaps this should be considered a minor issue?
The text was updated successfully, but these errors were encountered: