diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 17:10:20 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 17:10:20 -0700 |
| commit | 8bf9d3f838df8e8e42f496d9de5468e2946bd5e4 (patch) | |
| tree | 4509787bb791cda0e2e7024780b0a3bd5edb1bf9 /Dafny/Compiler.cs | |
| parent | dee846026331bfc0b97d11b98a69a5cd7cc6b06b (diff) | |
Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 39 |
1 files changed, 5 insertions, 34 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index d5b15300..454b47be 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -710,40 +710,11 @@ namespace Microsoft.Dafny { Contract.Requires(stmt != null);
if (stmt is AssumeStmt) {
Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);
- } else if (stmt is BlockStmt) {
- foreach (Statement s in ((BlockStmt)stmt).Body) {
- CheckHasNoAssumes(s);
- }
- } else if (stmt is IfStmt) {
- IfStmt s = (IfStmt)stmt;
- CheckHasNoAssumes(s.Thn);
- if (s.Els != null) {
- CheckHasNoAssumes(s.Els);
- }
- } else if (stmt is AlternativeStmt) {
- foreach (var alternative in ((AlternativeStmt)stmt).Alternatives) {
- foreach (Statement s in alternative.Body) {
- CheckHasNoAssumes(s);
- }
- }
- } else if (stmt is WhileStmt) {
- WhileStmt s = (WhileStmt)stmt;
- CheckHasNoAssumes(s.Body);
- } else if (stmt is AlternativeLoopStmt) {
- foreach (var alternative in ((AlternativeLoopStmt)stmt).Alternatives) {
- foreach (Statement s in alternative.Body) {
- CheckHasNoAssumes(s);
- }
- }
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- CheckHasNoAssumes(s.Body);
- } else if (stmt is MatchStmt) {
- MatchStmt s = (MatchStmt)stmt;
- foreach (MatchCaseStmt mc in s.Cases) {
- foreach (Statement bs in mc.Body) {
- CheckHasNoAssumes(bs);
- }
+ } else if (stmt is AssignSuchThatStmt) {
+ Error("an assign-such-that statement cannot be compiled (line {0})", stmt.Tok.line);
+ } else {
+ foreach (var ss in stmt.SubStatements) {
+ CheckHasNoAssumes(ss);
}
}
}
|