summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-12-05 11:57:51 -0800
committerGravatar qadeer <qadeer@microsoft.com>2011-12-05 11:57:51 -0800
commit4266ee07457dfacdee4f037f4907b4db1758bfec (patch)
tree9d08d6f67880363c43a179bf5f4e6e14d3e5494c /Source
parent70caaefc912aeaab556c7bfee6c1a9b7e8fe75a3 (diff)
parent090202f9034909878796f1c197f18c43e047bcbd (diff)
Merge
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/Absy.cs1
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0aaf3c46..11455259 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2017,6 +2017,7 @@ namespace Microsoft.Boogie {
stream.WriteLine(this, level, "// " + Comment);
}
stream.Write(this, level, "{0}requires ", Free ? "free " : "");
+ Cmd.EmitAttributes(stream, Attributes);
this.Condition.Emit(stream);
stream.WriteLine(";");
}