summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Dafny.atg22
-rw-r--r--Source/Dafny/DafnyAst.cs26
-rw-r--r--Source/Dafny/Parser.cs155
-rw-r--r--Source/Dafny/Printer.cs21
-rw-r--r--Source/Dafny/RefinementTransformer.cs23
5 files changed, 133 insertions, 114 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3000d348..4b9e0c27 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1036,11 +1036,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
/*------------------------------------------------------------------------*/
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression/*!*/ e = null; Attributes attrs = null;
+ Expression e = null; Attributes attrs = null;
.)
- "assert" (. x = t; s = null;.)
+ "assert" (. x = t; .)
{ IF(IsAttribute()) Attribute<ref attrs> }
- ( Expression<out e>
+ ( Expression<out e>
| "..."
)
";"
@@ -1052,9 +1052,21 @@ AssertStmt<out Statement/*!*/ s>
.)
.
AssumeStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+ .)
"assume" (. x = t; .)
- Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
+ { IF(IsAttribute()) Attribute<ref attrs> }
+ ( Expression<out e>
+ | "..."
+ )
+ (. if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+ .)
+ ";"
.
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1f3326da..a9e34dca 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1559,60 +1559,40 @@ namespace Microsoft.Dafny {
public abstract class PredicateStmt : Statement
{
- [Peer]
public readonly Expression Expr;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Expr != null);
}
- [Captured]
public PredicateStmt(IToken tok, Expression expr, Attributes attrs)
: base(tok, attrs) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
- cce.Owner.AssignSame(this, expr);
this.Expr = expr;
}
- [Captured]
public PredicateStmt(IToken tok, Expression expr)
: this(tok, expr, null) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
- cce.Owner.AssignSame(this, expr);
this.Expr = expr;
}
}
public class AssertStmt : PredicateStmt {
- [Captured]
public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)
: base(tok, expr, attrs) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
- }
-
- [Captured]
- public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr)
- : this(tok, expr, null) {
- Contract.Requires(tok != null);
- Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
}
}
public class AssumeStmt : PredicateStmt {
- [Captured]
- public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr)
- : base(tok, expr) {
+ public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)
+ : base(tok, expr, attrs) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
-
}
}
@@ -2412,6 +2392,8 @@ namespace Microsoft.Dafny {
/// S == null
/// * assert ...
/// ConditionOmitted == true
+ /// * assume ...
+ /// ConditionOmitted == true
/// * if ... { Stmt }
/// if ... { Stmt } else ElseStmt
/// ConditionOmitted == true
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 0c1920a6..a4e51924 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1157,10 +1157,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression/*!*/ e = null; Attributes attrs = null;
+ Expression e = null; Attributes attrs = null;
Expect(67);
- x = t; s = null;
+ x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1179,12 +1179,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void AssumeStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+
Expect(55);
x = t;
- Expression(out e);
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ if (StartOf(9)) {
+ Expression(out e);
+ } else if (la.kind == 30) {
+ Get();
+ } else SynErr(145);
+ if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+
Expect(18);
- s = new AssumeStmt(x, e);
}
void PrintStmt(out Statement/*!*/ s) {
@@ -1247,12 +1261,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
suchThatAssume = t;
}
Expression(out suchThat);
- } else SynErr(145);
+ } else SynErr(146);
Expect(18);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(146);
+ } else SynErr(147);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
@@ -1357,7 +1371,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 6) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs;
- } else SynErr(147);
+ } else SynErr(148);
}
if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1368,7 +1382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 6) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(148);
+ } else SynErr(149);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1400,7 +1414,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 30) {
Get();
bodyOmitted = true;
- } else SynErr(149);
+ } else SynErr(150);
if (guardOmitted || bodyOmitted) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1418,7 +1432,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives);
- } else SynErr(150);
+ } else SynErr(151);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1568,7 +1582,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(9)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(151);
+ } else SynErr(152);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -1589,7 +1603,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
- } else SynErr(152);
+ } else SynErr(153);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1612,7 +1626,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(153);
+ } else SynErr(154);
Expect(24);
}
@@ -1647,20 +1661,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (StartOf(16)) {
if (la.kind == 32 || la.kind == 65) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(155); Get();}
Expect(18);
invariants.Add(invariant);
} else if (la.kind == 35) {
- while (!(la.kind == 0 || la.kind == 35)) {SynErr(155); Get();}
+ while (!(la.kind == 0 || la.kind == 35)) {SynErr(156); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(157); Get();}
Expect(18);
} else {
- while (!(la.kind == 0 || la.kind == 31)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 31)) {SynErr(158); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1675,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(158); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(159); Get();}
Expect(18);
}
}
@@ -1683,7 +1697,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(160); Get();}
if (la.kind == 32) {
Get();
isFree = true;
@@ -1732,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(9)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(160);
+ } else SynErr(161);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1784,7 +1798,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(161);
+ } else SynErr(162);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1822,7 +1836,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(162);
+ } else SynErr(163);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1920,7 +1934,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 75) {
Get();
- } else SynErr(163);
+ } else SynErr(164);
}
void OrOp() {
@@ -1928,7 +1942,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 77) {
Get();
- } else SynErr(164);
+ } else SynErr(165);
}
void Term(out Expression/*!*/ e0) {
@@ -2020,7 +2034,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(165); break;
+ default: SynErr(166); break;
}
}
@@ -2042,7 +2056,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(166);
+ } else SynErr(167);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -2092,7 +2106,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
break;
}
- default: SynErr(167); break;
+ default: SynErr(168); break;
}
}
@@ -2107,7 +2121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 90) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(168);
+ } else SynErr(169);
}
void NegOp() {
@@ -2115,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 91) {
Get();
- } else SynErr(169);
+ } else SynErr(170);
}
void EndlessExpression(out Expression e) {
@@ -2192,7 +2206,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new LetExpr(x, letVars, letRHSs, e);
break;
}
- default: SynErr(170); break;
+ default: SynErr(171); break;
}
}
@@ -2266,7 +2280,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(171);
+ } else SynErr(172);
} else if (la.kind == 100) {
Get();
anyDots = true;
@@ -2274,7 +2288,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out ee);
e1 = ee;
}
- } else SynErr(172);
+ } else SynErr(173);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2298,7 +2312,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(58);
- } else SynErr(173);
+ } else SynErr(174);
}
void DisplayExpr(out Expression e) {
@@ -2322,7 +2336,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SeqDisplayExpr(x, elements);
Expect(58);
- } else SynErr(174);
+ } else SynErr(175);
}
void MultiSetExpr(out Expression e) {
@@ -2348,7 +2362,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(24);
} else if (StartOf(19)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(175);
+ } else SynErr(176);
}
void MapExpr(out Expression e) {
@@ -2382,7 +2396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new MapComprehension(x, bvars, range, body);
} else if (StartOf(19)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(176);
+ } else SynErr(177);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2459,7 +2473,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(24);
break;
}
- default: SynErr(177); break;
+ default: SynErr(178); break;
}
}
@@ -2495,7 +2509,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 106) {
Get();
- } else SynErr(178);
+ } else SynErr(179);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -2526,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 103 || la.kind == 104) {
Exists();
x = t;
- } else SynErr(179);
+ } else SynErr(180);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2596,7 +2610,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(180);
+ } else SynErr(181);
}
void Exists() {
@@ -2604,7 +2618,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 104) {
Get();
- } else SynErr(181);
+ } else SynErr(182);
}
void AttributeBody(ref Attributes attrs) {
@@ -2830,43 +2844,44 @@ public class Errors {
case 142: s = "this symbol not expected in OneStmt"; break;
case 143: s = "invalid OneStmt"; break;
case 144: s = "invalid AssertStmt"; break;
- case 145: s = "invalid UpdateStmt"; break;
+ case 145: s = "invalid AssumeStmt"; break;
case 146: s = "invalid UpdateStmt"; break;
- case 147: s = "invalid IfStmt"; break;
+ case 147: s = "invalid UpdateStmt"; break;
case 148: s = "invalid IfStmt"; break;
- case 149: s = "invalid WhileStmt"; break;
+ case 149: s = "invalid IfStmt"; break;
case 150: s = "invalid WhileStmt"; break;
- case 151: s = "invalid Rhs"; break;
- case 152: s = "invalid Lhs"; break;
- case 153: s = "invalid Guard"; break;
- case 154: s = "this symbol not expected in LoopSpec"; break;
+ case 151: s = "invalid WhileStmt"; break;
+ case 152: s = "invalid Rhs"; break;
+ case 153: s = "invalid Lhs"; break;
+ case 154: s = "invalid Guard"; break;
case 155: s = "this symbol not expected in LoopSpec"; break;
case 156: s = "this symbol not expected in LoopSpec"; break;
case 157: s = "this symbol not expected in LoopSpec"; break;
case 158: s = "this symbol not expected in LoopSpec"; break;
- case 159: s = "this symbol not expected in Invariant"; break;
- case 160: s = "invalid AttributeArg"; break;
- case 161: s = "invalid EquivOp"; break;
- case 162: s = "invalid ImpliesOp"; break;
- case 163: s = "invalid AndOp"; break;
- case 164: s = "invalid OrOp"; break;
- case 165: s = "invalid RelOp"; break;
- case 166: s = "invalid AddOp"; break;
- case 167: s = "invalid UnaryExpression"; break;
- case 168: s = "invalid MulOp"; break;
- case 169: s = "invalid NegOp"; break;
- case 170: s = "invalid EndlessExpression"; break;
- case 171: s = "invalid Suffix"; break;
+ case 159: s = "this symbol not expected in LoopSpec"; break;
+ case 160: s = "this symbol not expected in Invariant"; break;
+ case 161: s = "invalid AttributeArg"; break;
+ case 162: s = "invalid EquivOp"; break;
+ case 163: s = "invalid ImpliesOp"; break;
+ case 164: s = "invalid AndOp"; break;
+ case 165: s = "invalid OrOp"; break;
+ case 166: s = "invalid RelOp"; break;
+ case 167: s = "invalid AddOp"; break;
+ case 168: s = "invalid UnaryExpression"; break;
+ case 169: s = "invalid MulOp"; break;
+ case 170: s = "invalid NegOp"; break;
+ case 171: s = "invalid EndlessExpression"; break;
case 172: s = "invalid Suffix"; break;
case 173: s = "invalid Suffix"; break;
- case 174: s = "invalid DisplayExpr"; break;
- case 175: s = "invalid MultiSetExpr"; break;
- case 176: s = "invalid MapExpr"; break;
- case 177: s = "invalid ConstAtomExpression"; break;
- case 178: s = "invalid QSep"; break;
- case 179: s = "invalid QuantifierGuts"; break;
- case 180: s = "invalid Forall"; break;
- case 181: s = "invalid Exists"; break;
+ case 174: s = "invalid Suffix"; break;
+ case 175: s = "invalid DisplayExpr"; break;
+ case 176: s = "invalid MultiSetExpr"; break;
+ case 177: s = "invalid MapExpr"; break;
+ case 178: s = "invalid ConstAtomExpression"; break;
+ case 179: s = "invalid QSep"; break;
+ case 180: s = "invalid QuantifierGuts"; break;
+ case 181: s = "invalid Forall"; break;
+ case 182: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 498546c3..3654c672 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -433,24 +433,14 @@ namespace Microsoft.Dafny {
}
}
- if (stmt is AssertStmt) {
- Expression expr = ((AssertStmt)stmt).Expr;
-
- wr.Write("assert");
-
- if (stmt.HasAttributes())
- {
+ if (stmt is PredicateStmt) {
+ Expression expr = ((PredicateStmt)stmt).Expr;
+ wr.Write(stmt is AssertStmt ? "assert" : "assume");
+ if (stmt.HasAttributes()) {
PrintAttributes(stmt.Attributes);
}
-
wr.Write(" ");
PrintExpression(expr);
-
- wr.Write(";");
-
- } else if (stmt is AssumeStmt) {
- wr.Write("assume ");
- PrintExpression(((AssumeStmt)stmt).Expr);
wr.Write(";");
} else if (stmt is PrintStmt) {
@@ -635,6 +625,9 @@ namespace Microsoft.Dafny {
} else if (s.S is AssertStmt) {
Contract.Assert(s.ConditionOmitted);
wr.Write("assert ...;");
+ } else if (s.S is AssumeStmt) {
+ Contract.Assert(s.ConditionOmitted);
+ wr.Write("assume ...;");
} else if (s.S is IfStmt) {
PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);
} else if (s.S is WhileStmt) {
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 5afe1ba7..e3b778d8 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -476,11 +476,11 @@ namespace Microsoft.Dafny {
Statement r;
if (stmt is AssertStmt) {
var s = (AssertStmt)stmt;
- r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr));
+ r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
} else if (stmt is AssumeStmt) {
var s = (AssumeStmt)stmt;
- r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr));
+ r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
} else if (stmt is PrintStmt) {
var s = (PrintStmt)stmt;
@@ -864,6 +864,8 @@ namespace Microsoft.Dafny {
* assert ...; assert E; assert E;
* assert E; assert E;
*
+ * assume ...; assume E; assume E;
+ *
* var x := E; var x; var x := E;
* var x := E; var x := *; var x := E;
* var x := E1; var x :| E0; var x := E1; assert E0;
@@ -925,6 +927,19 @@ namespace Microsoft.Dafny {
i++; j++;
}
+ } else if (S is AssumeStmt) {
+ var skel = (AssumeStmt)S;
+ Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);
+ var oldAssume = oldS as AssumeStmt;
+ if (oldAssume == null) {
+ reporter.Error(cur.Tok, "assume template does not match inherited statement");
+ i++;
+ } else {
+ var e = CloneExpr(oldAssume.Expr);
+ body.Add(new AssumeStmt(skel.Tok, e, null));
+ i++; j++;
+ }
+
} else if (S is IfStmt) {
var skel = (IfStmt)S;
Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);
@@ -998,7 +1013,7 @@ namespace Microsoft.Dafny {
body.Add(cNew);
i++; j++;
if (addedAssert != null) {
- body.Add(new AssertStmt(addedAssert.tok, addedAssert));
+ body.Add(new AssertStmt(addedAssert.tok, addedAssert, null));
}
} else {
MergeAddStatement(cur, body);
@@ -1076,6 +1091,8 @@ namespace Microsoft.Dafny {
var S = ((SkeletonStatement)nxt).S;
if (S is AssertStmt) {
return other is PredicateStmt;
+ } else if (S is AssumeStmt) {
+ return other is AssumeStmt;
} else if (S is IfStmt) {
return other is IfStmt;
} else if (S is WhileStmt) {
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:56:20 +0000