diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 64 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 3 | ||||
| -rw-r--r-- | Test/dafny0/CoResolution.dfy.expect | 3 | ||||
| -rw-r--r-- | Test/dafny0/DisplayExpressions.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny0/DisplayExpressions.dfy.expect | 11 | ||||
| -rw-r--r-- | Test/dafny0/Parallel.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 85 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 15 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 2 | ||||
| -rw-r--r-- | Test/hofs/Underspecified.dfy.expect | 5 |
12 files changed, 160 insertions, 47 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index dfd37954..1ca5e4d9 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3332,7 +3332,7 @@ namespace Microsoft.Dafny { /// Here, Path may either be of the form C.Init
/// -- represents new C.Init(EE)
/// or all of Path denotes a type
- /// -- represents new C._ctor(EE), where _ctor is the default constructor for class C
+ /// -- represents new C._ctor(EE), where _ctor is the anonymous constructor for class C
/// * TypeRhs(Path, s, EE)
/// Here, Path must denote a type and s is a string that denotes the method/constructor Init
/// -- represents new Path.s(EE)
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 06e5e640..82d774fc 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -984,7 +984,7 @@ namespace Microsoft.Dafny members.Add(extraName, extraMember);
}
} else if (m is Constructor && !((Constructor)m).HasName) {
- Error(m, "More than one default constructor");
+ Error(m, "More than one anonymous constructor");
} else {
Error(m, "Duplicate member name: {0}", m.Name);
}
@@ -1804,10 +1804,9 @@ namespace Microsoft.Dafny }
}
}
- } else if (expr is MapDisplayExpr) {
- CheckTypeIsDetermined(expr.tok, expr.Type, "map constructor", true);
- } else if (expr is DisplayExpression) {
- CheckTypeIsDetermined(expr.tok, expr.Type, "collection constructor", true);
+ } else if (expr is IdentifierExpr) {
+ // by specializing for IdentifierExpr, error messages will be clearer
+ CheckTypeIsDetermined(expr.tok, expr.Type, "variable");
} else if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) {
var bin = expr as BinaryExpr;
if (bin != null) {
@@ -1816,12 +1815,14 @@ namespace Microsoft.Dafny }
}
/// <summary>
- /// This method checks to see if 'tp' has been determined and returns the result.
- /// However, if tp denotes an int-based or real-based type, then tp is set to int or real,
- /// respectively, here.
+ /// This method checks to see if 't' has been determined and returns the result.
+ /// However, if t denotes an int-based or real-based type, then t is set to int or real,
+ /// respectively, here. Similarly, if t is an unresolved type for "null", then t
+ /// is set to "object".
/// </summary>
public static bool IsDetermined(Type t) {
Contract.Requires(t != null);
+ Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);
// If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively
if (t is OperationTypeProxy) {
var proxy = (OperationTypeProxy)t;
@@ -1832,15 +1833,21 @@ namespace Microsoft.Dafny proxy.T = Type.Real;
return true;
}
+ } else if (t is ObjectTypeProxy) {
+ var proxy = (ObjectTypeProxy)t;
+ proxy.T = new ObjectType();
+ return true;
}
return !(t is TypeProxy); // all other proxies indicate the type has not yet been determined
}
- bool CheckTypeIsDetermined(IToken tok, Type t, string what, bool aggressive = false) {
+ ISet<TypeProxy> UnderspecifiedTypeProxies = new HashSet<TypeProxy>();
+ bool CheckTypeIsDetermined(IToken tok, Type t, string what) {
Contract.Requires(tok != null);
Contract.Requires(t != null);
Contract.Requires(what != null);
t = t.NormalizeExpand();
- // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively
+ // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively;
+ // similarly, if t refers to the type of "null", set its type to be "object".
if (t is OperationTypeProxy) {
var proxy = (OperationTypeProxy)t;
if (proxy.JustInts) {
@@ -1850,18 +1857,29 @@ namespace Microsoft.Dafny proxy.T = Type.Real;
return true;
}
+ } else if (t is ObjectTypeProxy) {
+ var proxy = (ObjectTypeProxy)t;
+ proxy.T = new ObjectType();
+ return true;
}
- if (t is TypeProxy && (aggressive || !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy))) {
- Error(tok, "the type of this {0} is underspecified, but it cannot be an opaque type.", what);
+ if (t is TypeProxy) {
+ var proxy = (TypeProxy)t;
+ if (!UnderspecifiedTypeProxies.Contains(proxy)) {
+ // report an error for this TypeProxy only once
+ Error(tok, "the type of this {0} is underspecified", what);
+ UnderspecifiedTypeProxies.Add(proxy);
+ }
return false;
- } else if (aggressive && t is MapType) {
- return CheckTypeIsDetermined(tok, ((MapType)t).Range, what, aggressive) &&
- CheckTypeIsDetermined(tok, ((MapType)t).Domain, what, aggressive);
- } else if (aggressive && t is CollectionType) {
- return CheckTypeIsDetermined(tok, ((CollectionType)t).Arg, what, aggressive);
- } else if (aggressive && t is UserDefinedType) {
- return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what, aggressive));
+ }
+ // Recurse on type arguments:
+ if (t is MapType) {
+ return CheckTypeIsDetermined(tok, ((MapType)t).Range, what) &&
+ CheckTypeIsDetermined(tok, ((MapType)t).Domain, what);
+ } else if (t is CollectionType) {
+ return CheckTypeIsDetermined(tok, ((CollectionType)t).Arg, what);
+ } else if (t is UserDefinedType) {
+ return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what));
} else {
return true;
}
@@ -5766,7 +5784,7 @@ namespace Microsoft.Dafny var initCallTok = rr.Tok;
if (rr.OptionalNameComponent == null && rr.Arguments != null) {
// Resolve rr.EType and do one of three things:
- // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the default constructor.
+ // * If rr.EType denotes a type, then set rr.OptionalNameComponent to "_ctor", which sets up a call to the anonymous constructor.
// * If the all-but-last components of rr.EType denote a type, then do EType,OptionalNameComponent := allButLast(EType),last(EType)
// * Otherwise, report an error
var ret = ResolveTypeLenient(stmt.Tok, rr.EType, codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null, true);
@@ -5856,7 +5874,7 @@ namespace Microsoft.Dafny #endif
var kind = cd is IteratorDecl ? "iterator" : "class";
if (memberName == "_ctor") {
- Error(tok, "{0} {1} does not have a default constructor", kind, ctype.Name);
+ Error(tok, "{0} {1} does not have a anonymous constructor", kind, ctype.Name);
} else {
Error(tok, "member {0} does not exist in {2} {1}", memberName, ctype.Name, kind);
}
@@ -6768,7 +6786,7 @@ namespace Microsoft.Dafny QuantifierExpr e = (QuantifierExpr)expr;
int prevErrorCount = ErrorCount;
bool _val = true;
- bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val);
+ bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val) && _val;
allTypeParameters.PushMarker();
ResolveTypeParameters(e.TypeArgs, true, e);
scope.PushMarker();
@@ -6776,7 +6794,7 @@ namespace Microsoft.Dafny if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
- var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer);
+ var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies);
ResolveType(v.tok, v.Type, opts.codeContext, option, typeQuantifier ? e.TypeArgs : null);
}
if (e.TypeArgs.Count > 0 && !typeQuantifier) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 21a5dea5..bfd748a2 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -6505,8 +6505,7 @@ namespace Microsoft.Dafny { while (true) {
type = type.NormalizeExpand();
if (type is TypeProxy) {
- // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
- return predef.RefType;
+ Contract.Assume(false); // we assume that all proxies should have been dealt with in the resolver
}
var d = type.AsNewtype;
if (d == null) {
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index 196b3faa..9acb5a58 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -20,5 +20,6 @@ CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only 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,19): Error: type variable '_T0' in the function call to 'S' could not be determined
-23 resolution/type errors detected in CoResolution.dfy
+24 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/DisplayExpressions.dfy b/Test/dafny0/DisplayExpressions.dfy index 767cfcdb..ef7d4062 100644 --- a/Test/dafny0/DisplayExpressions.dfy +++ b/Test/dafny0/DisplayExpressions.dfy @@ -2,20 +2,25 @@ // RUN: %diff "%s.expect" "%t"
method M()
{
- var m := map[];
+ var m := map[]; // error: underspecified type
}
method N()
{
- var n := multiset{};
+ var n := multiset{}; // error: underspecified type
}
method O()
{
- var o := [];
+ var o := []; // error: underspecified type
}
method P()
{
- var p := {};
+ var p := {}; // error: underspecified type
+}
+
+method Q()
+{
+ assert (((map[]))) == (((((map[]))))); // error (but not 10 errors)
}
diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect index 7374db2a..e12353f7 100644 --- a/Test/dafny0/DisplayExpressions.dfy.expect +++ b/Test/dafny0/DisplayExpressions.dfy.expect @@ -1,5 +1,6 @@ -DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an opaque type.
-DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
-DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
-DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
-4 resolution/type errors detected in DisplayExpressions.dfy
+DisplayExpressions.dfy(5,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(10,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(15,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(20,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(25,12): Error: the type of this expression is underspecified
+5 resolution/type errors detected in DisplayExpressions.dfy
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 9a76777a..d343a84d 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -196,7 +196,7 @@ ghost method DontDoMuch(x: int) }
method OmittedRange() {
- forall (x) { }
+ forall (x: int) { } // a type is still needed for the bound variable
forall (x) {
DontDoMuch(x);
}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 38f2f9c2..79e7ac57 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -555,8 +555,8 @@ module NonInferredType { method NonInferredType0(x: int)
{
var t;
- assume forall z :: P(z) && z == t;
- assume t == x; // this statement determined the type of z
+ assume forall z :: P(z) && z == t; // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers.
+ assume t == x; // this statement determines the type of t and z
}
method NonInferredType1(x: int)
@@ -1159,3 +1159,84 @@ method NonTermination_D() n := n + 1;
}
}
+
+// ------------ type variables whose values are not inferred ----------
+
+module NonInferredTypeVariables {
+ class C<CT> {
+ var f: CT;
+ }
+
+ predicate method P<PT>(x: int)
+ {
+ x < 100
+ }
+ function Q<QT>(x: int): QT
+ {
+ var qt :| true; qt
+ }
+ method M<MT>(n: nat)
+ {
+ var a := new MT[n];
+ }
+ method N<NT>(n: nat) returns (x: NT)
+ {
+ var a := new NT[10];
+ x := a[3];
+ }
+
+ method DeterminedClient(n: nat)
+ {
+ ghost var q := Q(n);
+ var x := N(n);
+ var a := new array;
+ var c := new C;
+ var s: set;
+ var ss := new set[15];
+
+ q := 3.14; // this will determine the type parameter of Q to be 'real'
+ x := 3.14; // this will determine the type parameter of N to be 'real'
+ if a.Length != 0 {
+ a[0] := 3.14; // this will determine the type parameter of 'array' to be 'real'
+ }
+ c.f := 3.14; // this will determine the type parameter of 'C' to be 'real'
+ var containsPi := 3.14 in s; // this will determine the type parameter of 'set' to be 'real'
+ ss[12] := s; // this will determine the type parameter of 'array<set< _ >>' to be 'real'
+ }
+ method BadClient(n: nat)
+ {
+ var p := P(n); // error: cannot infer the type argument for P
+ ghost var q := Q(n); // error: cannot infer the type argument for Q
+ M(n); // error: cannot infer the type argument for M
+ var x := N(n); // error: cannot infer the type argument for N
+ var a := new array; // error: cannot infer the type argument for 'array'
+ var c := new C; // error: cannot infer the type argument for 'C'
+ var s: set; // type argument for 'set'
+ var ss := new set[15]; // error: cannot infer the type argument in 'array<set< _ >>'
+ var what; // error: the type of this local variable in underspecified
+ }
+ method MoreBadClient()
+ {
+ var b0 := forall s :: s <= {} ==> s == {}; // error: type of s underspecified
+ var b1 := forall s: set :: s <= {} ==> s == {}; // error: type of s underspecified
+ var b2 := forall c: C :: c in {null} ==> c == null; // error: type of s underspecified
+
+ // In the following, the type of the bound variable is completely determined.
+ var S: set<set<int>>;
+ ghost var d0 := forall s :: s == {7} ==> s != {};
+ var d1 := forall s: set :: s in S ==> s == {};
+ var ggcc0: C;
+ var ggcc1: C;
+ ghost var d2 := forall c: C :: c != null ==> c.f == 10;
+ ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10;
+ ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined
+
+ /* TODO: Dafny's heuristic that looks for bounds should look for equality to
+ * accept these.
+ var d0' := forall s :: s == {7} ==> s != {};
+ var d0'' := forall s :: s <= {7} ==> s == {};
+ var ggcc2: C;
+ var d2''' := forall c :: c == ggcc2 && c != null ==> c.f == 10;
+ */
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 3f08e72a..1b802687 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -2,7 +2,9 @@ ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
+ResolutionErrors.dfy(558,25): Error: the type of this variable is underspecified
ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(565,25): Error: the type of this variable is underspecified
ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be determined
ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts
@@ -16,8 +18,7 @@ ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
+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(689,20): Error: 'decreases *' is not allowed on ghost loops
@@ -78,7 +79,11 @@ ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<b ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)
ResolutionErrors.dfy(1113,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
ResolutionErrors.dfy(1115,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(429,2): Error: More than one default constructor
+ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
@@ -99,7 +104,7 @@ ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this cont ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor
+ResolutionErrors.dfy(443,9): Error: class Lamb does not have a anonymous constructor
ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
@@ -175,4 +180,4 @@ 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(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-177 resolution/type errors detected in ResolutionErrors.dfy
+182 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index a208b1b6..d6658671 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -512,7 +512,7 @@ class AttributeTests { static method TestAttributesVarDecls()
{
- var {:foo} foo;
+ var {:foo} foo := null;
var {:bar} bar := 0;
var {:foo} {:bar} foobar : set<int> := {};
var {:baz} baz, {:foobaz} foobaz := true, false;
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 31819dcc..6086fcf1 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -68,7 +68,7 @@ method DuplicateVarName(x: int) returns (y: int) method ScopeTests()
{
var x := x; // error: the 'x' in the RHS is not in scope
- var y :| y == y; // fine, 'y' is in scope in the RHS
+ var y: real :| y == y; // fine, 'y' is in scope in the RHS
var z := DuplicateVarName(z); // error: the 'z' in the RHS is not in scope
var w0, w1 := IntTransform(w1), IntTransform(w0); // errors two
var c := new MyClass.Init(null); // fine
diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect index 04394d78..a5970830 100644 --- a/Test/hofs/Underspecified.dfy.expect +++ b/Test/hofs/Underspecified.dfy.expect @@ -1,5 +1,8 @@ +Underspecified.dfy(6,6): Error: the type of this variable is underspecified
Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not be determined; please specify the type explicitly
+Underspecified.dfy(7,6): Error: the type of this variable is underspecified
Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not be determined; please specify the type explicitly
Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not be determined; please specify the type explicitly
+Underspecified.dfy(8,6): Error: the type of this variable is underspecified
Underspecified.dfy(8,11): Error: type of bound variable 'a' could not be determined; please specify the type explicitly
-4 resolution/type errors detected in Underspecified.dfy
+7 resolution/type errors detected in Underspecified.dfy
|