diff options
author | 2010-08-27 23:03:39 +0000 | |
---|---|---|
committer | 2010-08-27 23:03:39 +0000 | |
commit | 26baa7644418ff146b18dfb4cfd72b484a43ea98 (patch) | |
tree | d8b76b0bb168ad64f153dbba34a49ece2109581a | |
parent | a54b325fc6a4986ff3c2fb69689e574802707fa4 (diff) |
Dafny: fallback to ShallowType (elements of IndexField arrays seem to have Type null)
-rw-r--r-- | Dafny/Translator.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index bdb436ce..cd084ca1 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -3946,8 +3946,9 @@ Contract.Requires(tok != null); args.Add(heap);
args.Add(r);
args.Add(f);
+ Bpl.Type t = (f.Type != null) ? f.Type : f.ShallowType;
return new Bpl.NAryExpr(tok,
- new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", f.Type.AsCtor.Arguments[0])),
+ new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])),
args);
}
|