Open DavePearce opened 2 years ago
Summary:
debug=true
this example doesn't verify because of a generated loop invariant involving HEAP
for p
But why doesn't it fail when debug=false
?
When debug=true
loop invariant is:
invariant (forall r:Ref :: Ref#within(HEAP$173,r,p) || (HEAP$173[r] == Void) || (HEAP$173[r] == HEAP[r]));
When debug=false
we have:
invariant (forall r:Ref :: Ref#within(HEAP$173,r,p$78) || (HEAP$173[r] == Void) || (HEAP$173[r] == HEAP[r]));
Hmmm that's not it
Ok, here we go:
When debug=true
we have this for g()
:
free ensures (forall p:Ref :: Ref#within(old(HEAP),p,p) || ...);
When debug=false
we have this:
free ensures (forall p:Ref :: Ref#within(old(HEAP),p,p$23) || ...);
These are not equivalent.
In the earlier version of the translator to Boogie, I used a weaker version of this 'debug' name mapping, maintained a map from each fully qualified name to its 'printable' name.
For example, for a base name of 'p', the first printable name would be just 'p', then other fully qualified variants of it would be mapped to 'p1', 'p2', etc. (a separate counter for each base name). This allows the most common cases (identifiers that appear only once) to retain their original names, but it still disambiguates other names when needed, with a short and readable name.
(One could make this even more sophisticated by taking detailed scopes into consideration, but a simple version that has just two levels of scope, global and local, would work pretty well I think).
Hey,
In general, expressions are already associated with a unique identifier and I typically use this. Not sure what's going wrong here. Its not a ideal, but not a big drama now I know the problem.
(@utting @leavens keeping you in the loop)
The following program generates a strange error message indeed:
UPDATE: this is related to
debug=true
in thewy.toml
file.