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

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



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
>