Created by bitbucket user nadmuell on 2016-09-29 20:18
Last updated on 2020-02-17 18:23
The following code fails in Carbon and Viper:
#!scala
field f: Int
predicate p2(r:Ref)
{
acc(r.f) && r.f == 5
}
method m3(x1: Ref, x2:Ref)
requires acc(p2(x1))
requires acc(p2(x2))
{
assert forall r:Ref :: r in Set(x1, x2) ==> unfolding p2(r) in r.f == 5
}
Even though the fact that when unfolding a predicate in the Set(x1, x2) is known when checking the definedness of the statement, the assertion fails when asserting.
An example of something similar in Quantified Predicate Pemrissions is:
#!scala
field f: Int
predicate p2(r:Ref)
{
acc(r.f) && r.f == 5
}
method m2(x: Ref, xs:Set[Ref])
requires x in xs
requires forall r:Ref :: r in xs ==> acc(p2(r))
{
assert forall r:Ref :: r in xs ==> unfolding p2(r) in r.f == 5
}
This example fails in Carbon, but suceeds in Silicon.
The following code fails in Carbon and Viper:
Even though the fact that when unfolding a predicate in the Set(x1, x2) is known when checking the definedness of the statement, the assertion fails when asserting.
An example of something similar in Quantified Predicate Pemrissions is:
This example fails in Carbon, but suceeds in Silicon.