diff options
author | 2011-04-22 22:57:58 -0700 | |
---|---|---|
committer | 2011-04-22 22:57:58 -0700 | |
commit | dcaef29ffbe2570632e7368d27377fb9ac282d7b (patch) | |
tree | a26c6cc36c473c789affea73c81485369a6dbb39 /Source/Dafny/DafnyAst.cs | |
parent | e6609f4aa8c29d32a3b590bf2b4337148a686bf5 (diff) |
Dafny: include source location for array types supplied in input
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d923e5dc..f76f24de 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -40,20 +40,21 @@ namespace Microsoft.Dafny { ClassDecl obj = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);
SystemModule.TopLevelDecls.Add(obj);
// add one-dimensional arrays, since they may arise during type checking
- UserDefinedType tmp = ArrayType(1, Type.Int, true);
+ UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
}
public UserDefinedType ArrayType(int dims, Type arg) {
- return ArrayType(dims, arg, false);
+ return ArrayType(Token.NoToken, dims, arg, false);
}
- public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
+ public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) {
+ Contract.Requires(tok != null);
Contract.Requires(1 <= dims);
Contract.Requires(arg != null);
Contract.Ensures(Contract.Result<UserDefinedType>() != null);
List<Type/*!*/> typeArgs = new List<Type/*!*/>();
typeArgs.Add(arg);
- UserDefinedType udt = new UserDefinedType(Token.NoToken, ArrayClassName(dims), typeArgs);
+ UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
for (int d = 0; d < dims; d++) {
|