diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-31 14:26:53 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-31 14:26:53 -0700 |
| commit | 990966db7dcea00045c5c104ded084348e8f7dde (patch) | |
| tree | b7ba5727c821848354de40c4149633ed9dc5a23d /Source/DafnyServer/Utilities.cs | |
| parent | 48fed349a2fc592e7f015ecaa6cf98582446278f (diff) | |
Split the server source into multiple files
Diffstat (limited to 'Source/DafnyServer/Utilities.cs')
| -rw-r--r-- | Source/DafnyServer/Utilities.cs | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs new file mode 100644 index 00000000..8fb03b05 --- /dev/null +++ b/Source/DafnyServer/Utilities.cs @@ -0,0 +1,60 @@ +using System;
+using System.IO;
+using System.Text;
+using System.Collections.Generic;
+using System.Runtime.Serialization;
+using System.Runtime.Serialization.Json;
+using Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+ class Interaction {
+ internal static string SUCCESS = "SUCCESS";
+ internal static string FAILURE = "FAILURE";
+ internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]";
+ internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]";
+
+ internal static void EOM(string header, string msg) {
+ var trailer = (msg == null) ? "" : "\n";
+ Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG);
+ Console.Out.Flush();
+ }
+
+ internal static void EOM(string header, Exception ex, string subHeader = "") {
+ var aggregate = ex as AggregateException;
+ subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " ";
+
+ if (aggregate == null) {
+ EOM(header, subHeader + ex.Message);
+ } else {
+ EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", "));
+ }
+ }
+ }
+
+ class ServerException : Exception {
+ internal ServerException(string message) : base(message) { }
+ internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { }
+ }
+
+ class ServerUtils {
+ internal static void checkArgs(string[] command, int expectedLength) {
+ if (command.Length - 1 != expectedLength) {
+ throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength);
+ }
+ }
+
+ internal static void ApplyArgs(string[] args) {
+ Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());
+
+ if (CommandLineOptions.Clo.Parse(args)) {
+ // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME
+ // Dafny.DafnyOptions.O.ModelViewFile = "-";
+ Dafny.DafnyOptions.O.ProverKillTime = 10;
+ Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);
+ Dafny.DafnyOptions.O.VerifySnapshots = 2;
+ } else {
+ throw new ServerException("Invalid command line options");
+ }
+ }
+ }
+}
|