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

[Sorawee Porncharoenwase]

Two more issues:

- https://github.com/dafny-lang/dafny/issues/1414
- https://github.com/dafny-lang/dafny/issues/1414#issuecomment-912142122

There are also a lot more bugs discovered related to multiset with zero
multiplicity. The bugs are scattered in several functions, but they all
stem from misunderstanding the invariant of the data structure, so I don't
know how to count the number of bugs properly. Perhaps we should count it
as one for each affected language?

On Sat, Aug 28, 2021 at 1:05 PM Sorawee Porncharoenwase <
sorawee.pwase at gmail.com> wrote:

> Two more issues (though I filed them together in one bug report, to not
> clutter GitHub issues)
>
> https://github.com/dafny-lang/dafny/issues/1402
>
> On Fri, Aug 27, 2021 at 4:31 AM Sorawee Porncharoenwase <
> sorawee.pwase at gmail.com> wrote:
>
>> One more bug:
>>
>> https://github.com/dafny-lang/dafny/issues/1397
>>
>> On Fri, Aug 27, 2021 at 2:36 AM Sorawee Porncharoenwase <
>> sorawee.pwase at gmail.com> wrote:
>>
>>> Two more bugs:
>>> - https://github.com/dafny-lang/dafny/issues/1396
>>> - https://github.com/dafny-lang/dafny/issues/1395
>>>
>>> The latter, again, is not discovered by the fuzzer, but by trying to
>>> formalizing it (well, I still couldn't implement it either -- see the
>>> original thread for the problem and question).
>>>
>>> On Thu, Aug 26, 2021 at 4:49 AM Sorawee Porncharoenwase <
>>> sorawee.pwase at gmail.com> wrote:
>>>
>>>> Here's another bug: https://github.com/dafny-lang/dafny/issues/1387
>>>>
>>>> On Tue, Aug 24, 2021 at 2:40 PM Sorawee Porncharoenwase <
>>>> sorawee.pwase at gmail.com> wrote:
>>>>
>>>>> One more bug:
>>>>>
>>>>> https://github.com/dafny-lang/dafny/issues/1384
>>>>>
>>>>> On Sun, Aug 22, 2021 at 5:34 PM Sorawee Porncharoenwase <
>>>>> sorawee.pwase at gmail.com> wrote:
>>>>>
>>>>>> More bugs!
>>>>>>
>>>>>> -
>>>>>> https://github.com/dafny-lang/dafny/issues/1372#issuecomment-903359423
>>>>>> - https://github.com/dafny-lang/dafny/issues/1374
>>>>>>
>>>>>> On Sun, Aug 22, 2021 at 12:56 PM John Regehr <regehr at cs.utah.edu>
>>>>>> wrote:
>>>>>>
>>>>>>> I'm just sort of lurking here, but I've really been enjoying this
>>>>>>> thread. Great work everyone!!!
>>>>>>>
>>>>>>> > The latter one is not discovered by fuzzing itself. I was writing
>>>>>>> a type
>>>>>>> > constraint to be put in the fuzzer, and thinking what will happen
>>>>>>> if we
>>>>>>> > violate the constraint, so I tried it out manually and discovered
>>>>>>> the issue.
>>>>>>>
>>>>>>> In my experience this happens a lot :)
>>>>>>>
>>>>>>> John
>>>>>>>
>>>>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210902/5beaf38c/attachment.html>