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

Re: [xsmith-dev] XSmith questions

And it doesn't have global variables that you could lift to?

I ask mostly because I don't have a great answer for the other question.

(The answer should be “oh, you can specify types that a variable can't
be, and just use that when you make a decision that precludes certain
types without having to fully commit to a type”, as we've discussed,
but I still haven't implemented that.)

On Fri, Aug 27, 2021 at 04:03:30PM -0700, Sorawee Porncharoenwase wrote:
Oh, and about this question:

In Dafny do function expressions not generate closures?

It does, but an important part of the language is top-level function
expression definition, which would not have a lifting target.

So yes, choice-filters-to-apply seems like a solution, but see my above
question about how to use it properly.