summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Bryan Parno <parno@microsoft.com>2015-01-13 14:02:24 -0800
committerGravatar Bryan Parno <parno@microsoft.com>2015-01-13 14:02:24 -0800
commitbe9a360dabe0f82bdcb82eb8282ab85c35f31e38 (patch)
tree30b923fa2322bfdd7aeb58b90ddb614679206467
parentb3317185acc805116fa6716a70d57bd147f2229f (diff)
parentcbdb1b0bafcd1c806e0ea4c3a0f3fefb073d4b1c (diff)
Merge
-rw-r--r--Source/Dafny/Cloner.cs1
-rw-r--r--Source/Dafny/DafnyAst.cs61
-rw-r--r--Source/Dafny/DafnyOptions.cs2
-rw-r--r--Source/Dafny/Resolver.cs90
-rw-r--r--Source/Dafny/Translator.cs12
-rw-r--r--Source/DafnyExtension/OutliningTagger.cs2
-rw-r--r--Test/dafny0/DiamondImports.dfy143
-rw-r--r--Test/dafny0/DiamondImports.dfy.expect32
-rw-r--r--Test/dafny0/ResolutionErrors.dfy24
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect3
10 files changed, 331 insertions, 39 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index ebb291fb..f95c05ed 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -115,7 +115,6 @@ namespace Microsoft.Dafny
} else if (d is AliasModuleDecl) {
var a = (AliasModuleDecl)d;
var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened);
- alias.ModuleReference = a.ModuleReference;
alias.Signature = a.Signature;
return alias;
} else if (d is ModuleFacadeDecl) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0742ee43..f1fbd7ff 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1323,7 +1323,17 @@ namespace Microsoft.Dafny {
// ------------------------------------------------------------------------------------------------------
- public abstract class Declaration : IUniqueNameGenerator {
+ /// <summary>
+ /// This interface is used by the Dafny IDE.
+ /// </summary>
+ public interface INamedRegion
+ {
+ IToken BodyStartTok { get; }
+ IToken BodyEndTok { get; }
+ string Name { get; }
+ }
+
+ public abstract class Declaration : IUniqueNameGenerator, INamedRegion {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(tok != null);
@@ -1334,6 +1344,9 @@ namespace Microsoft.Dafny {
public IToken BodyStartTok = Token.NoToken;
public IToken BodyEndTok = Token.NoToken;
public readonly string Name;
+ IToken INamedRegion.BodyStartTok { get { return BodyStartTok; } }
+ IToken INamedRegion.BodyEndTok { get { return BodyEndTok; } }
+ string INamedRegion.Name { get { return Name; } }
string compileName;
public virtual string CompileName {
get {
@@ -1452,6 +1465,7 @@ namespace Microsoft.Dafny {
Signature = null;
Opened = opened;
}
+ public abstract object Dereference();
}
// Represents module X { ... }
public class LiteralModuleDecl : ModuleDecl
@@ -1461,20 +1475,19 @@ namespace Microsoft.Dafny {
: base(module.tok, module.Name, parent, false) {
ModuleDef = module;
}
+ public override object Dereference() { return ModuleDef; }
}
- // Represents "module name = path;", where name is a identifier and path is a possibly qualified name.
+ // Represents "module name = path;", where name is an identifier and path is a possibly qualified name.
public class AliasModuleDecl : ModuleDecl
{
- public ModuleDecl ModuleReference; // should refer to another declaration somewhere. NOTE: cyclicity is possible, and should
- // be detected and warned.
public readonly List<IToken> Path; // generated by the parser, this is looked up
public ModuleDecl Root; // the moduleDecl that Path[0] refers to.
public AliasModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, bool opened)
: base(name, name.val, parent, opened) {
Contract.Requires(path != null && path.Count > 0);
Path = path;
- ModuleReference = null;
}
+ public override object Dereference() { return Signature.ModuleDef; }
}
// Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name.
public class ModuleFacadeDecl : ModuleDecl
@@ -1491,6 +1504,7 @@ namespace Microsoft.Dafny {
Root = null;
CompilePath = compilePath;
}
+ public override object Dereference() { return this; }
}
public class ModuleSignature {
@@ -1507,18 +1521,27 @@ namespace Microsoft.Dafny {
public bool FindSubmodule(string name, out ModuleSignature pp) {
TopLevelDecl top;
- pp = null;
- if (TopLevels.TryGetValue(name, out top)) {
- if (top is ModuleDecl) {
- pp = ((ModuleDecl)top).Signature;
- return true;
- } else return false;
- } else return false;
+ if (TopLevels.TryGetValue(name, out top) && top is ModuleDecl) {
+ pp = ((ModuleDecl)top).Signature;
+ return true;
+ } else {
+ pp = null;
+ return false;
+ }
}
-
-
}
- public class ModuleDefinition : TopLevelDecl {
+
+ public class ModuleDefinition : INamedRegion
+ {
+ public readonly IToken tok;
+ public IToken BodyStartTok = Token.NoToken;
+ public IToken BodyEndTok = Token.NoToken;
+ public readonly string Name;
+ IToken INamedRegion.BodyStartTok { get { return BodyStartTok; } }
+ IToken INamedRegion.BodyEndTok { get { return BodyEndTok; } }
+ string INamedRegion.Name { get { return Name; } }
+ public readonly ModuleDefinition Module;
+ public readonly Attributes Attributes;
public readonly List<IToken> RefinementBaseName; // null if no refinement base
public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0]
public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base)
@@ -1537,9 +1560,13 @@ namespace Microsoft.Dafny {
}
public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, List<IToken> refinementBase, ModuleDefinition parent, Attributes attributes, bool isBuiltinName)
- : base(tok, name, parent, new List<TypeParameter>(), attributes) {
+ {
Contract.Requires(tok != null);
Contract.Requires(name != null);
+ this.tok = tok;
+ this.Name = name;
+ this.Attributes = attributes;
+ this.Module = parent;
RefinementBaseName = refinementBase;
IsAbstract = isAbstract;
IsFacade = isFacade;
@@ -1554,7 +1581,7 @@ namespace Microsoft.Dafny {
}
}
string compileName;
- new public string CompileName {
+ public string CompileName {
get {
if (compileName == null) {
if (IsBuiltinName)
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 1690455f..61024688 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -149,7 +149,7 @@ namespace Microsoft.Dafny
case "noNLarith":
DisableNLarith = true;
- this.Z3Options.Add("NL_ARITH=false");
+ this.AddZ3Option("NL_ARITH=false");
return true;
case "autoReqPrint":
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c7f452f6..d29c7d8e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -92,15 +92,36 @@ namespace Microsoft.Dafny
}
}
- class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes"
+ interface IAmbiguousThing<Thing>
+ {
+ /// <summary>
+ /// Returns a non-zero number of non-null Thing's
+ /// </summary>
+ IEnumerable<Thing> AllDecls();
+ }
+ class AmbiguousTopLevelDecl : TopLevelDecl, IAmbiguousThing<TopLevelDecl> // only used with "classes"
{
readonly TopLevelDecl A;
readonly TopLevelDecl B;
public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b)
: base(a.tok, a.Name + "/" + b.Name, m, new List<TypeParameter>(), null) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
A = a;
B = b;
}
+ public IEnumerable<TopLevelDecl> AllDecls() {
+ foreach (var a in new TopLevelDecl[] { A, B }) {
+ var amb = a as AmbiguousTopLevelDecl;
+ if (amb != null) {
+ foreach (var decl in amb.AllDecls()) {
+ yield return decl;
+ }
+ } else {
+ yield return a;
+ }
+ }
+ }
public string ModuleNames() {
string nm;
if (A is AmbiguousTopLevelDecl) {
@@ -117,15 +138,35 @@ namespace Microsoft.Dafny
}
}
- class AmbiguousMemberDecl : MemberDecl // only used with "classes"
+ class AmbiguousMemberDecl : MemberDecl, IAmbiguousThing<MemberDecl> // only used with "classes"
{
readonly MemberDecl A;
readonly MemberDecl B;
public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)
: base(a.tok, a.Name + "/" + b.Name, true, a.IsGhost, null) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
A = a;
B = b;
}
+ public IEnumerable<MemberDecl> AllDecls() {
+ var amb = A as AmbiguousMemberDecl;
+ if (amb == null) {
+ yield return A;
+ } else {
+ foreach (var decl in amb.AllDecls()) {
+ yield return decl;
+ }
+ }
+ amb = B as AmbiguousMemberDecl;
+ if (amb == null) {
+ yield return B;
+ } else {
+ foreach (var decl in amb.AllDecls()) {
+ yield return decl;
+ }
+ }
+ }
public string ModuleNames() {
string nm;
if (A is AmbiguousMemberDecl) {
@@ -4028,7 +4069,7 @@ namespace Microsoft.Dafny
if (d == null) {
// error has been reported above
- } else if (d is AmbiguousTopLevelDecl) {
+ } else if (ReallyAmbiguousTopLevelDecl(ref d)) {
Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else {
string what;
@@ -4076,6 +4117,39 @@ namespace Microsoft.Dafny
return null;
}
+ bool ReallyAmbiguousTopLevelDecl(ref TopLevelDecl decl) {
+ return ReallyAmbiguousThing(ref decl, (d0, d1) => {
+ // We'd like to resolve any AliasModuleDecl to whatever module they refer to.
+ // It seems that the only way to do that is to look at alias.Signature.ModuleDef,
+ // but that is a ModuleDefinition, which is not a TopLevelDecl. Therefore, we
+ // convert to a ModuleDefinition anything that might refer to something that an
+ // AliasModuleDecl can refer to; this is AliasModuleDecl and LiteralModuleDecl.
+ object a = d0 is ModuleDecl ? ((ModuleDecl)d0).Dereference() : d0;
+ object b = d1 is ModuleDecl ? ((ModuleDecl)d1).Dereference() : d1;
+ return a == b;
+ });
+ }
+
+ bool ReallyAmbiguousThing<Thing>(ref Thing decl, Func<Thing, Thing, bool> eq = null) where Thing : class {
+ Contract.Requires(decl != null);
+ Contract.Ensures(decl != null);
+ Contract.Ensures(!Contract.Result<bool>() || (decl == Contract.OldValue<Thing>(decl) && decl is IAmbiguousThing<Thing>));
+ var amb = decl as IAmbiguousThing<Thing>;
+ if (amb != null) {
+ var allDecls = new List<Thing>(amb.AllDecls());
+ Contract.Assert(1 <= allDecls.Count); // that's what the specification of AllDecls says
+ var repr = allDecls[0]; // pick one of them
+ // check if all are the same
+ if (amb.AllDecls().All(d => eq == null ? d == repr : eq(d, repr))) {
+ // all ambiguity gets resolved to the same declaration, so there really isn't any ambiguity after all
+ decl = repr;
+ return false;
+ }
+ return true; // decl is an AmbiguousThing and the declarations it can stand for are not all the same--so this really is an ambiguity
+ }
+ return false;
+ }
+
/// <summary>
/// Adds to "typeArgs" a list of "n" type arguments, possibly extending "defaultTypeArguments".
/// </summary>
@@ -6390,7 +6464,7 @@ namespace Microsoft.Dafny
TopLevelDecl d;
if (!moduleInfo.TopLevels.TryGetValue(dtv.DatatypeName, out d)) {
Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName);
- } else if (d is AmbiguousTopLevelDecl) {
+ } else if (ReallyAmbiguousTopLevelDecl(ref d)) {
Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else if (!(d is DatatypeDecl)) {
Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);
@@ -7403,7 +7477,7 @@ namespace Microsoft.Dafny
}
} else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {
// ----- 3. Member of the enclosing module
- if (decl is AmbiguousTopLevelDecl) {
+ if (ReallyAmbiguousTopLevelDecl(ref decl)) {
Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());
} else {
// We have found a module name or a type name, neither of which is an expression. However, the NameSegment we're
@@ -7416,7 +7490,7 @@ namespace Microsoft.Dafny
} else if (moduleInfo.StaticMembers.TryGetValue(expr.Name, out member)) {
// ----- 4. static member of the enclosing module
Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
- if (member is AmbiguousMemberDecl) {
+ if (ReallyAmbiguousThing(ref member)) {
Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());
} else {
var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
@@ -7535,7 +7609,7 @@ namespace Microsoft.Dafny
}
} else if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {
// ----- 1. Member of the specified module
- if (decl is AmbiguousTopLevelDecl) {
+ if (ReallyAmbiguousTopLevelDecl(ref decl)) {
Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());
} else {
// We have found a module name or a type name, neither of which is an expression. However, the ExprDotName we're
@@ -7547,7 +7621,7 @@ namespace Microsoft.Dafny
} else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) {
// ----- 2. static member of the specified module
Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default
- if (member is AmbiguousMemberDecl) {
+ if (ReallyAmbiguousThing(ref member)) {
Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());
} else {
var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3decb1f8..9379fac7 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -9062,16 +9062,8 @@ namespace Microsoft.Dafny {
}
static public List<TypeParameter> GetTypeParams(TopLevelDecl d) {
- if (d is ClassDecl) {
- return Concat(GetTypeParams(d.Module), d.TypeArgs);
- } else if (d is DatatypeDecl) {
- return Concat(GetTypeParams(d.Module), d.TypeArgs);
- } else if (d is ModuleDefinition) {
- return new List<TypeParameter>();
- } else {
- Contract.Assert(false);
- return null;
- }
+ Contract.Requires(d is ClassDecl || d is DatatypeDecl);
+ return d.TypeArgs;
}
static List<TypeParameter> GetTypeParams(Function f) {
diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index 55f5e677..c4b88f98 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -200,7 +200,7 @@ namespace DafnyLanguage
public readonly int Start;
public readonly int Length;
public readonly string HoverText;
- public OutliningRegion(Dafny.Declaration decl, string kind) {
+ public OutliningRegion(Dafny.INamedRegion decl, string kind) {
int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself
int length = decl.BodyEndTok.pos - startPosition;
Start = startPosition;
diff --git a/Test/dafny0/DiamondImports.dfy b/Test/dafny0/DiamondImports.dfy
new file mode 100644
index 00000000..1292211f
--- /dev/null
+++ b/Test/dafny0/DiamondImports.dfy
@@ -0,0 +1,143 @@
+// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module ImportByName {
+ module A {
+ type T
+ function method P(): T
+ method M(t: T)
+ }
+
+ module B {
+ import A
+ }
+
+ module C {
+ import A
+ type K = A.T
+ import W_A = W_B
+ import W_B = A
+ }
+
+ module D {
+ import B
+ import C
+
+ method Client() returns (t: B.A.T, u: C.A.T) {
+ t := u;
+ u := t;
+ var x, y := B.A.P(), C.A.P();
+ assert x == y;
+ C.A.M(t);
+ B.A.M(u);
+ var anything;
+ assert t == anything; // error: (testing that it's not possible to prove false here)
+ }
+ }
+
+ module E {
+ import A
+ import B
+ import C
+ method Client() returns (r: A.T, k: C.K) {
+ var x, y, z := B.A.P(), C.A.P(), A.P();
+ assert x == z == y;
+ r, r, r := x, y, z;
+ k, k, k, k := x, y, z, r;
+ assert r == C.W_A.P();
+ assert r == C.W_B.P();
+ var anything;
+ assert r == anything; // error: (testing that it's not possible to prove false here)
+ }
+ }
+}
+
+// ------------------------------------------------------------
+
+module ImportOpened {
+ module A {
+ type T
+ function method P(): T
+ method M(t: T)
+ }
+
+ module B {
+ import opened A
+ }
+
+ module C {
+ import opened A
+ type K = T
+ type L = A.T // should work when name is qualified, too
+ import W_A = W_B
+ import W_B = A
+ }
+
+ module C' {
+ import A // import by name
+ type K = A.T
+ }
+
+ module D {
+ import opened B
+ import opened C
+ import opened C'
+
+ method Client() returns (t: B.A.T, u: C.A.T, v: C'.A.T, w: B.T) {
+ t,u, v, w := u, v, w, t;
+ var x, y, z := B.A.P(), C.A.P(), C'.A.P();
+ assert x == y == z;
+ var o;
+ x, y, z, o := B.P(), C.P(), C'.A.P(), A.P();
+ assert x == y == z == o;
+
+ B.A.M(u);
+ C.A.M(t);
+ C'.A.M(t);
+ B.M(t);
+ C.M(t);
+ M(t);
+ var anything;
+ assert t == anything; // error: (testing that it's not possible to prove false here)
+ }
+ }
+
+ module E {
+ import opened A
+ import opened B
+ import opened C
+ method Client() returns (r: A.T, k: C.K, l: C.L, m: K, n: L) {
+ var x, y, z := B.A.P(), C.A.P(), A.P();
+ assert x == z == y;
+ r, r, r := x, y, z;
+ k, k, k, k := x, y, z, r;
+ l, l, l, l, l := x, y, z, r, k;
+ m, n := k, l;
+ assert m == n == k;
+ assert r == C.W_A.P() == C.W_B.P();
+ assert r == W_A.P() == W_B.P();
+ var anything;
+ assert r == anything; // error: (testing that it's not possible to prove false here)
+ }
+ }
+}
+
+module AmbiguousModuleReference {
+ module A {
+ module Inner {
+ predicate Q()
+ }
+ }
+ module B {
+ module Inner {
+ predicate Q()
+ }
+ }
+ module Client {
+ import A
+ import B
+ method M() {
+ assert A.Inner.Q() <==> B.Inner.Q(); // error: no reason to think these would be equal
+ }
+ }
+}
diff --git a/Test/dafny0/DiamondImports.dfy.expect b/Test/dafny0/DiamondImports.dfy.expect
new file mode 100644
index 00000000..e9e8c2b9
--- /dev/null
+++ b/Test/dafny0/DiamondImports.dfy.expect
@@ -0,0 +1,32 @@
+DiamondImports.dfy(34,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+DiamondImports.dfy(50,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+ (0,0): anon2
+DiamondImports.dfy(101,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Then
+ (0,0): anon2
+ (0,0): anon8_Then
+ (0,0): anon9_Then
+ (0,0): anon6
+DiamondImports.dfy(120,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon2
+ (0,0): anon10_Then
+ (0,0): anon4
+ (0,0): anon11_Then
+ (0,0): anon6
+ (0,0): anon12_Then
+ (0,0): anon8
+DiamondImports.dfy(140,26): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 11 verified, 5 errors
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 4b290bb7..12593b8c 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1306,3 +1306,27 @@ module FrameTargetFields {
}
}
}
+
+// ------------------------------------------------------
+
+module AmbiguousModuleReference {
+ module A {
+ module Inner {
+ predicate Q()
+ }
+ }
+ module B {
+ module Inner {
+ predicate Q()
+ }
+ }
+ module OpenClient {
+ import opened A
+ import opened B
+ lemma M() {
+ var a := A.Inner.Q(); // fine
+ var b := B.Inner.Q(); // fine
+ var p := Inner.Q(); // error: Inner is ambiguous (A.Inner or B.Inner)
+ }
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index f1c5532e..89531a5c 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -86,6 +86,7 @@ ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type paramete
ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B
ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -181,4 +182,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1134,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(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-183 resolution/type errors detected in ResolutionErrors.dfy
+184 resolution/type errors detected in ResolutionErrors.dfy