diff options
Diffstat (limited to 'Test/dafny0/snapshots')
39 files changed, 339 insertions, 189 deletions
diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy index 73db9f9c..73db9f9c 100644 --- a/Test/dafny0/snapshots/Snapshots0.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy index db9fc01a..db9fc01a 100644 --- a/Test/dafny0/snapshots/Snapshots0.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy index 34d066c3..34d066c3 100644 --- a/Test/dafny0/snapshots/Snapshots1.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy index 184ac65d..184ac65d 100644 --- a/Test/dafny0/snapshots/Snapshots1.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy index 727e177d..727e177d 100644 --- a/Test/dafny0/snapshots/Snapshots2.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy index 02a91b52..02a91b52 100644 --- a/Test/dafny0/snapshots/Snapshots2.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy diff --git a/Test/dafny0/snapshots/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy index 72607412..72607412 100644 --- a/Test/dafny0/snapshots/Snapshots3.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy index 3b186318..3b186318 100644 --- a/Test/dafny0/snapshots/Snapshots3.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy diff --git a/Test/dafny0/snapshots/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy index beaadfeb..beaadfeb 100644 --- a/Test/dafny0/snapshots/Snapshots4.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy index cf9ae753..cf9ae753 100644 --- a/Test/dafny0/snapshots/Snapshots4.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy diff --git a/Test/dafny0/snapshots/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy index b81c1a2b..b81c1a2b 100644 --- a/Test/dafny0/snapshots/Snapshots5.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy index 05dbced0..7b207d74 100644 --- a/Test/dafny0/snapshots/Snapshots5.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy @@ -17,9 +17,9 @@ method M() }
else
{
- assert (exists b: bool :: b || !b) || 4 != 4;
+ assert (exists b: bool :: true) || 4 != 4;
}
- assert (exists b: bool :: b || !b) || 5 != 5;
+ assert (exists b: bool :: true) || 5 != 5;
}
diff --git a/Test/dafny0/snapshots/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy index c3742f4b..c3742f4b 100644 --- a/Test/dafny0/snapshots/Snapshots6.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy index aeb520cb..aeb520cb 100644 --- a/Test/dafny0/snapshots/Snapshots6.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy diff --git a/Test/dafny0/snapshots/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy index 27c7da5f..27c7da5f 100644 --- a/Test/dafny0/snapshots/Snapshots7.v0.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy diff --git a/Test/dafny0/snapshots/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy index b45dfe78..b45dfe78 100644 --- a/Test/dafny0/snapshots/Snapshots7.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy 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/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy new file mode 100644 index 00000000..5e016c12 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots0.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect new file mode 100644 index 00000000..bf7388cf --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -0,0 +1,25 @@ +Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> DoNothingToAssert
+Processing command (at Snapshots0.v0.dfy(4,10)) assert false;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 3 verified, 0 errors
+Processing implementation CheckWellformed$$_module.__default.bar (at Snapshots0.v1.dfy(7,8)):
+ >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
+ >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##2(call0old#AT#$Heap, $Heap) } ##extracted_function##2(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots0.v1.dfy(4,10)) assert false;
+ >>> MarkAsPartiallyVerified
+Snapshots0.v1.dfy(4,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 2 verified, 1 error
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy new file mode 100644 index 00000000..1907f4a0 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots1.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect new file mode 100644 index 00000000..1b5c8d24 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect @@ -0,0 +1,21 @@ +Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> DoNothingToAssert
+Processing command (at Snapshots1.v0.dfy(4,10)) assert false;
+ >>> DoNothingToAssert
+Processing command (at Snapshots1.v0.dfy(12,3)) assert true;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 4 verified, 0 errors
+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots1.v1.dfy(4,10)) assert false;
+ >>> DoNothingToAssert
+Snapshots1.v1.dfy(4,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy new file mode 100644 index 00000000..71f3e18a --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots2.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect new file mode 100644 index 00000000..949ecec9 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -0,0 +1,41 @@ +Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v0.dfy(4,10)) assert false;
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v0.dfy(14,11)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 6 verified, 0 errors
+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing implementation CheckWellformed$$_module.__default.P (at Snapshots2.v1.dfy(10,11)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1.dfy(13,11)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots2.v1.dfy(4,10)) assert false;
+ >>> DoNothingToAssert
+Snapshots2.v1.dfy(4,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v1.dfy(14,11)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 5 verified, 1 error
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy b/Test/dafny0/snapshots/Snapshots3.run.dfy new file mode 100644 index 00000000..40dd1012 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots3.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect new file mode 100644 index 00000000..a7f05a68 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -0,0 +1,18 @@ +Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0;
+ >>> DoNothingToAssert
+Snapshots3.v0.dfy(9,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+
+Dafny program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots3.v1.dfy(5,12)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0;
+ >>> RecycleError
+Snapshots3.v0.dfy(9,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+
+Dafny program verifier finished with 1 verified, 1 error
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy new file mode 100644 index 00000000..803403cf --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots4.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect new file mode 100644 index 00000000..e0f07849 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect @@ -0,0 +1,20 @@ +Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 2 verified, 0 errors
+Processing command (at Snapshots4.v1.dfy(5,14)) assert 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots4.v1.dfy(10,14)) assert 2 != 2;
+ >>> DoNothingToAssert
+Snapshots4.v1.dfy(5,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+Snapshots4.v1.dfy(10,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+
+Dafny program verifier finished with 1 verified, 2 errors
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy new file mode 100644 index 00000000..096df53c --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" /autoTriggers:1 > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect new file mode 100644 index 00000000..8cc44882 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -0,0 +1,35 @@ +Snapshots5.v0.dfy(10,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(13,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(20,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v0.dfy(26,11): Warning: /!\ No terms found to trigger on.
+Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> DoNothingToAssert
+Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> DoNothingToAssert
+Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
+ >>> DoNothingToAssert
+Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 3 verified, 0 errors
+Snapshots5.v1.dfy(10,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(13,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(20,12): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(22,10): Warning: /!\ No terms found to trigger on.
+Snapshots5.v1.dfy(27,11): Warning: /!\ No terms found to trigger on.
+Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots5.v1.dfy(20,37)) assert (exists b#5: bool :: Lit(true)) || 4 != 4;
+ >>> DoNothingToAssert
+Processing command (at Snapshots5.v1.dfy(22,35)) assert (exists b#7: bool :: Lit(true)) || 5 != 5;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy new file mode 100644 index 00000000..8f958cb9 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots6.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect new file mode 100644 index 00000000..cdb942bb --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect @@ -0,0 +1,11 @@ +Processing command (at Snapshots6.v0.dfy(20,14)) assert false;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 4 verified, 0 errors
+Processing command (at Snapshots6.v1.dfy(20,14)) assert false;
+ >>> DoNothingToAssert
+Snapshots6.v1.dfy(20,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy new file mode 100644 index 00000000..c84c41d2 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots7.dfy" > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect new file mode 100644 index 00000000..a08b32c6 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect @@ -0,0 +1,31 @@ +Processing command (at Snapshots7.v0.dfy(19,14)) assert false;
+ >>> DoNothingToAssert
+
+Dafny program verifier finished with 4 verified, 0 errors
+Processing implementation CheckWellformed$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):
+ >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing implementation Impl$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):
+ >>> added axiom: ##extracted_function##2() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##2();
+Processing implementation CheckWellformed$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):
+ >>> added axiom: ##extracted_function##3() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##3();
+Processing implementation Impl$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):
+ >>> added axiom: ##extracted_function##4() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##4();
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##3();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##4();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots7.v1.dfy(19,14)) assert false;
+ >>> MarkAsPartiallyVerified
+Snapshots7.v1.dfy(19,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
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..e1cbdbe0 --- /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<alpha> $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 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<alpha> $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 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
diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg deleted file mode 100644 index 07cb869f..00000000 --- a/Test/dafny0/snapshots/lit.local.cfg +++ /dev/null @@ -1,5 +0,0 @@ -# This test is unusual in that we don't use the .bpl files -# directly on the command line. So instead we'll invoke -# files in this directory with extension '.snapshot'. There -# will only be one for now -config.suffixes = ['.snapshot'] diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot deleted file mode 100644 index 62ccabb3..00000000 --- a/Test/dafny0/snapshots/runtest.snapshot +++ /dev/null @@ -1,2 +0,0 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy Snapshots4.dfy Snapshots5.dfy Snapshots6.dfy Snapshots7.dfy > "%t" -// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect deleted file mode 100644 index 8ad86f3b..00000000 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ /dev/null @@ -1,180 +0,0 @@ -
--------------------- Snapshots0.dfy --------------------
-Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> DoNothingToAssert
-Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 3 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
- >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
-Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
- >>> MarkAsPartiallyVerified
-Snapshots0.v1.dfy(4,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 2 verified, 1 error
-
--------------------- Snapshots1.dfy --------------------
-Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> DoNothingToAssert
-Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
- >>> DoNothingToAssert
-Processing command (at Snapshots1.v0.dfy(12,3)) assert true;
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 4 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
- >>> DoNothingToAssert
-Snapshots1.v1.dfy(4,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 3 verified, 1 error
-
--------------------- Snapshots2.dfy --------------------
-Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,11)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 6 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
- >>> DoNothingToAssert
-Snapshots2.v1.dfy(4,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
- >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,11)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 5 verified, 1 error
-
--------------------- Snapshots3.dfy --------------------
-Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);
- >>> DoNothingToAssert
-Snapshots3.v0.dfy(9,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-
-Dafny program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);
- >>> DoNothingToAssert
-Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);
- >>> RecycleError
-Snapshots3.v0.dfy(9,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-
-Dafny program verifier finished with 1 verified, 1 error
-
--------------------- Snapshots4.dfy --------------------
-Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 2 verified, 0 errors
-Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);
- >>> DoNothingToAssert
-Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);
- >>> DoNothingToAssert
-Snapshots4.v1.dfy(5,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-Snapshots4.v1.dfy(10,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-
-Dafny program verifier finished with 1 verified, 2 errors
-
--------------------- Snapshots5.dfy --------------------
-Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
- >>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1;
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 3 verified, 0 errors
-Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4;
- >>> DoNothingToAssert
-Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5;
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 3 verified, 0 errors
-
--------------------- Snapshots6.dfy --------------------
-Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false);
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 4 verified, 0 errors
-Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);
- >>> DoNothingToAssert
-Snapshots6.v1.dfy(20,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 3 verified, 1 error
-
--------------------- Snapshots7.dfy --------------------
-Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false);
- >>> DoNothingToAssert
-
-Dafny program verifier finished with 4 verified, 0 errors
-Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);
- >>> DoNothingToAssert
-Snapshots7.v1.dfy(19,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 3 verified, 1 error
|