From 19895aaed833d16bad36a07e9459abc882ccd6b6 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 24 Jun 2014 10:44:38 -0700 Subject: Invert LHS sub-expressions in forall assignment statements, which gives the opportunity to designate a good trigger. --- Test/vstte2012/RingBufferAuto.dfy | 18 ++++++++++++++++++ Test/vstte2012/RingBufferAuto.dfy.expect | 2 +- 2 files changed, 19 insertions(+), 1 deletion(-) (limited to 'Test/vstte2012') diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy index a9d36932..a4bdf0a0 100644 --- a/Test/vstte2012/RingBufferAuto.dfy +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -56,6 +56,24 @@ class {:autocontracts} RingBuffer Contents := Contents + [x]; } + method ResizingEnqueue(x: T) + ensures Contents == old(Contents) + [x] && N >= old(N); + { + if data.Length == len { + var more := data.Length + 1; + var d := new T[data.Length + more]; + forall i | 0 <= i < data.Length { + d[if i < start then i else i + more] := data[i]; + } + N, data, start := N + more, d, if len == 0 then 0 else start + more; + } + var nextEmpty := if start + len < data.Length + then start + len else start + len - data.Length; + data[nextEmpty] := x; + len := len + 1; + Contents := Contents + [x]; + } + method Dequeue() returns (x: T) requires Contents != []; modifies Repr; diff --git a/Test/vstte2012/RingBufferAuto.dfy.expect b/Test/vstte2012/RingBufferAuto.dfy.expect index aeb37948..b06ff8fc 100644 --- a/Test/vstte2012/RingBufferAuto.dfy.expect +++ b/Test/vstte2012/RingBufferAuto.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 13 verified, 0 errors +Dafny program verifier finished with 15 verified, 0 errors -- cgit v1.2.3 From 39a8abe0d2d6e4bda54fb3a481b049c19fe1dba9 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 1 Jul 2014 17:52:52 +0200 Subject: Removed the old test infrastructure. --- Test/Makefile | 17 - Test/VSComp2010/Answer | 20 - Test/VSComp2010/runtest.bat | 15 - Test/VSI-Benchmarks/Answer | 32 - Test/VSI-Benchmarks/runtest.bat | 13 - Test/alltests.txt | 10 - Test/cloudmake/Answer | 12 - Test/cloudmake/runtest.bat | 7 - Test/dafny0/Answer | 2616 ------------------------------------- Test/dafny0/runtest.bat | 61 - Test/dafny1/Answer | 124 -- Test/dafny1/runtest.bat | 26 - Test/dafny2/Answer | 60 - Test/dafny2/runtest.bat | 27 - Test/dafny3/Answer | 64 - Test/dafny3/runtest.bat | 19 - Test/dafny4/Answer | 43 - Test/dafny4/runtest.bat | 7 - Test/runtest.bat | 39 - Test/runtestall.bat | 24 - Test/vacid0/Answer | 12 - Test/vacid0/AnswerRuntimeChecking | 0 Test/vacid0/runtest.bat | 13 - Test/vstte2012/Answer | 24 - Test/vstte2012/runtest.bat | 23 - 25 files changed, 3308 deletions(-) delete mode 100644 Test/Makefile delete mode 100644 Test/VSComp2010/Answer delete mode 100644 Test/VSComp2010/runtest.bat delete mode 100644 Test/VSI-Benchmarks/Answer delete mode 100644 Test/VSI-Benchmarks/runtest.bat delete mode 100644 Test/alltests.txt delete mode 100644 Test/cloudmake/Answer delete mode 100644 Test/cloudmake/runtest.bat delete mode 100644 Test/dafny0/Answer delete mode 100644 Test/dafny0/runtest.bat delete mode 100644 Test/dafny1/Answer delete mode 100644 Test/dafny1/runtest.bat delete mode 100644 Test/dafny2/Answer delete mode 100644 Test/dafny2/runtest.bat delete mode 100644 Test/dafny3/Answer delete mode 100644 Test/dafny3/runtest.bat delete mode 100644 Test/dafny4/Answer delete mode 100644 Test/dafny4/runtest.bat delete mode 100644 Test/runtest.bat delete mode 100644 Test/runtestall.bat delete mode 100644 Test/vacid0/Answer delete mode 100644 Test/vacid0/AnswerRuntimeChecking delete mode 100644 Test/vacid0/runtest.bat delete mode 100644 Test/vstte2012/Answer delete mode 100644 Test/vstte2012/runtest.bat (limited to 'Test/vstte2012') diff --git a/Test/Makefile b/Test/Makefile deleted file mode 100644 index 6e02aed0..00000000 --- a/Test/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -TESTS_FILE = alltests.txt -LONG = $(shell awk '{ if (tolower($$2) ~ /^long$$/) print $$1 }' $(TESTS_FILE)) -NORMAL = $(shell awk '{ if (tolower($$2) ~ /^use$$/) print $$1 }' $(TESTS_FILE)) -TESTS = $(NORMAL) - -all: dafny - -dafny: $(addprefix rundfy-, $(TESTS)) - -rundfy-%: - @cmd /c "runtest.bat $* $(FLAGS)" || : - -long: - $(MAKE) TESTS="$(NORMAL) $(LONG)" all - -show: - @echo $(TESTS) diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer deleted file mode 100644 index ff491aa5..00000000 --- a/Test/VSComp2010/Answer +++ /dev/null @@ -1,20 +0,0 @@ - --------------------- Problem1-SumMax.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Problem2-Invert.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- Problem3-FindZero.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- Problem4-Queens.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- Problem5-DoubleEndedQueue.dfy -------------------- - -Dafny program verifier finished with 21 verified, 0 errors diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat deleted file mode 100644 index 2cfcdafb..00000000 --- a/Test/VSComp2010/runtest.bat +++ /dev/null @@ -1,15 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* Problem1-SumMax.dfy Problem2-Invert.dfy Problem3-FindZero.dfy Problem4-Queens.dfy Problem5-DoubleEndedQueue.dfy - -rem for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy -rem Problem3-FindZero.dfy Problem4-Queens.dfy -rem Problem5-DoubleEndedQueue.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer deleted file mode 100644 index 2a4587f4..00000000 --- a/Test/VSI-Benchmarks/Answer +++ /dev/null @@ -1,32 +0,0 @@ - --------------------- b1.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- b2.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- b3.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- b4.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- b5.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- b6.dfy -------------------- - -Dafny program verifier finished with 21 verified, 0 errors - --------------------- b7.dfy -------------------- - -Dafny program verifier finished with 23 verified, 0 errors - --------------------- b8.dfy -------------------- - -Dafny program verifier finished with 42 verified, 0 errors diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat deleted file mode 100644 index f950cf2a..00000000 --- a/Test/VSI-Benchmarks/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy - -rem for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/alltests.txt b/Test/alltests.txt deleted file mode 100644 index c586a561..00000000 --- a/Test/alltests.txt +++ /dev/null @@ -1,10 +0,0 @@ -dafny0 Use Dafny functionality tests -dafny1 Use Various Dafny examples -dafny2 Use More Dafny examples -dafny3 Use And more Dafny examples -dafny4 Use More, more, more! -cloudmake Use CloudMake formalization and proofs -VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges -vacid0 Use Dafny attempts to VACID Edition 0 benchmarks -vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition -VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer deleted file mode 100644 index 3758853e..00000000 --- a/Test/cloudmake/Answer +++ /dev/null @@ -1,12 +0,0 @@ - --------------------- CloudMake-ParallelBuilds.dfy -------------------- - -Dafny program verifier finished with 244 verified, 0 errors - --------------------- CloudMake-CachedBuilds.dfy -------------------- - -Dafny program verifier finished with 104 verified, 0 errors - --------------------- CloudMake-ConsistentBuilds.dfy -------------------- - -Dafny program verifier finished with 59 verified, 0 errors diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat deleted file mode 100644 index 8fc7ccbb..00000000 --- a/Test/cloudmake/runtest.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer deleted file mode 100644 index dc3f1eda..00000000 --- a/Test/dafny0/Answer +++ /dev/null @@ -1,2616 +0,0 @@ - --------------------- Simple.dfy -------------------- -// Simple.dfy - -class MyClass { - var x: int; - - method M(s: bool, lotsaObjects: set) - returns (t: object, u: set, v: seq>) - requires s; - modifies this, lotsaObjects; - ensures t == t; - ensures old(null) != this; - { - x := 12; - while x < 100 - invariant x <= 100; - { - x := x + 17; - if x % 20 == 3 { - x := this.x + 1; - } else { - this.x := x + 0; - } - t, u, v := M(true, lotsaObjects); - var to: MyClass; - to, u, v := this.M(true, lotsaObjects); - to, u, v := to.M(true, lotsaObjects); - assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10]; - } - } - - function F(x: int, y: int, h: WildData, k: WildData): WildData - { - if x < 0 then - h - else if x == 0 then - if if h == k then true else false then - h - else if y == 0 then - k - else - h - else - k - } -} - -datatype List = Nil | Cons(T, List) - -datatype WildData = Something | JustAboutAnything(bool, myName: set, int, WildData) | More(List) - -class C { - var w: WildData; - var list: List; -} - -lemma M(x: int) - ensures x < 8; -{ -} - -colemma M'(x': int) - ensures true; -{ -} - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- TypeTests.dfy -------------------- -TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D) -TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C) -TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int) -TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int) -TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool) -TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C) -TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int) -TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -TypeTests.dfy(56,6): Error: Duplicate local-variable name: z -TypeTests.dfy(58,6): Error: Duplicate local-variable name: x -TypeTests.dfy(61,8): Error: Duplicate local-variable name: x -TypeTests.dfy(64,6): Error: Duplicate local-variable name: y -TypeTests.dfy(70,11): Error: unresolved identifier: x -TypeTests.dfy(72,28): Error: unresolved identifier: z -TypeTests.dfy(73,29): Error: unresolved identifier: w1 -TypeTests.dfy(73,47): Error: unresolved identifier: w0 -TypeTests.dfy(76,28): Error: unresolved identifier: e -TypeTests.dfy(91,17): Error: member F in type C does not refer to a method -TypeTests.dfy(92,17): Error: a method called as an initialization method must not have any result arguments -TypeTests.dfy(101,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(103,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(105,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement) -TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type -TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(115,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(116,8): Error: sorry, cannot instantiate 'array' type with a subrange type -TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts -TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed -33 resolution/type errors detected in TypeTests.dfy - --------------------- NatTypes.dfy -------------------- -NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 -NatTypes.dfy(34,10): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - NatTypes.dfy(22,3): anon10_LoopHead - (0,0): anon10_LoopBody - NatTypes.dfy(22,3): anon11_Else - (0,0): anon12_Then -NatTypes.dfy(41,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -NatTypes.dfy(43,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -NatTypes.dfy(60,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -NatTypes.dfy(74,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -NatTypes.dfy(107,45): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - -Dafny program verifier finished with 15 verified, 9 errors - --------------------- RealTypes.dfy -------------------- -RealTypes.dfy(8,23): Error: assertion violation -Execution trace: - (0,0): anon0 -RealTypes.dfy(14,12): Error: possible division by zero -Execution trace: - (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else - (0,0): anon2 -RealTypes.dfy(14,20): Error: assertion violation -Execution trace: - (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else - (0,0): anon2 -RealTypes.dfy(22,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 6 verified, 4 errors - --------------------- Definedness.dfy -------------------- -Definedness.dfy(11,7): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Definedness.dfy(18,16): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(27,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(28,21): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Definedness.dfy(29,17): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(36,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(45,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(53,18): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(54,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(53,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(60,18): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(61,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(60,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(68,3): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(67,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Definedness.dfy(88,7): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(89,5): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 -Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Definedness.dfy(89,10): Error: target object may be null -Execution trace: - (0,0): anon0 -Definedness.dfy(90,10): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 -Definedness.dfy(95,14): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(95,23): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(96,15): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(101,12): Error: possible division by zero -Execution trace: - (0,0): anon0 -Definedness.dfy(108,15): Error: possible division by zero -Execution trace: - Definedness.dfy(108,5): anon7_LoopHead - (0,0): anon7_LoopBody - Definedness.dfy(108,5): anon8_Else -Definedness.dfy(117,23): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(116,5): anon12_LoopHead - (0,0): anon12_LoopBody - (0,0): anon13_Then -Definedness.dfy(123,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(116,5): anon12_LoopHead - (0,0): anon12_LoopBody - Definedness.dfy(116,5): anon13_Else - (0,0): anon14_Then - Definedness.dfy(122,5): anon15_LoopHead - (0,0): anon15_LoopBody - (0,0): anon16_Then -Definedness.dfy(133,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(132,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(133,22): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(134,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(132,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(143,15): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(143,5): anon8_LoopHead - (0,0): anon8_LoopBody - Definedness.dfy(143,5): anon9_Else -Definedness.dfy(162,15): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(156,5): anon16_LoopHead - (0,0): anon16_LoopBody - Definedness.dfy(156,5): anon17_Else - (0,0): anon18_Then - (0,0): anon5 - (0,0): anon19_Then - Definedness.dfy(162,5): anon20_LoopHead - (0,0): anon20_LoopBody - Definedness.dfy(162,5): anon21_Else -Definedness.dfy(175,28): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(181,17): Error: possible violation of function precondition -Definedness.dfy(79,16): Related location -Execution trace: - (0,0): anon0 - Definedness.dfy(173,5): anon18_LoopHead - (0,0): anon18_LoopBody - Definedness.dfy(173,5): anon19_Else - (0,0): anon20_Then - Definedness.dfy(180,5): anon21_LoopHead - (0,0): anon21_LoopBody - (0,0): anon22_Then - (0,0): anon23_Then - (0,0): anon11 -Definedness.dfy(196,19): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(194,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(196,23): Error BP5004: This loop invariant might not hold on entry. -Execution trace: - (0,0): anon0 -Definedness.dfy(196,28): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(194,5): anon6_LoopHead - (0,0): anon6_LoopBody - (0,0): anon7_Then -Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(217,46): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -Definedness.dfy(224,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path. -Definedness.dfy(240,24): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon2 - (0,0): anon8_Else - -Dafny program verifier finished with 21 verified, 37 errors - --------------------- FunctionSpecifications.dfy -------------------- -FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else -FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon11_Else - (0,0): anon14_Else - (0,0): anon15_Then -FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon3 -FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -FunctionSpecifications.dfy(108,23): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(111,23): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(126,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -FunctionSpecifications.dfy(130,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(153,15): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(172,15): Error: assertion violation -Execution trace: - (0,0): anon0 -FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path. -FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Else -FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(160,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(188,3): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 19 verified, 17 errors - --------------------- ResolutionErrors.dfy -------------------- -ResolutionErrors.dfy(499,7): Error: RHS (of type List) not assignable to LHS (of type List) -ResolutionErrors.dfy(504,7): Error: RHS (of type List) not assignable to LHS (of type List) -ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>) -ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree -ResolutionErrors.dfy(565,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly -ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements -ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations -ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context -ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. -ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type. -ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression -ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1) -ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object) -ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object) -ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object) -ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) -ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(429,2): Error: More than one default constructor -ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context -ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable -ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure -ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops -ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called -ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor -ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int) -ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) -ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3) -ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) -ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array) -ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name -ResolutionErrors.dfy(57,7): Error: unresolved identifier: F -ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name -ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance -ResolutionErrors.dfy(59,7): Error: unresolved identifier: G -ResolutionErrors.dfy(61,7): Error: unresolved identifier: M -ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance -ResolutionErrors.dfy(63,7): Error: unresolved identifier: N -ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters -ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global -ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') -ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') -ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') -ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') -ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1) -ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label -ResolutionErrors.dfy(263,2): Error: duplicate label -ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called -ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called -ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated -ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List) -ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int) -ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int) -ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts -ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass, got GenericClass) -ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) -ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool) -ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool) -ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(406,6): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint -ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts -ResolutionErrors.dfy(546,18): Error: unresolved identifier: w -ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses -ResolutionErrors.dfy(913,9): Error: unresolved identifier: s -135 resolution/type errors detected in ResolutionErrors.dfy - --------------------- ParseErrors.dfy -------------------- -ParseErrors.dfy(7,19): error: a chain cannot have more than one != operator -ParseErrors.dfy(9,37): error: this operator chain cannot continue with a descending operator -ParseErrors.dfy(10,38): error: this operator chain cannot continue with an ascending operator -ParseErrors.dfy(15,24): error: this operator chain cannot continue with a descending operator -ParseErrors.dfy(18,18): error: this operator cannot be part of a chain -ParseErrors.dfy(19,19): error: this operator cannot be part of a chain -ParseErrors.dfy(20,18): error: this operator cannot be part of a chain -ParseErrors.dfy(21,18): error: chaining not allowed from the previous operator -ParseErrors.dfy(49,8): error: the main operator of a calculation must be transitive -ParseErrors.dfy(65,2): error: this operator cannot continue this calculation -ParseErrors.dfy(66,2): error: this operator cannot continue this calculation -ParseErrors.dfy(71,2): error: this operator cannot continue this calculation -ParseErrors.dfy(72,2): error: this operator cannot continue this calculation -ParseErrors.dfy(78,2): error: this operator cannot continue this calculation -14 parse errors detected in ParseErrors.dfy - --------------------- Array.dfy -------------------- -Array.dfy(13,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(20,16): Error: target object may be null -Execution trace: - (0,0): anon0 -Array.dfy(27,6): Error: index out of range -Execution trace: - (0,0): anon0 -Array.dfy(51,20): Error: assertion violation -Execution trace: - (0,0): anon0 -Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(66,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(110,21): Error: upper bound below lower bound or above length of array -Execution trace: - (0,0): anon0 - (0,0): anon14_Else - (0,0): anon18_Then - (0,0): anon19_Then - (0,0): anon20_Then - (0,0): anon11 -Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Then -Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then - (0,0): anon12_Else -Array.dfy(150,6): Error: insufficient reads clause to read array element -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Then -Array.dfy(158,6): Error: insufficient reads clause to read array element -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Then -Array.dfy(174,6): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Array.dfy(181,6): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -Array.dfy(206,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(205,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(230,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(229,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(236,1): Error BP5003: A postcondition might not hold on this return path. -Array.dfy(235,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Array.dfy(251,10): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then -Array.dfy(252,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon2 - (0,0): anon6_Then - -Dafny program verifier finished with 41 verified, 20 errors - --------------------- MultiDimArray.dfy -------------------- -MultiDimArray.dfy(56,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon12_Then -MultiDimArray.dfy(83,25): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - -Dafny program verifier finished with 8 verified, 2 errors - --------------------- NonGhostQuantifiers.dfy -------------------- -NonGhostQuantifiers.dfy(149,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(153,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(158,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(163,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c' -NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c' -NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd' -NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n' -NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i' -NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j' -NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j' -NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j' -NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y' -NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x' -NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -20 resolution/type errors detected in NonGhostQuantifiers.dfy - --------------------- AdvancedLHS.dfy -------------------- -AdvancedLHS.dfy(34,23): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon15_Else - -Dafny program verifier finished with 7 verified, 1 error - --------------------- ModulesCycle.dfy -------------------- -ModulesCycle.dfy(5,9): Error: module T does not exist -ModulesCycle.dfy(8,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B -2 resolution/type errors detected in ModulesCycle.dfy - --------------------- Modules0.dfy -------------------- -Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA -Modules0.dfy(13,7): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(14,8): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB -Modules0.dfy(56,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) -Modules0.dfy(57,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(68,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(75,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) -Modules0.dfy(75,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?) -Modules0.dfy(78,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?) -Modules0.dfy(83,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) -Modules0.dfy(92,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?) -Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) -Modules0.dfy(224,8): Error: new can be applied only to reference types (got X) -Modules0.dfy(233,13): Error: Undeclared type X in module B -Modules0.dfy(243,13): Error: unresolved identifier: X -Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X -Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?) -Modules0.dfy(283,12): Error: new can be applied only to reference types (got D) -Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(287,6): Error: expected method call, found expression -Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point -Modules0.dfy(288,6): Error: expected method call, found expression -Modules0.dfy(310,24): Error: module Q_Imp does not exist -Modules0.dfy(100,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) -28 resolution/type errors detected in Modules0.dfy - --------------------- Modules1.dfy -------------------- -Modules1.dfy(79,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Modules1.dfy(92,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Modules1.dfy(94,18): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0 -Execution trace: - (0,0): anon0 -Modules1.dfy(62,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 26 verified, 5 errors - --------------------- Modules2.dfy -------------------- -Modules2.dfy(46,17): Error: The name C ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name) -Modules2.dfy(46,10): Error: new can be applied only to reference types (got C) -Modules2.dfy(49,14): Error: the name 'E' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'D.E') -Modules2.dfy(50,14): Error: The name D ambiguously refers to a type in one of the modules A, B -Modules2.dfy(52,11): Error: The name f ambiguously refers to a static member in one of the modules A, B -5 resolution/type errors detected in Modules2.dfy - --------------------- BadFunction.dfy -------------------- -BadFunction.dfy(9,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 2 verified, 1 error - --------------------- Comprehensions.dfy -------------------- -Comprehensions.dfy(12,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon10_Then - (0,0): anon4 - (0,0): anon11_Then - (0,0): anon12_Then - (0,0): anon8 - -Dafny program verifier finished with 6 verified, 1 error - --------------------- Basics.dfy -------------------- -Basics.dfy(45,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Basics.dfy(69,42): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Then - (0,0): anon15_Then - Basics.dfy(69,72): anon16_Else - Basics.dfy(69,82): anon17_Else - Basics.dfy(69,95): anon18_Else - (0,0): anon12 -Basics.dfy(113,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 - (0,0): anon10_Then - (0,0): anon3 - (0,0): anon11_Then - (0,0): anon6 - (0,0): anon12_Then - (0,0): anon9 -Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 -Basics.dfy(158,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then -Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3 -Basics.dfy(160,10): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon3 -Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Then -Basics.dfy(176,15): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Else - (0,0): anon6 - (0,0): anon13_Then - (0,0): anon8 - (0,0): anon14_Then -Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value -Execution trace: - (0,0): anon0 -Basics.dfy(429,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Basics.dfy(440,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -Basics.dfy(442,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 - -Dafny program verifier finished with 61 verified, 14 errors - --------------------- ControlStructures.dfy -------------------- -ControlStructures.dfy(8,3): Error: missing case in case statement: Purple -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -ControlStructures.dfy(8,3): Error: missing case in case statement: Blue -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Else - (0,0): anon9_Then -ControlStructures.dfy(17,3): Error: missing case in case statement: Purple -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -ControlStructures.dfy(46,5): Error: missing case in case statement: Red -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Else - (0,0): anon10_Then -ControlStructures.dfy(54,3): Error: missing case in case statement: Red -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Else - (0,0): anon10_Else - (0,0): anon11_Else - (0,0): anon12_Then -ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -ControlStructures.dfy(218,18): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - (0,0): anon71_Then -ControlStructures.dfy(235,21): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - ControlStructures.dfy(213,9): anon71_Else - (0,0): anon72_Then - (0,0): after_4 - ControlStructures.dfy(224,7): anon74_LoopHead - (0,0): anon74_LoopBody - ControlStructures.dfy(224,7): anon75_Else - ControlStructures.dfy(224,7): anon76_Else - (0,0): anon78_Then - (0,0): anon38 - (0,0): anon83_Then - (0,0): anon52 -ControlStructures.dfy(238,30): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon65_Then - (0,0): anon84_Then - (0,0): anon85_Then - (0,0): anon56 -ControlStructures.dfy(241,17): Error: assertion violation -Execution trace: - (0,0): anon0 - ControlStructures.dfy(197,3): anon59_LoopHead - (0,0): anon59_LoopBody - ControlStructures.dfy(197,3): anon60_Else - ControlStructures.dfy(197,3): anon61_Else - ControlStructures.dfy(201,5): anon62_LoopHead - (0,0): anon62_LoopBody - ControlStructures.dfy(201,5): anon63_Else - ControlStructures.dfy(201,5): anon64_Else - (0,0): anon68_Then - ControlStructures.dfy(213,9): anon69_LoopHead - (0,0): anon69_LoopBody - ControlStructures.dfy(213,9): anon70_Else - ControlStructures.dfy(213,9): anon71_Else - (0,0): anon72_Then - (0,0): after_4 - ControlStructures.dfy(224,7): anon74_LoopHead - (0,0): anon74_LoopBody - ControlStructures.dfy(224,7): anon75_Else - ControlStructures.dfy(224,7): anon76_Else - (0,0): anon79_Then - (0,0): anon82_Then - (0,0): anon86_Then - (0,0): anon58 - -Dafny program verifier finished with 22 verified, 10 errors - --------------------- Termination.dfy -------------------- -Termination.dfy(359,47): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Else -Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop -Execution trace: - (0,0): anon0 - Termination.dfy(108,3): anon6_LoopHead - (0,0): anon6_LoopBody - Termination.dfy(108,3): anon7_Else - Termination.dfy(108,3): anon8_Else -Termination.dfy(116,3): Error: cannot prove termination; try supplying a decreases clause for the loop -Execution trace: - (0,0): anon0 - Termination.dfy(116,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(116,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(116,3): anon11_Else -Termination.dfy(125,3): Error: decreases expression might not decrease -Execution trace: - (0,0): anon0 - Termination.dfy(125,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(125,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(125,3): anon11_Else -Termination.dfy(126,17): Error: decreases expression must be bounded below by 0 at end of loop iteration -Execution trace: - (0,0): anon0 - Termination.dfy(125,3): anon8_LoopHead - (0,0): anon8_LoopBody - Termination.dfy(125,3): anon9_Else - (0,0): anon10_Then - (0,0): anon5 - Termination.dfy(125,3): anon11_Else -Termination.dfy(254,35): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -Termination.dfy(294,3): Error: decreases expression might not decrease -Execution trace: - Termination.dfy(294,3): anon9_LoopHead - (0,0): anon9_LoopBody - Termination.dfy(294,3): anon10_Else - Termination.dfy(294,3): anon11_Else - (0,0): anon12_Else - -Dafny program verifier finished with 59 verified, 7 errors - --------------------- DTypes.dfy -------------------- -DTypes.dfy(18,14): Error: assertion violation -Execution trace: - (0,0): anon0 -DTypes.dfy(56,18): Error: assertion violation -Execution trace: - (0,0): anon0 -DTypes.dfy(120,13): Error: assertion violation -DTypes.dfy(92,30): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(126,13): Error: assertion violation -DTypes.dfy(92,20): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(136,12): Error: assertion violation -DTypes.dfy(131,6): Related location -DTypes.dfy(92,20): Related location -Execution trace: - (0,0): anon0 -DTypes.dfy(157,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon4 - -Dafny program verifier finished with 27 verified, 6 errors - --------------------- ParallelResolveErrors.dfy -------------------- -ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable -ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements -ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods -ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement -ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations -ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -21 resolution/type errors detected in ParallelResolveErrors.dfy - --------------------- Parallel.dfy -------------------- -Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold. -Parallel.dfy(60,14): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Then - (0,0): anon34_Then - (0,0): anon35_Then - (0,0): anon14 -Parallel.dfy(38,5): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon38_Then - (0,0): anon20 -Parallel.dfy(42,18): Error: possible violation of postcondition of forall statement -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Else - (0,0): anon39_Then - (0,0): anon40_Then - (0,0): anon26 -Parallel.dfy(47,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon29_Else - (0,0): anon32_Else - (0,0): anon33_Else - (0,0): anon36_Else - (0,0): anon39_Then - (0,0): anon40_Then -Parallel.dfy(93,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon10_Else - (0,0): anon11_Then -Parallel.dfy(99,20): Error: possible violation of postcondition of forall statement -Execution trace: - (0,0): anon0 - (0,0): anon10_Else - (0,0): anon11_Then - (0,0): anon12_Then -Parallel.dfy(122,12): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - (0,0): anon7_Then - (0,0): anon3 -Parallel.dfy(185,12): Error: left-hand sides for different forall-statement bound variables may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon19_Then - (0,0): anon20_Then - (0,0): anon5 -Parallel.dfy(296,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - -Dafny program verifier finished with 43 verified, 9 errors - --------------------- TypeParameters.dfy -------------------- -TypeParameters.dfy(47,22): Error: assertion violation -Execution trace: - (0,0): anon0 -TypeParameters.dfy(69,27): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -TypeParameters.dfy(156,12): Error: assertion violation -TypeParameters.dfy(156,28): Related location -Execution trace: - (0,0): anon0 - (0,0): anon20_Then - TypeParameters.dfy(156,32): anon21_Else - (0,0): anon5 -TypeParameters.dfy(158,12): Error: assertion violation -TypeParameters.dfy(158,33): Related location -Execution trace: - (0,0): anon0 - (0,0): anon23_Then - TypeParameters.dfy(158,37): anon24_Else - (0,0): anon11 -TypeParameters.dfy(160,12): Error: assertion violation -TypeParameters.dfy(160,20): Related location -Execution trace: - (0,0): anon0 - (0,0): anon25_Then -TypeParameters.dfy(162,12): Error: assertion violation -TypeParameters.dfy(147,5): Related location -TypeParameters.dfy(162,21): Related location -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -TypeParameters.dfy(164,12): Error: assertion violation -TypeParameters.dfy(149,8): Related location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then -TypeParameters.dfy(178,15): Error BP5005: This loop invariant might not be maintained by the loop. -TypeParameters.dfy(178,38): Related location -Execution trace: - (0,0): anon0 - TypeParameters.dfy(171,3): anon16_LoopHead - (0,0): anon16_LoopBody - TypeParameters.dfy(171,3): anon17_Else - (0,0): anon19_Then - TypeParameters.dfy(177,3): anon20_LoopHead - (0,0): anon20_LoopBody - TypeParameters.dfy(177,3): anon21_Else - TypeParameters.dfy(177,3): anon23_Else - -Dafny program verifier finished with 58 verified, 8 errors - --------------------- Datatypes.dfy -------------------- -Datatypes.dfy(297,10): Error BP5003: A postcondition might not hold on this return path. -Datatypes.dfy(295,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Else - (0,0): anon15_Then - (0,0): anon6 -Datatypes.dfy(298,12): Error: missing case in case statement: Appendix -Execution trace: - (0,0): anon0 - (0,0): anon13_Then - (0,0): anon14_Else - (0,0): anon15_Else - (0,0): anon16_Then -Datatypes.dfy(349,5): Error: missing case in case statement: Cons -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then -Datatypes.dfy(349,5): Error: missing case in case statement: Nil -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Else - (0,0): anon8_Then -Datatypes.dfy(356,8): Error: missing case in case statement: Cons -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Then -Datatypes.dfy(356,8): Error: missing case in case statement: Nil -Execution trace: - (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else - (0,0): anon12_Then -Datatypes.dfy(82,20): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon20_Else - (0,0): anon21_Then - (0,0): anon4 - (0,0): anon22_Else - (0,0): anon23_Then - (0,0): anon24_Else - (0,0): anon25_Then -Datatypes.dfy(170,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then -Datatypes.dfy(172,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon5_Then -Datatypes.dfy(201,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons' -Execution trace: - (0,0): anon0 -Datatypes.dfy(204,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons' -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -Datatypes.dfy(225,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T'' -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - -Dafny program verifier finished with 44 verified, 12 errors - --------------------- StatementExpressions.dfy -------------------- -StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - (0,0): anon8_Then -StatementExpressions.dfy(59,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - StatementExpressions.dfy(53,7): anon8_Else -StatementExpressions.dfy(77,6): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - -Dafny program verifier finished with 17 verified, 5 errors - --------------------- Coinductive.dfy -------------------- -Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed -Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed -Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed -Coinductive.dfy(64,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed -Coinductive.dfy(93,8): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(94,8): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(95,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(95,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(101,5): Error: a copredicate can be called recursively only in positive positions -Coinductive.dfy(104,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(105,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier -Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates -16 resolution/type errors detected in Coinductive.dfy - --------------------- Corecursion.dfy -------------------- -Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 20 verified, 8 errors - --------------------- CoResolution.dfy -------------------- -CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default -CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared# -CoResolution.dfy(21,7): Error: unresolved identifier: _k -CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) -CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause -CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause -CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas -21 resolution/type errors detected in CoResolution.dfy - --------------------- CoPrefix.dfy -------------------- -CoPrefix.dfy(164,3): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(163,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -CoPrefix.dfy(169,3): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(168,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoPrefix.dfy(63,7): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Else - (0,0): anon9_Then -CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Else - (0,0): anon9_Then -CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold. -CoPrefix.dfy(101,17): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoPrefix.dfy(138,25): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon10_Then -CoPrefix.dfy(142,25): Error: assertion violation -CoPrefix.dfy(117,23): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - (0,0): anon12_Then -CoPrefix.dfy(151,1): Error BP5003: A postcondition might not hold on this return path. -CoPrefix.dfy(150,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 41 verified, 9 errors - --------------------- CoinductiveProofs.dfy -------------------- -CoinductiveProofs.dfy(29,12): Error: assertion violation -CoinductiveProofs.dfy(13,17): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(54,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(74,12): Error: assertion violation -CoinductiveProofs.dfy(54,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(80,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(100,12): Error: assertion violation -CoinductiveProofs.dfy(80,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then -CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(106,3): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(4,24): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - -Dafny program verifier finished with 35 verified, 8 errors - --------------------- TypeAntecedents.dfy -------------------- -TypeAntecedents.dfy(35,13): Error: assertion violation -Execution trace: - (0,0): anon0 -TypeAntecedents.dfy(58,1): Error BP5003: A postcondition might not hold on this return path. -TypeAntecedents.dfy(57,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon25_Then - (0,0): anon6 - (0,0): anon28_Then - (0,0): anon8 - (0,0): anon29_Else - (0,0): anon31_Else - (0,0): anon33_Then - (0,0): anon20 - (0,0): anon34_Then - (0,0): anon35_Then - (0,0): anon24 -TypeAntecedents.dfy(66,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon25_Else - (0,0): anon26_Then - (0,0): anon27_Else - -Dafny program verifier finished with 12 verified, 3 errors - --------------------- NoTypeArgs.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- EqualityTypes.dfy -------------------- -EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype -EqualityTypes.dfy(35,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality -EqualityTypes.dfy(40,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes a different number of type parameters -EqualityTypes.dfy(41,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters -EqualityTypes.dfy(45,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality -EqualityTypes.dfy(46,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality -EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) -EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) -EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) -EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D) -EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D) -11 resolution/type errors detected in EqualityTypes.dfy - --------------------- SplitExpr.dfy -------------------- -SplitExpr.dfy(92,15): Error: loop invariant violation -SplitExpr.dfy(86,44): Related location -Execution trace: - SplitExpr.dfy(91,3): anon7_LoopHead - -Dafny program verifier finished with 10 verified, 1 error - --------------------- LoopModifies.dfy -------------------- -LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(16,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(16,4): anon9_Else - LoopModifies.dfy(16,4): anon11_Else -LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(44,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(44,4): anon9_Else - LoopModifies.dfy(44,4): anon11_Else -LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(59,4): anon9_LoopHead - (0,0): anon9_LoopBody - LoopModifies.dfy(59,4): anon10_Else - LoopModifies.dfy(59,4): anon12_Else -LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause -Execution trace: - (0,0): anon0 -LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(92,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(92,4): anon9_Else - LoopModifies.dfy(92,4): anon11_Else -LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(136,4): anon17_LoopHead - (0,0): anon17_LoopBody - LoopModifies.dfy(136,4): anon18_Else - LoopModifies.dfy(136,4): anon20_Else - LoopModifies.dfy(141,7): anon21_LoopHead - (0,0): anon21_LoopBody - LoopModifies.dfy(141,7): anon22_Else - LoopModifies.dfy(141,7): anon24_Else -LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(195,4): anon8_LoopHead - (0,0): anon8_LoopBody - LoopModifies.dfy(195,4): anon9_Else - LoopModifies.dfy(195,4): anon11_Else -LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - LoopModifies.dfy(275,4): anon16_LoopHead - (0,0): anon16_LoopBody - LoopModifies.dfy(275,4): anon17_Else - LoopModifies.dfy(275,4): anon19_Else - LoopModifies.dfy(283,7): anon20_LoopHead - (0,0): anon20_LoopBody - LoopModifies.dfy(283,7): anon21_Else - LoopModifies.dfy(283,7): anon23_Else - -Dafny program verifier finished with 23 verified, 9 errors - --------------------- Refinement.dfy -------------------- -Refinement.dfy(15,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(14,17): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(33,20): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy(64,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Refinement.dfy(74,17): Error: assertion violation -Execution trace: - (0,0): anon0 -Refinement.dfy(93,12): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(72,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Refinement.dfy(96,3): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy(77,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy[IncorrectConcrete](115,15): Related location: This is the postcondition that might not hold. -Refinement.dfy(180,9): Related location -Execution trace: - (0,0): anon0 -Refinement.dfy(187,5): Error BP5003: A postcondition might not hold on this return path. -Refinement.dfy[IncorrectConcrete](123,15): Related location: This is the postcondition that might not hold. -Refinement.dfy(180,9): Related location -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Refinement.dfy(193,7): Error: assertion violation -Refinement.dfy[IncorrectConcrete](131,24): Related location -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 48 verified, 9 errors - --------------------- RefinementErrors.dfy -------------------- -RefinementErrors.dfy(30,17): Error: a refining method is not allowed to add preconditions -RefinementErrors.dfy(31,15): Error: a refining method is not allowed to extend the modifies clause -RefinementErrors.dfy(34,14): Error: a predicate declaration (abc) can only refine a predicate -RefinementErrors.dfy(35,8): Error: a field re-declaration (xyz) must be to ghostify the field -RefinementErrors.dfy(37,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F -RefinementErrors.dfy(38,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C') -RefinementErrors.dfy(38,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A') -RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B') -RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq' instead of 'set') -RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines -RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G -11 resolution/type errors detected in RefinementErrors.dfy - --------------------- ReturnErrors.dfy -------------------- -ReturnErrors.dfy(32,10): Error: cannot have method call in return statement. -ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement. -ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'. -3 resolution/type errors detected in ReturnErrors.dfy - --------------------- ReturnTests.dfy -------------------- - -Dafny program verifier finished with 20 verified, 0 errors - --------------------- ChainingDisjointTests.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- CallStmtTests.dfy -------------------- -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable -CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable -2 resolution/type errors detected in CallStmtTests.dfy - --------------------- MultiSets.dfy -------------------- -MultiSets.dfy(159,3): Error BP5003: A postcondition might not hold on this return path. -MultiSets.dfy(158,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MultiSets.dfy(165,3): Error BP5003: A postcondition might not hold on this return path. -MultiSets.dfy(164,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MultiSets.dfy(178,11): Error: new number of occurrences might be negative -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -MultiSets.dfy(269,24): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 - (0,0): anon12_Then - (0,0): anon14_Else - -Dafny program verifier finished with 54 verified, 4 errors - --------------------- PredExpr.dfy -------------------- -PredExpr.dfy(7,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -PredExpr.dfy(52,17): Error: assertion violation -Execution trace: - (0,0): anon0 -PredExpr.dfy(77,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Else - (0,0): anon3 - PredExpr.dfy(76,20): anon10_Else - (0,0): anon6 - -Dafny program verifier finished with 11 verified, 4 errors - --------------------- Predicates.dfy -------------------- -Predicates.dfy[B](21,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[B](20,15): Related location: This is the postcondition that might not hold. -Predicates.dfy(31,9): Related location -Execution trace: - (0,0): anon0 -Predicates.dfy(88,16): Error: assertion violation -Execution trace: - (0,0): anon0 -Predicates.dfy(92,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Predicates.dfy[Tricky_Full](126,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[Tricky_Full](125,15): Related location: This is the postcondition that might not hold. -Predicates.dfy(136,7): Related location -Predicates.dfy[Tricky_Full](116,9): Related location -Execution trace: - (0,0): anon0 -Predicates.dfy(164,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy(163,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Predicates.dfy[Q1](154,5): Error BP5003: A postcondition might not hold on this return path. -Predicates.dfy[Q1](153,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 52 verified, 6 errors - --------------------- Skeletons.dfy -------------------- -Skeletons.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. -Skeletons.dfy(44,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - Skeletons.dfy[C0](32,5): anon11_LoopHead - (0,0): anon11_LoopBody - Skeletons.dfy[C0](32,5): anon12_Else - (0,0): anon13_Then - Skeletons.dfy[C0](37,19): anon15_Else - (0,0): anon10 - -Dafny program verifier finished with 9 verified, 1 error - --------------------- OpaqueFunctions.dfy -------------------- -OpaqueFunctions.dfy(27,16): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(58,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(60,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(63,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(66,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(77,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -OpaqueFunctions.dfy(86,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(88,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(91,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(94,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(105,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold. -OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -OpaqueFunctions.dfy(114,20): Error: assertion violation -Execution trace: - (0,0): anon0 -OpaqueFunctions.dfy(116,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -OpaqueFunctions.dfy(119,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -OpaqueFunctions.dfy(122,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -OpaqueFunctions.dfy(138,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 43 verified, 19 errors - --------------------- Maps.dfy -------------------- -Maps.dfy(78,8): Error: element may not be in domain -Execution trace: - (0,0): anon0 -Maps.dfy(128,13): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 32 verified, 2 errors - --------------------- LiberalEquality.dfy -------------------- -LiberalEquality.dfy(20,14): Error: arguments must have the same type (got T and U) -LiberalEquality.dfy(39,14): Error: arguments must have the same type (got Weird and Weird) -LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array and array) -3 resolution/type errors detected in LiberalEquality.dfy - --------------------- RefinementModificationChecking.dfy -------------------- -RefinementModificationChecking.dfy(19,4): Error: cannot assign to variable defined previously -RefinementModificationChecking.dfy(20,4): Error: cannot assign to variable defined previously -2 resolution/type errors detected in RefinementModificationChecking.dfy - --------------------- TailCalls.dfy -------------------- -TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code -TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods -TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods -5 resolution/type errors detected in TailCalls.dfy - --------------------- IteratorResolution.dfy -------------------- -IteratorResolution.dfy(62,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(67,18): Error: arguments must have the same type (got _T0 and int) -IteratorResolution.dfy(79,19): Error: RHS (of type bool) not assignable to LHS (of type int) -IteratorResolution.dfy(82,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called -IteratorResolution.dfy(86,15): Error: logical negation expects a boolean argument (instead got int) -IteratorResolution.dfy(20,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(126,9): Error: unresolved identifier: _decreases3 -IteratorResolution.dfy(127,21): Error: arguments must have the same type (got int and ?) -IteratorResolution.dfy(128,2): Error: LHS of assignment must denote a mutable field -IteratorResolution.dfy(135,9): Error: unresolved identifier: _decreases1 -IteratorResolution.dfy(140,9): Error: unresolved identifier: _decreases0 -12 resolution/type errors detected in IteratorResolution.dfy - --------------------- Iterators.dfy -------------------- -Iterators.dfy(251,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(274,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(284,24): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 -Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 -Iterators.dfy(343,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 -Iterators.dfy(370,9): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Else -Iterators.dfy(103,22): Error: assertion violation -Execution trace: - (0,0): anon0 -Iterators.dfy(106,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Iterators.dfy(177,28): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon15_Then -Iterators.dfy(208,7): Error: an assignment to _new is only allowed to shrink the set -Execution trace: - (0,0): anon0 - Iterators.dfy(197,3): anon16_LoopHead - (0,0): anon16_LoopBody - Iterators.dfy(197,3): anon17_Else - Iterators.dfy(197,3): anon19_Else - (0,0): anon20_Then -Iterators.dfy(212,21): Error: assertion violation -Execution trace: - (0,0): anon0 - Iterators.dfy(197,3): anon16_LoopHead - (0,0): anon16_LoopBody - Iterators.dfy(197,3): anon17_Else - Iterators.dfy(197,3): anon19_Else - (0,0): anon21_Then -Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold. -Iterators.dfy(4,10): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon35_Then - (0,0): anon2 - (0,0): anon36_Then - (0,0): anon5 - (0,0): anon37_Then -Iterators.dfy(89,14): Error: assertion violation -Execution trace: - (0,0): anon0 -Iterators.dfy(119,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Iterators.dfy(150,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold. -Iterators.dfy(125,10): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon3 -Iterators.dfy(234,14): Error: assertion violation -Execution trace: - (0,0): anon0 - Iterators.dfy(225,3): anon14_LoopHead - (0,0): anon14_LoopBody - Iterators.dfy(225,3): anon15_Else - Iterators.dfy(225,3): anon18_Else - (0,0): anon19_Else - -Dafny program verifier finished with 65 verified, 20 errors - --------------------- RankPos.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- RankNeg.dfy -------------------- -RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then -RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then - -Dafny program verifier finished with 1 verified, 4 errors - --------------------- Computations.dfy -------------------- - -Dafny program verifier finished with 58 verified, 0 errors - --------------------- ComputationsNeg.dfy -------------------- -ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path. -ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(23,1): Error BP5003: A postcondition might not hold on this return path. -ComputationsNeg.dfy(22,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(36,13): Error: assertion violation -Execution trace: - (0,0): anon0 -ComputationsNeg.dfy(45,13): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 7 verified, 5 errors - --------------------- Include.dfy -------------------- -Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(17,20): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -Includee.dfy[Concrete](22,16): Error: assertion violation -Execution trace: - (0,0): anon0 -Include.dfy(27,7): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy[Concrete](20,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Then - -Dafny program verifier finished with 4 verified, 3 errors - --------------------- Includee.dfy -------------------- -Includee.dfy(21,3): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(20,15): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -Includee.dfy(24,18): Error: assertion violation -Execution trace: - (0,0): anon0 -Includee.dfy(6,1): Error BP5003: A postcondition might not hold on this return path. -Includee.dfy(5,13): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 5 verified, 3 errors - --------------------- AutoReq.dfy -------------------- -AutoReq.dfy(247,3): Error: possible violation of function precondition -AutoReq.dfy(239,12): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(13,3): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(25,3): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -AutoReq.dfy(38,12): Error: assertion violation -AutoReq.dfy(31,13): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then -AutoReq.dfy(38,12): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon9_Then -AutoReq.dfy(40,12): Error: assertion violation -AutoReq.dfy(31,27): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -AutoReq.dfy(40,12): Error: possible violation of function precondition -AutoReq.dfy(5,14): Related location -Execution trace: - (0,0): anon0 - (0,0): anon10_Then -AutoReq.dfy(45,12): Error: assertion violation -AutoReq.dfy(31,13): Related location -AutoReq.dfy(7,5): Related location -Execution trace: - (0,0): anon0 - (0,0): anon11_Then - -Dafny program verifier finished with 52 verified, 8 errors - --------------------- DatatypeUpdate.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ModifyStmt.dfy -------------------- -ModifyStmt.dfy(27,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(42,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(48,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(61,5): Error: modify statement may violate context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(70,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(89,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon9_Then - ModifyStmt.dfy(81,7): anon10_LoopHead - (0,0): anon10_LoopBody - ModifyStmt.dfy(81,7): anon11_Else - (0,0): anon12_Then - (0,0): anon8 -ModifyStmt.dfy(99,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(110,14): Error: assertion violation -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(122,16): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -ModifyStmt.dfy(134,7): Error: assignment may update an object not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 -ModifyStmt.dfy(172,15): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 25 verified, 11 errors - --------------------- SeqSlice.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- RealCompare.dfy -------------------- -RealCompare.dfy(35,5): Error: failure to decrease termination measure -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0 -Execution trace: - (0,0): anon0 -RealCompare.dfy(141,12): Error: assertion violation -Execution trace: - (0,0): anon0 - RealCompare.dfy(133,3): anon7_LoopHead - (0,0): anon7_LoopBody - RealCompare.dfy(133,3): anon8_Else - (0,0): anon9_Then -RealCompare.dfy(156,12): Error: assertion violation -Execution trace: - (0,0): anon0 - RealCompare.dfy(147,3): anon9_LoopHead - (0,0): anon9_LoopBody - RealCompare.dfy(147,3): anon10_Else - (0,0): anon12_Then - -Dafny program verifier finished with 24 verified, 4 errors - --------------------- AssumptionVariables0.dfy -------------------- -AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && " -AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost -AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool' -AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " -AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " -AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost -AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool' -AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -13 resolution/type errors detected in AssumptionVariables0.dfy - --------------------- AssumptionVariables1.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Superposition.dfy -------------------- - -Verifying CheckWellformed$$_0_M0.C.M ... - [0 proof obligations] verified - -Verifying Impl$$_0_M0.C.M ... - [4 proof obligations] verified - -Verifying CheckWellformed$$_0_M0.C.P ... - [4 proof obligations] verified - -Verifying CheckWellformed$$_0_M0.C.Q ... - [3 proof obligations] error -Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy(28,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - -Verifying CheckWellformed$$_0_M0.C.R ... - [3 proof obligations] error -Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy(34,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon5_Else - -Verifying CheckWellformed$$_1_M1.C.M ... - [0 proof obligations] verified - -Verifying Impl$$_1_M1.C.M ... - [1 proof obligation] verified - -Verifying CheckWellformed$$_1_M1.C.P ... - [1 proof obligation] error -Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path. -Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon7_Else - (0,0): anon9_Then - (0,0): anon6 - -Verifying CheckWellformed$$_1_M1.C.Q ... - [0 proof obligations] verified - -Verifying CheckWellformed$$_1_M1.C.R ... - [0 proof obligations] verified - -Dafny program verifier finished with 7 verified, 3 errors - --------------------- SmallTests.dfy -------------------- -SmallTests.dfy(33,11): Error: index out of range -Execution trace: - (0,0): anon0 -SmallTests.dfy(64,36): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -SmallTests.dfy(65,51): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Else - (0,0): anon3 - (0,0): anon13_Else -SmallTests.dfy(66,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - (0,0): anon3 - (0,0): anon13_Then - (0,0): anon6 -SmallTests.dfy(85,24): Error: target object may be null -Execution trace: - (0,0): anon0 - SmallTests.dfy(84,5): anon8_LoopHead - (0,0): anon8_LoopBody - (0,0): anon9_Then -SmallTests.dfy(119,5): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon3 -SmallTests.dfy(132,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -SmallTests.dfy(134,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(174,9): Error: assignment may update an object field not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon22_Else - (0,0): anon24_Else - (0,0): anon26_Else - (0,0): anon28_Then - (0,0): anon29_Then - (0,0): anon19 -SmallTests.dfy(198,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -SmallTests.dfy(205,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Then -SmallTests.dfy(207,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Else -SmallTests.dfy(253,24): Error BP5002: A precondition for this call might not hold. -SmallTests.dfy(231,30): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - SmallTests.dfy(248,19): anon3_Else - (0,0): anon2 -SmallTests.dfy(358,12): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(368,12): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(378,6): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(682,14): Error: assertion violation -Execution trace: - (0,0): anon0 - SmallTests.dfy(679,5): anon7_LoopHead - (0,0): anon7_LoopBody - SmallTests.dfy(679,5): anon8_Else - (0,0): anon9_Then -SmallTests.dfy(703,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Then - (0,0): anon3 -SmallTests.dfy(288,3): Error BP5003: A postcondition might not hold on this return path. -SmallTests.dfy(282,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon18_Else - (0,0): anon23_Then - (0,0): anon24_Then - (0,0): anon15 - (0,0): anon25_Else -SmallTests.dfy(329,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon7 -SmallTests.dfy(336,10): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(346,4): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -SmallTests.dfy(390,10): Error BP5003: A postcondition might not hold on this return path. -SmallTests.dfy(393,41): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -SmallTests.dfy(553,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -SmallTests.dfy(567,20): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - (0,0): anon28_Then - (0,0): anon4 - (0,0): anon29_Then - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Then - (0,0): anon32_Then - (0,0): anon12 -SmallTests.dfy(569,15): Error: left-hand sides 1 and 2 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - SmallTests.dfy(562,18): anon28_Else - (0,0): anon4 - (0,0): anon29_Else - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Else - (0,0): anon35_Then - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon22 - (0,0): anon38_Then -SmallTests.dfy(576,25): Error: target object may be null -Execution trace: - (0,0): anon0 -SmallTests.dfy(589,10): Error: assertion violation -Execution trace: - (0,0): anon0 -SmallTests.dfy(613,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 -SmallTests.dfy(636,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Then - (0,0): anon4 - (0,0): anon10_Then - (0,0): anon7 -SmallTests.dfy(650,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon3 -SmallTests.dfy(652,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Else -SmallTests.dfy(665,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 87 verified, 33 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- LetExpr.dfy -------------------- -LetExpr.dfy(8,12): Error: assertion violation -Execution trace: - (0,0): anon0 -LetExpr.dfy(107,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then -LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon5_Then -LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -LetExpr.dfy(256,24): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -LetExpr.dfy(285,14): Error: RHS is not certain to look like the pattern 'Agnes' -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -LetExpr.dfy(302,42): Error: value assigned to a nat must be non-negative -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -LetExpr.dfy(304,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - -Dafny program verifier finished with 38 verified, 8 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- Calculations.dfy -------------------- -Calculations.dfy(6,6): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon24_Then -Calculations.dfy(11,15): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(11,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(55,12): Error: assertion violation -Execution trace: - (0,0): anon0 - Calculations.dfy(50,3): anon5_Else -Calculations.dfy(78,15): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -Calculations.dfy(78,19): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - -Dafny program verifier finished with 9 verified, 6 errors - -Dafny program verifier finished with 0 verified, 0 errors - --------------------- DirtyLoops.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - -Dafny program verifier finished with 0 verified, 0 errors - -Dafny program verifier finished with 44 verified, 0 errors -Compiled assembly into Compilation.exe - -Dafny program verifier finished with 15 verified, 0 errors -Compilation error: Arbitrary type ('_module.MyType') cannot be compiled -Compilation error: Iterator _module.Iter has no body -Compilation error: Method _module._default.M has no body -Compilation error: Method _module._default.P has no body -Compilation error: an assume statement cannot be compiled (line 11) -Compilation error: Function _module._default.F has no body -Compilation error: Function _module._default.H has no body -Compilation error: an assume statement cannot be compiled (line 20) -Compilation error: an assume statement cannot be compiled (line 23) -Compilation error: an assume statement cannot be compiled (line 28) -Compilation error: an assume statement cannot be compiled (line 37) diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat deleted file mode 100644 index 1a371ba3..00000000 --- a/Test/dafny0/runtest.bat +++ /dev/null @@ -1,61 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -for %%f in (Simple.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f -) - -for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy - FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy - Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy - ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy - Comprehensions.dfy Basics.dfy ControlStructures.dfy - Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy - TypeParameters.dfy Datatypes.dfy StatementExpressions.dfy - Coinductive.dfy Corecursion.dfy CoResolution.dfy - CoPrefix.dfy CoinductiveProofs.dfy - TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy - LoopModifies.dfy Refinement.dfy RefinementErrors.dfy - ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy - CallStmtTests.dfy MultiSets.dfy PredExpr.dfy - Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy - Maps.dfy LiberalEquality.dfy - RefinementModificationChecking.dfy TailCalls.dfy - IteratorResolution.dfy Iterators.dfy - RankPos.dfy RankNeg.dfy - Computations.dfy ComputationsNeg.dfy - Include.dfy Includee.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy SeqSlice.dfy - RealCompare.dfy - AssumptionVariables0.dfy AssumptionVariables1.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f -) - -for %%f in (Superposition.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f -) - -for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f - %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy -) - -for %%f in (DirtyLoops.dfy) do ( - echo. - echo -------------------- %%f -------------------- - %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f - %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy -) - -%DAFNY_EXE% %* Compilation.dfy -%DAFNY_EXE% %* CompilationErrors.dfy diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer deleted file mode 100644 index e60451c2..00000000 --- a/Test/dafny1/Answer +++ /dev/null @@ -1,124 +0,0 @@ - --------------------- Queue.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- PriorityQueue.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- ExtensibleArray.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- ExtensibleArrayAuto.dfy -------------------- - -Dafny program verifier finished with 11 verified, 0 errors - --------------------- BinaryTree.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- UnboundedStack.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SeparationLogicList.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- ListCopy.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- ListReverse.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- ListContents.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- MatrixFun.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- pow2.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- SchorrWaite.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- SchorrWaite-stages.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- Cubes.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- SumOfCubes.dfy -------------------- - -Dafny program verifier finished with 17 verified, 0 errors - --------------------- FindZero.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- TerminationDemos.dfy -------------------- - -Dafny program verifier finished with 14 verified, 0 errors - --------------------- Substitution.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- TreeDatatype.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- KatzManna.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Induction.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- Rippling.dfy -------------------- - -Dafny program verifier finished with 141 verified, 0 errors - --------------------- MoreInduction.dfy -------------------- -MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 -MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 15 verified, 4 errors - --------------------- Celebrity.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- BDD.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- UltraFilter.dfy -------------------- - -Dafny program verifier finished with 19 verified, 0 errors diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat deleted file mode 100644 index f02a7965..00000000 --- a/Test/dafny1/runtest.bat +++ /dev/null @@ -1,26 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy - -rem for %%f in (Queue.dfy PriorityQueue.dfy -rem ExtensibleArray.dfy ExtensibleArrayAuto.dfy -rem BinaryTree.dfy -rem UnboundedStack.dfy -rem SeparationLogicList.dfy -rem ListCopy.dfy ListReverse.dfy ListContents.dfy -rem MatrixFun.dfy pow2.dfy -rem SchorrWaite.dfy SchorrWaite-stages.dfy -rem Cubes.dfy SumOfCubes.dfy FindZero.dfy -rem TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy -rem Induction.dfy Rippling.dfy MoreInduction.dfy -rem Celebrity.dfy BDD.dfy -rem UltraFilter.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer deleted file mode 100644 index 9fa6f4ef..00000000 --- a/Test/dafny2/Answer +++ /dev/null @@ -1,60 +0,0 @@ - --------------------- Classics.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- TreeBarrier.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- COST-verif-comp-2011-1-MaxArray.dfy -------------------- - -Dafny program verifier finished with 2 verified, 0 errors - --------------------- COST-verif-comp-2011-2-MaxTree-class.dfy -------------------- - -Dafny program verifier finished with 8 verified, 0 errors - --------------------- COST-verif-comp-2011-2-MaxTree-datatype.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- COST-verif-comp-2011-3-TwoDuplicates.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy -------------------- - -Dafny program verifier finished with 25 verified, 0 errors - --------------------- StoreAndRetrieve.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors - --------------------- Intervals.dfy -------------------- - -Dafny program verifier finished with 5 verified, 0 errors - --------------------- TreeFill.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- TuringFactorial.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- MajorityVote.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- SegmentSum.dfy -------------------- - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- MonotonicHeapstate.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors - --------------------- Calculations.dfy -------------------- - -Dafny program verifier finished with 31 verified, 0 errors diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat deleted file mode 100644 index d038acce..00000000 --- a/Test/dafny2/runtest.bat +++ /dev/null @@ -1,27 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -REM soon again: SnapshotableTrees.dfy - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Classics.dfy TreeBarrier.dfy COST-verif-comp-2011-1-MaxArray.dfy COST-verif-comp-2011-2-MaxTree-class.dfy COST-verif-comp-2011-2-MaxTree-datatype.dfy COST-verif-comp-2011-3-TwoDuplicates.dfy COST-verif-comp-2011-4-FloydCycleDetect.dfy StoreAndRetrieve.dfy Intervals.dfy TreeFill.dfy TuringFactorial.dfy MajorityVote.dfy SegmentSum.dfy MonotonicHeapstate.dfy Calculations.dfy - -rem for %%f in ( -rem Classics.dfy -rem TreeBarrier.dfy -rem COST-verif-comp-2011-1-MaxArray.dfy -rem COST-verif-comp-2011-2-MaxTree-class.dfy -rem COST-verif-comp-2011-2-MaxTree-datatype.dfy -rem COST-verif-comp-2011-3-TwoDuplicates.dfy -rem COST-verif-comp-2011-4-FloydCycleDetect.dfy -rem StoreAndRetrieve.dfy -rem Intervals.dfy TreeFill.dfy TuringFactorial.dfy -rem MajorityVote.dfy SegmentSum.dfy -rem MonotonicHeapstate.dfy Calculations.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer deleted file mode 100644 index 9e8ac835..00000000 --- a/Test/dafny3/Answer +++ /dev/null @@ -1,64 +0,0 @@ - --------------------- Iter.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- Streams.dfy -------------------- - -Dafny program verifier finished with 52 verified, 0 errors - --------------------- Dijkstra.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- CachedContainer.dfy -------------------- - -Dafny program verifier finished with 47 verified, 0 errors - --------------------- SimpleInduction.dfy -------------------- - -Dafny program verifier finished with 12 verified, 0 errors - --------------------- SimpleCoinduction.dfy -------------------- - -Dafny program verifier finished with 31 verified, 0 errors - --------------------- CalcExample.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- InductionVsCoinduction.dfy -------------------- - -Dafny program verifier finished with 20 verified, 0 errors - --------------------- Zip.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- SetIterations.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- Paulson.dfy -------------------- - -Dafny program verifier finished with 28 verified, 0 errors - --------------------- Filter.dfy -------------------- - -Dafny program verifier finished with 43 verified, 0 errors - --------------------- WideTrees.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - --------------------- InfiniteTrees.dfy -------------------- - -Dafny program verifier finished with 88 verified, 0 errors - --------------------- OpaqueTrees.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- GenericSort.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat deleted file mode 100644 index 41971d4e..00000000 --- a/Test/dafny3/runtest.bat +++ /dev/null @@ -1,19 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy GenericSort.dfy - -rem for %%f in ( -rem Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy -rem SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy -rem InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy -rem Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy -rem OpaqueTrees.dfy GenericSort.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer deleted file mode 100644 index 14986a59..00000000 --- a/Test/dafny4/Answer +++ /dev/null @@ -1,43 +0,0 @@ - --------------------- CoqArt-InsertionSort.dfy -------------------- - -Dafny program verifier finished with 36 verified, 0 errors - --------------------- GHC-MergeSort.dfy -------------------- - -Dafny program verifier finished with 83 verified, 0 errors - --------------------- Fstar-QuickSort.dfy -------------------- - -Dafny program verifier finished with 6 verified, 0 errors - --------------------- Primes.dfy -------------------- - -Dafny program verifier finished with 24 verified, 0 errors - --------------------- KozenSilva.dfy -------------------- - -Dafny program verifier finished with 47 verified, 0 errors - --------------------- SoftwareFoundations-Basics.dfy -------------------- -SoftwareFoundations-Basics.dfy(41,12): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 82 verified, 1 error - --------------------- NumberRepresentations.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- Circ.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors - --------------------- ACL2-extractor.dfy -------------------- - -Dafny program verifier finished with 33 verified, 0 errors - --------------------- ClassRefinement.dfy -------------------- - -Dafny program verifier finished with 18 verified, 0 errors diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat deleted file mode 100644 index cec5d271..00000000 --- a/Test/dafny4/runtest.bat +++ /dev/null @@ -1,7 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy ACL2-extractor.dfy ClassRefinement.dfy diff --git a/Test/runtest.bat b/Test/runtest.bat deleted file mode 100644 index dfc3ae00..00000000 --- a/Test/runtest.bat +++ /dev/null @@ -1,39 +0,0 @@ -@echo off -rem Usage: runtest.bat -if "%1" == "" goto noDirSpecified -if not exist %1\nul goto noDirExists -echo ----- Running regression test %1 -pushd %1 -if not exist runtest.bat goto noRunTest -call runtest.bat -nologo -logPrefix:%* > Output -rem There seem to be some race between finishing writing to the Output file, and running fc. -rem Calling fc twice seems to fix (or at least alleviate) the problem. -fc /W Answer Output > nul -fc /W Answer Output > nul -if not errorlevel 1 goto passTest -echo ============ %1 FAILED ==================================== -goto errorEnd - -:passTest -echo Success: %1 -goto end - -:noDirSpecified -echo runtest: Error: Syntax: runtest testDirectory [ additionalTestArguments ... ] -goto errorEnd - -:noDirExists -echo runtest: Error: There is no test directory %1 -goto errorEnd - -:noRunTest -echo runtest: Error: no runtest.bat found in test directory %1 -goto errorEnd - -:errorEnd -popd -exit /b 1 - -:end -popd -exit /b 0 diff --git a/Test/runtestall.bat b/Test/runtestall.bat deleted file mode 100644 index 207bb030..00000000 --- a/Test/runtestall.bat +++ /dev/null @@ -1,24 +0,0 @@ -@echo off -setlocal - -set errors=0 - -if "%1" == "short" goto UseShort - -set IncludeLong=True -goto Loop - -:UseShort -set IncludeLong=False -shift -goto Loop - -:Loop -for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Use call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1 - -if not %IncludeLong%==True goto End - -for /F "eol=; tokens=1,2,3*" %%i in (alltests.txt) do if %%j==Long call runtest.bat %%i %1 %2 %3 %4 %5 %6 %7 %8 %9 || set errors=1 - -:End -exit /b %errors% \ No newline at end of file diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer deleted file mode 100644 index 90bbcc78..00000000 --- a/Test/vacid0/Answer +++ /dev/null @@ -1,12 +0,0 @@ - --------------------- LazyInitArray.dfy -------------------- - -Dafny program verifier finished with 7 verified, 0 errors - --------------------- SparseArray.dfy -------------------- - -Dafny program verifier finished with 9 verified, 0 errors - --------------------- Composite.dfy -------------------- - -Dafny program verifier finished with 16 verified, 0 errors diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking deleted file mode 100644 index e69de29b..00000000 diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat deleted file mode 100644 index d7f31c3b..00000000 --- a/Test/vacid0/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /verifySeparately %* LazyInitArray.dfy SparseArray.dfy Composite.dfy - -rem for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 %* %%f -rem ) diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer deleted file mode 100644 index 43eddcb1..00000000 --- a/Test/vstte2012/Answer +++ /dev/null @@ -1,24 +0,0 @@ - --------------------- Two-Way-Sort.dfy -------------------- - -Dafny program verifier finished with 4 verified, 0 errors - --------------------- Combinators.dfy -------------------- - -Dafny program verifier finished with 25 verified, 0 errors - --------------------- RingBuffer.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- RingBufferAuto.dfy -------------------- - -Dafny program verifier finished with 13 verified, 0 errors - --------------------- Tree.dfy -------------------- - -Dafny program verifier finished with 15 verified, 0 errors - --------------------- BreadthFirstSearch.dfy -------------------- - -Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat deleted file mode 100644 index 7e597fd4..00000000 --- a/Test/vstte2012/runtest.bat +++ /dev/null @@ -1,23 +0,0 @@ -@echo off -setlocal - -set BINARIES=..\..\Binaries -set DAFNY_EXE=%BINARIES%\Dafny.exe - -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy - -echo. -echo -------------------- BreadthFirstSearch.dfy -------------------- -%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /vcsMaxKeepGoingSplits:10 %* BreadthFirstSearch.dfy - -rem for %%f in ( -rem Two-Way-Sort.dfy -rem Combinators.dfy -rem RingBuffer.dfy RingBufferAuto.dfy -rem Tree.dfy -rem BreadthFirstSearch.dfy -rem ) do ( -rem echo. -rem echo -------------------- %%f -------------------- -rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -rem ) -- cgit v1.2.3