-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add test suite that I used while developing magic wand snap functions.
- Loading branch information
Showing
12 changed files
with
466 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
# Test Suite for Magic Wand Snap Functions | ||
|
||
This folder contains Viper test files that I used when working on MagicWandSnapFunctions for the Silicon project. | ||
|
||
## Overview | ||
|
||
| Name | Description | Expected Result | | ||
|----------------------------|-------------------------------------------------------------------------------------------------|-----------------| | ||
| [test01.vpr](./test01.vpr) | Boolean Magic Wand with trivial LHS | ✓ | | ||
| [test02.vpr](./test02.vpr) | Integer Magic Wand with trivial LHS | ✓ | | ||
| [test03.vpr](./test03.vpr) | Integer Magic Wand with LHS = RHS | ✓ | | ||
| [test04.vpr](./test04.vpr) | Integer Magic Wand with LHS < RHS | ✓ | | ||
| [test05.vpr](./test05.vpr) | Integer Magic Wand with LHS > RHS | ✓ | | ||
| [test06.vpr](./test06.vpr) | Applying the magic wand multiple times. Original version leaks information into the outer state | × | | ||
| [test07.vpr](./test07.vpr) | Assigning result of applying expression to the same field using booleans | × | | ||
| [test08.vpr](./test08.vpr) | Assigning result of applying expression to the same field using integers | × | | ||
| [test09.vpr](./test09.vpr) | Inhaling a magic wand | ✓ | | ||
| [test10.vpr](./test10.vpr) | Magic wand with predicates | ✓ | | ||
| [test11.vpr](./test11.vpr) | Iterate over a List | ✓ | | ||
|
||
Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were: | ||
* [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr) | ||
* [wands/new_syntax/QPFields.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPFields.vpr) | ||
* [wands/new_syntax/SnapshotsNestedMagicWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/SnapshotsNestedMagicWands.vpr) | ||
* [wands/regression/conditionals2.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/conditionals2.vpr) | ||
* [wands/regression/issue024.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue024.vpr) | ||
* [wands/regression/issue029.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue029.vpr) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
field b: Bool | ||
|
||
method test01a(x: Ref) | ||
{ | ||
inhale acc(x.b) && x.b | ||
|
||
package true --* acc(x.b) | ||
|
||
assert applying (true --* acc(x.b)) in x.b | ||
} | ||
|
||
method test01b(x: Ref) | ||
{ | ||
inhale acc(x.b) && x.b | ||
|
||
package true --* acc(x.b) | ||
|
||
apply true --* acc(x.b) | ||
|
||
assert x.b | ||
} | ||
|
||
method test01c(x: Ref) | ||
{ | ||
inhale acc(x.b) && x.b | ||
|
||
package true --* acc(x.b) | ||
|
||
assert applying (true --* acc(x.b)) in x.b | ||
|
||
apply true --* acc(x.b) | ||
|
||
assert x.b | ||
} | ||
|
||
method test01d(x: Ref, a: Bool) | ||
{ | ||
inhale acc(x.b) && x.b == a | ||
|
||
package true --* acc(x.b) | ||
|
||
assert applying (true --* acc(x.b)) in x.b == a | ||
|
||
apply true --* acc(x.b) | ||
|
||
assert x.b == a | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
field f: Int | ||
|
||
method test02a(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package true --* acc(x.f) | ||
|
||
assert applying (true --* acc(x.f)) in x.f == 42 | ||
} | ||
|
||
method test02b(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package true --* acc(x.f) | ||
|
||
apply true --* acc(x.f) | ||
|
||
assert x.f == 42 | ||
} | ||
|
||
method test02c(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package true --* acc(x.f) | ||
|
||
assert applying (true --* acc(x.f)) in x.f == 42 | ||
|
||
apply true --* acc(x.f) | ||
|
||
assert x.f == 42 | ||
} | ||
|
||
method test02d(x: Ref, a: Int) | ||
{ | ||
inhale acc(x.f) && x.f == a | ||
|
||
package true --* acc(x.f) | ||
|
||
assert applying (true --* acc(x.f)) in x.f == a | ||
|
||
apply true --* acc(x.f) | ||
|
||
assert x.f == a | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
field f: Int | ||
|
||
method test03a(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package acc(x.f) --* acc(x.f) | ||
|
||
assert applying (acc(x.f) --* acc(x.f)) in x.f == 42 | ||
} | ||
|
||
method test03b(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package acc(x.f) --* acc(x.f) | ||
|
||
apply acc(x.f) --* acc(x.f) | ||
|
||
assert x.f == 42 | ||
} | ||
|
||
method test03c(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package acc(x.f) --* acc(x.f) | ||
|
||
assert applying (acc(x.f) --* acc(x.f)) in x.f == 42 | ||
|
||
apply acc(x.f) --* acc(x.f) | ||
|
||
assert x.f == 42 | ||
} | ||
|
||
method test03d(x: Ref, a: Int) | ||
{ | ||
inhale acc(x.f) && x.f == a | ||
|
||
package acc(x.f) --* acc(x.f) | ||
|
||
assert applying (acc(x.f) --* acc(x.f)) in x.f == a | ||
|
||
apply acc(x.f) --* acc(x.f) | ||
|
||
assert x.f == a | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
field f: Int | ||
|
||
method test04a(x: Ref, y: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37 | ||
|
||
package acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37 | ||
} | ||
|
||
method test04b(x: Ref, y: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37 | ||
|
||
package acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
apply acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
assert x.f == 42 && y.f == 37 | ||
} | ||
|
||
method test04c(x: Ref, y: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37 | ||
|
||
package acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37 | ||
|
||
apply acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
assert x.f == 42 && y.f == 37 | ||
} | ||
|
||
method test04d(x: Ref, y: Ref, a: Int, b: Int) | ||
{ | ||
inhale acc(x.f) && x.f == a && acc(y.f) && y.f == b | ||
|
||
package acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == a && y.f == b | ||
|
||
apply acc(x.f) --* acc(x.f) && acc(y.f) | ||
|
||
assert x.f == a && y.f == b | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
field f: Int | ||
|
||
method test05a(x: Ref, y: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37 | ||
|
||
package acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == 42) && y.f == 37 | ||
} | ||
|
||
method test05b(x: Ref, y: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37 | ||
|
||
package acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
apply acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
assert x.f == 42 && acc(y.f, none) | ||
} | ||
|
||
method test05c(x: Ref, y: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37 | ||
|
||
package acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == 42) && y.f == 37 | ||
|
||
apply acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
assert x.f == 42 && acc(y.f, none) | ||
} | ||
|
||
method test05d(x: Ref, y: Ref, a: Int, b: Int) | ||
{ | ||
inhale acc(x.f) && x.f == a && acc(y.f) && y.f == b | ||
|
||
package acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == a) && y.f == b | ||
|
||
apply acc(x.f) && acc(y.f) --* acc(x.f) | ||
|
||
assert x.f == a && acc(y.f, none) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
field b: Bool | ||
|
||
method test06(x: Ref) { | ||
inhale acc(x.b) | ||
|
||
package acc(x.b) --* true | ||
|
||
x.b := true | ||
assert applying (acc(x.b) --* true) in true | ||
|
||
x.b := false | ||
assert applying (acc(x.b) --* true) in true | ||
|
||
//:: ExpectedOutput(assert.failed:assertion.false) | ||
assert false | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
field b: Bool | ||
|
||
method test07a(x: Ref) | ||
requires acc(x.b) | ||
{ | ||
package acc(x.b) --* acc(x.b) | ||
|
||
x.b := applying (acc(x.b) --* acc(x.b)) in !x.b | ||
|
||
apply acc(x.b) --* acc(x.b) | ||
|
||
assert acc(x.b) && x.b != old(x.b) | ||
|
||
//:: ExpectedOutput(assert.failed:assertion.false) | ||
assert false | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
field f: Int | ||
|
||
method test08a(x: Ref) | ||
requires acc(x.f) | ||
{ | ||
package acc(x.f) --* acc(x.f) | ||
|
||
x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1 | ||
|
||
apply acc(x.f) --* acc(x.f) | ||
|
||
assert acc(x.f) && x.f == old(x.f) + 1 | ||
//:: ExpectedOutput(assert.failed:assertion.false) | ||
assert false | ||
} | ||
|
||
method test08b(x: Ref) | ||
requires acc(x.f) && x.f == 42 | ||
{ | ||
package acc(x.f) --* acc(x.f) | ||
|
||
x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1 | ||
|
||
apply acc(x.f) --* acc(x.f) | ||
|
||
assert acc(x.f) && x.f == 43 | ||
//:: ExpectedOutput(assert.failed:assertion.false) | ||
assert false | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
field f: Int | ||
|
||
method test09a(x: Ref, y: Ref) | ||
requires acc(x.f) && x.f == 42 | ||
requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37 | ||
{ | ||
assert applying (acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37) in y.f == 37 | ||
} | ||
|
||
method test09b(x: Ref, y: Ref) | ||
requires acc(x.f) && x.f == 42 | ||
requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37 | ||
{ | ||
apply acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37 | ||
|
||
assert y.f == 37 | ||
} | ||
|
||
method test09c(x: Ref, y: Ref, z: Ref) | ||
requires acc(x.f) && x.f == 42 | ||
requires acc(x.f) --* acc(x.f) && acc(y.f) && acc(z.f) && y.f == 37 | ||
{ | ||
apply acc(x.f) --* acc(x.f) && acc(y.f) && acc(z.f) && y.f == 37 | ||
|
||
assert y.f == 37 | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
field f: Int | ||
field g: Int | ||
|
||
predicate foo(x: Ref) { | ||
acc(x.f) | ||
} | ||
|
||
method test10a(x: Ref) | ||
{ | ||
inhale foo(x) && unfolding foo(x) in x.f == 42 | ||
|
||
package foo(x) --* foo(x) | ||
|
||
apply foo(x) --* foo(x) | ||
|
||
assert foo(x) && unfolding foo(x) in x.f == 42 | ||
} | ||
|
||
method test10b(x: Ref) | ||
{ | ||
inhale acc(x.f) && x.f == 42 | ||
|
||
package acc(x.f) --* foo(x) { | ||
fold foo(x) | ||
} | ||
|
||
apply acc(x.f) --* foo(x) | ||
|
||
assert foo(x) && unfolding foo(x) in x.f == 42 | ||
} |
Oops, something went wrong.