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/DafnyDriver/DafnyDriver.cs | |
| 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/DafnyDriver/DafnyDriver.cs')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 |
1 files changed, 1 insertions, 1 deletions
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:
|