diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 19 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 10 |
2 files changed, 26 insertions, 3 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 78ea8d3d..71e28b98 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -389,6 +389,25 @@ namespace Microsoft.Dafny { return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;
}
+ public bool HasMain(Program program) {
+ foreach (var module in program.Modules) {
+ foreach (var decl in module.TopLevelDecls) {
+ var c = decl as ClassDecl;
+ if (c != null) {
+ foreach (var member in c.Members) {
+ var m = member as Method;
+ if (m != null) {
+ if (!m.IsGhost && m.Name == "Main" && m.Ins.Count == 0 && m.Outs.Count == 0) {
+ return true;
+ }
+ }
+ }
+ }
+ }
+ }
+ return false;
+ }
+
void CompileClassMembers(ClassDecl c, int indent)
{
Contract.Requires(c != null);
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index c7a929b8..062af148 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -222,11 +222,15 @@ namespace Microsoft.Dafny var provider = CodeDomProvider.CreateProvider("CSharp");
var cp = new System.CodeDom.Compiler.CompilerParameters();
cp.GenerateExecutable = true;
- // TODO: an improvement would be to generate a .dll if there is no Main method
- cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "exe");
+ if (compiler.HasMain(dafnyProgram)) {
+ cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "exe");
+ cp.CompilerOptions = "/debug";
+ } else {
+ cp.OutputAssembly = Path.ChangeExtension(dafnyProgramName, "dll");
+ cp.CompilerOptions = "/debug /target:library";
+ }
cp.GenerateInMemory = false;
cp.ReferencedAssemblies.Add("System.Numerics.dll");
- cp.CompilerOptions = "/debug";
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
if (cr.Errors.Count == 0) {
|