diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-17 14:14:43 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-17 14:14:43 -0800 |
| commit | 915225c14ba71e94ed0f43fef8aaeb4dfbf49e71 (patch) | |
| tree | ce77a51b332cde6063eb220c3ae2d1937e70b183 /Source/Core/Parser.cs | |
| parent | 0eb9ff4e155aa102d67b7dd3250831962d922886 (diff) | |
changed the semantics of requires and ensures for inlined procedures
Diffstat (limited to 'Source/Core/Parser.cs')
| -rw-r--r-- | Source/Core/Parser.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 34f43896..5bfbbfc2 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -503,7 +503,7 @@ private class BvBounds : Expr { }
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
} else SynErr(91);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
|