Marco Eilers
Marco Eilers
The trigger generation code (I think only in Silicon?) does it when all possible trigger expressions it finds in the quantifier body contain arithmetic, like in this example. ``offset(start, 0...
As far as I know that's correct, yes.
For what it's worth, Silicon crashes if it gets an impure assertion in this position. So if we get rid of the consistency check, we'll also need to extend the...
For what it's worth, I updated the floating point support PRs; there were some discussions between Malte and I but I think we agreed that we could merge it in...
Right. That PR only supports IEEE floats though, not reals in the ordinary sense. Those should be easy to support, too, but we'd basically have to build it into Viper...
Note: I thought at first that this could be fixed by just doing the self-framing check for the exhale version of the precondition from an arbitrary valid mask instead of...
Hey, thanks a lot! To be honest, I don't think I was 100% certain that we never merge quantified chunks. We should definitely do that at least sometimes. I'll need...
I finally started looking into this, sorry this took so long. Regarding this last point: > it seem to also [speed up] if I disable merging quantified heap chunks by...
These also fail: ``` method m2(r: Ref) { inhale acc(r.f, flag() ? write : none) var tmp : Int tmp := assuming(flag(), r).f } method m3(r: Ref) { inhale acc(r.f,...