summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com>2011-11-16 10:34:45 +0530
committerGravatar Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com>2011-11-16 10:34:45 +0530
commit7ae95fdc63d65bf9768f07a873d36f87842da0cf (patch)
treea83b51d5ba24ad06f5066334b45591f08207763c /Source/Core
parentb13899eb71d162ca976bfcd6ed774a1c99717372 (diff)
Debugging output for stratified inlining. Emit attribute on Ensures while
printing it.
Diffstat (limited to 'Source/Core')
-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 0c9538d4..32b27ae6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2112,6 +2112,7 @@ namespace Microsoft.Boogie {
stream.WriteLine(this, level, "// " + Comment);
}
stream.Write(this, level, "{0}ensures ", Free ? "free " : "");
+ Cmd.EmitAttributes(stream, Attributes);
this.Condition.Emit(stream);
stream.WriteLine(";");
}