-------------------- Simple.dfy -------------------- // Simple.dfy class MyClass { var x: int; method M(s: bool, lotsaObjects: set) returns (t: object, u: set, v: seq>) requires s; modifies this, lotsaObjects; ensures t == t; ensures old(null) != this; { x := 12; while (x < 100) invariant x <= 100; { x := x + 17; if (x % 20 == 3) { x := this.x + 1; } else { this.x := x + 0; } t, u, v := M(true, lotsaObjects); var to: MyClass; to, u, v := this.M(true, lotsaObjects); to, u, v := to.M(true, lotsaObjects); assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10]; } } function F(x: int, y: int, h: WildData, k: WildData): WildData { if x < 0 then h else if x == 0 then if if h == k then true else false then h else if y == 0 then k else h else k } } datatype List = Nil | Cons(T, List); datatype WildData = Something | JustAboutAnything(bool, myName: set, int, WildData) | More(List); class C { var w: WildData; var list: List; } Dafny program verifier finished with 0 verified, 0 errors -------------------- TypeTests.dfy -------------------- TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type 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(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed 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) 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) 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) 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,9): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type 34 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(199,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Then SmallTests.dfy(206,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Else (0,0): anon3 (0,0): anon13_Then SmallTests.dfy(226,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Else (0,0): anon3 (0,0): anon13_Else (0,0): anon6 (0,0): anon14_Then (0,0): anon11 SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold. SmallTests.dfy(249,30): Related location: This is the precondition that might not hold. Execution trace: (0,0): anon0 SmallTests.dfy(266,19): anon3_Else (0,0): anon2 SmallTests.dfy(376,12): Error: assertion violation Execution trace: (0,0): anon0 SmallTests.dfy(386,12): Error: assertion violation Execution trace: (0,0): anon0 SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon3_Else SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path. SmallTests.dfy(300,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(347,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon8_Then (0,0): anon7 SmallTests.dfy(354,10): Error: assertion violation Execution trace: (0,0): anon0 SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon3_Else SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this return path. SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon6_Else SmallTests.dfy(561,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then (0,0): anon2 SmallTests.dfy(575,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(577,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(570,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(584,18): Error: target object may be null Execution trace: (0,0): anon0 SmallTests.dfy(597,10): Error: assertion violation Execution trace: (0,0): anon0 Dafny program verifier finished with 68 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: assignment may update an object not in the enclosing context's modifies clause Execution trace: (0,0): anon0 Definedness.dfy(86,10): Error: target object may be null 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 Dafny program verifier finished with 3 verified, 3 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 this is a ghost method or because the statement 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) ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3) ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array) 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, got GenericClass) ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList, expected GList) 48 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 8 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(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) 11 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(12,7): Error: module T named among imports does not exist ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G 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(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T) Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M Modules0.dfy(48,12): Error: new can be applied only to reference types (got T) Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?) Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?) Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?) Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?) Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?) Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?) Modules0.dfy(250,15): Error: unresolved identifier: X Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X Modules0.dfy(294,16): Error: member R does not exist in class B Modules0.dfy(294,6): Error: expected method call, found expression Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context 30 resolution/type errors detected in Modules0.dfy -------------------- Modules1.dfy -------------------- Modules1.dfy(74,16): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then Modules1.dfy(86,16): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then Modules1.dfy(88,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Else Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0 Execution trace: (0,0): anon0 Modules1.dfy(58,3): Error: failure to decrease termination measure Execution trace: (0,0): anon0 Dafny program verifier finished with 19 verified, 5 errors -------------------- 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(113,12): Error: left-hand sides 0 and 1 may refer to the same location Execution trace: (0,0): anon0 (0,0): anon3 (0,0): anon11_Else (0,0): anon6 (0,0): anon12_Then Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location 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: left-hand sides 0 and 1 may refer to the same location 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 Dafny program verifier finished with 19 verified, 11 errors -------------------- ControlStructures.dfy -------------------- 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(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(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 -------------------- 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 -------------------- 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(179,5): Error BP5003: A postcondition might not hold on this return path. Refinement.dfy(112,15): Related location: This is the postcondition that might not hold. Refinement.dfy(176,9): Related location: Related location Execution trace: (0,0): anon0 Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path. Refinement.dfy(120,15): Related location: This is the postcondition that might not hold. Refinement.dfy(176,9): Related location: Related location Execution trace: (0,0): anon0 (0,0): anon4_Then (0,0): anon3 Refinement.dfy(189,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 declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base 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' instead of 'set') 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(84,16): Error: assertion violation Execution trace: (0,0): anon0 Predicates.dfy(88,14): Error: assertion violation Execution trace: (0,0): anon0 Predicates.dfy[Tricky_Full](121,5): Error BP5003: A postcondition might not hold on this return path. Predicates.dfy[Tricky_Full](120,15): Related location: This is the postcondition that might not hold. Predicates.dfy(131,7): Related location: Related location Predicates.dfy[Tricky_Full](111,9): Related location: Related location Execution trace: (0,0): anon0 Predicates.dfy(159,5): Error BP5003: A postcondition might not hold on this return path. Predicates.dfy(158,15): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 Predicates.dfy[Q1](149,5): Error BP5003: A postcondition might not hold on this return path. Predicates.dfy[Q1](148,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 -------------------- 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(199,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Then SmallTests.dfy(206,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Else (0,0): anon3 (0,0): anon13_Then SmallTests.dfy(226,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Else (0,0): anon3 (0,0): anon13_Else (0,0): anon6 (0,0): anon14_Then (0,0): anon11 SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold. SmallTests.dfy(249,30): Related location: This is the precondition that might not hold. Execution trace: (0,0): anon0 SmallTests.dfy(266,19): anon3_Else (0,0): anon2 SmallTests.dfy(376,12): Error: assertion violation Execution trace: (0,0): anon0 SmallTests.dfy(386,12): Error: assertion violation Execution trace: (0,0): anon0 SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon3_Else SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path. SmallTests.dfy(300,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(347,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon8_Then (0,0): anon7 SmallTests.dfy(354,10): Error: assertion violation Execution trace: (0,0): anon0 SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon3_Else SmallTests.dfy(408,10): Error BP5003: A postcondition might not hold on this return path. SmallTests.dfy(411,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon6_Else SmallTests.dfy(561,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then (0,0): anon2 SmallTests.dfy(575,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(577,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(570,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(584,18): Error: target object may be null Execution trace: (0,0): anon0 SmallTests.dfy(597,10): Error: assertion violation Execution trace: (0,0): anon0 Dafny program verifier finished with 68 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(202,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Then out.tmp.dfy(208,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Else (0,0): anon3 (0,0): anon13_Then out.tmp.dfy(229,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon12_Else (0,0): anon3 (0,0): anon13_Else (0,0): anon6 (0,0): anon14_Then (0,0): anon11 out.tmp.dfy(266,24): Error BP5002: A precondition for this call might not hold. out.tmp.dfy(247,30): Related location: This is the precondition that might not hold. Execution trace: (0,0): anon0 out.tmp.dfy(263,19): anon3_Else (0,0): anon2 out.tmp.dfy(286,12): Error: assertion violation Execution trace: (0,0): anon0 out.tmp.dfy(296,12): Error: assertion violation Execution trace: (0,0): anon0 out.tmp.dfy(306,6): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon3_Else out.tmp.dfy(422,3): Error BP5003: A postcondition might not hold on this return path. out.tmp.dfy(416,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(446,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon8_Then (0,0): anon7 out.tmp.dfy(451,10): Error: assertion violation Execution trace: (0,0): anon0 out.tmp.dfy(461,4): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon3_Else out.tmp.dfy(469,10): Error BP5003: A postcondition might not hold on this return path. out.tmp.dfy(470,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon6_Else out.tmp.dfy(507,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then (0,0): anon2 out.tmp.dfy(521,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(523,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(516,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(530,18): Error: target object may be null Execution trace: (0,0): anon0 out.tmp.dfy(543,10): Error: assertion violation Execution trace: (0,0): anon0 Dafny program verifier finished with 68 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