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

[Sorawee Porncharoenwase]

Great question! I have an overly complicated setup to deal with this issue.

- Yesterday, I did submit a couple of PRs to fix some of these bugs:
https://github.com/dafny-lang/dafny/pull/1368,
https://github.com/dafny-lang/dafny/pull/1369, and
https://github.com/dafny-lang/dafny/pull/1370. And just now I finished
implementing a patcher that takes as input a list of PRs and applies them
before compiling Dafny
- Some constructs are needed to be disabled temporarily to not trigger
known bugs
- Some other bugs (mostly printing issues) can be temporarily suppressed by
normalizing the outputs before comparing them.

But yes, the situation is not ideal and does slow me down.

On Sun, Aug 22, 2021 at 12:32 PM Eric Eide <eeide at cs.utah.edu> wrote:

> Sorawee Porncharoenwase <sorawee.pwase at gmail.com> writes:
>
> > Two more bugs:
> >
> > - https://github.com/dafny-lang/dafny/issues/1372
> > - https://github.com/dafny-lang/dafny/issues/1373
>
> Thanks!
>
> I've noticed that these bugs are not being resolved very quickly.  As I
> look
> now, you have 16 open issues and zero closed.  (One open bug is labeled
> with
> "resolution"?)
>
> Is this slowing down you?  After a while, it becomes hard to find new bugs
> if
> old ones are not resolved.  (Because the fuzzer hits the same bugs over an
> over.)
>
> Eric.
>
> --
>
> -------------------------------------------------------------------------------
> Eric Eide <eeide at cs.utah.edu>   .        University of Utah School of
> Computing
> 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/20210822/7e7355bd/attachment.html>