[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [xsmith-dev] Early Dafny Results (Re: XSmith questions)

Two more bugs:

- https://github.com/dafny-lang/dafny/issues/1356
- https://github.com/dafny-lang/dafny/issues/1357

The latter bug is not discovered by differential testing, and in fact can't be discovered by differential testing, because all Dafny compiler backends are buggy in the same way. However, it is discovered by our verification testing. We essentially correlate printed output with source location, and add assertions to those locations. We expect the Dafny static verifier to output verified, but it returns not verified.

On Tue, Jul 27, 2021 at 9:41 AM Sorawee Porncharoenwase <sorawee.pwase@gmail.com> wrote:
Hmm, that was not a hard bug. Apparently, Dafny intentionally limits the depth of an AST structure to be at most 20, causing the crash. Perhaps it should not crash like that, but it seems to "work" the way Dafny developers intend.

On Tue, Jul 27, 2021 at 9:33 AM Sorawee Porncharoenwase <sorawee.pwase@gmail.com> wrote:
Here's another one: https://github.com/dafny-lang/dafny/issues/1331

On Sun, Jul 25, 2021 at 11:20 AM John Regehr <regehr@cs.utah.edu> wrote:
This is cool. I hope someone is tweeting about it :)

John


On 7/25/21 12:08 AM, Sorawee Porncharoenwase wrote:
> Here's another one: https://github.com/dafny-lang/dafny/issues/1325
> <https://github.com/dafny-lang/dafny/issues/1325>
>
> On Tue, Jul 20, 2021 at 11:02 AM Eric Eide <eeide@cs.utah.edu
> <mailto:eeide@cs.utah.edu>> wrote:
>
>     Sorawee Porncharoenwase <sorawee.pwase@gmail.com
>     <mailto:sorawee.pwase@gmail.com>> writes:
>
>      > By the way, here are the results so far:
>      > - https://github.com/dafny-lang/dafny/issues/1291
>     <https://github.com/dafny-lang/dafny/issues/1291>
>      > - https://github.com/dafny-lang/dafny/issues/1297
>     <https://github.com/dafny-lang/dafny/issues/1297>
>
>     Thank you!  We are eager to keep track of these.
>
>     --
>     -------------------------------------------------------------------------------
>     Eric Eide <eeide@cs.utah.edu <mailto:eeide@cs.utah.edu>>   .       
>     University of Utah School of Computing
>     https://www.cs.utah.edu/~eeide/ <https://www.cs.utah.edu/~eeide/> .
>     +1 801-585-5512 .   Salt Lake City, Utah, USA
>