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/Snapshots2.run.dfy.expect | |
| parent | 1f53d595ff0e4282ac51a68b124e94cd1af951ec (diff) | |
Split snapshot tests into separate files and add support for %S in runTests.py
Diffstat (limited to 'Test/dafny0/snapshots/Snapshots2.run.dfy.expect')
| -rw-r--r-- | Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 41 |
1 files changed, 41 insertions, 0 deletions
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
|