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

Sorawee Porncharoenwase sorawee.pwase at gmail.com
Tue Jul 27 10:41:11 MDT 2021


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/20210727/8686a71b/attachment.html>


More information about the xsmith-dev mailing list