diff options
author | 2011-12-04 13:14:23 +0530 | |
---|---|---|
committer | 2011-12-04 13:14:23 +0530 | |
commit | 090202f9034909878796f1c197f18c43e047bcbd (patch) | |
tree | fdb2a22573a6d58a39fe5b57e61b2979a522264b /Source/Core/Absy.cs | |
parent | 7b8a0e0a4e75f28a1721bee9179f65bd405301c2 (diff) |
Emit attribute on a requires
Diffstat (limited to 'Source/Core/Absy.cs')
-rw-r--r-- | Source/Core/Absy.cs | 1 |
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(";");
}
|