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.

Sign up for GitHub

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

Jump to bottom

Redundant- and contradictory-assumptions warnings are incorrectly formatted #4787

Closed
alex-chew opened this issue Nov 16, 2023 · 0 comments · Fixed by #4788
Closed

Redundant- and contradictory-assumptions warnings are incorrectly formatted #4787

alex-chew opened this issue Nov 16, 2023 · 0 comments · Fixed by #4788
Assignees
@atomb @alex-chew
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line

Comments

@alex-chew
Copy link
Contributor

Dafny version

master (f81c316)

Code to produce this issue

module M {
  opaque function ToSet(xs: seq<int>): set<int> {
    set x: int | x in xs
  }

  lemma LemmaCardinality(xs: seq<int>)
    ensures |ToSet(xs)| <= |xs|
  {}

  lemma LemmaEmpty(xs: seq<int>)
    requires xs == []
    ensures |ToSet(xs)| == 0
  {
    assume false;
  }
}

Command to run and resulting output

$ dafny verify --warn-redundant-assumptions --warn-contradictory-assumptions tmp.dfy
tmp.dfy(8,2): Error: a postcondition could not be proved on this return path
  |
8 |   {}
  |   ^

tmp.dfy(7,12): Related location: this is the postcondition that could not be proved
  |
7 |     ensures |ToSet(xs)| <= |xs|
  |             ^^^^^^^^^^^^^^^^^^^

   |
12 |     ensures |ToSet(xs)| == 0
   |             ^^^^^^^^^^^^^^^^

tmp.dfy(12,12): Warning: ensures clause proved using contradictory assumptions
   |
11 |     requires xs == []
   |              ^^^^^^^^

tmp.dfy(11,13): Warning: unnecessary requires clause

Dafny program verifier finished with 1 verified, 1 error

What happened?

The two errors and two warnings are all correct, but the warnings' messages are displayed below the code snippet context, whereas they should appear above the context.

What type of operating system are you experiencing the problem on?

Mac
@alex-chew alex-chew added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line labels Nov 16, 2023
@atomb atomb self-assigned this Nov 16, 2023
@alex-chew alex-chew mentioned this issue Nov 16, 2023
Merged
@alex-chew alex-chew self-assigned this Nov 16, 2023
alex-chew added a commit that referenced this issue Nov 16, 2023
@alex-chew
fix: print error context snippets after their messages (#4788)
1b89c34 
Fixes #4787.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@atomb atomb

@alex-chew alex-chew

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: CLI interacting with Dafny on the command line
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: print error context snippets after their messages alex-chew/dafny
2 participants
@atomb @alex-chew