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

[Sorawee Porncharoenwase]

Oh, and some rarely triggered bugs that have unique error messages are also
whitelisted, so that when they occur, they are not reported as errors.

On Sun, Aug 22, 2021 at 12:43 PM Sorawee Porncharoenwase <
sorawee.pwase at gmail.com> wrote:

> 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/ecb3c415/attachment.html>