diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 8 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 36 |
2 files changed, 26 insertions, 18 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 8f2d0c68..22264c8f 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -159,6 +159,7 @@ namespace Microsoft.Boogie { public string DafnyPrelude = null;
public string DafnyPrintFile = null;
public bool Compile = true;
+ public bool ForceCompile = false;
public enum ProverWarnings {
None,
@@ -712,8 +713,9 @@ namespace Microsoft.Boogie { case "-compile":
case "/compile": {
int compile = 0;
- if (ps.GetNumericArgument(ref compile, 2)) {
- Compile = compile == 1;
+ if (ps.GetNumericArgument(ref compile, 3)) {
+ Compile = compile == 1 || compile == 2;
+ ForceCompile = compile == 2;
}
break;
}
@@ -2097,6 +2099,8 @@ namespace Microsoft.Boogie { /compile:<n> : 0 - do not compile Dafny program
1 (default) - upon successful verification of the Dafny
program, compile Dafny program to C# program out.cs
+ 2 - always attempt to compile Dafny program to C# program
+ out.cs, regardless of verification outcome
---- Boogie options --------------------------------------------------------
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 91e33ea9..73f7fc71 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -166,24 +166,14 @@ namespace Microsoft.Boogie PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
switch (oc) {
case PipelineOutcome.VerificationCompleted:
- if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) {
- string targetFilename = "out.cs";
- using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
- Dafny.Compiler compiler = new Dafny.Compiler(target);
- compiler.Compile(dafnyProgram);
- WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- if (compiler.ErrorCount == 0) {
- Console.WriteLine("Compiled program written to {0}", targetFilename);
- } else {
- Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
- }
- }
- } else {
- WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- }
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if ((CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) || CommandLineOptions.Clo.ForceCompile)
+ CompileDafnyProgram(dafnyProgram);
break;
case PipelineOutcome.Done:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if (CommandLineOptions.Clo.ForceCompile)
+ CompileDafnyProgram(dafnyProgram);
break;
default:
// error has already been reported to user
@@ -192,7 +182,21 @@ namespace Microsoft.Boogie }
}
}
-
+
+ private static void CompileDafnyProgram(Dafny.Program dafnyProgram)
+ {
+ string targetFilename = "out.cs";
+ using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
+ Dafny.Compiler compiler = new Dafny.Compiler(target);
+ compiler.Compile(dafnyProgram);
+ if (compiler.ErrorCount == 0) {
+ Console.WriteLine("Compiled program written to {0}", targetFilename);
+ }
+ else {
+ Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
+ }
+ }
+ }
static void PrintBplFile (string filename, Program program, bool allowPrintDesugaring)
{
|