diff options
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 2098 |
1 files changed, 0 insertions, 2098 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer deleted file mode 100644 index ee455e7b..00000000 --- a/Test/dafny0/Answer +++ /dev/null @@ -1,2098 +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>;
-}
-
-Dafny program verifier finished with 0 verified, 0 errors
-
--------------------- TypeTests.dfy --------------------
-TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
-TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
-TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
-TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(44,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(53,6): Error: Duplicate local-variable name: z
-TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
-TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
-TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
-TypeTests.dfy(68,17): Error: member F in type C does not refer to a method
-TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)
-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)
-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type
-TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-36 resolution/type errors detected in TypeTests.dfy
-
--------------------- NatTypes.dfy --------------------
-NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon0
-NatTypes.dfy(31,10): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon0
- NatTypes.dfy(19,3): anon10_LoopHead
- (0,0): anon10_LoopBody
- NatTypes.dfy(19,3): anon11_Else
- (0,0): anon3
- (0,0): anon12_Then
- (0,0): anon9
-NatTypes.dfy(38,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Then
-NatTypes.dfy(40,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Then
-NatTypes.dfy(57,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-NatTypes.dfy(71,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon5_Else
- (0,0): anon6_Then
-NatTypes.dfy(89,19): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon6_Else
- (0,0): anon7_Else
- (0,0): anon8_Then
-NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon3_Then
-
-Dafny program verifier finished with 15 verified, 9 errors
-
--------------------- SmallTests.dfy --------------------
-SmallTests.dfy(30,11): Error: index out of range
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(61,36): Error: possible division by zero
-Execution trace:
- (0,0): anon12_Then
-SmallTests.dfy(62,51): Error: possible division by zero
-Execution trace:
- (0,0): anon12_Else
- (0,0): anon3
- (0,0): anon13_Else
-SmallTests.dfy(63,22): Error: target object may be null
-Execution trace:
- (0,0): anon12_Then
- (0,0): anon3
- (0,0): anon13_Then
- (0,0): anon6
-SmallTests.dfy(82,24): Error: target object may be null
-Execution trace:
- (0,0): anon0
- SmallTests.dfy(81,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- (0,0): anon10_Then
-SmallTests.dfy(116,5): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
-SmallTests.dfy(129,9): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-SmallTests.dfy(131,9): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-SmallTests.dfy(171,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): anon5
- (0,0): anon24_Else
- (0,0): anon11
- (0,0): anon26_Else
- (0,0): anon16
- (0,0): anon28_Then
- (0,0): anon29_Then
- (0,0): anon19
-SmallTests.dfy(195,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Then
-SmallTests.dfy(202,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon3
- (0,0): anon7_Then
-SmallTests.dfy(204,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon3
- (0,0): anon7_Else
-SmallTests.dfy(250,24): Error BP5002: A precondition for this call might not hold.
-SmallTests.dfy(228,30): Related location: This is the precondition that might not hold.
-Execution trace:
- (0,0): anon0
- SmallTests.dfy(245,19): anon3_Else
- (0,0): anon2
-SmallTests.dfy(355,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(365,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-SmallTests.dfy(285,3): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(279,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
- (0,0): anon18_Else
- (0,0): anon11
- (0,0): anon23_Then
- (0,0): anon24_Then
- (0,0): anon15
- (0,0): anon25_Else
-SmallTests.dfy(326,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon8_Then
- (0,0): anon7
-SmallTests.dfy(333,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon6_Else
-SmallTests.dfy(540,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-SmallTests.dfy(554,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(556,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(549,18): anon28_Else
- (0,0): anon4
- (0,0): anon29_Else
- (0,0): anon7
- (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(563,25): Error: target object may be null
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(576,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 70 verified, 26 errors
-
--------------------- Definedness.dfy --------------------
-Definedness.dfy(8,7): Error: possible division by zero
-Execution trace:
- (0,0): anon3_Else
-Definedness.dfy(15,16): Error: possible division by zero
-Execution trace:
- (0,0): anon0
-Definedness.dfy(24,16): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Definedness.dfy(25,21): Error: target object may be null
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-Definedness.dfy(26,17): Error: possible division by zero
-Execution trace:
- (0,0): anon0
-Definedness.dfy(33,16): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Definedness.dfy(50,18): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Definedness.dfy(51,3): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(50,22): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Definedness.dfy(57,18): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Definedness.dfy(58,3): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(57,22): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Definedness.dfy(65,3): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(64,22): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Definedness.dfy(85,7): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Definedness.dfy(86,5): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
-Definedness.dfy(87,10): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
-Definedness.dfy(92,14): Error: possible division by zero
-Execution trace:
- (0,0): anon0
-Definedness.dfy(92,23): Error: possible division by zero
-Execution trace:
- (0,0): anon0
-Definedness.dfy(93,15): Error: possible division by zero
-Execution trace:
- (0,0): anon0
-Definedness.dfy(98,12): Error: possible division by zero
-Execution trace:
- (0,0): anon0
-Definedness.dfy(105,15): Error: possible division by zero
-Execution trace:
- Definedness.dfy(105,5): anon8_LoopHead
- (0,0): anon8_LoopBody
- Definedness.dfy(105,5): anon9_Else
- (0,0): anon3
-Definedness.dfy(114,23): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
- Definedness.dfy(113,5): anon13_LoopHead
- (0,0): anon13_LoopBody
- (0,0): anon14_Then
-Definedness.dfy(120,17): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
- Definedness.dfy(113,5): anon13_LoopHead
- (0,0): anon13_LoopBody
- Definedness.dfy(113,5): anon14_Else
- (0,0): anon3
- (0,0): anon15_Then
- (0,0): anon6
- Definedness.dfy(119,5): anon16_LoopHead
- (0,0): anon16_LoopBody
- (0,0): anon17_Then
-Definedness.dfy(130,17): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
- Definedness.dfy(129,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
-Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry.
-Execution trace:
- (0,0): anon0
-Definedness.dfy(131,17): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
- Definedness.dfy(129,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
-Definedness.dfy(140,15): Error: possible division by zero
-Execution trace:
- (0,0): anon0
- Definedness.dfy(140,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- Definedness.dfy(140,5): anon10_Else
- (0,0): anon3
-Definedness.dfy(159,15): Error: possible division by zero
-Execution trace:
- (0,0): anon0
- Definedness.dfy(153,5): anon17_LoopHead
- (0,0): anon17_LoopBody
- Definedness.dfy(153,5): anon18_Else
- (0,0): anon3
- (0,0): anon19_Then
- (0,0): anon5
- (0,0): anon20_Then
- (0,0): anon8
- Definedness.dfy(159,5): anon21_LoopHead
- (0,0): anon21_LoopBody
- Definedness.dfy(159,5): anon22_Else
- (0,0): anon11
-Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry.
-Execution trace:
- (0,0): anon0
-Definedness.dfy(178,17): Error: possible violation of function precondition
-Execution trace:
- (0,0): anon0
- Definedness.dfy(170,5): anon19_LoopHead
- (0,0): anon19_LoopBody
- Definedness.dfy(170,5): anon20_Else
- (0,0): anon3
- (0,0): anon21_Then
- (0,0): anon6
- Definedness.dfy(177,5): anon22_LoopHead
- (0,0): anon22_LoopBody
- (0,0): anon23_Then
- (0,0): anon24_Then
- (0,0): anon11
-Definedness.dfy(193,19): Error: possible division by zero
-Execution trace:
- (0,0): anon0
- Definedness.dfy(191,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
-Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.
-Execution trace:
- (0,0): anon0
-Definedness.dfy(193,28): Error: possible division by zero
-Execution trace:
- (0,0): anon0
- Definedness.dfy(191,5): anon7_LoopHead
- (0,0): anon7_LoopBody
- (0,0): anon8_Then
-Definedness.dfy(212,10): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(214,46): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
- (0,0): anon5_Else
-Definedness.dfy(221,22): Error: target object may be null
-Execution trace:
- (0,0): anon5_Then
- (0,0): anon2
- (0,0): anon6_Then
-Definedness.dfy(234,10): Error BP5003: A postcondition might not hold on this return path.
-Definedness.dfy(237,24): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon7_Then
- (0,0): anon2
- (0,0): anon8_Else
-
-Dafny program verifier finished with 22 verified, 36 errors
-
--------------------- FunctionSpecifications.dfy --------------------
-FunctionSpecifications.dfy(32,3): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(28,13): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon9_Else
- (0,0): anon10_Else
- (0,0): anon11_Then
- (0,0): anon12_Else
- (0,0): anon7
-FunctionSpecifications.dfy(35,10): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(37,24): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon12_Else
- (0,0): anon15_Else
- (0,0): anon16_Then
- (0,0): anon11
-FunctionSpecifications.dfy(50,11): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon0
- (0,0): anon9_Then
- (0,0): anon3
-FunctionSpecifications.dfy(56,10): Error BP5003: A postcondition might not hold on this return path.
-FunctionSpecifications.dfy(57,22): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon5_Else
-
-Dafny program verifier finished with 3 verified, 4 errors
-
--------------------- ResolutionErrors.dfy --------------------
-ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
-ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
-ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
-ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)
-ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
-ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
-ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
-ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
-ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
-ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
-ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
-ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
-ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
-ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
-ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
-ResolutionErrors.dfy(84,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(89,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(90,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: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(261,2): Error: duplicate label
-ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
-ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
-ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
-ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
-ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)
-ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)
-ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(382,4): 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)
-57 resolution/type errors detected in ResolutionErrors.dfy
-
--------------------- ParseErrors.dfy --------------------
-ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
-ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
-ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
-ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
-ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
-ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive
-ParseErrors.dfy(62,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(63,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(68,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(69,2): error: this operator cannot continue this calculation
-ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
-14 parse errors detected in ParseErrors.dfy
-
--------------------- Array.dfy --------------------
-Array.dfy(10,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(17,16): Error: target object may be null
-Execution trace:
- (0,0): anon0
-Array.dfy(24,6): Error: index out of range
-Execution trace:
- (0,0): anon0
-Array.dfy(48,20): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Array.dfy(56,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(63,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(107,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(117,8): Error: insufficient reads clause to read the indicated range of array elements
-Execution trace:
- (0,0): anon9_Else
- (0,0): anon10_Then
- (0,0): anon11_Then
- (0,0): anon12_Then
-Array.dfy(119,8): Error: insufficient reads clause to read the indicated range of array elements
-Execution trace:
- (0,0): anon9_Else
- (0,0): anon10_Then
- (0,0): anon11_Then
- (0,0): anon12_Else
-Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements
-Execution trace:
- (0,0): anon9_Else
- (0,0): anon10_Then
- (0,0): anon11_Then
- (0,0): anon12_Else
-Array.dfy(121,8): Error: insufficient reads clause to read the indicated range of array elements
-Execution trace:
- (0,0): anon9_Else
- (0,0): anon10_Then
- (0,0): anon11_Then
- (0,0): anon12_Else
-Array.dfy(147,6): Error: insufficient reads clause to read array element
-Execution trace:
- (0,0): anon7_Else
- (0,0): anon8_Then
- (0,0): anon9_Then
-Array.dfy(155,6): Error: insufficient reads clause to read array element
-Execution trace:
- (0,0): anon7_Else
- (0,0): anon8_Then
- (0,0): anon9_Then
-Array.dfy(171,6): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
-Array.dfy(178,6): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
-Array.dfy(203,1): Error BP5003: A postcondition might not hold on this return path.
-Array.dfy(202,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Array.dfy(227,1): Error BP5003: A postcondition might not hold on this return path.
-Array.dfy(226,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Array.dfy(233,1): Error BP5003: A postcondition might not hold on this return path.
-Array.dfy(232,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Array.dfy(248,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(249,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 34 verified, 20 errors
-
--------------------- MultiDimArray.dfy --------------------
-MultiDimArray.dfy(53,21): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon11_Then
- (0,0): anon12_Then
-MultiDimArray.dfy(80,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(146,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(150,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(155,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(160,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(164,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(168,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(173,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(178,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(183,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(13,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(42,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(46,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(50,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(74,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(78,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(88,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(103,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(111,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(120,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(137,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(32,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(3,9): Error: module T does not exist
-ModulesCycle.dfy(6,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(5,8): Error: Duplicate name of top-level declaration: WazzupA
-Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA
-Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
-Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
-Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
-Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
-Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
-Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)
-Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)
-Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
-Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
-Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-Modules0.dfy(221,8): Error: new can be applied only to reference types (got X)
-Modules0.dfy(230,13): Error: Undeclared type X in module B
-Modules0.dfy(240,13): Error: unresolved identifier: X
-Modules0.dfy(241,15): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
-Modules0.dfy(280,12): Error: new can be applied only to reference types (got D)
-Modules0.dfy(283,25): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(284,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(284,6): Error: expected method call, found expression
-Modules0.dfy(285,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(285,6): Error: expected method call, found expression
-Modules0.dfy(307,24): Error: module Q_Imp does not exist
-Modules0.dfy(97,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(75,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-Modules1.dfy(88,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-Modules1.dfy(90,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-Modules1.dfy(53,3): Error: decreases expression must be bounded below by 0
-Execution trace:
- (0,0): anon0
-Modules1.dfy(59,3): Error: failure to decrease termination measure
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 22 verified, 5 errors
-
--------------------- Modules2.dfy --------------------
-Modules2.dfy(44,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(44,10): Error: new can be applied only to reference types (got C)
-Modules2.dfy(47,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(48,14): Error: The name D ambiguously refers to a type in one of the modules A, B
-Modules2.dfy(50,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(6,3): Error: failure to decrease termination measure
-Execution trace:
- (0,0): anon3_Else
-
-Dafny program verifier finished with 2 verified, 1 error
-
--------------------- Comprehensions.dfy --------------------
-Comprehensions.dfy(9,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(42,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-Basics.dfy(66,42): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon13_Then
- (0,0): anon14_Then
- (0,0): anon15_Then
- Basics.dfy(66,72): anon16_Else
- (0,0): anon8
- Basics.dfy(66,82): anon17_Else
- (0,0): anon10
- Basics.dfy(66,95): anon18_Else
- (0,0): anon12
-Basics.dfy(100,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon10_Then
-Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have 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(133,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
-Execution trace:
- (0,0): anon0
-Basics.dfy(145,19): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon11_Then
-Basics.dfy(147,10): Error: target object may be null
-Execution trace:
- (0,0): anon0
- (0,0): anon3
-Basics.dfy(147,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(152,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(163,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(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 32 verified, 11 errors
-
--------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,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(5,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(14,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(43,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(51,3): Error: missing case in case statement: Red
-Execution trace:
- (0,0): anon8_Else
- (0,0): anon9_Else
- (0,0): anon10_Else
- (0,0): anon11_Else
- (0,0): anon12_Then
-ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibilties
-Execution trace:
- (0,0): anon0
- (0,0): anon5_Else
-ControlStructures.dfy(215,18): Error: assertion violation
-Execution trace:
- (0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
- (0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- (0,0): anon3
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- (0,0): anon8
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon71_Then
- ControlStructures.dfy(210,9): anon72_LoopHead
- (0,0): anon72_LoopBody
- ControlStructures.dfy(210,9): anon73_Else
- (0,0): anon20
- (0,0): anon74_Then
- (0,0): anon29
-ControlStructures.dfy(232,21): Error: assertion violation
-Execution trace:
- (0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
- (0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- (0,0): anon3
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- (0,0): anon8
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon71_Then
- ControlStructures.dfy(210,9): anon72_LoopHead
- (0,0): anon72_LoopBody
- ControlStructures.dfy(210,9): anon73_Else
- (0,0): anon20
- ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon75_Then
- (0,0): after_4
- ControlStructures.dfy(221,7): anon77_LoopHead
- (0,0): anon77_LoopBody
- ControlStructures.dfy(221,7): anon78_Else
- (0,0): anon33
- ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon81_Then
- (0,0): anon38
- (0,0): after_9
- (0,0): anon86_Then
- (0,0): anon53
-ControlStructures.dfy(235,30): Error: assertion violation
-Execution trace:
- (0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
- (0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- (0,0): anon3
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- (0,0): anon8
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon68_Then
- (0,0): after_5
- (0,0): anon87_Then
- (0,0): anon88_Then
- (0,0): anon58
-ControlStructures.dfy(238,17): Error: assertion violation
-Execution trace:
- (0,0): anon0
- ControlStructures.dfy(194,3): anon62_LoopHead
- (0,0): anon62_LoopBody
- ControlStructures.dfy(194,3): anon63_Else
- (0,0): anon3
- ControlStructures.dfy(194,3): anon64_Else
- ControlStructures.dfy(198,5): anon65_LoopHead
- (0,0): anon65_LoopBody
- ControlStructures.dfy(198,5): anon66_Else
- (0,0): anon8
- ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon71_Then
- ControlStructures.dfy(210,9): anon72_LoopHead
- (0,0): anon72_LoopBody
- ControlStructures.dfy(210,9): anon73_Else
- (0,0): anon20
- ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon75_Then
- (0,0): after_4
- ControlStructures.dfy(221,7): anon77_LoopHead
- (0,0): anon77_LoopBody
- ControlStructures.dfy(221,7): anon78_Else
- (0,0): anon33
- ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon82_Then
- (0,0): anon85_Then
- (0,0): after_8
- (0,0): anon89_Then
- (0,0): anon61
-
-Dafny program verifier finished with 18 verified, 10 errors
-
--------------------- Termination.dfy --------------------
-Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop
-Execution trace:
- (0,0): anon0
- Termination.dfy(105,3): anon7_LoopHead
- (0,0): anon7_LoopBody
- Termination.dfy(105,3): anon8_Else
- (0,0): anon3
- Termination.dfy(105,3): anon9_Else
-Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
-Execution trace:
- (0,0): anon0
- Termination.dfy(113,3): anon9_LoopHead
- (0,0): anon9_LoopBody
- Termination.dfy(113,3): anon10_Else
- (0,0): anon11_Then
- (0,0): anon5
- Termination.dfy(113,3): anon12_Else
-Termination.dfy(122,3): Error: decreases expression might not decrease
-Execution trace:
- (0,0): anon0
- Termination.dfy(122,3): anon9_LoopHead
- (0,0): anon9_LoopBody
- Termination.dfy(122,3): anon10_Else
- (0,0): anon11_Then
- (0,0): anon5
- Termination.dfy(122,3): anon12_Else
-Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
-Execution trace:
- (0,0): anon0
- Termination.dfy(122,3): anon9_LoopHead
- (0,0): anon9_LoopBody
- Termination.dfy(122,3): anon10_Else
- (0,0): anon11_Then
- (0,0): anon5
- Termination.dfy(122,3): anon12_Else
-Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon6_Else
- (0,0): anon7_Else
- (0,0): anon8_Then
-Termination.dfy(291,3): Error: decreases expression might not decrease
-Execution trace:
- (0,0): anon0
- Termination.dfy(291,3): anon10_LoopHead
- (0,0): anon10_LoopBody
- Termination.dfy(291,3): anon11_Else
- Termination.dfy(291,3): anon12_Else
- (0,0): anon13_Else
-
-Dafny program verifier finished with 45 verified, 6 errors
-
--------------------- DTypes.dfy --------------------
-DTypes.dfy(15,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-DTypes.dfy(53,18): Error: assertion violation
-Execution trace:
- (0,0): anon0
-DTypes.dfy(117,13): Error: assertion violation
-DTypes.dfy(89,30): Related location: Related location
-Execution trace:
- (0,0): anon0
-DTypes.dfy(123,13): Error: assertion violation
-DTypes.dfy(89,20): Related location: Related location
-Execution trace:
- (0,0): anon0
-DTypes.dfy(133,12): Error: assertion violation
-DTypes.dfy(128,6): Related location: Related location
-DTypes.dfy(89,20): Related location: Related location
-Execution trace:
- (0,0): anon0
-DTypes.dfy(154,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(7,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(17,6): Error: LHS of assignment must denote a mutable variable or field
-ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement
-ParallelResolveErrors.dfy(40,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(52,13): Error: set choose operator not supported inside the enclosing parallel statement
-ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements
-ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods
-ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement
-ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause
-ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations
-15 resolution/type errors detected in ParallelResolveErrors.dfy
-
--------------------- Parallel.dfy --------------------
-Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.
-Parallel.dfy(57,14): Related location: This is the precondition that might not hold.
-Execution trace:
- (0,0): anon0
- (0,0): anon29_Else
- (0,0): anon7
- (0,0): anon32_Else
- (0,0): anon10
- (0,0): anon33_Then
- (0,0): anon34_Then
- (0,0): anon35_Then
- (0,0): anon14
-Parallel.dfy(35,5): Error: target object may be null
-Execution trace:
- (0,0): anon0
- (0,0): anon29_Else
- (0,0): anon7
- (0,0): anon32_Else
- (0,0): anon10
- (0,0): anon33_Else
- (0,0): anon16
- (0,0): anon36_Then
- (0,0): anon37_Then
- (0,0): anon38_Then
- (0,0): anon20
-Parallel.dfy(39,18): Error: possible violation of postcondition of parallel statement
-Execution trace:
- (0,0): anon0
- (0,0): anon29_Else
- (0,0): anon7
- (0,0): anon32_Else
- (0,0): anon10
- (0,0): anon33_Else
- (0,0): anon16
- (0,0): anon36_Else
- (0,0): anon22
- (0,0): anon39_Then
- (0,0): anon40_Then
- (0,0): anon26
-Parallel.dfy(44,19): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon29_Else
- (0,0): anon7
- (0,0): anon32_Else
- (0,0): anon10
- (0,0): anon33_Else
- (0,0): anon16
- (0,0): anon36_Else
- (0,0): anon22
- (0,0): anon39_Then
- (0,0): anon40_Then
-Parallel.dfy(90,19): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon10_Else
- (0,0): anon3
- (0,0): anon11_Then
-Parallel.dfy(96,20): Error: possible violation of postcondition of parallel statement
-Execution trace:
- (0,0): anon0
- (0,0): anon10_Else
- (0,0): anon3
- (0,0): anon11_Then
- (0,0): anon12_Then
-Parallel.dfy(119,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(182,12): Error: left-hand sides for different parallel-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(214,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
-Parallel.dfy(226,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
-Parallel.dfy(254,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon5
-Parallel.dfy(270,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon5
-Parallel.dfy(307,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
-
-Dafny program verifier finished with 41 verified, 13 errors
-
--------------------- TypeParameters.dfy --------------------
-TypeParameters.dfy(44,22): Error: assertion violation
-Execution trace:
- (0,0): anon0
-TypeParameters.dfy(66,27): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-TypeParameters.dfy(138,12): Error: assertion violation
-TypeParameters.dfy(138,28): Related location: Related location
-Execution trace:
- (0,0): anon0
- (0,0): anon14_Then
- TypeParameters.dfy(138,32): anon15_Else
- (0,0): anon5
-TypeParameters.dfy(140,12): Error: assertion violation
-TypeParameters.dfy(140,33): Related location: Related location
-Execution trace:
- (0,0): anon0
- (0,0): anon17_Then
- TypeParameters.dfy(140,37): anon18_Else
- (0,0): anon11
-TypeParameters.dfy(154,15): Error BP5005: This loop invariant might not be maintained by the loop.
-TypeParameters.dfy(154,38): Related location: Related location
-Execution trace:
- (0,0): anon0
- TypeParameters.dfy(147,3): anon17_LoopHead
- (0,0): anon17_LoopBody
- TypeParameters.dfy(147,3): anon18_Else
- (0,0): anon5
- (0,0): anon20_Then
- (0,0): anon8
- TypeParameters.dfy(153,3): anon21_LoopHead
- (0,0): anon21_LoopBody
- TypeParameters.dfy(153,3): anon22_Else
- (0,0): anon13
- TypeParameters.dfy(153,3): anon24_Else
-
-Dafny program verifier finished with 35 verified, 5 errors
-
--------------------- Datatypes.dfy --------------------
-Datatypes.dfy(79,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(167,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Then
-Datatypes.dfy(169,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon5_Then
-Datatypes.dfy(198,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
-Execution trace:
- (0,0): anon0
-Datatypes.dfy(201,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(222,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 32 verified, 6 errors
-
--------------------- Coinductive.dfy --------------------
-Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
-Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
-Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
-Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions
-8 resolution/type errors detected in Coinductive.dfy
-
--------------------- Corecursion.dfy --------------------
-Corecursion.dfy(15,13): Error: failure to decrease termination measure (note that only functions without side effects can called co-recursively)
-Execution trace:
- (0,0): anon3_Else
-Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-
-Dafny program verifier finished with 5 verified, 2 errors
-
--------------------- CoPredicates.dfy --------------------
-CoPredicates.dfy(45,1): Error BP5003: A postcondition might not hold on this return path.
-CoPredicates.dfy(44,11): Related location: This is the postcondition that might not hold.
-CoPredicates.dfy(30,22): Related location: Related location
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 12 verified, 1 error
-
--------------------- TypeAntecedents.dfy --------------------
-TypeAntecedents.dfy(32,13): Error: assertion violation
-Execution trace:
- (0,0): anon0
-TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this return path.
-TypeAntecedents.dfy(54,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): anon13
- (0,0): anon31_Else
- (0,0): anon18
- (0,0): anon33_Then
- (0,0): anon20
- (0,0): anon34_Then
- (0,0): anon35_Then
- (0,0): anon24
-TypeAntecedents.dfy(63,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 12 verified, 0 errors
-
--------------------- EqualityTypes.dfy --------------------
-EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
-EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
-EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes a different number of type parameters
-EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters
-EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
-EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
-EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
-EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
-8 resolution/type errors detected in EqualityTypes.dfy
-
--------------------- SplitExpr.dfy --------------------
-
-Dafny program verifier finished with 5 verified, 0 errors
-
--------------------- LoopModifies.dfy --------------------
-LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
-LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(14,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(14,4): anon10_Else
- (0,0): anon5
- LoopModifies.dfy(14,4): anon12_Else
-LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(42,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(42,4): anon10_Else
- (0,0): anon5
- LoopModifies.dfy(42,4): anon12_Else
-LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(57,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(57,4): anon10_Else
- (0,0): anon5
- LoopModifies.dfy(57,4): anon12_Else
-LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
-Execution trace:
- (0,0): anon0
-LoopModifies.dfy(98,8): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(90,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(90,4): anon10_Else
- (0,0): anon5
- LoopModifies.dfy(90,4): anon12_Else
-LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(134,4): anon17_LoopHead
- (0,0): anon17_LoopBody
- LoopModifies.dfy(134,4): anon18_Else
- (0,0): anon5
- LoopModifies.dfy(134,4): anon20_Else
- LoopModifies.dfy(139,7): anon21_LoopHead
- (0,0): anon21_LoopBody
- LoopModifies.dfy(139,7): anon22_Else
- (0,0): anon12
- LoopModifies.dfy(139,7): anon24_Else
-LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(193,4): anon9_LoopHead
- (0,0): anon9_LoopBody
- LoopModifies.dfy(193,4): anon10_Else
- (0,0): anon5
- LoopModifies.dfy(193,4): anon12_Else
-LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause
-Execution trace:
- (0,0): anon0
- LoopModifies.dfy(273,4): anon17_LoopHead
- (0,0): anon17_LoopBody
- LoopModifies.dfy(273,4): anon18_Else
- (0,0): anon5
- LoopModifies.dfy(273,4): anon20_Else
- LoopModifies.dfy(281,7): anon21_LoopHead
- (0,0): anon21_LoopBody
- LoopModifies.dfy(281,7): anon22_Else
- (0,0): anon12
- LoopModifies.dfy(281,7): anon24_Else
-
-Dafny program verifier finished with 23 verified, 9 errors
-
--------------------- Refinement.dfy --------------------
-Refinement.dfy(12,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(11,17): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Refinement.dfy[B](12,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(30,20): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Refinement.dfy(61,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Refinement.dfy(71,17): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Refinement.dfy(90,12): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(69,15): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon3_Else
-Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Refinement.dfy(180,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](112,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(177,9): Related location: Related location
-Execution trace:
- (0,0): anon0
-Refinement.dfy(184,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](120,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(177,9): Related location: Related location
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Then
- (0,0): anon3
-Refinement.dfy(190,7): Error: assertion violation
-Refinement.dfy[IncorrectConcrete](128,24): Related location: Related location
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 48 verified, 9 errors
-
--------------------- RefinementErrors.dfy --------------------
-RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions
-RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause
-RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate
-RefinementErrors.dfy(32,8): Error: a field re-declaration (xyz) must be to ghostify the field
-RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F
-RefinementErrors.dfy(35,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(35,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(35,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(36,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(37,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(54,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(30,10): Error: cannot have method call in return statement.
-ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
-ReturnErrors.dfy(41,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 16 verified, 0 errors
-
--------------------- ChainingDisjointTests.dfy --------------------
-
-Dafny program verifier finished with 6 verified, 0 errors
-
--------------------- CallStmtTests.dfy --------------------
-CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
-2 resolution/type errors detected in CallStmtTests.dfy
-
--------------------- MultiSets.dfy --------------------
-
-Dafny program verifier finished with 22 verified, 0 errors
-
--------------------- PredExpr.dfy --------------------
-PredExpr.dfy(4,12): Error: condition in assert expression might not hold
-Execution trace:
- (0,0): anon3_Else
-PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon6_Else
- (0,0): anon7_Else
-PredExpr.dfy(49,17): Error: condition in assert expression might not hold
-Execution trace:
- (0,0): anon0
-PredExpr.dfy(74,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon8_Else
- (0,0): anon3
- PredExpr.dfy(73,20): anon10_Else
- (0,0): anon6
-
-Dafny program verifier finished with 11 verified, 4 errors
-
--------------------- LetExpr.dfy --------------------
-LetExpr.dfy(5,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-LetExpr.dfy(104,21): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon11_Then
-
-Dafny program verifier finished with 19 verified, 2 errors
-
--------------------- Predicates.dfy --------------------
-Predicates.dfy[B](18,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[B](17,15): Related location: This is the postcondition that might not hold.
-Predicates.dfy(28,9): Related location: Related location
-Execution trace:
- (0,0): anon0
-Predicates.dfy(85,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Predicates.dfy(89,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Predicates.dfy[Tricky_Full](123,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Tricky_Full](122,15): Related location: This is the postcondition that might not hold.
-Predicates.dfy(133,7): Related location: Related location
-Predicates.dfy[Tricky_Full](113,9): Related location: Related location
-Execution trace:
- (0,0): anon0
-Predicates.dfy(161,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy(160,15): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-Predicates.dfy[Q1](151,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Q1](150,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(42,3): Error BP5003: A postcondition might not hold on this return path.
-Skeletons.dfy(41,15): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
- Skeletons.dfy[C0](29,5): anon12_LoopHead
- (0,0): anon12_LoopBody
- Skeletons.dfy[C0](29,5): anon13_Else
- (0,0): anon9
- Skeletons.dfy[C0](34,19): anon16_Else
- (0,0): anon11
-
-Dafny program verifier finished with 9 verified, 1 error
-
--------------------- Maps.dfy --------------------
-Maps.dfy(76,8): Error: element may not be in domain
-Execution trace:
- (0,0): anon0
-Maps.dfy(126,13): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 32 verified, 2 errors
-
--------------------- LiberalEquality.dfy --------------------
-LiberalEquality.dfy(18,14): Error: arguments must have the same type (got T and U)
-LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
-LiberalEquality.dfy(52,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(17,4): Error: cannot assign to variable defined previously
-RefinementModificationChecking.dfy(18,4): Error: cannot assign to variable defined previously
-2 resolution/type errors detected in RefinementModificationChecking.dfy
-
--------------------- TailCalls.dfy --------------------
-TailCalls.dfy(18,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
-TailCalls.dfy(30,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(37,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
-5 resolution/type errors detected in TailCalls.dfy
-
--------------------- Calculations.dfy --------------------
-Calculations.dfy(3,4): Error: index out of range
-Execution trace:
- (0,0): anon0
- (0,0): anon11_Then
-Calculations.dfy(8,13): Error: index out of range
-Execution trace:
- (0,0): anon0
- (0,0): anon13_Then
-Calculations.dfy(8,17): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon13_Then
-Calculations.dfy(36,11): Error: assertion violation
-Execution trace:
- (0,0): anon0
- Calculations.dfy(31,2): anon5_Else
-
-Dafny program verifier finished with 4 verified, 4 errors
-
--------------------- IteratorResolution.dfy --------------------
-IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
-IteratorResolution.dfy(76,19): Error: RHS (of type bool) not assignable to LHS (of type int)
-IteratorResolution.dfy(79,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
-IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)
-IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(123,9): Error: unresolved identifier: _decreases3
-IteratorResolution.dfy(124,21): Error: arguments must have the same type (got int and ?)
-IteratorResolution.dfy(125,14): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(132,9): Error: unresolved identifier: _decreases1
-IteratorResolution.dfy(137,9): Error: unresolved identifier: _decreases0
-12 resolution/type errors detected in IteratorResolution.dfy
-
--------------------- Iterators.dfy --------------------
-Iterators.dfy(100,22): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Iterators.dfy(103,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Then
- (0,0): anon3
-Iterators.dfy(174,28): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon15_Then
-Iterators.dfy(205,7): Error: an assignment to _new is only allowed to shrink the set
-Execution trace:
- (0,0): anon0
- Iterators.dfy(194,3): anon17_LoopHead
- (0,0): anon17_LoopBody
- Iterators.dfy(194,3): anon18_Else
- (0,0): anon5
- Iterators.dfy(194,3): anon20_Else
- (0,0): anon21_Then
-Iterators.dfy(209,21): Error: assertion violation
-Execution trace:
- (0,0): anon0
- Iterators.dfy(194,3): anon17_LoopHead
- (0,0): anon17_LoopBody
- Iterators.dfy(194,3): anon18_Else
- (0,0): anon5
- Iterators.dfy(194,3): anon20_Else
- (0,0): anon22_Then
-Iterators.dfy(37,14): Error BP5002: A precondition for this call might not hold.
-Iterators.dfy(1,10): Related location: This is the precondition that might not hold.
-Execution trace:
- (0,0): anon0
- (0,0): anon37_Then
- (0,0): anon2
- (0,0): anon38_Then
- (0,0): anon5
- (0,0): anon39_Then
-Iterators.dfy(86,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
-Iterators.dfy(116,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-Iterators.dfy(147,16): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
-Iterators.dfy(152,16): Error BP5002: A precondition for this call might not hold.
-Iterators.dfy(122,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(231,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- Iterators.dfy(222,3): anon15_LoopHead
- (0,0): anon15_LoopBody
- Iterators.dfy(222,3): anon16_Else
- (0,0): anon8
- Iterators.dfy(222,3): anon19_Else
- (0,0): anon20_Else
-
-Dafny program verifier finished with 38 verified, 11 errors
-
--------------------- Superposition.dfy --------------------
-
-Verifying CheckWellformed$$_0_M0.C.M ...
- [0 proof obligations] verified
-
-Verifying _0_M0.C.M ...
- [4 proof obligations] verified
-
-Verifying CheckWellformed$$_0_M0.C.P ...
- [4 proof obligations] verified
-
-Verifying CheckWellformed$$_0_M0.C.Q ...
-Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon5_Else
- [3 proof obligations] error
-
-Verifying CheckWellformed$$_0_M0.C.R ...
-Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon5_Else
- [3 proof obligations] error
-
-Verifying CheckWellformed$$_1_M1.C.M ...
- [0 proof obligations] verified
-
-Verifying RefinementImpl_M1$$_1_M1.C.M ...
- [0 proof obligations] verified
-
-Verifying CheckWellformed$$_1_M1.C.P ...
-Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy[M1](19,26): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon7_Else
- (0,0): anon9_Then
- (0,0): anon6
- [1 proof obligation] error
-
-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(30,11): Error: index out of range
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(61,36): Error: possible division by zero
-Execution trace:
- (0,0): anon12_Then
-SmallTests.dfy(62,51): Error: possible division by zero
-Execution trace:
- (0,0): anon12_Else
- (0,0): anon3
- (0,0): anon13_Else
-SmallTests.dfy(63,22): Error: target object may be null
-Execution trace:
- (0,0): anon12_Then
- (0,0): anon3
- (0,0): anon13_Then
- (0,0): anon6
-SmallTests.dfy(82,24): Error: target object may be null
-Execution trace:
- (0,0): anon0
- SmallTests.dfy(81,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- (0,0): anon10_Then
-SmallTests.dfy(116,5): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
-SmallTests.dfy(129,9): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-SmallTests.dfy(131,9): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-SmallTests.dfy(171,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): anon5
- (0,0): anon24_Else
- (0,0): anon11
- (0,0): anon26_Else
- (0,0): anon16
- (0,0): anon28_Then
- (0,0): anon29_Then
- (0,0): anon19
-SmallTests.dfy(195,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Then
-SmallTests.dfy(202,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon3
- (0,0): anon7_Then
-SmallTests.dfy(204,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon3
- (0,0): anon7_Else
-SmallTests.dfy(250,24): Error BP5002: A precondition for this call might not hold.
-SmallTests.dfy(228,30): Related location: This is the precondition that might not hold.
-Execution trace:
- (0,0): anon0
- SmallTests.dfy(245,19): anon3_Else
- (0,0): anon2
-SmallTests.dfy(355,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(365,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-SmallTests.dfy(285,3): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(279,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
- (0,0): anon18_Else
- (0,0): anon11
- (0,0): anon23_Then
- (0,0): anon24_Then
- (0,0): anon15
- (0,0): anon25_Else
-SmallTests.dfy(326,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon8_Then
- (0,0): anon7
-SmallTests.dfy(333,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon6_Else
-SmallTests.dfy(540,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-SmallTests.dfy(554,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(556,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(549,18): anon28_Else
- (0,0): anon4
- (0,0): anon29_Else
- (0,0): anon7
- (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(563,25): Error: target object may be null
-Execution trace:
- (0,0): anon0
-SmallTests.dfy(576,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 70 verified, 26 errors
-out.tmp.dfy(33,11): Error: index out of range
-Execution trace:
- (0,0): anon0
-out.tmp.dfy(69,37): Error: possible division by zero
-Execution trace:
- (0,0): anon12_Then
-out.tmp.dfy(70,52): Error: possible division by zero
-Execution trace:
- (0,0): anon12_Else
- (0,0): anon3
- (0,0): anon13_Else
-out.tmp.dfy(71,22): Error: target object may be null
-Execution trace:
- (0,0): anon12_Then
- (0,0): anon3
- (0,0): anon13_Then
- (0,0): anon6
-out.tmp.dfy(88,24): Error: target object may be null
-Execution trace:
- (0,0): anon0
- out.tmp.dfy(87,5): anon9_LoopHead
- (0,0): anon9_LoopBody
- (0,0): anon10_Then
-out.tmp.dfy(122,5): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
-out.tmp.dfy(135,9): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
-out.tmp.dfy(137,9): Error: call may violate context's modifies clause
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Else
-out.tmp.dfy(177,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): anon5
- (0,0): anon24_Else
- (0,0): anon11
- (0,0): anon26_Else
- (0,0): anon16
- (0,0): anon28_Then
- (0,0): anon29_Then
- (0,0): anon19
-out.tmp.dfy(199,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Then
-out.tmp.dfy(205,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon3
- (0,0): anon7_Then
-out.tmp.dfy(207,14): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon6_Else
- (0,0): anon3
- (0,0): anon7_Else
-out.tmp.dfy(245,24): Error BP5002: A precondition for this call might not hold.
-out.tmp.dfy(226,30): Related location: This is the precondition that might not hold.
-Execution trace:
- (0,0): anon0
- out.tmp.dfy(242,19): anon3_Else
- (0,0): anon2
-out.tmp.dfy(265,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-out.tmp.dfy(275,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-out.tmp.dfy(401,3): Error BP5003: A postcondition might not hold on this return path.
-out.tmp.dfy(395,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
- (0,0): anon18_Else
- (0,0): anon11
- (0,0): anon23_Then
- (0,0): anon24_Then
- (0,0): anon15
- (0,0): anon25_Else
-out.tmp.dfy(425,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon8_Then
- (0,0): anon7
-out.tmp.dfy(430,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-out.tmp.dfy(440,4): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon3_Else
-out.tmp.dfy(448,10): Error BP5003: A postcondition might not hold on this return path.
-out.tmp.dfy(449,41): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon6_Else
-out.tmp.dfy(486,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon3_Then
- (0,0): anon2
-out.tmp.dfy(500,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
-out.tmp.dfy(502,15): Error: left-hand sides 1 and 2 may refer to the same location
-Execution trace:
- (0,0): anon0
- (0,0): anon27_Then
- out.tmp.dfy(495,18): anon28_Else
- (0,0): anon4
- (0,0): anon29_Else
- (0,0): anon7
- (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
-out.tmp.dfy(509,25): Error: target object may be null
-Execution trace:
- (0,0): anon0
-out.tmp.dfy(522,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 70 verified, 26 errors
-
--------------------- LetExpr.dfy --------------------
-LetExpr.dfy(5,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-LetExpr.dfy(104,21): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon11_Then
-
-Dafny program verifier finished with 19 verified, 2 errors
-out.tmp.dfy(10,12): Error: assertion violation
-Execution trace:
- (0,0): anon0
-out.tmp.dfy(101,21): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon11_Then
-
-Dafny program verifier finished with 19 verified, 2 errors
-
-Dafny program verifier finished with 23 verified, 0 errors
-Compiled assembly into Compilation.exe
|