diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-09-11 13:20:52 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-09-11 13:20:52 -0700 |
| commit | 0d06cb1b6a16fee1a789f3b1b674d59cfcd11d92 (patch) | |
| tree | 53d25d76f411daebd462d5deff6ffbb244478891 /Source | |
| parent | 1561cbe8636d0a083aef03532aeb8153de372d42 (diff) | |
Dafny: generate a compiler error upon encountering an assume statement
Dafny: don't compile programs unless all methods have been verified (or a forced compile is requested)
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 46 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 |
3 files changed, 54 insertions, 8 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f0e325e8..f7ccca9c 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -394,7 +394,7 @@ namespace Microsoft.Boogie { private string methodToBreakOn = null;
[ContractInvariantMethod]
void ObjectInvariant5() {
- Contract.Invariant(cce.NonNullElements(procsToCheck, true));
+ Contract.Invariant(cce.NonNullElements(ProcsToCheck, true));
Contract.Invariant(cce.NonNullElements(methodsToTranslateClass, true));
Contract.Invariant(cce.NonNullElements(methodsToTranslateClassQualified, true));
Contract.Invariant(cce.NonNullElements(methodsToTranslateExclude));
@@ -406,7 +406,7 @@ namespace Microsoft.Boogie { }
[Rep]
- private List<string/*!*/> procsToCheck = null; // null means "no restriction"
+ public List<string/*!*/> ProcsToCheck = null; // null means "no restriction"
[Rep]
private List<string/*!*/> methodsToTranslateSubstring = null; // null means "no restriction"
[Rep]
@@ -606,11 +606,11 @@ namespace Microsoft.Boogie { case "-proc":
case "/proc":
- if (procsToCheck == null) {
- procsToCheck = new List<string/*!*/>();
+ if (ProcsToCheck == null) {
+ ProcsToCheck = new List<string/*!*/>();
}
if (ps.ConfirmArgumentCount(1)) {
- procsToCheck.Add(cce.NonNull(args[ps.i]));
+ ProcsToCheck.Add(cce.NonNull(args[ps.i]));
}
break;
@@ -1551,11 +1551,11 @@ namespace Microsoft.Boogie { public bool UserWantsToCheckRoutine(string methodFullname) {
Contract.Requires(methodFullname != null);
- if (procsToCheck == null) {
+ if (ProcsToCheck == null) {
// no preference
return true;
}
- return Contract.Exists(procsToCheck, s => 0 <= methodFullname.IndexOf(s));
+ return Contract.Exists(ProcsToCheck, s => 0 <= methodFullname.IndexOf(s));
}
#if CCI
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 69008d26..c8051e2b 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -658,10 +658,56 @@ namespace Microsoft.Dafny { // ----- Stmt ---------------------------------------------------------------------------------
+ void CheckHasNoAssumes(Statement stmt) {
+ 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 ForeachStmt) {
+ ForeachStmt s = (ForeachStmt)stmt;
+ foreach (PredicateStmt t in s.BodyPrefix) {
+ CheckHasNoAssumes(t);
+ }
+ CheckHasNoAssumes(s.GivenBody);
+ } else if (stmt is MatchStmt) {
+ MatchStmt s = (MatchStmt)stmt;
+ foreach (MatchCaseStmt mc in s.Cases) {
+ foreach (Statement bs in mc.Body) {
+ CheckHasNoAssumes(bs);
+ }
+ }
+ }
+ }
+
void TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
+ CheckHasNoAssumes(stmt);
return;
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index d8d0e0e0..1c6c1e77 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -176,7 +176,7 @@ namespace Microsoft.Boogie switch (oc) {
case PipelineOutcome.VerificationCompleted:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- if ((CommandLineOptions.Clo.Compile && allOk) || CommandLineOptions.Clo.ForceCompile)
+ if ((CommandLineOptions.Clo.Compile && allOk && CommandLineOptions.Clo.ProcsToCheck == null) || CommandLineOptions.Clo.ForceCompile)
CompileDafnyProgram(dafnyProgram);
break;
case PipelineOutcome.Done:
|