diff options
author | qadeer <qadeer@microsoft.com> | 2011-12-06 21:14:27 -0800 |
---|---|---|
committer | qadeer <qadeer@microsoft.com> | 2011-12-06 21:14:27 -0800 |
commit | 30c8dbffe8dc1a450205c78a97a5d7b402876558 (patch) | |
tree | 3131b43cd88c5d2ebed9bdc6994efe778370e5f0 /Source/Dafny/Dafny.atg | |
parent | 9cddddd5e14e41f60e1ea882624f843a78f93cd7 (diff) | |
parent | 0309df8a19b721a6e4813d41170989e65eaa3794 (diff) |
Merge
Diffstat (limited to 'Source/Dafny/Dafny.atg')
-rw-r--r-- | Source/Dafny/Dafny.atg | 57 |
1 files changed, 35 insertions, 22 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2eaaca7f..7019a22b 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -191,6 +191,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c> List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
.)
+ SYNC
"class"
{ Attribute<ref attrs> }
Ident<out id>
@@ -234,6 +235,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt> List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
IToken bodyStart = Token.NoToken; // dummy assignment
.)
+ SYNC
"datatype"
{ Attribute<ref attrs> }
Ident<out id>
@@ -241,7 +243,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt> "=" (. bodyStart = t; .)
DatatypeMemberDecl<ctors>
{ "|" DatatypeMemberDecl<ctors> }
- ";"
+ SYNC ";"
(. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
@@ -263,6 +265,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
.)
+ SYNC
"var"
(. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -271,7 +274,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
{ "," IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
- ";"
+ SYNC ";"
.
CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
@@ -379,6 +382,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
+ SYNC
( "method"
| "constructor" (. if (allowConstructor) {
isConstructor = true;
@@ -423,16 +427,17 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/ = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false;
.)
+ SYNC
( "modifies" [ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
- ] ";"
+ ] SYNC ";"
| [ "free" (. isFree = true; .)
]
- ( "requires" Expression<out e> ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
- | "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
+ ( "requires" Expression<out e> SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
+ | "ensures" Expression<out e> SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
)
- | "decreases" DecreasesList<decreases, false> ";"
+ | "decreases" DecreasesList<decreases, false> SYNC ";"
)
.
Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
@@ -555,13 +560,15 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> 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); .)
+ (
+ SYNC
+ "requires" Expression<out e> SYNC ";" (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
}
- ] ";"
- | "ensures" Expression<out e> ";" (. ens.Add(e); .)
- | "decreases" DecreasesList<decreases, false> ";"
+ ] SYNC ";"
+ | "ensures" Expression<out e> SYNC ";" (. ens.Add(e); .)
+ | "decreases" DecreasesList<decreases, false> SYNC ";"
)
.
PossiblyWildExpression<out Expression/*!*/ e>
@@ -622,6 +629,7 @@ OneStmt<out Statement/*!*/ s> int breakCount;
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
+ SYNC
( BlockStmt<out s, out bodyStart, out bodyEnd>
| AssertStmt<out s>
| AssumeStmt<out s>
@@ -640,6 +648,7 @@ OneStmt<out Statement/*!*/ s> | { "break" (. breakCount++; .)
}
)
+ SYNC
";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
| ReturnStmt<out s>
)
@@ -814,25 +823,29 @@ WhileStmt<out Statement/*!*/ stmt> )
.
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
-= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
+= (. FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
+ MaybeFreeExpression invariant = null;
decreases = new List<Expression/*!*/>();
mod = null;
.)
- { (. isFree = false; .)
- [ "free" (. isFree = true; .)
- ]
- "invariant"
- Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
- ";"
- | "decreases" DecreasesList<decreases, true> ";"
- | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ {
+ Invariant<out invariant> SYNC ";" (. invariants.Add(invariant); .)
+ | SYNC "decreases" DecreasesList<decreases, true> SYNC ";"
+ | SYNC "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
[ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
- ] ";"
+ ] SYNC ";"
}
.
+Invariant<out MaybeFreeExpression/*!*/ invariant>
+= (. bool isFree = false; Expression/*!*/ e; invariant = null; .)
+ SYNC
+ ["free" (. isFree = true; .)
+ ]
+ "invariant" Expression<out e> (. invariant = new MaybeFreeExpression(e, isFree); .)
+ .
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
@@ -1310,8 +1323,8 @@ Suffix<ref Expression/*!*/ e> }
)
| ".." (. anyDots = true; .)
- [ Expression<out ee> (. e1 = ee; .)
- ]
+ [ Expression<out ee> (. e1 = ee; .)
+ ]
)
(. if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
|