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 | a4b9ca4e83da80a7e0b994196272cf28c9cd370e (patch) | |
| tree | c49cbceebac7c8790af842821b00cae917267906 /Source/Dafny/Compiler.cs | |
| parent | f73c3a1f909f55bee986b654f05013df96d3ad7c (diff) | |
Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 39 |
1 files changed, 5 insertions, 34 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index d5b15300..454b47be 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/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);
}
}
}
|