Apparent wildcard and possibly QP related incompleteness
marcoeilers opened this issue · 1 comments
marcoeilers commented
The following program verifies in Carbon, but results in a permission error in Silicon:
method keydict___init__() returns (self: Ref)
ensures forall key: Ref :: {keydict___item__(self, key)} acc(keydict___item__(self, key).keydict_val) && !keydict___contains__(self, key)
function keydict___item__(self: Ref, key: Ref): Ref
ensures keydict___item__inv(self, result) == key
function keydict___item__inv(self: Ref, val_ref: Ref): Ref
field keydict_val: Option[Ref]
function keydict___contains__(self: Ref, key: Ref) : Bool
requires acc(keydict___item__(self, key).keydict_val, wildcard)
ensures result == keydict___item__(self, key).keydict_val.isSome
adt Option[T] {
Some(value:T)
None()
}
marcoeilers commented
This was fixed in PR #817