diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-02 14:17:15 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-02 14:17:15 -0700 |
| commit | cb24e4e69da6283835cc5f42c7b0f50dc604568d (patch) | |
| tree | 4646c1a614bfbf8a4f643fd9d651073c4a95e043 /Dafny/Printer.cs | |
| parent | 42c116169feb1019824d43be376acded2b491a0c (diff) | |
Dafny: incomplete snapshot of verification of iterators
Diffstat (limited to 'Dafny/Printer.cs')
| -rw-r--r-- | Dafny/Printer.cs | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 1e2424ed..fe602f86 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -269,7 +269,15 @@ namespace Microsoft.Dafny { PrintAttributes(field.Attributes);
wr.Write(" {0}: ", field.Name);
PrintType(field.Type);
- wr.WriteLine(";");
+ wr.Write(";");
+ if (field.IsUserMutable) {
+ // nothing more to say
+ } else if (field.IsMutable) {
+ wr.Write(" // may change, but not directly by program");
+ } else {
+ wr.Write(" // immutable");
+ }
+ wr.WriteLine();
}
public void PrintFunction(Function f, int indent) {
|