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

[Sorawee Porncharoenwase]

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 at 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 at 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 at 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 at cs.utah.edu
>>> > <mailto:eeide at cs.utah.edu>> wrote:
>>> >
>>> >     Sorawee Porncharoenwase <sorawee.pwase at gmail.com
>>> >     <mailto:sorawee.pwase at 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 at cs.utah.edu <mailto:eeide at 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
>>> >
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210819/e7598ddd/attachment.html>