diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-07 17:24:46 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-07 17:24:46 -0700 |
| commit | 661faf59f8e1003cdbf339260d1293e8dd77f2df (patch) | |
| tree | 37e11e8a86658fe4d69b38572f3b6fadd8d287c9 /Test | |
| parent | 8de9fcae1a91acce9a1e59f292f05a95c81b3dbc (diff) | |
| parent | 93d9965a347b1a6ad70007822f01c2b032ea5436 (diff) | |
Merge
Diffstat (limited to 'Test')
57 files changed, 775 insertions, 3337 deletions
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 c15049ba..00000000 --- a/Test/dafny0/Answer +++ /dev/null @@ -1,2609 +0,0 @@ -
--------------------- Simple.dfy --------------------
-// Simple.dfy
-
-class MyClass<T, U> {
- var x: int;
-
- method M(s: bool, lotsaObjects: set<object>)
- returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
- 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<T,U>;
- 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<T> = Nil | Cons(T, List<T>)
-
-datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)
-
-class C {
- var w: WildData;
- var list: List<bool>;
-}
-
-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<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-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<int>)
-ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-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<T>)
-ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
-ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)
-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<int>, got GenericClass<bool>)
-ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-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
-134 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<T>)
-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<C>' instead of 'set<C>')
-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<T,int,V> and Weird<T,bool,V>)
-LiberalEquality.dfy(54,14): Error: arguments must have the same type (got array<int> and array<bool>)
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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 && <boolean expression>"
-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
-
-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/Array.dfy b/Test/dafny0/Array.dfy index 1b41267e..f6477708 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -137,6 +137,19 @@ class A { a != null && 0 <= j && j <= a.Length &&
a[j..j] == []
}
+
+ predicate Q0(s: seq<int>)
+ predicate Q1(s: seq<int>)
+ method FrameTest(a: array<int>) returns (b: array<int>)
+ requires a != null && Q0(a[..]);
+ {
+ b := CreateArray(a);
+ assert Q0(a[..]); // this should still be known after the call to CreateArray
+ assert Q1(b[..]);
+ }
+ method CreateArray(a: array<int>) returns (b: array<int>)
+ requires a != null;
+ ensures fresh(b) && Q1(b[..]);
}
type B;
diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect index 86a19c51..081fd258 100644 --- a/Test/dafny0/Array.dfy.expect +++ b/Test/dafny0/Array.dfy.expect @@ -61,47 +61,47 @@ Execution trace: (0,0): anon10_Then
(0,0): anon11_Then
(0,0): anon12_Else
-Array.dfy(150,6): Error: insufficient reads clause to read array element
+Array.dfy(163,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
+Array.dfy(171,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
+Array.dfy(187,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
+Array.dfy(194,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.
+Array.dfy(219,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(218,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.
+Array.dfy(243,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(242,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.
+Array.dfy(249,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(248,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
+Array.dfy(264,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
+Array.dfy(265,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
+Dafny program verifier finished with 46 verified, 20 errors
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy index 8050aded..83b2a571 100644 --- a/Test/dafny0/Computations.dfy +++ b/Test/dafny0/Computations.dfy @@ -184,3 +184,26 @@ ghost method test_fib3(k: nat, m: nat) var y := 12;
assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
}
+
+module NeedsAllLiteralsAxiom {
+ // The following test shows that there exist an example that
+ // benefits from the all-literals axiom. (It's not clear how
+ // important such an example is, nor is it clear what the cost
+ // of including the all-literals axiom is.)
+
+ function trick(n: nat, m: nat): nat
+ decreases n; // note that m is not included
+ {
+ if n < m || m==0 then n else trick(n-m, m) + m
+ }
+
+ lemma lemma_trick(n: nat, m: nat)
+ ensures trick(n, m) == n;
+ {
+ }
+
+ lemma calc_trick(n: nat, m: nat)
+ ensures trick(100, 10) == 100;
+ {
+ }
+}
diff --git a/Test/dafny0/Computations.dfy.expect b/Test/dafny0/Computations.dfy.expect index 85c793d4..71fc8a81 100644 --- a/Test/dafny0/Computations.dfy.expect +++ b/Test/dafny0/Computations.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 58 verified, 0 errors
+Dafny program verifier finished with 63 verified, 0 errors
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy new file mode 100644 index 00000000..6a49e733 --- /dev/null +++ b/Test/dafny0/DirtyLoops.dfy @@ -0,0 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M(S: set<int>) {
+ forall s | s in S ensures s < 0;
+}
diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect new file mode 100644 index 00000000..5c12e1ef --- /dev/null +++ b/Test/dafny0/DirtyLoops.dfy.expect @@ -0,0 +1,4 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
+
+Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Test/dafny0/Inverses.dfy b/Test/dafny0/Inverses.dfy new file mode 100644 index 00000000..7995255a --- /dev/null +++ b/Test/dafny0/Inverses.dfy @@ -0,0 +1,112 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This identity function is used to so that if the occurrence of i below
+// that is enclosed by Id gets chosen by the SMT solver as a trigger, then
+// Id will be part of that trigger. This means that the quantifier will
+// not match, and thus the 'forall' statement will be useless and the method
+// will not verify. If, however, the inverting functionality in Dafny
+// works properly, then the 'i' in the right-hand side of the forall assignments
+// below will not be chosen in any trigger, and then the methods should
+// verify.
+function method Id(x: int): int { x }
+
+method Copy<T>(a: array<T>) returns (r: array<T>)
+ requires a != null;
+ ensures fresh(r) && r.Length == a.Length && forall k :: 0 <= k < a.Length ==> r[k] == a[k];
+{
+ r := new T[a.Length];
+ forall i | 0 <= i < a.Length {
+ r[i] := a[Id(i)];
+ }
+}
+
+method ShiftLeftA<T>(a: array<T>, n: nat) returns (r: array<T>)
+ requires a != null && n <= a.Length;
+ ensures fresh(r) && r.Length == a.Length - n && forall k :: n <= k < a.Length ==> r[k - n] == a[k];
+{
+ r := new T[a.Length - n];
+ forall i | 0 <= i < a.Length - n {
+ r[i] := a[i + n];
+ }
+}
+
+method ShiftLeftB<T>(a: array<T>, n: nat) returns (r: array<T>)
+ requires a != null && n <= a.Length;
+ ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];
+{
+ r := new T[a.Length - n];
+ forall i | n <= i < a.Length {
+ r[i - n] := a[Id(i)];
+ }
+}
+
+method ShiftLeftC<T>(a: array<T>, n: nat) returns (r: array<T>)
+ requires a != null && n <= a.Length;
+ ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];
+{
+ r := new T[a.Length - n];
+ forall i | n <= i < a.Length {
+ r[i + 15 - n - 15] := a[Id(i)];
+ }
+}
+
+method Insert<T>(a: array<T>, p: nat, n: nat) returns (r: array<T>)
+ requires a != null && p <= a.Length;
+ ensures fresh(r) && r.Length == a.Length + n;
+ ensures forall k :: 0 <= k < p ==> r[k] == a[k];
+ ensures forall k :: p <= k < a.Length ==> r[k + n] == a[k];
+{
+ r := new T[a.Length + n];
+ forall i | 0 <= i < a.Length {
+ r[if i < p then i else i + n] := a[Id(i)];
+ }
+}
+
+method RotateA<T>(a: array<T>) returns (r: array<T>)
+ requires a != null;
+ ensures fresh(r) && r.Length == a.Length;
+ ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+ r := new T[a.Length];
+ forall i | 0 <= i < a.Length {
+ r[(i + 1) % a.Length] := a[Id(i)]; // error: Dafny does not find an inverse for this one,
+ // which causes Z3 to pick Id(i) as the trigger, which
+ // causes the verification to fail.
+ }
+}
+
+method RotateB<T>(a: array<T>) returns (r: array<T>)
+ requires a != null;
+ ensures fresh(r) && r.Length == a.Length;
+ ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+ r := new T[a.Length];
+ forall i | 0 <= i < a.Length {
+ r[if i + 1 == a.Length then 0 else i + 1] := a[Id(i)]; // error: Dafny does not find an inverse
+ // for this one, so (like in RotateA),
+ // the verification fails.
+ }
+}
+
+method RotateC<T>(a: array<T>) returns (r: array<T>)
+ requires a != null;
+ ensures fresh(r) && r.Length == a.Length;
+ ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+ r := new T[a.Length];
+ forall i | 0 <= i < a.Length {
+ r[if i == a.Length - 1 then 0 else i + 1] := a[Id(i)]; // yes, Dafny can invert this one
+ }
+}
+
+method RotateD<T>(a: array<T>) returns (r: array<T>)
+ requires a != null;
+ ensures fresh(r) && r.Length == a.Length;
+ ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];
+{
+ r := new T[a.Length];
+ forall i | 0 <= i < a.Length {
+ r[if a.Length - 1 == i then 0 else i + 1] := a[Id(i)]; // yes, Dafny can invert this one
+ }
+}
diff --git a/Test/dafny0/Inverses.dfy.expect b/Test/dafny0/Inverses.dfy.expect new file mode 100644 index 00000000..a04f21dc --- /dev/null +++ b/Test/dafny0/Inverses.dfy.expect @@ -0,0 +1,12 @@ +Inverses.dfy(70,1): Error BP5003: A postcondition might not hold on this return path.
+Inverses.dfy(69,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Else
+Inverses.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.
+Inverses.dfy(82,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Else
+
+Dafny program verifier finished with 17 verified, 2 errors
diff --git a/Test/dafny0/MatchBraces.dfy b/Test/dafny0/MatchBraces.dfy new file mode 100644 index 00000000..7da3647d --- /dev/null +++ b/Test/dafny0/MatchBraces.dfy @@ -0,0 +1,147 @@ +// RUN: %dafny /print:"%t.print" /env:0 /dprint:- "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Color = Red | Green | Blue
+
+// ----- match expressions in general positions
+
+method M(c: Color, d: Color) {
+ var x := match c
+ case Red => 5
+ case Green => 7
+ case Blue => 11;
+ var y := match c
+ case Red => 0.3
+ case Green => (match d case Red => 0.18 case Green => 0.21 case Blue => 0.98)
+ case Blue => 98.0;
+ var z := match c
+ case Red => Green
+ case Green => match d {
+ case Red => Red
+ case Green => Blue
+ case Blue => Red
+ }
+ case Blue => Green;
+ var w := match c { case Red => 2 case Green => 3 case Blue => 4 } + 10;
+ var t := match c
+ case Red => 0
+ case Green => (match d {
+ case Red => 2
+ case Green => 2
+ case Blue => 1
+ } + (((match d case Red => 10 case Green => 8 case Blue => 5))))
+ case Blue => (match d {
+ case Red => 20
+ case Green => 20
+ case Blue => 10
+ } + (((match d case Red => 110 case Green => 108 case Blue => 105))));
+}
+
+// ----- match expressions in top-level positions
+
+function Heat(c: Color): int
+{
+ match c
+ case Red => 10
+ case Green => 12
+ case Blue => 14
+}
+
+function IceCream(c: Color): int
+{
+ match c {
+ case Red => 0
+ case Green => 4
+ case Blue => 1
+ }
+}
+
+function Flowers(c: Color, d: Color): int
+{
+ match c {
+ case Red =>
+ match d {
+ case Red => 0
+ case Green => 1
+ case Blue => 2
+ }
+ case Green =>
+ match d {
+ case Red => 3
+ case Green => 3
+ case Blue => 2
+ } + 20
+ case Blue =>
+ match d {
+ case Red => 9
+ case Green => 8
+ case Blue => 7
+ } +
+ ((match d case Red => 23 case Green => 29 case Blue => 31))
+ }
+}
+
+// ----- match statements
+
+method P(c: Color, d: Color) {
+ var x: int;
+ match c {
+ case Red =>
+ x := 20;
+ case Green =>
+ case Blue =>
+ }
+ match c
+ case Red =>
+ match d {
+ case Red =>
+ case Green =>
+ case Blue =>
+ }
+ case Green =>
+ var y := 25;
+ var z := y + 3;
+ case Blue =>
+ {
+ var y := 25;
+ var z := y + 3;
+ }
+ match d // note: this 'match' is part of the previous case
+ case Red =>
+ case Green =>
+ x := x + 1;
+ case Blue =>
+}
+
+lemma HeatIsEven(c: Color)
+ ensures Heat(c) % 2 == 0;
+{
+ match c
+ case Red =>
+ assert 10 % 2 == 0;
+ case Green =>
+ assert 12 % 2 == 0;
+ case Blue => // all looks nice, huh? :)
+ // obvious
+}
+
+method DegenerateExamples(c: Color)
+ requires Heat(c) == 10; // this implies c == Red
+{
+ match c
+ case Red =>
+ case Green =>
+ match c { }
+ case Blue =>
+ match c
+}
+
+method MoreDegenerateExamples(c: Color)
+ requires Heat(c) == 10; // this implies c == Red
+{
+ if c == Green {
+ var x: int := match c;
+ var y: int := match c {};
+ var z := match c case Blue => 4;
+ }
+}
diff --git a/Test/dafny0/MatchBraces.dfy.expect b/Test/dafny0/MatchBraces.dfy.expect new file mode 100644 index 00000000..dfe1215f --- /dev/null +++ b/Test/dafny0/MatchBraces.dfy.expect @@ -0,0 +1,121 @@ +// MatchBraces.dfy
+
+datatype Color = Red | Green | Blue
+
+method M(c: Color, d: Color)
+{
+ var x := match c case Red => 5 case Green => 7 case Blue => 11;
+ var y := match c case Red => 0.3 case Green => (match d case Red => 0.18 case Green => 0.21 case Blue => 0.98) case Blue => 98.0;
+ var z := match c case Red => Green case Green => match d { case Red => Red case Green => Blue case Blue => Red } case Blue => Green;
+ var w := match c { case Red => 2 case Green => 3 case Blue => 4 } + 10;
+ var t := match c case Red => 0 case Green => match d { case Red => 2 case Green => 2 case Blue => 1 } + (match d case Red => 10 case Green => 8 case Blue => 5) case Blue => match d { case Red => 20 case Green => 20 case Blue => 10 } + match d case Red => 110 case Green => 108 case Blue => 105;
+}
+
+function Heat(c: Color): int
+{
+ match c
+ case Red =>
+ 10
+ case Green =>
+ 12
+ case Blue =>
+ 14
+}
+
+function IceCream(c: Color): int
+{
+ match c {
+ case Red =>
+ 0
+ case Green =>
+ 4
+ case Blue =>
+ 1
+ }
+}
+
+function Flowers(c: Color, d: Color): int
+{
+ match c {
+ case Red =>
+ match d {
+ case Red =>
+ 0
+ case Green =>
+ 1
+ case Blue =>
+ 2
+ }
+ case Green =>
+ match d { case Red => 3 case Green => 3 case Blue => 2 } + 20
+ case Blue =>
+ match d { case Red => 9 case Green => 8 case Blue => 7 } + match d case Red => 23 case Green => 29 case Blue => 31
+ }
+}
+
+method P(c: Color, d: Color)
+{
+ var x: int;
+ match c {
+ case Red =>
+ x := 20;
+ case Green =>
+ case Blue =>
+ }
+ match c
+ case Red =>
+ match d {
+ case Red =>
+ case Green =>
+ case Blue =>
+ }
+ case Green =>
+ var y := 25;
+ var z := y + 3;
+ case Blue =>
+ {
+ var y := 25;
+ var z := y + 3;
+ }
+ match d
+ case Red =>
+ case Green =>
+ x := x + 1;
+ case Blue =>
+}
+
+lemma HeatIsEven(c: Color)
+ ensures Heat(c) % 2 == 0;
+{
+ match c
+ case Red =>
+ assert 10 % 2 == 0;
+ case Green =>
+ assert 12 % 2 == 0;
+ case Blue =>
+}
+
+method DegenerateExamples(c: Color)
+ requires Heat(c) == 10;
+{
+ match c
+ case Red =>
+ case Green =>
+ match c {
+ }
+ case Blue =>
+ match c
+}
+
+method MoreDegenerateExamples(c: Color)
+ requires Heat(c) == 10;
+{
+ if c == Green {
+ var x: int := match c;
+ var y: int := match c { };
+ var z := match c case Blue => 4;
+ }
+}
+
+Dafny program verifier finished with 13 verified, 0 errors
+Compiled assembly into MatchBraces.dll
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 3d6034ad..3535f857 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -269,3 +269,29 @@ method MultiSetProperty0(s: multiset<object>, t: multiset<object>, p: object) assert s + (t - s) == t; // error
}
}
+
+// ---------- additional properties
+
+lemma UpperBoundOnOccurrenceCount(s: multiset<int>, x: int)
+ ensures 0 <= s[x] <= |s|;
+{
+}
+
+lemma MultisetCardinalityFromSequenceLength(s: seq<int>)
+ ensures |multiset(s)| == |s|;
+{
+}
+
+lemma Set_and_Multiset_Cardinalities(x: int, y: int)
+{
+ if * {
+ assert 1 <= |{x,y}| <= 2;
+ if x != y {
+ assert 2 <= |{x,y}|;
+ } else {
+ assert 2 <= |{x,y}|; // error
+ }
+ } else {
+ assert |multiset{x,y}| == 2;
+ }
+}
diff --git a/Test/dafny0/MultiSets.dfy.expect b/Test/dafny0/MultiSets.dfy.expect index cdee5d20..30534b11 100644 --- a/Test/dafny0/MultiSets.dfy.expect +++ b/Test/dafny0/MultiSets.dfy.expect @@ -18,5 +18,11 @@ Execution trace: (0,0): anon3
(0,0): anon12_Then
(0,0): anon14_Else
+MultiSets.dfy(292,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon3
+ (0,0): anon9_Else
-Dafny program verifier finished with 54 verified, 4 errors
+Dafny program verifier finished with 59 verified, 5 errors
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index e49f9823..74405fa5 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -905,3 +905,63 @@ module LhsLvalue { method MyLemma() returns (w: int)
}
+
+// ------------------- dirty loops -------------------
+
+method DirtyM(S: set<int>) {
+ forall s | s in S ensures s < 0;
+ assert s < 0; // error: s is unresolved
+}
+
+// ------------------- tuples -------------------
+
+method TupleResolution(x: int, y: int, r: real)
+{
+ var unit: () := ();
+ var expr: int := (x);
+ var pair: (int,int) := (x, x);
+ var triple: (int,int,int) := (y, x, x);
+ var badTriple: (int,real,int) := (y, x, r); // error: parameters 1 and 2 have the wrong types
+ var quadruple: (int,real,int,real) := (y, r, x); // error: trying to use a triple as a quadruple
+
+ assert unit == ();
+ assert pair.0 == pair.1;
+ assert triple.2 == x;
+
+ assert triple.2; // error: 2 has type int, not the expected bool
+ assert triple.3 == pair.x; // error(s): 3 and x are not destructors
+
+ var k0 := (5, (true, 2, 3.14));
+ var k1 := (((false, 10, 2.7)), 100, 120);
+ if k0.1 == k1.0 {
+ assert false;
+ } else if k0.1.1 < k1.0.1 {
+ assert k1.2 == 120;
+ }
+
+ // int and (int) are the same type (i.e., there are no 1-tuples)
+ var pp: (int) := x;
+ var qq: int := pp;
+}
+
+// --- filling in type arguments and checking that there aren't too many ---
+
+module TypeArgumentCount {
+ class C<T> {
+ var f: T;
+ }
+
+ method R0(a: array3, c: C)
+
+ method R1()
+ {
+ var a: array3;
+ var c: C;
+ }
+
+ method R2<T>()
+ {
+ var a: array3<T,int>; // error: too many type arguments
+ var c: C<T,int>; // error: too many type arguments
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index a811669c..e8e18ab7 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -54,6 +54,8 @@ ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements ( 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(964,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
+ResolutionErrors.dfy(965,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
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
@@ -133,4 +135,11 @@ ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specifi 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
-135 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
+144 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/Tuples.dfy b/Test/dafny0/Tuples.dfy new file mode 100644 index 00000000..81d054dd --- /dev/null +++ b/Test/dafny0/Tuples.dfy @@ -0,0 +1,34 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M(x: int)
+{
+ var unit := ();
+ var expr := (x);
+ var pair := (x, x);
+ var triple := (x, x, x);
+}
+
+method N(x: int, y: int)
+{
+ var unit: () := ();
+ var expr: int := (x);
+ var pair: (int,int) := (x, x);
+ var triple: (int,int,int) := (y, x, x);
+
+ assert unit == ();
+ assert pair.0 == pair.1;
+ assert triple.2 == x;
+ assert triple.0 == triple.1; // error: they may be different
+
+ var k := (24, 100 / y); // error: possible division by zero
+ assert 2 <= k.0 < 29;
+
+ var k0 := (5, (true, 2, 3.14));
+ var k1 := (((false, 10, 2.7)), 100, 120);
+ if k0.1 == k1.0 {
+ assert false;
+ } else if k0.1.1 < k1.0.1 {
+ assert k1.2 == 120;
+ }
+}
diff --git a/Test/dafny0/Tuples.dfy.expect b/Test/dafny0/Tuples.dfy.expect new file mode 100644 index 00000000..13c706d3 --- /dev/null +++ b/Test/dafny0/Tuples.dfy.expect @@ -0,0 +1,8 @@ +Tuples.dfy(22,19): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Tuples.dfy(24,21): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 2 errors
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 963916f0..900b6110 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -321,3 +321,35 @@ method IdentityMap(s: set<Pair>) returns (m: map) m, s := m[p.0 := p.1], s - {p};
}
}
+
+// -------------- auto filled-in type arguments for array types ------
+
+module ArrayTypeMagic {
+ method M(a: array2)
+ {
+ }
+
+ method F(b: array) returns (s: seq)
+ requires b != null;
+ {
+ return b[..];
+ }
+
+ datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)
+ datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)
+ datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)
+
+ function G(t: ArrayCubeTree): array3
+ {
+ match t
+ case Leaf(d) => d
+ case Node(l, _) => G(l)
+ }
+
+ datatype Nat = Zero | Succ(Nat)
+
+ datatype List<T> = Nil | Cons(T, List)
+
+ datatype Cell<T> = Mk(T)
+ datatype DList<T,U> = Nil(Cell) | Cons(T, U, DList)
+}
diff --git a/Test/dafny0/TypeParameters.dfy.expect b/Test/dafny0/TypeParameters.dfy.expect index 00efc26f..3d00e89a 100644 --- a/Test/dafny0/TypeParameters.dfy.expect +++ b/Test/dafny0/TypeParameters.dfy.expect @@ -49,4 +49,4 @@ Execution trace: TypeParameters.dfy(177,3): anon21_Else
TypeParameters.dfy(177,3): anon23_Else
-Dafny program verifier finished with 58 verified, 8 errors
+Dafny program verifier finished with 63 verified, 8 errors
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat deleted file mode 100644 index fe3a29e1..00000000 --- a/Test/dafny0/runtest.bat +++ /dev/null @@ -1,54 +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
-)
-
-%DAFNY_EXE% %* Compilation.dfy
-%DAFNY_EXE% %* CompilationErrors.dfy
diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy new file mode 100644 index 00000000..73db9f9c --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.v0.dfy @@ -0,0 +1,8 @@ +method foo()
+{
+ bar();
+ assert false;
+}
+
+method bar()
+ ensures false;
diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy new file mode 100644 index 00000000..db9fc01a --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy @@ -0,0 +1,8 @@ +method foo()
+{
+ bar();
+ assert false; // error
+}
+
+method bar()
+ ensures true;
diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Snapshots1.v0.dfy new file mode 100644 index 00000000..dd1e7deb --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.v0.dfy @@ -0,0 +1,13 @@ +method M()
+{
+ N();
+ assert false;
+}
+
+method N()
+ ensures P;
+
+predicate P
+{
+ false
+}
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy new file mode 100644 index 00000000..93ad6068 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.v1.dfy @@ -0,0 +1,13 @@ +method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P;
+
+predicate P
+{
+ true
+}
diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Snapshots2.v0.dfy new file mode 100644 index 00000000..37b9982b --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.v0.dfy @@ -0,0 +1,19 @@ +method M()
+{
+ N();
+ assert false;
+}
+
+method N()
+ ensures P;
+
+predicate P
+ ensures P == Q;
+
+predicate Q
+ ensures Q == R;
+
+predicate R
+{
+ false
+}
diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Snapshots2.v1.dfy new file mode 100644 index 00000000..03719744 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.v1.dfy @@ -0,0 +1,19 @@ +method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P;
+
+predicate P
+ ensures P == Q;
+
+predicate Q
+ ensures Q == R;
+
+predicate R
+{
+ true
+}
diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg new file mode 100644 index 00000000..07cb869f --- /dev/null +++ b/Test/dafny0/snapshots/lit.local.cfg @@ -0,0 +1,5 @@ +# This test is unusual in that we don't use the .bpl files +# directly on the command line. So instead we'll invoke +# files in this directory with extension '.snapshot'. There +# will only be one for now +config.suffixes = ['.snapshot'] diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot new file mode 100644 index 00000000..c3cf6b00 --- /dev/null +++ b/Test/dafny0/snapshots/runtest.snapshot @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect new file mode 100644 index 00000000..87827811 --- /dev/null +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -0,0 +1,27 @@ +
+-------------------- Snapshots0.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+Snapshots0.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 2 verified, 1 error
+
+-------------------- Snapshots1.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+Snapshots1.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
+
+-------------------- Snapshots2.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
+Snapshots2.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 5 verified, 1 error
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/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 7b2e7eda..a51a9fd0 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -176,6 +176,7 @@ abstract module M1 refines M0 { // discharge the "everything reachable is marked" postcondition, whose proof we postponed above
// by supplying an assume statement. Here, we refine that assume statement into an assert.
assert ...;
+ assume ...;
}
}
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/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index d7c142ee..5b7f3a0f 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -8,6 +8,7 @@ function eval(digits: seq<int>, base: int): int
requires 2 <= base;
+ decreases digits; // see comment in test_eval()
{
if |digits| == 0 then 0 else digits[0] + base * eval(digits[1..], base)
}
@@ -16,36 +17,21 @@ lemma test_eval() {
assert forall base :: 2 <= base ==> eval([], base) == 0;
assert forall base :: 2 <= base ==> eval([0], base) == 0;
- forall base | 2 <= base {
- calc {
- eval([0, 0], base);
- 0;
- }
- }
- calc {
- eval([3, 2], 10);
- 3 + 10 * eval([2], 10);
- 23;
- }
+ // To prove this automatically, it is necessary that the Lit axiom is sensitive only to the
+ // 'digits' argument being a literal. Hence, the explicit 'decreases digits' clause on the
+ // 'eval' function.
+ assert forall base :: 2 <= base ==> eval([0, 0], base) == 0;
+
+ assert eval([3, 2], 10) == 23;
+
var oct, dec := 8, 10;
- calc {
- eval([1, 3], oct);
- 1 + oct * eval([3], oct);
- 5 + dec * eval([2], dec);
- eval([5, 2], dec);
- }
+ assert eval([1, 3], oct) == eval([5, 2], dec);
assert eval([29], 420) == 29;
assert eval([29], 8) == 29;
- calc {
- eval([-2, 1, -3], 5);
- -2 + 5 * eval([1, -3], 5);
- -2 + 5 * 1 + 25 * eval([-3], 5);
- -2 + 5 * 1 + 25 * (-3);
- -72;
- }
+ assert eval([-2, 1, -3], 5) == -72;
}
// To achieve a unique (except for leading zeros) representation of each number, we
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/lit.site.cfg b/Test/lit.site.cfg index c9597a4c..d0b3a85b 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -125,7 +125,7 @@ else: lit_config.warning('Skipping solver sanity check on Windows') # Add diff tool substitution -commonDiffFlags=' --unified=3 --strip-trailing-cr --ignore-all-space' +commonDiffFlags=' --unified=3 --strip-trailing-cr' diffExecutable = None if os.name == 'posix': diffExecutable = 'diff' + commonDiffFlags 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 <dir>
-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 --- a/Test/vacid0/AnswerRuntimeChecking +++ /dev/null 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/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<T> 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
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 )
|