Boogie: Renaming core sources in preparation for port commit

1 files changed, 291 insertions, 0 deletions

diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs
new file mode 100644
index 00000000..e0583793
--- /dev/null
+++ b/Source/Core/Xml.cs
@@ -0,0 +1,291 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.IO;

+using System.Xml;

+using System.Collections.Generic;

+using Microsoft.Contracts;

+using Cci = System.Compiler;

+

+namespace Microsoft.Boogie

+{

+

+  public class XmlSink {

+    string! filename;

+    [Rep] XmlWriter wr;

+    public bool IsOpen {

+      get { return wr != null; }

+    }

+    

+    public XmlSink(string! filename) {

+      this.filename = filename;

+    }

+    

+    /// <summary>

+    /// Returns null on success, in which case the caller should eventually invoke Close.

+    /// Returns an error string on failure.

+    /// </summary>

+    public string Open()

+      modifies this.*;

+      ensures IsOpen;

+    {

+      if (wr != null) {

+        Close();

+      }

+      expose (this) {

+        XmlWriterSettings settings = new XmlWriterSettings();

+        settings.Indent = true;

+        wr = XmlWriter.Create(filename, settings);

+        wr.WriteStartDocument();

+        wr.WriteStartElement("boogie");

+        wr.WriteAttributeString("version", CommandLineOptions.VersionNumber);

+        wr.WriteAttributeString("commandLine", Environment.CommandLine);

+      }

+      return null;  // success

+    }

+    

+    public void Close()

+      modifies this.*;

+    {

+      if (wr != null) {

+        expose (this) {

+          wr.WriteEndDocument();

+          wr.Close();

+          wr = null;

+        }

+      }

+    }

+    

+    const string DateTimeFormatString = "u";

+    

+    public void WriteStartMethod(string! methodName, DateTime startTime)

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteStartElement("method");

+        wr.WriteAttributeString("name", methodName);

+        wr.WriteAttributeString("startTime", startTime.ToString(DateTimeFormatString));

+      }

+    }

+    

+    public void WriteEndMethod(string! outcome, DateTime endTime, TimeSpan elapsed)

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteStartElement("conclusion");

+        wr.WriteAttributeString("endTime", endTime.ToString(DateTimeFormatString));

+        wr.WriteAttributeString("duration", elapsed.TotalSeconds.ToString());

+        wr.WriteAttributeString("outcome", outcome);

+        

+        wr.WriteEndElement();  // outcome

+        wr.WriteEndElement();  // method

+      }

+    }

+    

+    public void WriteError(string! message, IToken! errorToken, IToken relatedToken, BlockSeq trace)

+      requires IsOpen && (trace == null || Owner.Different(this, trace));

+      modifies this.*, errorToken.*, relatedToken.*, trace.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose(this){

+        wr.WriteStartElement("error");

+        wr.WriteAttributeString("message", message);

+        WriteTokenAttributes(errorToken);

+        if (relatedToken != null)

+        {

+          wr.WriteStartElement("related");

+          WriteTokenAttributes(relatedToken);

+          wr.WriteEndElement();

+        }

+        if (trace != null)

+        {

+          wr.WriteStartElement("trace");

+          {

+            foreach (object bo in trace)

+              invariant wr != null;

+            {

+              assume bo is Block;

+              Block b = (Block)bo;

+              wr.WriteStartElement("traceNode");

+              {

+                WriteTokenAttributes(b.tok);

+                wr.WriteAttributeString("label", b.Label);

+              }

+              wr.WriteEndElement();
+            }

+            wr.WriteEndElement();

+          }

+        }

+        wr.WriteEndElement();
+      } 

+    }     

+

+    public void WriteError(string! message, Cci.Node! offendingNode, BlockSeq trace)

+      requires IsOpen && Owner.Different(this, offendingNode);

+      requires trace == null || Owner.Different(this, trace);

+      modifies this.*, offendingNode.*, trace.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose(this){

+        wr.WriteStartElement("error");

+        wr.WriteAttributeString("message", message);

+        WriteTokenAttributes(offendingNode);

+        if (trace != null)

+        {

+          wr.WriteStartElement("trace");

+          {

+            foreach (object bo in trace)

+              invariant wr != null;

+            {

+              assume bo is Block;

+              Block b = (Block)bo;

+              wr.WriteStartElement("traceNode");

+              {

+                this.WriteTokenAttributes(b.tok);

+                wr.WriteAttributeString("label", b.Label);

+              }

+              wr.WriteEndElement();
+            }

+            wr.WriteEndElement();

+          }

+        }

+        wr.WriteEndElement();
+      } 

+    }

+

+    [Inside]

+    private void WriteTokenAttributes(IToken tok) 

+      requires wr != null && wr.IsPeerConsistent;

+      modifies this.0, wr.*;

+    {

+      if (tok != null && tok.filename != null)

+      {

+        wr.WriteAttributeString("file", tok.filename);

+        wr.WriteAttributeString("line", tok.line.ToString());

+        wr.WriteAttributeString("column", tok.col.ToString());

+      }

+    }

+

+    [Inside]

+    private void WriteTokenAttributes(Cci.Node! node) 

+      requires wr != null && wr.IsPeerConsistent;

+      modifies this.0, wr.*;

+    {

+      assert wr != null;

+      if (node.SourceContext.Document != null)

+      {

+        wr.WriteAttributeString("file", node.SourceContext.Document.Name);

+        wr.WriteAttributeString("line", node.SourceContext.StartLine.ToString());

+        wr.WriteAttributeString("column", node.SourceContext.StartColumn.ToString());

+      }

+    }

+    

+    public void WriteStartInference(string! inferenceName)

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteStartElement("inference");

+        wr.WriteAttributeString("name", inferenceName);

+      }

+    }

+    

+    public void WriteEndInference()

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteEndElement();  // inference

+      }

+    }

+    

+    public void WriteContractParaAssignment(string! varName, string val)

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteStartElement("assignment");

+        wr.WriteAttributeString("name", varName);

+        wr.WriteAttributeString("value", val);

+        wr.WriteEndElement();

+      }

+    }

+    

+    public void WriteStartFile(string! filename)

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteStartElement("file");

+        wr.WriteAttributeString("name", filename);

+      }

+    }

+

+    public void WriteEndFile()

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteEndElement();

+      }

+    }

+    

+    public void WriteFileFragment(string! fragment)

+      requires IsOpen;

+      modifies this.*;

+      ensures IsOpen;

+    {

+      assert wr != null;

+      expose (this) {

+        wr.WriteStartElement("fileFragment");

+        wr.WriteAttributeString("name", fragment);

+        wr.WriteEndElement();

+      }

+    }

+  }

+  

+  public class XmlFileScope : IDisposable {

+    [Peer] [SpecPublic] XmlSink sink;

+    

+    [Captured]

+    public XmlFileScope(XmlSink? sink, string! filename)

+      requires sink != null ==> sink.IsOpen;

+      modifies sink.*;

+    {

+      if (sink != null) {

+        sink.WriteStartFile(filename);  // invoke this method while "sink" is still peer consistent

+        Owner.AssignSame(this, sink);

+        this.sink = sink;

+      }

+    }

+    

+    public void Dispose()

+    {

+      if (sink != null) {

+        assume sink.IsOpen;

+        sink.WriteEndFile();

+      }

+    }

+  }

+}