diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 93860cc6..afab0c1f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -575,6 +575,7 @@ namespace Microsoft.Dafny { wr.WriteLine(")");
Indent(indent); wr.WriteLine("{");
TrReq(m.Req, indent + IndentAmount);
+ TrEns(m.Ens, indent + IndentAmount);
foreach (Formal p in m.Outs) {
if (!p.IsGhost) {
Indent(indent + IndentAmount);
@@ -2243,6 +2244,25 @@ namespace Microsoft.Dafny { }
}
+ void TrEns(List<MaybeFreeExpression/*!*/>/*!*/ ens, int indent)
+ {
+ Contract.Requires(cce.NonNullElements(ens));
+
+ if (DafnyOptions.O.RuntimeChecking)
+ {
+ foreach (MaybeFreeExpression e in ens)
+ {
+ if (!e.IsFree)
+ {
+ Indent(indent);
+ wr.Write("Contract.Ensures(");
+ TrExpr(e.E);
+ wr.WriteLine(");");
+ }
+ }
+ }
+ }
+
#endregion
#region Runtime checking helper methods
|