diff options
Diffstat (limited to 'Test')
32 files changed, 145 insertions, 140 deletions
diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect index 82fc2933..ab2bbc52 100644 --- a/Test/dafny0/Backticks.dfy.expect +++ b/Test/dafny0/Backticks.dfy.expect @@ -3,7 +3,7 @@ Execution trace: (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Backticks.dfy(77,7): Error: call may violate context's modifies clause
+Backticks.dfy(77,8): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect index 57a33c62..8a334754 100644 --- a/Test/dafny0/CallStmtTests.dfy.expect +++ b/Test/dafny0/CallStmtTests.dfy.expect @@ -1,3 +1,3 @@ CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(17,8): Error: actual out-parameter 0 is required to be a ghost variable
+CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/CoPrefix.dfy.expect b/Test/dafny0/CoPrefix.dfy.expect index c2453a09..c92a09c1 100644 --- a/Test/dafny0/CoPrefix.dfy.expect +++ b/Test/dafny0/CoPrefix.dfy.expect @@ -8,17 +8,17 @@ CoPrefix.dfy(168,15): Related location: This is the postcondition that might not Execution trace:
(0,0): anon0
(0,0): anon3_Else
-CoPrefix.dfy(176,5): Error: cannot prove termination; try supplying a decreases clause
+CoPrefix.dfy(176,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoPrefix.dfy(63,7): Error: failure to decrease termination measure
+CoPrefix.dfy(63,57): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon8_Else
(0,0): anon9_Then
-CoPrefix.dfy(76,7): Error: cannot prove termination; try supplying a decreases clause
+CoPrefix.dfy(76,56): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon7_Then
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index 9acb5a58..45d1e598 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -7,19 +7,19 @@ CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any read CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause
CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(95,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(115,24): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(121,28): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(135,26): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(141,30): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined
-CoResolution.dfy(202,12): Error: the type of this expression is underspecified
+CoResolution.dfy(202,13): Error: the type of this expression is underspecified
CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined
24 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect index ce3e3a8d..26fec211 100644 --- a/Test/dafny0/Coinductive.dfy.expect +++ b/Test/dafny0/Coinductive.dfy.expect @@ -13,5 +13,5 @@ Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
-Coinductive.dfy(148,5): Error: a recursive call from a copredicate can go only to other copredicates
+Coinductive.dfy(148,21): Error: a recursive call from a copredicate can go only to other copredicates
16 resolution/type errors detected in Coinductive.dfy
diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy index 7869fba3..f39aa4ce 100644 --- a/Test/dafny0/DatatypeUpdate.dfy +++ b/Test/dafny0/DatatypeUpdate.dfy @@ -28,3 +28,10 @@ function F(d: Dt): Dt {
d[x := 5]
}
+
+datatype NumericNames = NumNam(010: int)
+
+method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)
+{
+ pp := nn[010 := y]; // not to be confused with a field name 10
+}
diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect index 52595bf9..790f6509 100644 --- a/Test/dafny0/DatatypeUpdate.dfy.expect +++ b/Test/dafny0/DatatypeUpdate.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect index f6b51252..874df45e 100644 --- a/Test/dafny0/Datatypes.dfy.expect +++ b/Test/dafny0/Datatypes.dfy.expect @@ -47,11 +47,11 @@ Execution trace: (0,0): anon23_Then
(0,0): anon24_Else
(0,0): anon25_Then
-Datatypes.dfy(170,14): Error: assertion violation
+Datatypes.dfy(170,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-Datatypes.dfy(172,14): Error: assertion violation
+Datatypes.dfy(172,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect index f296ed4b..9f277582 100644 --- a/Test/dafny0/EqualityTypes.dfy.expect +++ b/Test/dafny0/EqualityTypes.dfy.expect @@ -5,7 +5,7 @@ EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality
EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
-EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)
+EqualityTypes.dfy(85,9): Error: type parameter 0 (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality)
EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)
@@ -26,10 +26,10 @@ EqualityTypes.dfy(210,8): Error: set argument type must support equality (got Co EqualityTypes.dfy(211,20): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(211,29): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(212,17): Error: set argument type must support equality (got Co)
-EqualityTypes.dfy(233,4): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)
+EqualityTypes.dfy(233,12): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)
EqualityTypes.dfy(233,13): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(234,19): Error: set argument type must support equality (got Co)
-EqualityTypes.dfy(236,4): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)
+EqualityTypes.dfy(236,34): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)
EqualityTypes.dfy(236,35): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(238,24): Error: set argument type must support equality (got Co)
EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)
diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect index e7df68f7..4b9aa202 100644 --- a/Test/dafny0/FunctionSpecifications.dfy.expect +++ b/Test/dafny0/FunctionSpecifications.dfy.expect @@ -41,7 +41,7 @@ FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplyin Execution trace:
(0,0): anon0
(0,0): anon3_Else
-FunctionSpecifications.dfy(167,3): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(167,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
diff --git a/Test/dafny0/Iterators.dfy.expect b/Test/dafny0/Iterators.dfy.expect index 0087691b..f0c6e400 100644 --- a/Test/dafny0/Iterators.dfy.expect +++ b/Test/dafny0/Iterators.dfy.expect @@ -1,38 +1,38 @@ -Iterators.dfy(251,9): Error: failure to decrease termination measure
+Iterators.dfy(251,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(274,9): Error: failure to decrease termination measure
+Iterators.dfy(274,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(284,24): Error: failure to decrease termination measure
+Iterators.dfy(284,32): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(296,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(317,10): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(326,24): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(326,32): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-Iterators.dfy(343,9): Error: failure to decrease termination measure
+Iterators.dfy(343,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Else
-Iterators.dfy(353,24): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(353,32): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-Iterators.dfy(370,9): Error: failure to decrease termination measure
+Iterators.dfy(370,10): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -65,7 +65,7 @@ Execution trace: Iterators.dfy(197,3): anon17_Else
Iterators.dfy(197,3): anon19_Else
(0,0): anon21_Then
-Iterators.dfy(40,14): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(40,22): Error BP5002: A precondition for this call might not hold.
Iterators.dfy(4,10): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -85,13 +85,13 @@ Iterators.dfy(150,16): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Iterators.dfy(155,16): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(155,24): Error BP5002: A precondition for this call might not hold.
Iterators.dfy(125,10): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Iterators.dfy(234,14): Error: assertion violation
+Iterators.dfy(234,21): Error: assertion violation
Execution trace:
(0,0): anon0
Iterators.dfy(225,3): anon14_LoopHead
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index e50dc797..90436ed8 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -8,11 +8,11 @@ Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down
-Modules0.dfy(76,6): Error: expected method call, found expression
+Modules0.dfy(76,13): Error: expected method call, found expression
Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down
-Modules0.dfy(79,6): Error: expected method call, found expression
+Modules0.dfy(79,13): Error: expected method call, found expression
Modules0.dfy(84,8): Error: type MyClassY does not have a member M
-Modules0.dfy(84,6): Error: expected method call, found expression
+Modules0.dfy(84,9): Error: expected method call, found expression
Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)
@@ -23,12 +23,12 @@ Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)
Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point
Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(287,6): Error: expected method call, found expression
+Modules0.dfy(287,17): Error: expected method call, found expression
Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(288,6): Error: expected method call, found expression
+Modules0.dfy(288,17): Error: expected method call, found expression
Modules0.dfy(310,24): Error: module Q_Imp does not exist
Modules0.dfy(102,6): Error: type MyClassY does not have a member M
-Modules0.dfy(102,4): Error: expected method call, found expression
+Modules0.dfy(102,7): Error: expected method call, found expression
Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts
diff --git a/Test/dafny0/Modules1.dfy.expect b/Test/dafny0/Modules1.dfy.expect index b269e3b2..342b5808 100644 --- a/Test/dafny0/Modules1.dfy.expect +++ b/Test/dafny0/Modules1.dfy.expect @@ -10,11 +10,11 @@ Modules1.dfy(94,18): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Modules1.dfy(56,3): Error: decreases expression must be bounded below by 0
+Modules1.dfy(56,9): Error: decreases expression must be bounded below by 0
Modules1.dfy(54,13): Related location
Execution trace:
(0,0): anon0
-Modules1.dfy(62,3): Error: failure to decrease termination measure
+Modules1.dfy(62,9): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect index b0613150..7bee017c 100644 --- a/Test/dafny0/NatTypes.dfy.expect +++ b/Test/dafny0/NatTypes.dfy.expect @@ -25,7 +25,7 @@ Execution trace: (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(92,19): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(92,22): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -35,7 +35,7 @@ Execution trace: (0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-NatTypes.dfy(130,21): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(130,35): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect index bb1624f9..28b745c5 100644 --- a/Test/dafny0/NewtypesResolution.dfy.expect +++ b/Test/dafny0/NewtypesResolution.dfy.expect @@ -14,14 +14,14 @@ NewtypesResolution.dfy(91,31): Error: old expressions are not allowed in this co NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N
NewtypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle
NewtypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle
-NewtypesResolution.dfy(120,21): Error: name of type ('N9') is used as a variable
+NewtypesResolution.dfy(120,21): Error: name of type (N9) is used as a variable
NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)
NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)
-NewtypesResolution.dfy(156,9): Error: name of type ('B') is used as a variable
-NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variable
-NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass
-NewtypesResolution.dfy(162,4): Error: expected method call, found expression
-NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
+NewtypesResolution.dfy(156,9): Error: name of type (B) is used as a variable
+NewtypesResolution.dfy(157,11): Error: name of type (Syn) is used as a variable
+NewtypesResolution.dfy(162,8): Error: member 'U' does not exist in type 'Y'
+NewtypesResolution.dfy(162,9): Error: expected method call, found expression
+NewtypesResolution.dfy(188,60): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
NewtypesResolution.dfy(219,11): Error: new must use an integer-based expression for the array size (got real for index 2)
NewtypesResolution.dfy(221,13): Error: arguments to < must have the same type (got Even and nat)
NewtypesResolution.dfy(223,13): Error: arguments to < must have the same type (got Even and int)
diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect index df076f60..3aa09714 100644 --- a/Test/dafny0/OpaqueFunctions.dfy.expect +++ b/Test/dafny0/OpaqueFunctions.dfy.expect @@ -1,30 +1,30 @@ OpaqueFunctions.dfy(27,16): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(52,7): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(52,8): Error BP5002: A precondition for this call might not hold.
OpaqueFunctions.dfy(24,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
OpaqueFunctions.dfy(58,20): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(60,14): Error: assertion violation
+OpaqueFunctions.dfy(60,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(63,14): Error: assertion violation
+OpaqueFunctions.dfy(63,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(66,14): Error: assertion violation
+OpaqueFunctions.dfy(66,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(77,14): Error: assertion violation
+OpaqueFunctions.dfy(77,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-OpaqueFunctions.dfy(79,9): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(79,10): Error BP5002: A precondition for this call might not hold.
OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -32,23 +32,23 @@ Execution trace: OpaqueFunctions.dfy(86,20): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(88,14): Error: assertion violation
+OpaqueFunctions.dfy(88,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(91,14): Error: assertion violation
+OpaqueFunctions.dfy(91,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(94,14): Error: assertion violation
+OpaqueFunctions.dfy(94,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(105,14): Error: assertion violation
+OpaqueFunctions.dfy(105,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-OpaqueFunctions.dfy(107,9): Error BP5002: A precondition for this call might not hold.
+OpaqueFunctions.dfy(107,10): Error BP5002: A precondition for this call might not hold.
OpaqueFunctions.dfy[A'](24,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -56,19 +56,19 @@ Execution trace: OpaqueFunctions.dfy(114,20): Error: assertion violation
Execution trace:
(0,0): anon0
-OpaqueFunctions.dfy(116,14): Error: assertion violation
+OpaqueFunctions.dfy(116,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-OpaqueFunctions.dfy(119,14): Error: assertion violation
+OpaqueFunctions.dfy(119,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-OpaqueFunctions.dfy(122,14): Error: assertion violation
+OpaqueFunctions.dfy(122,21): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-OpaqueFunctions.dfy(138,12): Error: assertion violation
+OpaqueFunctions.dfy(138,13): Error: assertion violation
Execution trace:
(0,0): anon0
OpaqueFunctions.dfy(202,12): Error: assertion violation
diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect index c994cd39..6b726cd5 100644 --- a/Test/dafny0/Parallel.dfy.expect +++ b/Test/dafny0/Parallel.dfy.expect @@ -1,4 +1,4 @@ -Parallel.dfy(34,5): Error BP5002: A precondition for this call might not hold.
+Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.
Parallel.dfy(60,14): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
@@ -60,7 +60,7 @@ Execution trace: (0,0): anon19_Then
(0,0): anon20_Then
(0,0): anon5
-Parallel.dfy(296,10): Error: assertion violation
+Parallel.dfy(296,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 78a43ed9..7305bfce 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -7,8 +7,8 @@ ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost con ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(65,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(66,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(65,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement
ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops
@@ -17,6 +17,6 @@ ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scop ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop
ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ParallelResolveErrors.dfy(115,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(120,6): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
21 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/RealCompare.dfy.expect b/Test/dafny0/RealCompare.dfy.expect index e0f70fc0..5b25fa25 100644 --- a/Test/dafny0/RealCompare.dfy.expect +++ b/Test/dafny0/RealCompare.dfy.expect @@ -1,8 +1,8 @@ -RealCompare.dfy(35,5): Error: failure to decrease termination measure
+RealCompare.dfy(35,6): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-RealCompare.dfy(50,3): Error: decreases expression must be bounded below by 0.0
+RealCompare.dfy(50,4): Error: decreases expression must be bounded below by 0.0
RealCompare.dfy(48,13): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index bb51b01f..2f340557 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -95,8 +95,8 @@ method TestNameResolution1() { // parameters match the signature of only one of those constructors)
var d3 := Abc.David(20, 40); // error: wrong number of parameters
var d4 := Rst.David(20, 40);
- var e := Eleanor;
- assert Tuv(e, this.Eleanor) == 10;
+ var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
+ assert Tuv(Abc.Eleanor, e) == 10;
}
// --------------- ghost tests -------------------------------------
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 7789c6f8..9ba6a1b3 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -16,27 +16,27 @@ ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(619,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(621,17): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(676,18): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(686,22): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(702,18): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(724,22): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(734,9): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(762,17): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(763,18): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(764,18): Error: wrong number of method result arguments (got 0, expected 1)
ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts
@@ -92,13 +92,13 @@ ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(117,10): Error: actual out-parameter 0 is required to be a ghost variable
ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(149,10): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
@@ -124,32 +124,31 @@ ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)
-ResolutionErrors.dfy(56,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,14): Error: accessing member 'X' requires an instance expression
ResolutionErrors.dfy(57,7): Error: unresolved identifier: F
-ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name
-ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(58,14): Error: accessing member 'F' requires an instance expression
ResolutionErrors.dfy(59,7): Error: unresolved identifier: G
ResolutionErrors.dfy(61,7): Error: unresolved identifier: M
-ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance expression
ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
-ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters
-ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
+ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(96,16): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(263,2): Error: duplicate label
ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(292,9): Error: a constructor is allowed to be called only when an object is being allocated
ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts
ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(345,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)
@@ -160,7 +159,7 @@ ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(406,6): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(406,9): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts
@@ -174,14 +173,13 @@ ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies cla ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(931,16): Error: condition is expected to be of type bool, but is int
ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1129,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-186 resolution/type errors detected in ResolutionErrors.dfy
+184 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/ReturnErrors.dfy.expect b/Test/dafny0/ReturnErrors.dfy.expect index a2b9d86d..3f43c226 100644 --- a/Test/dafny0/ReturnErrors.dfy.expect +++ b/Test/dafny0/ReturnErrors.dfy.expect @@ -1,4 +1,4 @@ -ReturnErrors.dfy(32,10): Error: cannot have method call in return statement.
-ReturnErrors.dfy(38,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(32,11): Error: cannot have method call in return statement.
+ReturnErrors.dfy(38,11): Error: cannot have effectful parameter in multi-return statement.
ReturnErrors.dfy(43,10): Error: can only have initialization methods which modify at most 'this'.
3 resolution/type errors detected in ReturnErrors.dfy
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 824ad991..1983d2ac 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -24,16 +24,16 @@ Execution trace: SmallTests.dfy(84,5): anon8_LoopHead
(0,0): anon8_LoopBody
(0,0): anon9_Then
-SmallTests.dfy(119,5): Error: call may violate context's modifies clause
+SmallTests.dfy(119,6): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(132,9): Error: call may violate context's modifies clause
+SmallTests.dfy(132,10): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(134,9): Error: call may violate context's modifies clause
+SmallTests.dfy(134,10): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -174,7 +174,7 @@ Execution trace: SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-SmallTests.dfy(644,10): Error: assertion violation
+SmallTests.dfy(644,23): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
diff --git a/Test/dafny0/StatementExpressions.dfy.expect b/Test/dafny0/StatementExpressions.dfy.expect index 3f50d6d9..313c8884 100644 --- a/Test/dafny0/StatementExpressions.dfy.expect +++ b/Test/dafny0/StatementExpressions.dfy.expect @@ -1,4 +1,4 @@ -StatementExpressions.dfy(55,11): Error: cannot prove termination; try supplying a decreases clause
+StatementExpressions.dfy(55,12): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Then
@@ -16,7 +16,7 @@ StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negat Execution trace:
(0,0): anon0
(0,0): anon3_Else
-StatementExpressions.dfy(98,11): Error: cannot prove termination; try supplying a decreases clause
+StatementExpressions.dfy(98,18): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Then
diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect index dc1eec5b..5c63112a 100644 --- a/Test/dafny0/TailCalls.dfy.expect +++ b/Test/dafny0/TailCalls.dfy.expect @@ -1,4 +1,4 @@ -TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
+TailCalls.dfy(21,16): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
TailCalls.dfy(38,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
TailCalls.dfy(43,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
3 resolution/type errors detected in TailCalls.dfy
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect index ef8ee72e..fd86c8cb 100644 --- a/Test/dafny0/Termination.dfy.expect +++ b/Test/dafny0/Termination.dfy.expect @@ -1,4 +1,4 @@ -Termination.dfy[TerminationRefinement1](440,5): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](440,6): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
Termination.dfy(360,47): Error: failure to decrease termination measure
diff --git a/Test/dafny0/Trait/TraitExtend.dfy.expect b/Test/dafny0/Trait/TraitExtend.dfy.expect index 73a24ad8..2051fd81 100644 --- a/Test/dafny0/Trait/TraitExtend.dfy.expect +++ b/Test/dafny0/Trait/TraitExtend.dfy.expect @@ -1,3 +1,3 @@ -TraitExtend.dfy(40,20): Error: wrong number of function arguments (got 2, expected 3)
-TraitExtend.dfy(41,20): Error: wrong number of function arguments (got 3, expected 2)
+TraitExtend.dfy(40,24): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)
+TraitExtend.dfy(41,24): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)
2 resolution/type errors detected in TraitExtend.dfy
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 55fc916c..0a15ad67 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,13 +1,13 @@ TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
-TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D)
-TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C)
-TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int)
-TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
+TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
+TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
+TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, got int)
+TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index eedfce29..b37633ae 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -1,14 +1,14 @@ -------------------- Snapshots0.dfy --------------------
-Processing command (at Snapshots0.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,3)):
+Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
>>> added after: a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);
-Processing command (at Snapshots0.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at <unknown location>) a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);
>>> AssumeNegationOfAssumptionVariable
@@ -21,7 +21,7 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error
-------------------- Snapshots1.dfy --------------------
-Processing command (at Snapshots1.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -29,11 +29,11 @@ Processing command (at Snapshots1.v0.dfy(12,3)) assert true; >>> DoNothingToAssert
Dafny program verifier finished with 4 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,3)):
+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
>>> added after: a##post##0 := a##post##0 && false;
Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -44,7 +44,7 @@ Execution trace: Dafny program verifier finished with 3 verified, 1 error
-------------------- Snapshots2.dfy --------------------
-Processing command (at Snapshots2.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -60,11 +60,11 @@ Processing command (at Snapshots2.v0.dfy(18,3)) assert true; >>> DoNothingToAssert
Dafny program verifier finished with 6 verified, 0 errors
-Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,3)):
+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):
>>> added after: a##post##0 := a##post##0 && false;
Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
@@ -125,11 +125,11 @@ Execution trace: Dafny program verifier finished with 1 verified, 2 errors
-------------------- Snapshots5.dfy --------------------
-Processing command (at Snapshots5.v0.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
>>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> DoNothingToAssert
@@ -137,11 +137,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: tru >>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
-Processing command (at Snapshots5.v1.dfy(3,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
>>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
+Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> MarkAsFullyVerified
diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect index d84bdc45..849b9e38 100644 --- a/Test/dafny2/SnapshotableTrees.dfy.expect +++ b/Test/dafny2/SnapshotableTrees.dfy.expect @@ -1,4 +1,4 @@ -SnapshotableTrees.dfy(68,16): Error BP5002: A precondition for this call might not hold.
+SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold.
SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect index 927d8b06..9f6998f5 100644 --- a/Test/hofs/Field.dfy.expect +++ b/Test/hofs/Field.dfy.expect @@ -1,14 +1,14 @@ -Field.dfy(12,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
Field.dfy(12,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(21,10): Error: assertion violation
+Field.dfy(12,15): Error: assertion violation
Execution trace:
(0,0): anon0
Field.dfy(21,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
+Field.dfy(21,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
Dafny program verifier finished with 2 verified, 4 errors
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect index 2cf19369..c3e0c242 100644 --- a/Test/hofs/ResolveError.dfy.expect +++ b/Test/hofs/ResolveError.dfy.expect @@ -1,5 +1,5 @@ ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable to LHS (of type (int,bool) -> real)
-ResolveError.dfy(91,14): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
+ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)
ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)
ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
@@ -8,12 +8,12 @@ ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)
ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)
ResolveError.dfy(33,13): Error: type mismatch for argument 0 (function expects int, got bool)
-ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)
+ResolveError.dfy(34,22): Error: type mismatch for argument 0 (function expects int, got bool)
ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)
-ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)
-ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected int, got bool)
+ResolveError.dfy(36,21): Error: wrong number of arguments to function application (function 'requires' expects 1, got 2)
+ResolveError.dfy(37,19): Error: type mismatch for argument 0 (function expects int, got bool)
ResolveError.dfy(38,22): Error: arguments must have the same type (got set<object> and int)
-ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expected 1)
+ResolveError.dfy(39,18): Error: wrong number of arguments to function application (function 'reads' expects 1, got 2)
ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)
ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)
ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool
|