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

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

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@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@gmail.com> wrote:
One more bug:


On Fri, Aug 27, 2021 at 2:36 AM Sorawee Porncharoenwase <sorawee.pwase@gmail.com> wrote:
Two more bugs:

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@gmail.com> wrote:

On Tue, Aug 24, 2021 at 2:40 PM Sorawee Porncharoenwase <sorawee.pwase@gmail.com> wrote:

On Sun, Aug 22, 2021 at 5:34 PM Sorawee Porncharoenwase <sorawee.pwase@gmail.com> wrote:

On Sun, Aug 22, 2021 at 12:56 PM John Regehr <regehr@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