diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 12 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 13 |
2 files changed, 24 insertions, 1 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index a6827d5f..125ab11e 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -55,6 +55,7 @@ namespace Microsoft.Dafny public bool ignoreAutoReq = false;
public bool AllowGlobals = false;
public bool CountVerificationErrors = true;
+ public bool Optimize = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -180,6 +181,11 @@ namespace Microsoft.Dafny return true;
}
+ case "optimize": {
+ Optimize = true;
+ return true;
+ }
+
default:
break;
}
@@ -270,6 +276,12 @@ namespace Microsoft.Dafny of verification errors.
1 (default) - If preprocessing succeeds, set exit code to the number of
verification errors.
+ /optimize Produce optimized C# code, meaning:
+ - selects optimized C# prelude by passing
+ /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires
+ System.Collections.Immutable.dll in the source directory to successfully
+ compile).
+ - passes /optimize flag to csc.exe.
");
base.Usage(); // also print the Boogie options
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a769b829..cf464754 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -15,6 +15,8 @@ namespace Microsoft.Dafny using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.IO;
+ using System.Reflection;
+
using Microsoft.Boogie;
using Bpl = Microsoft.Boogie;
@@ -330,7 +332,7 @@ namespace Microsoft.Dafny }
else
{
- var provider = CodeDomProvider.CreateProvider("CSharp");
+ var provider = CodeDomProvider.CreateProvider("CSharp", new Dictionary<string, string> { { "CompilerVersion", "v4.0" } });
var cp = new System.CodeDom.Compiler.CompilerParameters();
cp.GenerateExecutable = hasMain;
if (DafnyOptions.O.RunAfterCompile) {
@@ -344,6 +346,15 @@ namespace Microsoft.Dafny }
cp.CompilerOptions = "/debug /nowarn:0164 /nowarn:0219"; // warning CS0164 complains about unreferenced labels, CS0219 is about unused variables
cp.ReferencedAssemblies.Add("System.Numerics.dll");
+ cp.ReferencedAssemblies.Add("System.Core.dll");
+ cp.ReferencedAssemblies.Add("System.dll");
+
+ if (DafnyOptions.O.Optimize) {
+ var libPath = Path.GetDirectoryName(dafnyProgramName);
+ cp.CompilerOptions += string.Format(" /optimize /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE /lib:{0}", libPath);
+ cp.ReferencedAssemblies.Add("System.Collections.Immutable.dll");
+ cp.ReferencedAssemblies.Add("System.Runtime.dll");
+ }
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
var assemblyName = Path.GetFileName(cr.PathToAssembly);
|