-
Notifications
You must be signed in to change notification settings - Fork 256
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
JavaScript compiler and labels issue #2608
Labels
logic
An inconsistency in Dafny's logic (e.g. in the Boogie prelude)
Comments
MikaelMayer
added
the
logic
An inconsistency in Dafny's logic (e.g. in the Boogie prelude)
label
Aug 17, 2022
Duplicate of #2576 for Javascript, but good catch re. soundness |
I'm closing this issue to track the problem in a separate issue dedicated to soundness problems coming from unbound variables: #2691. |
I'm reopening this issue because #2691 was tracking two issues that were independently resolved, and a third one which is this one. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The following code crashes a compiled JavaScript code.
bug_js.dfy:
The generated code is ill-formed, but it's not possible to see it until it's executed:
The text was updated successfully, but these errors were encountered: