diff options
author | Rustan Leino <unknown> | 2015-08-28 15:52:03 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2015-08-28 15:52:03 -0700 |
commit | cd441778a003d0c1af5b3b9e59efa69283f47e01 (patch) | |
tree | 70aa10c5192d59c8c464392e513345b0e5292896 /Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy | |
parent | d0fb19ff74b0397749362beedf39ffb8d1c623a9 (diff) |
Added tests for Boogie's new /verifySnapshots:3, which will be used by the Dafny emacs mode
Diffstat (limited to 'Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy')
-rw-r--r-- | Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy new file mode 100644 index 00000000..97fcfccb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy @@ -0,0 +1,29 @@ +method M(x: int)
+{ assert x < 20 || 10 <= x; // always true
+ assert x < 10; // error
+ Other(x); // error: precondition violation
+}
+
+method Other(y: int)
+ requires 0 <= y
+{
+}
+
+method Posty() returns (z: int)
+ ensures 2 <= z // error: postcondition violation
+{
+ var t := 20;
+ if t < z {
+ } else { // the postcondition violation occurs on this 'else' branch
+ }
+}
+
+method NoChangeWhazzoeva(u: int)
+{
+ assert u != 53; // error
+}
+
+method NoChangeAndCorrect()
+{
+ assert true;
+}
|