diff options
| author |  Unknown <afd@afd-THINK> | 2012-08-09 10:45:37 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK> | 2012-08-09 10:45:37 +0100 |
| commit | e7b03040bd2bdd5bc3fe0e76fabb56b012c12cd5 (patch) | |
| tree | d02907527b5ac2fee58827c7b19c4360140d124c /Source | |
| parent | 172bf3b8839c987d34101895bea83c2078102d04 (diff) | |
| parent | cd6ffa2c7166a5ddb2052cade723de11daf0452a (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 2 |
5 files changed, 8 insertions, 4 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index ff1a0eb1..4e134b3c 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -254,7 +254,7 @@ namespace Microsoft.Boogie { /// <summary>
/// This method is called after all parsing is done, if no parse errors were encountered.
/// </summary>
- protected virtual void ApplyDefaultOptions() {
+ public virtual void ApplyDefaultOptions() {
}
/// <summary>
@@ -1244,7 +1244,7 @@ namespace Microsoft.Boogie { return base.ParseOption(name, ps); // defer to superclass
}
- protected override void ApplyDefaultOptions() {
+ public override void ApplyDefaultOptions() {
Contract.Ensures(TheProverFactory != null);
Contract.Ensures(vcVariety != VCVariety.Unspecified);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index ce0ccf16..ebf01c4c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/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/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8ea17a52..98319473 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -20,7 +20,7 @@ namespace Microsoft.Dafny { public readonly string Name;
public List<ModuleDefinition/*!*/>/*!*/ Modules; // filled in during resolution.
- // Resolution essentially flattens the module heirarchy, for
+ // Resolution essentially flattens the module hierarchy, for
// purposes of translation and compilation.
public List<ModuleDefinition> CompileModules; // filled in during resolution.
// Contains the definitions to be used for compilation.
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 34fa0487..d5057017 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/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/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a7de690e..d01fe161 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/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);
}
|