Open jwkai opened 3 weeks ago
Is there any reason why this might be expected behaviour in Silicon, perhaps based on Silicon's heap model?
No, this is not expected, it's an incompleteness. I'll look into it.
Turns out there is an old issue that seems to describe the exact same problem (that I just didn't know about): #327
I'm working on a fix.
Thanks! Sorry, I had done a search through old issues, but I guess I had missed that one.
Hello,
I've found an unknown source of incompleteness in Silicon while working with heap-dependent functions that are set-valued (and hence require quantified permissions).
The following Viper code will verify in Carbon, but not Silicon:
(This is a minimized example; my original issue used a heap-dependent trigger on a limited version of
hfun
, i.e.{ hfun_prime(rs2) }
, and also had theassume (forall rs2 ...)
statement written as a postcondition forhfun
, but neither of these seem to be the source of incompleteness, so I have simplified things here.)On the other hand, Silicon (and Carbon) will verify a variant of this code where
hfun
is not set-valued and therefore lacks the precondition for quantified permissions:Is there any reason why this might be expected behaviour in Silicon, perhaps based on Silicon's heap model?