diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-08 18:42:57 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-08 18:42:57 -0700 |
| commit | c777b247b8cc689447acc64934f801e2d7d98393 (patch) | |
| tree | 34764c176290dda4a95a2788fe3c7f69acec3d08 /Dafny | |
| parent | 20d5a1e85f8b6f5c32c9c7fb7c1986a3165f8aec (diff) | |
Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and visually indicates a non-verified buffer
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Dafny/DafnyOptions.cs | 2 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 2 |
3 files changed, 5 insertions, 1 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index ce0ccf16..ebf01c4c 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -1031,6 +1031,8 @@ WhileStmt<out Statement/*!*/ stmt> stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);
} else {
+ // The following statement protects against crashes in case of parsing errors
+ body = body ?? new BlockStmt(x, new List<Statement>());
stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
.)
diff --git a/Dafny/DafnyOptions.cs b/Dafny/DafnyOptions.cs index 34fa0487..d5057017 100644 --- a/Dafny/DafnyOptions.cs +++ b/Dafny/DafnyOptions.cs @@ -97,7 +97,7 @@ namespace Microsoft.Dafny return base.ParseOption(name, ps);
}
- protected override void ApplyDefaultOptions() {
+ public override void ApplyDefaultOptions() {
base.ApplyDefaultOptions();
// expand macros in filenames, now that LogPrefix is fully determined
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index a7de690e..d01fe161 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -1515,6 +1515,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);
} else {
+ // The following statement protects against crashes in case of parsing errors
+ body = body ?? new BlockStmt(x, new List<Statement>());
stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
|