applying-twice-qp-fields.vpr

field f: Int

// based on test7 in QPFields.vpr
method test14a(x: Ref)
    requires forall y: Ref :: true ==> acc(y.f)
{
    package (forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))

    x.f := 0
    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
    x.f := 1
    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true

    //:: ExpectedOutput(assert.failed:assertion.false)
    assert false
}

// based on test9 in QPFields.vpr
method test14b(x: Ref)
    requires forall y: Ref :: true ==> acc(y.f)
{
    package (forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)

    x.f := 0
    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
    x.f := 1
    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true

    //:: ExpectedOutput(assert.failed:assertion.false)
    assert false
}

// based on test11 in QPFields.vpr
method test14c(x: Ref, z: Ref)
    requires acc(x.f) && z != x
{
    package (forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
    inhale forall y: Ref :: y != x ==> acc(y.f)

    assert acc(z.f)

    z.f := 0
    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
    z.f := 1
    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true

    //:: ExpectedOutput(assert.failed:assertion.false)
    assert false
}