Skip to content

Commit

Permalink
Remove some invalid test annotations.
Browse files Browse the repository at this point in the history
  • Loading branch information
stefanheule committed Jul 12, 2013
1 parent 77668d5 commit 2a0bf7a
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 9 deletions.
18 changes: 10 additions & 8 deletions src/test/resources/all/chalice/nestedPredicates.sil
Original file line number Diff line number Diff line change
Expand Up @@ -44,14 +44,14 @@
requires acc(this.p(), wildcard)
{
unfold acc(this.p(), wildcard)
//:: ExpectedError(assertion.false)
assert ((this) != (this.next))
if (((this.next) != (null))) {
unfold acc(this.next.q(), wildcard)
//:: ExpectedError(assertion.false)
assert ((this.next) != (this.next.next))
assert ((this) != (this.next.next))
}
//:: ExpectedError(assertion.false)
assert false
}
method testNestingFoldTwo(this: Ref)
requires acc(this.next, wildcard) && acc(this.value, wildcard)
Expand All @@ -63,12 +63,11 @@
, wildcard)
{
fold acc(this.next.q(), wildcard)
//:: ExpectedError(assertion.false)
assert ((this) != (this.next))
//:: ExpectedError(assertion.false)
assert ((this.next) != (this.next.next))
//:: ExpectedError(assertion.false)
assert ((this) != (this.next.next))
//:: ExpectedError(assertion.false)
assert false
}
method testNestingFoldThree(this: Ref)
requires acc(this.next, wildcard) && acc(this.value, wildcard)
Expand All @@ -86,20 +85,21 @@
fold acc(this.next.q(), wildcard)
fold acc(this.p(), wildcard)
assert ((this) != (this.next))
//:: ExpectedError(assertion.false)
assert ((this.next) != (this.next.next))
assert ((this) != (this.next.next))
//:: ExpectedError(assertion.false)
assert false
}
method testNestingUnfoldingTwo(this: Ref)
requires acc(this.p(), wildcard)
{
//:: ExpectedError(assertion.false)
assert ((this) != ((unfolding acc(this.p(), wildcard) in this.next)))
if ((((unfolding acc(this.p(), wildcard) in this.next)) != (null))) {
//:: ExpectedError(assertion.false)
assert (((unfolding acc(this.p(), wildcard) in this.next)) != ((unfolding acc(this.p(), wildcard) in (unfolding acc(this.next.q(), wildcard) in this.next.next))))
assert ((this) != ((unfolding acc(this.p(), wildcard) in (unfolding acc(this.next.q(), wildcard) in this.next.next))))
}
//:: ExpectedError(assertion.false)
assert false
}
method testNestingUnfoldingPrecondition(this: Ref, x: Ref)
requires acc(this.valid(), wildcard) && (unfolding acc(this.valid(), wildcard) in ((this.next) == (x)))
Expand All @@ -113,4 +113,6 @@
requires acc(this.valid(), wildcard)
ensures acc(this.valid(), wildcard) && (unfolding acc(this.valid(), wildcard) in true)
{
//:: ExpectedError(assertion.false)
assert false
}
1 change: 0 additions & 1 deletion src/test/resources/all/predicates/receiverless.sil
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ predicate valid(b: Bool) {
method t1(this: Ref, b: Bool)
requires acc(false.valid(), write)
{
//:: ExpectedError(assert.failed:assertion.false)
assert false
}

Expand Down

0 comments on commit 2a0bf7a

Please sign in to comment.