From ff0d676f5202ebecdd25a5dcdbbcd2480860857d Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sun, 17 May 2015 13:08:38 +0200 Subject: Updated test output after change in Boogie. --- Test/dafny0/snapshots/runtest.snapshot.expect | 45 ++++++++++++++++++++++----- 1 file changed, 37 insertions(+), 8 deletions(-) (limited to 'Test/dafny0/snapshots/runtest.snapshot.expect') diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index 8ad86f3b..f1050f62 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -6,12 +6,17 @@ 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##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $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); + >>> 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 $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 ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> MarkAsFullyVerified -Processing command (at ) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); +Processing command (at ) 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 @@ -31,7 +36,7 @@ Processing command (at Snapshots1.v0.dfy(12,3)) assert true; 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; + >>> 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 $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); @@ -62,7 +67,11 @@ Processing command (at Snapshots2.v0.dfy(18,3)) assert true; 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; + >>> 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 $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); @@ -73,11 +82,11 @@ Snapshots2.v1.dfy(4,10): Error: assertion violation Execution trace: (0,0): anon0 Processing command (at Snapshots2.v1.dfy(11,11)) assert true; - >>> MarkAsFullyVerified + >>> 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; - >>> MarkAsFullyVerified + >>> DoNothingToAssert Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap)); >>> DoNothingToAssert @@ -171,8 +180,28 @@ 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 ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##3(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##4(); + >>> AssumeNegationOfAssumptionVariable Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false); - >>> DoNothingToAssert + >>> MarkAsPartiallyVerified Snapshots7.v1.dfy(19,14): Error: assertion violation Execution trace: (0,0): anon0 -- cgit v1.2.3 From 82cd6194369a376e51a6b525e577f7cc8852ebef Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 20 Jul 2015 13:00:10 -0700 Subject: Split snapshot tests into separate files and add support for %S in runTests.py --- Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy | 8 + Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy | 8 + Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy | 13 ++ Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy | 13 ++ Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy | 19 +++ Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy | 19 +++ Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy | 11 ++ Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy | 11 ++ Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy | 11 ++ Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy | 12 ++ Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy | 26 +++ Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy | 27 +++ Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy | 23 +++ Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy | 23 +++ Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy | 22 +++ Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy | 22 +++ Test/dafny0/snapshots/Snapshots0.run.dfy | 2 + Test/dafny0/snapshots/Snapshots0.run.dfy.expect | 25 +++ Test/dafny0/snapshots/Snapshots0.v0.dfy | 8 - Test/dafny0/snapshots/Snapshots0.v1.dfy | 8 - Test/dafny0/snapshots/Snapshots1.run.dfy | 2 + Test/dafny0/snapshots/Snapshots1.run.dfy.expect | 21 +++ Test/dafny0/snapshots/Snapshots1.v0.dfy | 13 -- Test/dafny0/snapshots/Snapshots1.v1.dfy | 13 -- Test/dafny0/snapshots/Snapshots2.run.dfy | 2 + Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 41 +++++ Test/dafny0/snapshots/Snapshots2.v0.dfy | 19 --- Test/dafny0/snapshots/Snapshots2.v1.dfy | 19 --- Test/dafny0/snapshots/Snapshots3.run.dfy | 2 + Test/dafny0/snapshots/Snapshots3.run.dfy.expect | 18 ++ Test/dafny0/snapshots/Snapshots3.v0.dfy | 11 -- Test/dafny0/snapshots/Snapshots3.v1.dfy | 11 -- Test/dafny0/snapshots/Snapshots4.run.dfy | 2 + Test/dafny0/snapshots/Snapshots4.run.dfy.expect | 20 +++ Test/dafny0/snapshots/Snapshots4.v0.dfy | 11 -- Test/dafny0/snapshots/Snapshots4.v1.dfy | 12 -- Test/dafny0/snapshots/Snapshots5.run.dfy | 2 + Test/dafny0/snapshots/Snapshots5.run.dfy.expect | 26 +++ Test/dafny0/snapshots/Snapshots5.v0.dfy | 26 --- Test/dafny0/snapshots/Snapshots5.v1.dfy | 27 --- Test/dafny0/snapshots/Snapshots6.run.dfy | 2 + Test/dafny0/snapshots/Snapshots6.run.dfy.expect | 11 ++ Test/dafny0/snapshots/Snapshots6.v0.dfy | 23 --- Test/dafny0/snapshots/Snapshots6.v1.dfy | 23 --- Test/dafny0/snapshots/Snapshots7.run.dfy | 2 + Test/dafny0/snapshots/Snapshots7.run.dfy.expect | 31 ++++ Test/dafny0/snapshots/Snapshots7.v0.dfy | 22 --- Test/dafny0/snapshots/Snapshots7.v1.dfy | 22 --- Test/dafny0/snapshots/lit.local.cfg | 5 - Test/dafny0/snapshots/runtest.snapshot | 2 - Test/dafny0/snapshots/runtest.snapshot.expect | 209 ------------------------ Test/lit.site.cfg | 2 +- Test/runTests.py | 4 +- 53 files changed, 481 insertions(+), 486 deletions(-) create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots0.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots0.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots0.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots0.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots1.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots1.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots1.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots1.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots2.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots2.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots2.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots2.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots3.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots3.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots3.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots3.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots4.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots4.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots4.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots4.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots5.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots5.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots5.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots5.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots6.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots6.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots6.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots6.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots7.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots7.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots7.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots7.v1.dfy delete mode 100644 Test/dafny0/snapshots/lit.local.cfg delete mode 100644 Test/dafny0/snapshots/runtest.snapshot delete mode 100644 Test/dafny0/snapshots/runtest.snapshot.expect (limited to 'Test/dafny0/snapshots/runtest.snapshot.expect') diff --git a/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy new file mode 100644 index 00000000..73db9f9c --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy @@ -0,0 +1,8 @@ +method foo() +{ + bar(); + assert false; +} + +method bar() + ensures false; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy new file mode 100644 index 00000000..db9fc01a --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy @@ -0,0 +1,8 @@ +method foo() +{ + bar(); + assert false; // error +} + +method bar() + ensures true; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy new file mode 100644 index 00000000..34d066c3 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy @@ -0,0 +1,13 @@ +method M() +{ + N(); + assert false; +} + +method N() + ensures P(); + +predicate P() +{ + false +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy new file mode 100644 index 00000000..184ac65d --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy @@ -0,0 +1,13 @@ +method M() +{ + N(); + assert false; // error +} + +method N() + ensures P(); + +predicate P() +{ + true +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy new file mode 100644 index 00000000..727e177d --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy @@ -0,0 +1,19 @@ +method M() +{ + N(); + assert false; +} + +method N() + ensures P(); + +predicate P() + ensures P() == Q(); + +predicate Q() + ensures Q() == R(); + +predicate R() +{ + false +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy new file mode 100644 index 00000000..02a91b52 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy @@ -0,0 +1,19 @@ +method M() +{ + N(); + assert false; // error +} + +method N() + ensures P(); + +predicate P() + ensures P() == Q(); + +predicate Q() + ensures Q() == R(); + +predicate R() +{ + true +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy new file mode 100644 index 00000000..72607412 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy @@ -0,0 +1,11 @@ +method M() +{ + if (*) + { + + } + else + { + assert 0 != 0; // error + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy new file mode 100644 index 00000000..3b186318 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy @@ -0,0 +1,11 @@ +method M() +{ + if (*) + { + assert true; + } + else + { + assert 0 != 0; // error + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy new file mode 100644 index 00000000..beaadfeb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy @@ -0,0 +1,11 @@ +method M() +{ + if (*) + { + + } + else + { + assert 0 == 0; + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy new file mode 100644 index 00000000..cf9ae753 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy @@ -0,0 +1,12 @@ +method M() +{ + if (*) + { + assert 1 != 1; // error + } + else + { + assert 0 == 0; + assert 2 != 2; // error + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy new file mode 100644 index 00000000..b81c1a2b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy @@ -0,0 +1,26 @@ +method M() +{ + N(); + if (*) + { + + } + else + { + assert (forall b: bool :: b || !b) || 0 != 0; + } + N(); + assert (forall b: bool :: b || !b) || 3 != 3; + if (*) + { + + } + else + { + assert (forall b: bool :: b || !b) || 1 != 1; + } +} + + +method N() + ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy new file mode 100644 index 00000000..05dbced0 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy @@ -0,0 +1,27 @@ +method M() +{ + N(); + if (*) + { + + } + else + { + assert (forall b: bool :: b || !b) || 0 != 0; + } + N(); + assert (forall b: bool :: b || !b) || 3 != 3; + if (*) + { + + } + else + { + assert (exists b: bool :: b || !b) || 4 != 4; + } + assert (exists b: bool :: b || !b) || 5 != 5; +} + + +method N() + ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy new file mode 100644 index 00000000..c3742f4b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy @@ -0,0 +1,23 @@ +module M0 +{ + class C + { + method Foo() + { + assume false; + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo() + { + ...; + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy new file mode 100644 index 00000000..aeb520cb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy @@ -0,0 +1,23 @@ +module M0 +{ + class C + { + method Foo() + { + assume true; + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo() + { + ...; + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy new file mode 100644 index 00000000..27c7da5f --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy @@ -0,0 +1,22 @@ +module M0 +{ + class C + { + method Foo() + requires false; + { + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo... + { + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy new file mode 100644 index 00000000..b45dfe78 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy @@ -0,0 +1,22 @@ +module M0 +{ + class C + { + method Foo() + requires true; + { + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo... + { + assert false; + } + } +} 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 $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 $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 ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at ) 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/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy deleted file mode 100644 index 73db9f9c..00000000 --- a/Test/dafny0/snapshots/Snapshots0.v0.dfy +++ /dev/null @@ -1,8 +0,0 @@ -method foo() -{ - bar(); - assert false; -} - -method bar() - ensures false; diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy deleted file mode 100644 index db9fc01a..00000000 --- a/Test/dafny0/snapshots/Snapshots0.v1.dfy +++ /dev/null @@ -1,8 +0,0 @@ -method foo() -{ - bar(); - assert false; // error -} - -method bar() - ensures true; 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 $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 $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/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Snapshots1.v0.dfy deleted file mode 100644 index 34d066c3..00000000 --- a/Test/dafny0/snapshots/Snapshots1.v0.dfy +++ /dev/null @@ -1,13 +0,0 @@ -method M() -{ - N(); - assert false; -} - -method N() - ensures P(); - -predicate P() -{ - false -} diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy deleted file mode 100644 index 184ac65d..00000000 --- a/Test/dafny0/snapshots/Snapshots1.v1.dfy +++ /dev/null @@ -1,13 +0,0 @@ -method M() -{ - N(); - assert false; // error -} - -method N() - ensures P(); - -predicate P() -{ - true -} 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 $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 $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/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Snapshots2.v0.dfy deleted file mode 100644 index 727e177d..00000000 --- a/Test/dafny0/snapshots/Snapshots2.v0.dfy +++ /dev/null @@ -1,19 +0,0 @@ -method M() -{ - N(); - assert false; -} - -method N() - ensures P(); - -predicate P() - ensures P() == Q(); - -predicate Q() - ensures Q() == R(); - -predicate R() -{ - false -} diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Snapshots2.v1.dfy deleted file mode 100644 index 02a91b52..00000000 --- a/Test/dafny0/snapshots/Snapshots2.v1.dfy +++ /dev/null @@ -1,19 +0,0 @@ -method M() -{ - N(); - assert false; // error -} - -method N() - ensures P(); - -predicate P() - ensures P() == Q(); - -predicate Q() - ensures Q() == R(); - -predicate R() -{ - true -} 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/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Snapshots3.v0.dfy deleted file mode 100644 index 72607412..00000000 --- a/Test/dafny0/snapshots/Snapshots3.v0.dfy +++ /dev/null @@ -1,11 +0,0 @@ -method M() -{ - if (*) - { - - } - else - { - assert 0 != 0; // error - } -} diff --git a/Test/dafny0/snapshots/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Snapshots3.v1.dfy deleted file mode 100644 index 3b186318..00000000 --- a/Test/dafny0/snapshots/Snapshots3.v1.dfy +++ /dev/null @@ -1,11 +0,0 @@ -method M() -{ - if (*) - { - assert true; - } - else - { - assert 0 != 0; // 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/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Snapshots4.v0.dfy deleted file mode 100644 index beaadfeb..00000000 --- a/Test/dafny0/snapshots/Snapshots4.v0.dfy +++ /dev/null @@ -1,11 +0,0 @@ -method M() -{ - if (*) - { - - } - else - { - assert 0 == 0; - } -} diff --git a/Test/dafny0/snapshots/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Snapshots4.v1.dfy deleted file mode 100644 index cf9ae753..00000000 --- a/Test/dafny0/snapshots/Snapshots4.v1.dfy +++ /dev/null @@ -1,12 +0,0 @@ -method M() -{ - if (*) - { - assert 1 != 1; // error - } - else - { - assert 0 == 0; - assert 2 != 2; // error - } -} 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 $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 $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 $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 $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/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Snapshots5.v0.dfy deleted file mode 100644 index b81c1a2b..00000000 --- a/Test/dafny0/snapshots/Snapshots5.v0.dfy +++ /dev/null @@ -1,26 +0,0 @@ -method M() -{ - N(); - if (*) - { - - } - else - { - assert (forall b: bool :: b || !b) || 0 != 0; - } - N(); - assert (forall b: bool :: b || !b) || 3 != 3; - if (*) - { - - } - else - { - assert (forall b: bool :: b || !b) || 1 != 1; - } -} - - -method N() - ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Snapshots5.v1.dfy deleted file mode 100644 index 05dbced0..00000000 --- a/Test/dafny0/snapshots/Snapshots5.v1.dfy +++ /dev/null @@ -1,27 +0,0 @@ -method M() -{ - N(); - if (*) - { - - } - else - { - assert (forall b: bool :: b || !b) || 0 != 0; - } - N(); - assert (forall b: bool :: b || !b) || 3 != 3; - if (*) - { - - } - else - { - assert (exists b: bool :: b || !b) || 4 != 4; - } - assert (exists b: bool :: b || !b) || 5 != 5; -} - - -method N() - ensures (forall b: bool :: b || !b) || 2 != 2; 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/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Snapshots6.v0.dfy deleted file mode 100644 index c3742f4b..00000000 --- a/Test/dafny0/snapshots/Snapshots6.v0.dfy +++ /dev/null @@ -1,23 +0,0 @@ -module M0 -{ - class C - { - method Foo() - { - assume false; - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo() - { - ...; - assert false; - } - } -} diff --git a/Test/dafny0/snapshots/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Snapshots6.v1.dfy deleted file mode 100644 index aeb520cb..00000000 --- a/Test/dafny0/snapshots/Snapshots6.v1.dfy +++ /dev/null @@ -1,23 +0,0 @@ -module M0 -{ - class C - { - method Foo() - { - assume true; - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo() - { - ...; - assert false; - } - } -} 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 ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##3(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) 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/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Snapshots7.v0.dfy deleted file mode 100644 index 27c7da5f..00000000 --- a/Test/dafny0/snapshots/Snapshots7.v0.dfy +++ /dev/null @@ -1,22 +0,0 @@ -module M0 -{ - class C - { - method Foo() - requires false; - { - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo... - { - assert false; - } - } -} diff --git a/Test/dafny0/snapshots/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Snapshots7.v1.dfy deleted file mode 100644 index b45dfe78..00000000 --- a/Test/dafny0/snapshots/Snapshots7.v1.dfy +++ /dev/null @@ -1,22 +0,0 @@ -module M0 -{ - class C - { - method Foo() - requires true; - { - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo... - { - assert false; - } - } -} 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 $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 $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 ) a##cached##0 := a##cached##0 && ##extracted_function##1(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> MarkAsFullyVerified -Processing command (at ) 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 $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 $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 $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 $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 $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 $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 $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 $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 ) a##cached##0 := a##cached##0 && ##extracted_function##1(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##3(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at ) 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/lit.site.cfg b/Test/lit.site.cfg index 1fe593f4..a960bdbc 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -22,7 +22,7 @@ config.suffixes = ['.dfy'] # excludes: A list of directories to exclude from the testsuite. The 'Inputs' # subdirectories contain auxiliary inputs for various tests in their parent # directories. -config.excludes = [] +config.excludes = ['Inputs'] # test_source_root: The root path where tests are located. config.test_source_root = os.path.dirname(os.path.abspath(__file__)) diff --git a/Test/runTests.py b/Test/runTests.py index b8d8e6f4..d2bb61c9 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -34,7 +34,7 @@ except ImportError: pass class Defaults: - ALWAYS_EXCLUDED = ["Output", "snapshots", "sandbox", "desktop"] + ALWAYS_EXCLUDED = ["Inputs", "Output", "sandbox", "desktop"] DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:120"] @@ -108,7 +108,9 @@ class Test: self.timeout = timeout self.compiler_id = compiler_id self.cmds = [cmd.replace("%s", self.source_path) for cmd in self.cmds] + self.cmds = [cmd.replace("%S", self.source_directory) for cmd in self.cmds] self.cmds = [cmd.replace("%t", self.temp_output_path) for cmd in self.cmds] + self.cmds = [cmd.replace("%T", self.temp_directory) for cmd in self.cmds] self.status = TestStatus.PENDING self.proc_info = platform.processor() -- cgit v1.2.3