diff options
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 14 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 50 |
2 files changed, 44 insertions, 20 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b69a9536..31fe6edd 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -38,6 +38,7 @@ namespace Microsoft.Dafny public string DafnyPrintResolvedFile = null;
public bool Compile = true;
public bool ForceCompile = false;
+ public bool RunAfterCompile = false;
public bool SpillTargetCode = false;
public bool DisallowIncludes = false;
@@ -65,10 +66,11 @@ namespace Microsoft.Dafny case "compile": {
int compile = 0;
- if (ps.GetNumericArgument(ref compile, 3)) {
+ if (ps.GetNumericArgument(ref compile, 4)) {
// convert option to two booleans
- Compile = compile == 1 || compile == 2;
+ Compile = compile != 0;
ForceCompile = compile == 2;
+ RunAfterCompile = compile == 3;
}
return true;
}
@@ -136,9 +138,15 @@ namespace Microsoft.Dafny (use - as <file> to print to console)
/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
+ program, compile Dafny program to .NET assembly
+ Program.exe (if the program has a Main method) or
+ Program.dll (othewise), where Program.dfy is the name
+ of the last .dfy file on the command line
2 - always attempt to compile Dafny program to C# program
out.cs, regardless of verification outcome
+ 3 - if there is a Main method and there are no verification
+ errors, compiles program in memory (i.e., does not write
+ an output file) and runs it
/spillTargetCode:<n>
0 (default) - don't write the compiled Dafny program (but
still compile it, if /compile indicates to do so)
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 10c7e90a..4983c51f 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -103,7 +103,8 @@ namespace Microsoft.Dafny {
foreach (var f in fileNames)
{
- Console.WriteLine("\n-------------------- {0} --------------------", f);
+ Console.WriteLine();
+ Console.WriteLine("-------------------- {0} --------------------", f);
var ev = ProcessFiles(new List<string> { f });
if (exitValue != ev && ev != ExitValue.VERIFIED)
{
@@ -242,9 +243,15 @@ namespace Microsoft.Dafny public static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)
{
Contract.Requires(dafnyProgram != null);
+
// Compile the Dafny program into a string that contains the C# program
StringWriter sw = new StringWriter();
Dafny.Compiler compiler = new Dafny.Compiler(sw);
+ var hasMain = compiler.HasMain(dafnyProgram);
+ if (DafnyOptions.O.RunAfterCompile && !hasMain) {
+ // do no more
+ return;
+ }
compiler.Compile(dafnyProgram);
var csharpProgram = sw.ToString();
bool completeProgram = compiler.ErrorCount == 0;
@@ -280,30 +287,39 @@ namespace Microsoft.Dafny {
var provider = CodeDomProvider.CreateProvider("CSharp");
var cp = new System.CodeDom.Compiler.CompilerParameters();
- cp.GenerateExecutable = true;
- if (compiler.HasMain(dafnyProgram))
- {
+ cp.GenerateExecutable = hasMain;
+ if (DafnyOptions.O.RunAfterCompile) {
+ cp.GenerateInMemory = true;
+ } else if (hasMain) {
cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "exe");
- cp.CompilerOptions = "/debug /nowarn:0164"; // warning CS0164 complains about unreferenced labels
- }
- else
- {
+ cp.GenerateInMemory = false;
+ } else {
cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "dll");
- cp.CompilerOptions = "/debug /nowarn:0164 /target:library"; // warning CS0164 complains about unreferenced labels
+ cp.GenerateInMemory = false;
}
- cp.GenerateInMemory = false;
+ cp.CompilerOptions = "/debug /nowarn:0164"; // warning CS0164 complains about unreferenced labels
cp.ReferencedAssemblies.Add("System.Numerics.dll");
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
- if (cr.Errors.Count == 0)
- {
+ if (DafnyOptions.O.RunAfterCompile && cr.Errors.Count == 0) {
+ Console.WriteLine("Program compiled successfully");
+ Console.WriteLine("Running...");
+ Console.WriteLine();
+ var entry = cr.CompiledAssembly.EntryPoint;
+ try {
+ entry.Invoke(null, new object[] { new string[0] });
+ } catch (System.Reflection.TargetInvocationException e) {
+ Console.WriteLine("Error: Execution resulted in exception: {0}", e.Message);
+ Console.WriteLine(e.InnerException.ToString());
+ } catch (Exception e) {
+ Console.WriteLine("Error: Execution resulted in exception: {0}", e.Message);
+ Console.WriteLine(e.ToString());
+ }
+ } else if (cr.Errors.Count == 0) {
Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);
- }
- else
- {
+ } else {
Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);
- foreach (var ce in cr.Errors)
- {
+ foreach (var ce in cr.Errors) {
Console.WriteLine(ce.ToString());
Console.WriteLine();
}
|