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

Dafny verifies program with NPE #1377

Closed
mschlaipfer opened this issue Aug 23, 2021 · 0 comments · Fixed by #1383
Closed

Dafny verifies program with NPE #1377

mschlaipfer opened this issue Aug 23, 2021 · 0 comments · Fixed by #1383
Assignees
@RustanLeino
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude)

Comments

@mschlaipfer
Copy link
Member

The following program verifies and crashes with a NPE:

module Test {
  class C1 {
    method crash() {}
  }

  trait T {
    function method baz(): C1
  }

  class C2 extends T {
    constructor () {}
    function method baz(): C1? {
      null
    }
  }

  method bar(x: T) {
    assert x.baz() != null;
    x.baz().crash();
  }

  method Main() {
    var e := new C2();
    bar(e);
  }
}
> $ ../dafny/dafny /compile:3 ../tmp/test.dfy                
test.dfy(23,19): Warning: the type of the other operand is a non-null type, so this comparison with 'null' will always return 'true'

Dafny program verifier finished with 3 verified, 0 errors
Running...

Error: Execution resulted in exception: Exception has been thrown by the target of an invocation.
System.NullReferenceException: Object reference not set to an instance of an object.
   at Test_Compile.__default.bar(T x)
   at Test_Compile.__default._Main()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)
@mschlaipfer mschlaipfer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) labels Aug 23, 2021
@RustanLeino RustanLeino self-assigned this Aug 24, 2021
@RustanLeino RustanLeino mentioned this issue Aug 24, 2021
Merged
keyboardDrummer pushed a commit that referenced this issue Aug 25, 2021
@RustanLeino
fix: Check type equality in override signatures (#1383)
2ca4677 
Previously, the type-equality checks for overriding methods/functions ignored type constraints. With this PR, the proper type equality is used.

Note, one can imagine allowing some co-/contra-variance among the parameters in an override. That would indeed be sound, but it may cause complications in compilation, since target languages may have different rules. Therefore, I suggest we continue to insist on type equality in Dafny. If a strong need for co-/contra-variance comes up, we can consider changing the language.

Fixes #1377
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RustanLeino RustanLeino

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Check type equality in override signatures RustanLeino/dafny
2 participants
@mschlaipfer @RustanLeino