diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 19:58:46 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 19:58:46 -0700 |
| commit | e676ad0877d31cb73a1a6bb5aae677ac64593fd6 (patch) | |
| tree | 5ea6563ed11ae2df0c60de418b8036751ae9ec3c /Source/DafnyServer | |
| parent | 24812516d64ed809d7446680a79eac492ea6a201 (diff) | |
Cleanup a number of FIXMEs that I had left in the code
Diffstat (limited to 'Source/DafnyServer')
| -rw-r--r-- | Source/DafnyServer/DafnyHelper.cs | 2 | ||||
| -rw-r--r-- | Source/DafnyServer/Server.cs | 9 | ||||
| -rw-r--r-- | Source/DafnyServer/Utilities.cs | 6 |
3 files changed, 4 insertions, 13 deletions
diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 952f71c5..3204fdb3 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -74,7 +74,7 @@ namespace Microsoft.Dafny { ExecutionEngine.CoalesceBlocks(boogieProgram);
ExecutionEngine.Inline(boogieProgram);
- //FIXME Could capture errors instead of printing them (pass a delegate instead of null)
+ //NOTE: We could capture errors instead of printing them (pass a delegate instead of null)
switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) {
case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index e524a9a3..77840007 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -32,9 +32,8 @@ namespace Microsoft.Dafny { private void SetupConsole() {
var utf8 = new UTF8Encoding(false, true);
+ Console.InputEncoding = utf8;
Console.OutputEncoding = utf8;
- Console.OutputEncoding = utf8;
- Console.CancelKeyPress += CancelKeyPress;
}
public Server() {
@@ -43,12 +42,6 @@ namespace Microsoft.Dafny { SetupConsole();
}
- void CancelKeyPress(object sender, ConsoleCancelEventArgs e) {
- // e.Cancel = true;
- // FIXME TerminateProver and RunningProverFromCommandLine
- // Cancel the current verification? TerminateProver()? Or kill entirely?
- }
-
bool EndOfPayload(out string line) {
line = Console.ReadLine();
return line == null || line == Interaction.CLIENT_EOM_TAG;
diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index d6654ac1..59b3abb9 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,11 @@ namespace Microsoft.Dafny { internal static void ApplyArgs(string[] args) {
Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());
- Dafny.DafnyOptions.O.ProverKillTime = 10;
+ Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden
if (CommandLineOptions.Clo.Parse(args)) {
- // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME
- // Dafny.DafnyOptions.O.ModelViewFile = "-";
DafnyOptions.O.VerifySnapshots = 2; // Use caching
- DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME
+ DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores
DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout
DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs
DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification
|