diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-24 22:43:11 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-24 22:43:11 -0700 |
| commit | 9be7b83c4e6a7badb2e2ea3a0776a7acaf63bbb6 (patch) | |
| tree | 9706c050e29ea3d9880890a1585ebb99d3e64829 /Dafny/Compiler.cs | |
| parent | 4882523dcc2bf0c46d2cb3154ecb19bc9ea4f5cb (diff) | |
Dafny: changed local "var" introductions to use new VarDeclStmt instead of parsing as the old VarDecl's with RHS's
To-do: automatically make some variables introduce ghost variables, depending on RHS of initial assignment
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 86fd1688..c73b51a1 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -967,15 +967,7 @@ namespace Microsoft.Dafny { Indent(indent);
wr.Write("{0} @{1}", TypeName(s.Type), s.Name);
- if (s.Rhs != null) {
- wr.Write(" = ");
- TrAssignmentRhs(s.Rhs);
- wr.WriteLine(";");
- var tRhs = s.Rhs as TypeRhs;
- if (tRhs != null && tRhs.InitCall != null) {
- TrCallStmt(tRhs.InitCall, s.Name, indent);
- }
- } else if (alwaysInitialize) {
+ if (alwaysInitialize) {
// produce a default value
wr.WriteLine(" = {0};", DefaultValue(s.Type));
} else {
|