1 files changed, 238 insertions, 238 deletions
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 87b8f3e6..63dca024 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -1,238 +1,238 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Reflection;
-using System.Text;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-namespace Microsoft.Boogie {
-
-  public class ProverOptions {
-    public class OptionException : Exception {
-      public OptionException(string msg)
-        : base(msg) {
-        Contract.Requires(msg != null);
-      }
-    }
-
-    public string/*?*/ LogFilename = null;
-    public bool AppendLogFile = false;
-    public bool SeparateLogFiles = false;
-    // Say (DBG_WAS_VALID) or (DBG_WAS_INVALID) after query
-    public bool ForceLogStatus = false;
-    public int TimeLimit = 0;
-    public int MemoryLimit = 0;
-    public int Verbosity = 0;
-    public string ProverPath;
-
-    private string/*!*/ stringRepr = "";
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(stringRepr != null);
-    }
-
-
-    [Pure]
-    public override string ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      return stringRepr;
-    }
-
-    // The usual thing to override.
-    protected virtual bool Parse(string opt) {
-      Contract.Requires(opt != null);
-      return ParseString(opt, "LOG_FILE", ref LogFilename) ||
-             ParseBool(opt, "APPEND_LOG_FILE", ref AppendLogFile) ||
-             ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) ||
-             ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) ||
-             ParseInt(opt, "VERBOSITY", ref Verbosity) ||
-             ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || 
-             ParseString(opt, "PROVER_PATH", ref ProverPath);
-      // || base.Parse(opt)
-    }
-
-    public virtual string Help
-    {
-      get
-      {
-        return
-@"
-Generic prover options :
-~~~~~~~~~~~~~~~~~~~~~~~
-LOG_FILE=<string>         Log input for the theorem prover. The string @PROC@ in the filename
-                          causes there to be one prover log file per verification condition, 
-                          and is expanded to the name of the procedure that the verification 
-                          condition is for.
-APPEND_LOG_FILE=<bool>    Append, rather than overwrite the log file.
-MEMORY_LIMIT=<int>        Memory limit of the prover in megabytes.
-VERBOSITY=<int>           The higher, the more verbose.
-TIME_LIMIT=<int>          Time limit per verification condition in miliseconds.
-PROVER_PATH=<string>      Path to the prover to use.
-
-The generic options may or may not be used by the prover plugin.
-";
-
-      }
-    }
-
-    public virtual void Parse(IEnumerable<string/*!*/>/*!*/ opts) {
-      Contract.Requires(cce.NonNullElements(opts));
-      StringBuilder sb = new StringBuilder(stringRepr);
-      Contract.Assert(sb != null);
-      foreach (string/*!*/ opt in opts) {
-        Contract.Assert(opt != null);
-        if (!Parse(opt)) {
-          ReportError("Unrecognised prover option: " + opt);
-        }
-        sb.Append(opt).Append(" ");
-      }
-      stringRepr = sb.ToString();
-      PostParse();
-    }
-
-    public virtual void PostParse() {
-      if (LogFilename != null && LogFilename.Contains("@PROC@")) {
-        SeparateLogFiles = true;
-      }
-    }
-
-    protected void ReportError(string msg) {
-      Contract.Requires(msg != null);
-      throw new OptionException(msg + "\n\n" + Help);
-    }
-
-    protected virtual bool ParseString(string opt, string name, ref string field) {
-      Contract.Requires(name != null);
-      Contract.Requires(opt != null);
-      if (opt.Length >= name.Length && opt.StartsWith(name)) {
-        if (opt.Length == name.Length) {
-          field = "";
-          return true;
-        } else if (opt[name.Length] == '=' || opt[name.Length] == ':') {
-          field = opt.Substring(name.Length + 1);
-          return true;
-        }
-      }
-      return false;
-    }
-
-    protected virtual bool ParseBool(string opt, string name, ref bool field) {
-      Contract.Requires(name != null);
-      Contract.Requires(opt != null);
-      string tmp = null;
-      if (ParseString(opt, name, ref tmp))
-        switch (cce.NonNull(tmp).ToLower()) {
-          case "1":
-          case "true":
-          case "":
-            field = true;
-            return true;
-          case "0":
-          case "false":
-            field = false;
-            return true;
-          default:
-            ReportError("Invalid Boolean option \"" + opt + "\"");
-            return false;
-        }
-      return false;
-    }
-
-    protected virtual bool ParseInt(string opt, string name, ref int field) {
-      Contract.Requires(name != null);
-      Contract.Requires(opt != null);
-      string tmp = null;
-      int t2;
-      if (ParseString(opt, name, ref tmp)) {
-        if (int.TryParse(cce.NonNull(tmp), out t2)) {
-          field = t2;
-          return true;
-        } else {
-          ReportError("Invalid integer option \"" + opt + "\"");
-        }
-      }
-      return false;
-    }
-
-    public virtual TextWriter OpenLog(string/*?*/ descName) {
-      if (LogFilename != null) {
-        string filename = LogFilename;
-        Contract.Assert(filename != null);
-        if (descName != null)
-          filename = Helpers.SubstituteAtPROC(descName, filename);
-        return new StreamWriter(filename, AppendLogFile);
-      } else {
-        return null;
-      }
-    }
-  }
-
-  [ContractClass(typeof(ProverFactoryContracts))]
-  public abstract class ProverFactory {
-    // Really returns ProverInterface.
-    //public abstract object! SpawnProver(ProverOptions! options, object! ctxt);
-    public abstract object SpawnProver(ProverOptions options, object ctxt);
-
-    // Really returns ProverContext
-    public abstract object/*!*/ NewProverContext(ProverOptions/*!*/ options);
-
-    public virtual ProverOptions BlankProverOptions() {
-      Contract.Ensures(Contract.Result<ProverOptions>() != null);
-      return new ProverOptions();
-    }
-
-    // return true if the prover supports DAG AST as opposed to LET AST
-    public virtual bool SupportsDags {
-      get {
-        return false;
-      }
-    }
-
-    public virtual CommandLineOptions.VCVariety DefaultVCVariety {
-      get {
-        Contract.Ensures(Contract.Result<CommandLineOptions.VCVariety>() != CommandLineOptions.VCVariety.Unspecified);
-        return CommandLineOptions.VCVariety.DagIterative;
-      }
-    }
-
-    public virtual bool SupportsLabels(ProverOptions options) {
-      return true;
-    }
-
-    public virtual void Close() {
-    }
-
-    public static ProverFactory Load(string proverName) {
-      Contract.Requires(proverName != null);
-      Contract.Ensures(Contract.Result<ProverFactory>() != null);
-      Contract.Ensures(cce.IsNew(Contract.Result<ProverFactory>()) && cce.Owner.New(Contract.Result<ProverFactory>()));
-      string/*!*/ path;
-      if (proverName.IndexOf("/") > 0 || proverName.IndexOf("\\") > 0) {
-        path = proverName;
-      } else {
-        string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(
-                                 cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
-        path = System.IO.Path.Combine(codebase, "Provers." + proverName + ".dll");
-      }
-      Assembly asm = cce.NonNull(Assembly.LoadFrom(path));
-      string name = cce.NonNull(asm.GetName().Name);
-      System.Type factoryType = cce.NonNull(asm.GetType("Microsoft.Boogie." + name.Replace("Provers.", "") + ".Factory"));
-      return cce.NonNull((ProverFactory/*!*/)Activator.CreateInstance(factoryType));
-    }
-  }
-  [ContractClassFor(typeof(ProverFactory))]
-  public abstract class ProverFactoryContracts : ProverFactory {
-    public override object NewProverContext(ProverOptions options) {
-      Contract.Requires(options != null);
-      Contract.Ensures(Contract.Result<object>() != null);
-
-      throw new NotImplementedException();
-    }
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Reflection;
+using System.Text;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+namespace Microsoft.Boogie {
+
+  public class ProverOptions {
+    public class OptionException : Exception {
+      public OptionException(string msg)
+        : base(msg) {
+        Contract.Requires(msg != null);
+      }
+    }
+
+    public string/*?*/ LogFilename = null;
+    public bool AppendLogFile = false;
+    public bool SeparateLogFiles = false;
+    // Say (DBG_WAS_VALID) or (DBG_WAS_INVALID) after query
+    public bool ForceLogStatus = false;
+    public int TimeLimit = 0;
+    public int MemoryLimit = 0;
+    public int Verbosity = 0;
+    public string ProverPath;
+
+    private string/*!*/ stringRepr = "";
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(stringRepr != null);
+    }
+
+
+    [Pure]
+    public override string ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return stringRepr;
+    }
+
+    // The usual thing to override.
+    protected virtual bool Parse(string opt) {
+      Contract.Requires(opt != null);
+      return ParseString(opt, "LOG_FILE", ref LogFilename) ||
+             ParseBool(opt, "APPEND_LOG_FILE", ref AppendLogFile) ||
+             ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) ||
+             ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) ||
+             ParseInt(opt, "VERBOSITY", ref Verbosity) ||
+             ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || 
+             ParseString(opt, "PROVER_PATH", ref ProverPath);
+      // || base.Parse(opt)
+    }
+
+    public virtual string Help
+    {
+      get
+      {
+        return
+@"
+Generic prover options :
+~~~~~~~~~~~~~~~~~~~~~~~
+LOG_FILE=<string>         Log input for the theorem prover. The string @PROC@ in the filename
+                          causes there to be one prover log file per verification condition, 
+                          and is expanded to the name of the procedure that the verification 
+                          condition is for.
+APPEND_LOG_FILE=<bool>    Append, rather than overwrite the log file.
+MEMORY_LIMIT=<int>        Memory limit of the prover in megabytes.
+VERBOSITY=<int>           The higher, the more verbose.
+TIME_LIMIT=<int>          Time limit per verification condition in miliseconds.
+PROVER_PATH=<string>      Path to the prover to use.
+
+The generic options may or may not be used by the prover plugin.
+";
+
+      }
+    }
+
+    public virtual void Parse(IEnumerable<string/*!*/>/*!*/ opts) {
+      Contract.Requires(cce.NonNullElements(opts));
+      StringBuilder sb = new StringBuilder(stringRepr);
+      Contract.Assert(sb != null);
+      foreach (string/*!*/ opt in opts) {
+        Contract.Assert(opt != null);
+        if (!Parse(opt)) {
+          ReportError("Unrecognised prover option: " + opt);
+        }
+        sb.Append(opt).Append(" ");
+      }
+      stringRepr = sb.ToString();
+      PostParse();
+    }
+
+    public virtual void PostParse() {
+      if (LogFilename != null && LogFilename.Contains("@PROC@")) {
+        SeparateLogFiles = true;
+      }
+    }
+
+    protected void ReportError(string msg) {
+      Contract.Requires(msg != null);
+      throw new OptionException(msg + "\n\n" + Help);
+    }
+
+    protected virtual bool ParseString(string opt, string name, ref string field) {
+      Contract.Requires(name != null);
+      Contract.Requires(opt != null);
+      if (opt.Length >= name.Length && opt.StartsWith(name)) {
+        if (opt.Length == name.Length) {
+          field = "";
+          return true;
+        } else if (opt[name.Length] == '=' || opt[name.Length] == ':') {
+          field = opt.Substring(name.Length + 1);
+          return true;
+        }
+      }
+      return false;
+    }
+
+    protected virtual bool ParseBool(string opt, string name, ref bool field) {
+      Contract.Requires(name != null);
+      Contract.Requires(opt != null);
+      string tmp = null;
+      if (ParseString(opt, name, ref tmp))
+        switch (cce.NonNull(tmp).ToLower()) {
+          case "1":
+          case "true":
+          case "":
+            field = true;
+            return true;
+          case "0":
+          case "false":
+            field = false;
+            return true;
+          default:
+            ReportError("Invalid Boolean option \"" + opt + "\"");
+            return false;
+        }
+      return false;
+    }
+
+    protected virtual bool ParseInt(string opt, string name, ref int field) {
+      Contract.Requires(name != null);
+      Contract.Requires(opt != null);
+      string tmp = null;
+      int t2;
+      if (ParseString(opt, name, ref tmp)) {
+        if (int.TryParse(cce.NonNull(tmp), out t2)) {
+          field = t2;
+          return true;
+        } else {
+          ReportError("Invalid integer option \"" + opt + "\"");
+        }
+      }
+      return false;
+    }
+
+    public virtual TextWriter OpenLog(string/*?*/ descName) {
+      if (LogFilename != null) {
+        string filename = LogFilename;
+        Contract.Assert(filename != null);
+        if (descName != null)
+          filename = Helpers.SubstituteAtPROC(descName, filename);
+        return new StreamWriter(filename, AppendLogFile);
+      } else {
+        return null;
+      }
+    }
+  }
+
+  [ContractClass(typeof(ProverFactoryContracts))]
+  public abstract class ProverFactory {
+    // Really returns ProverInterface.
+    //public abstract object! SpawnProver(ProverOptions! options, object! ctxt);
+    public abstract object SpawnProver(ProverOptions options, object ctxt);
+
+    // Really returns ProverContext
+    public abstract object/*!*/ NewProverContext(ProverOptions/*!*/ options);
+
+    public virtual ProverOptions BlankProverOptions() {
+      Contract.Ensures(Contract.Result<ProverOptions>() != null);
+      return new ProverOptions();
+    }
+
+    // return true if the prover supports DAG AST as opposed to LET AST
+    public virtual bool SupportsDags {
+      get {
+        return false;
+      }
+    }
+
+    public virtual CommandLineOptions.VCVariety DefaultVCVariety {
+      get {
+        Contract.Ensures(Contract.Result<CommandLineOptions.VCVariety>() != CommandLineOptions.VCVariety.Unspecified);
+        return CommandLineOptions.VCVariety.DagIterative;
+      }
+    }
+
+    public virtual bool SupportsLabels(ProverOptions options) {
+      return true;
+    }
+
+    public virtual void Close() {
+    }
+
+    public static ProverFactory Load(string proverName) {
+      Contract.Requires(proverName != null);
+      Contract.Ensures(Contract.Result<ProverFactory>() != null);
+      Contract.Ensures(cce.IsNew(Contract.Result<ProverFactory>()) && cce.Owner.New(Contract.Result<ProverFactory>()));
+      string/*!*/ path;
+      if (proverName.IndexOf("/") > 0 || proverName.IndexOf("\\") > 0) {
+        path = proverName;
+      } else {
+        string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(
+                                 cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
+        path = System.IO.Path.Combine(codebase, "Provers." + proverName + ".dll");
+      }
+      Assembly asm = cce.NonNull(Assembly.LoadFrom(path));
+      string name = cce.NonNull(asm.GetName().Name);
+      System.Type factoryType = cce.NonNull(asm.GetType("Microsoft.Boogie." + name.Replace("Provers.", "") + ".Factory"));
+      return cce.NonNull((ProverFactory/*!*/)Activator.CreateInstance(factoryType));
+    }
+  }
+  [ContractClassFor(typeof(ProverFactory))]
+  public abstract class ProverFactoryContracts : ProverFactory {
+    public override object NewProverContext(ProverOptions options) {
+      Contract.Requires(options != null);
+      Contract.Ensures(Contract.Result<object>() != null);
+
+      throw new NotImplementedException();
+    }
+  }
+}