triggerFoldPackage.vpr

// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

field f: Int

method m1(xs: Set[Ref], y: Ref, zs: Seq[Ref]) {
    inhale forall x: Ref :: x == y ==> acc(x.f)
    inhale forall x: Ref :: {acc(x.f) --* acc(y.f)} x in xs ==> acc(x.f) --* acc(y.f)
    assume forall x: Ref :: {acc(x.f) --* acc(y.f)} x in zs ==> x != y

    var z: Ref
    assume z in zs
    assume !(z in xs)
    package acc(z.f) --* acc(y.f)
    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
    //:: ExpectedOutput(assert.failed:assertion.false)
    assert z != y
}

method m2(xs: Set[Ref], ys: Set[Ref], z: Ref) {
    inhale forall x: Ref :: x == z ==> acc(x.f)
    inhale forall x: Ref :: {p1(x)} x in xs ==> p1(x)
    inhale forall x: Ref :: {p1(x)} x in ys ==> x != z

    var y: Ref
    assume !(y in xs)
    inhale acc(y.f)
    assume y in ys
    assume y.f == 0
    fold p1(y)
    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
    //:: MissingOutput(assert.failed:assertion.false, /carbon/issue/000/)
    //:: ExpectedOutput(assert.failed:assertion.false)
    assert y != z
}

method m3(xs: Seq[Ref], y: Ref, zs: Seq[Ref]) {
        inhale forall x: Ref :: x == y ==> acc(x.f)
        inhale forall x: Ref :: {acc(x.f) --* acc(y.f)} x in xs ==> acc(x.f) --* acc(y.f)

        var z: Ref
        assume z in zs
        assume !(z in xs)
        package acc(z.f) --* acc(y.f)
        assume forall x: Ref :: {acc(x.f) --* acc(y.f)} x in zs ==> x != y
        //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/000/)
        assert z != y
}

method m4(xs: Set[Ref], ys: Set[Ref], z: Ref) {
    inhale forall x: Ref :: x == z ==> acc(x.f)
    inhale forall x: Ref :: {p1(x)} x in xs ==> p1(x)

    var y: Ref
    assume !(y in xs)
    inhale acc(y.f)
    assume y in ys
    assume y.f == 0
    fold p1(y)
    inhale forall x: Ref :: {p1(x)} x in ys ==> x != z
    assert y != z
}

predicate p1(x: Ref) {
    acc(x.f) && x.f == 0
}