From cd441778a003d0c1af5b3b9e59efa69283f47e01 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 28 Aug 2015 15:52:03 -0700 Subject: Added tests for Boogie's new /verifySnapshots:3, which will be used by the Dafny emacs mode --- Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy | 29 +++++++++++++ Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy | 33 +++++++++++++++ Test/dafny0/snapshots/Snapshots8.run.dfy | 2 + Test/dafny0/snapshots/Snapshots8.run.dfy.expect | 55 +++++++++++++++++++++++++ 4 files changed, 119 insertions(+) create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots8.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots8.run.dfy.expect (limited to 'Test/dafny0') 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; +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy new file mode 100644 index 00000000..8d8b215b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy @@ -0,0 +1,33 @@ +method M(x: int) +{ +assert x < 20 || 10 <= x; // always true + + assert x < 10; // error + Other(x); // error: precondition violation + assert x == 7; // error: this is a new error in v1 +} + + + method Other(y: int) + requires 0 <= y + { + } + + + +method Posty() returns (z: int) + ensures 2 <= z // error: postcondition violation +{ + var t := 20; + if t < z { + assert true; // this is a new assert + } else { // the postcondition violation occurs on this 'else' branch + } +} + + method NoChangeWhazzoeva(u: int) + { + assert u != 53; // error + } + +method NoChangeAndCorrect() { assert true; } diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy b/Test/dafny0/snapshots/Snapshots8.run.dfy new file mode 100644 index 00000000..00d20f91 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:3 /traceCaching:1 /errorTrace:0 "%S/Inputs/Snapshots8.dfy" > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect new file mode 100644 index 00000000..625b71b4 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect @@ -0,0 +1,55 @@ +Processing command (at Snapshots8.v0.dfy(2,37)) assert x#0 < 20 || LitInt(10) <= x#0; + >>> DoNothingToAssert +Processing command (at Snapshots8.v0.dfy(3,12)) assert x#0 < 10; + >>> DoNothingToAssert +Processing command (at Snapshots8.v0.dfy(4,9)) assert true; + >>> DoNothingToAssert +Processing command (at Snapshots8.v0.dfy(4,8)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> DoNothingToAssert +Processing command (at Snapshots8.v0.dfy(4,8)) assert LitInt(0) <= call0formal#AT#y#0; + >>> DoNothingToAssert +Snapshots8.v0.dfy(3,11): Error: assertion violation +Snapshots8.v0.dfy(4,7): Error BP5002: A precondition for this call might not hold. +Snapshots8.v0.dfy(8,13): Related location: This is the precondition that might not hold. +Processing command (at Snapshots8.v0.dfy(15,12)) assert true; + >>> DoNothingToAssert +Processing command (at Snapshots8.v0.dfy(13,13)) assert LitInt(2) <= z#0; + >>> DoNothingToAssert +Snapshots8.v0.dfy(17,9): Error BP5003: A postcondition might not hold on this return path. +Snapshots8.v0.dfy(13,12): Related location: This is the postcondition that might not hold. +Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53; + >>> DoNothingToAssert +Snapshots8.v0.dfy(23,11): Error: assertion violation +Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true); + >>> DoNothingToAssert + +Dafny program verifier finished with 7 verified, 4 errors +Processing command (at Snapshots8.v1.dfy(30,17)) assert u#0 != 53; + >>> RecycleError +Snapshots8.v1.dfy(30,16): Error: assertion violation +Processing command (at Snapshots8.v1.dfy(3,15)) assert x#0 < 20 || LitInt(10) <= x#0; + >>> MarkAsFullyVerified +Processing command (at Snapshots8.v1.dfy(5,17)) assert x#0 < 10; + >>> RecycleError +Processing command (at Snapshots8.v1.dfy(6,9)) assert true; + >>> MarkAsFullyVerified +Processing command (at Snapshots8.v1.dfy(6,8)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at Snapshots8.v1.dfy(6,8)) assert LitInt(0) <= call0formal#AT#y#0; + >>> RecycleError +Processing command (at Snapshots8.v1.dfy(7,12)) assert x#0 == LitInt(7); + >>> DoNothingToAssert +Snapshots8.v1.dfy(5,16): Error: assertion violation +Snapshots8.v1.dfy(6,7): Error BP5002: A precondition for this call might not hold. +Snapshots8.v1.dfy(12,20): Related location: This is the precondition that might not hold. +Snapshots8.v1.dfy(7,11): Error: assertion violation +Processing command (at Snapshots8.v1.dfy(21,12)) assert true; + >>> MarkAsFullyVerified +Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true); + >>> DoNothingToAssert +Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0; + >>> DoNothingToAssert +Snapshots8.v1.dfy(24,9): Error BP5003: A postcondition might not hold on this return path. +Snapshots8.v1.dfy(19,12): Related location: This is the postcondition that might not hold. + +Dafny program verifier finished with 7 verified, 5 errors -- cgit v1.2.3