search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

Example crashes the language server (or VSCode extension?) #1988

Open mschlaipfer opened 2 years ago

mschlaipfer commented 2 years ago 
datatype D = C0
method foo(d: D, s: string) returns (resD: D, resS: string)
  ensures old(d) == resD
  ensures old(s) == resS
{
  return (d,s);
}

Callstack: https://gist.github.com/mschlaipfer/379ee86a5105b6211e4f00ad4f463ce3 Dafny version: 3.5.0.40314 VSCode plugin: 2.3.0

keyboardDrummer commented 2 years ago

I can't reproduce this. It seems like you need a sequence of steps for this crash to occur.

Reproduced. Note that this problem also occurs on the Dafny CLI for 3.5.0.40314