diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
-rw-r--r-- | Source/Dafny/Dafny.atg | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index eeb8024a..ef7164bc 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -574,6 +574,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> List<Formal/*!*/> formals = new List<Formal/*!*/>();
Type/*!*/ returnType;
List<Expression/*!*/> reqs = new List<Expression/*!*/>();
+ List<Expression/*!*/> ens = new List<Expression/*!*/>();
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
Expression/*!*/ bb; Expression body = null;
@@ -594,18 +595,18 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> ":"
Type<out returnType>
( ";"
- { FunctionSpec<reqs, reads, decreases> }
- | { FunctionSpec<reqs, reads, decreases> }
+ { FunctionSpec<reqs, reads, ens, decreases> }
+ | { FunctionSpec<reqs, reads, ens, decreases> }
FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
)
(. parseVarScope.PopMarker();
- f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
.)
.
-FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ decreases.>
+FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
( "requires" Expression<out e> ";" (. reqs.Add(e); .)
@@ -613,6 +614,7 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r { "," PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
}
] ";"
+ | "ensures" Expression<out e> ";" (. ens.Add(e); .)
| "decreases" Expressions<decreases> ";"
)
.
|