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

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

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@cs.utah.edu> wrote:
Sorawee Porncharoenwase <sorawee.pwase@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@cs.utah.edu>   .        University of Utah School of Computing
https://www.cs.utah.edu/~eeide/ . +1 801-585-5512 .   Salt Lake City, Utah, USA