diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-20 13:00:10 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-20 13:00:10 -0700 |
commit | 82cd6194369a376e51a6b525e577f7cc8852ebef (patch) | |
tree | f52e3788b9b685d3dba82b092934b1fad7273bd0 /Test/dafny0/snapshots | |
parent | 1f53d595ff0e4282ac51a68b124e94cd1af951ec (diff) |
Split snapshot tests into separate files and add support for %S in runTests.py
Diffstat (limited to 'Test/dafny0/snapshots')
35 files changed, 209 insertions, 216 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..05dbced0 100644 --- a/Test/dafny0/snapshots/Snapshots5.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy 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/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy new file mode 100644 index 00000000..cb96468e --- /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..96c280d9 --- /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 Lit(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 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
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy new file mode 100644 index 00000000..7c277b3e --- /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..878f9905 --- /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 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##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 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
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy new file mode 100644 index 00000000..889a8153 --- /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..a6a9bc4c --- /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 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##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 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;
+ >>> 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..3df182d6 --- /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..07e2d063 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -0,0 +1,18 @@ +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
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy new file mode 100644 index 00000000..fd6bef41 --- /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..fdc97775 --- /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 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
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy new file mode 100644 index 00000000..4f26aac4 --- /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 > "%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..2ad73416 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -0,0 +1,26 @@ +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
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy new file mode 100644 index 00000000..157fc5b7 --- /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..af440327 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect @@ -0,0 +1,11 @@ +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
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy new file mode 100644 index 00000000..b192f090 --- /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..7c073a9a --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect @@ -0,0 +1,31 @@ +Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(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 Lit(false);
+ >>> MarkAsPartiallyVerified
+Snapshots7.v1.dfy(19,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
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 f1050f62..00000000 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ /dev/null @@ -1,209 +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 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 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##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 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##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 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;
- >>> 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
-
--------------------- 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 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 Lit(false);
- >>> MarkAsPartiallyVerified
-Snapshots7.v1.dfy(19,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 3 verified, 1 error
|