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

Insert {:axiom} quick fix fails on assume clauses #494

Open
masecla22 opened this issue Sep 3, 2024 · 0 comments
Open

Insert {:axiom} quick fix fails on assume clauses #494

masecla22 opened this issue Sep 3, 2024 · 0 comments

Comments

@masecla22
Copy link

Info

I'm working with the Dafny intergration for VSCode (v3.3.1) and I have upgraded to the latest version of Dafny (4.7.0)

Reproducing steps

  1. Open VSCode with Dafny Integration enabled
  2. Place the following code:
method Main() {
  assume 1+1==2; 
}
  1. Wait for assume statement has no {:axiom} annotationVerifier[r_assume_statement_without_axiom](https://dafny.org/dafny/HowToFAQ/Errors#r_assume_statement_without_axiom) warning to show up.
  2. Apply "insert {:axiom}" quick-fix
  3. Obtain the following code
method Main() {
  {:axiom}assume 1+1==2;
}

Expected behaviour

I would expect the axiom annotation to show up in the intended spot as such:

method Main() {
  assume {:axiom} 1+1==2;
}

Let me know if there is any further information I should add.

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

No branches or pull requests

1 participant