Right-clicking on a state allows to display the source code for it

12 files changed, 457 insertions, 19 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 80d2e3c9..7f8e4ae2 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -23,13 +23,11 @@ namespace Microsoft.Boogie.ModelViewer.Base
 

   public class GenericModel : LanguageModel

   {

-    internal Model m;

     List<BaseState> states = new List<BaseState>();

 

     public GenericModel(Model m, ViewOptions opts)

-        : base(opts)

+        : base(m, opts)

     {

-      this.m = m;

       foreach (var s in m.States)

         states.Add(new BaseState(this, s) { Name = s.Name });

       foreach (var s in states)

@@ -69,8 +67,13 @@ namespace Microsoft.Boogie.ModelViewer.Base
         }

       }

 

-      nodes.Add(new ContainerNode<Model.Func>("[Functions]", f => f.Arity == 0 ? null : Function(f), m.m.Functions));

-      nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.m.Functions));

+      nodes.Add(new ContainerNode<Model.Func>("[Functions]", f => f.Arity == 0 ? null : Function(f), m.model.Functions));

+      nodes.Add(new ContainerNode<Model.Func>("[Constants]", f => f.Arity != 0 ? null : new AppNode(this, f.Apps.First()), m.model.Functions));

+    }

+

+    public virtual SourceLocation ShowSource()

+    {

+      return null;

     }

 

     IDisplayNode Function(Model.Func f)

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index bcad3ca5..0a032f06 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -30,7 +30,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

   class DafnyModel : LanguageModel

   {

-    public readonly Model model;

     public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field, f_dtype, f_null;

     public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();

     public readonly Dictionary<Model.Element, Model.FuncTuple> DatatypeValues = new Dictionary<Model.Element, Model.FuncTuple>();

@@ -38,9 +37,8 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
     public List<StateNode> states = new List<StateNode>();

 

     public DafnyModel(Model m, ViewOptions opts)

-      : base(opts)

+      : base(m, opts)

     {

-      model = m;

       f_heap_select = m.MkFunc("[3]", 3);

       f_set_select = m.MkFunc("[2]", 2);

       f_seq_length = m.MkFunc("Seq#Length", 1);

@@ -327,6 +325,11 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       }

     }

 

+    public SourceLocation ShowSource()

+    {

+      return dm.GetSourceLocation(state);

+    }

+

   }

 

   class ElementNode : DisplayNode

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index 57729e4d..807158e2 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -42,9 +42,38 @@ namespace Microsoft.Boogie.ModelViewer
     IEnumerable<string> SortFields(IEnumerable<IDisplayNode> fields);

   }

 

+  public class SourceLocation

+  {

+    public string Header;

+    public string RichTextContent;

+    public int Location;

+

+    public static void RtfAppend(StringBuilder sb, char c, ref int pos)

+    {

+      pos++;

+      switch (c) {

+        case '\r': pos--;  break;

+        case '\\': sb.Append("\\\\"); break;

+        case '\n': sb.Append("\\par\n"); break;

+        case '{': sb.Append("\\{"); break;

+        case '}': sb.Append("\\}"); break;

+        default: sb.Append(c); break;

+      }

+    }

+

+    public static void RtfAppendStateIdx(StringBuilder sb, string label, ref int pos)

+    {

+      label += ".";

+      pos += label.Length;

+      sb.Append(@"{\sub\cf5\highlight4 ").Append(label).Append("}");

+    }

+

+  }

+

   public interface IState

   {

     string Name { get; }

+    SourceLocation ShowSource();

     IEnumerable<IDisplayNode> Nodes { get; }

   }

 

@@ -94,6 +123,13 @@ namespace Microsoft.Boogie.ModelViewer
     {

       get { return children; }

     }

+

+

+    public SourceLocation ShowSource()

+    {

+      return null;

+    }

+

   }

   

   public abstract class DisplayNode : IDisplayNode

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 0449e6b5..44754782 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -49,6 +49,7 @@
       this.columnHeader2 = ((System.Windows.Forms.ColumnHeader)(new System.Windows.Forms.ColumnHeader()));

       this.menuStrip1 = new System.Windows.Forms.MenuStrip();

       this.fileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

+      this.reloadModelFileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.exitToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.viewToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.normalToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

@@ -58,7 +59,8 @@
       this.toolStripMenuItem1 = new System.Windows.Forms.ToolStripSeparator();

       this.debugToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.modelsToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

-      this.reloadModelFileToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

+      this.contextMenuStrip1 = new System.Windows.Forms.ContextMenuStrip(this.components);

+      this.showSourceToolStripMenuItem = new System.Windows.Forms.ToolStripMenuItem();

       this.stateViewMenu.SuspendLayout();

       ((System.ComponentModel.ISupportInitialize)(this.splitContainer1)).BeginInit();

       this.splitContainer1.Panel1.SuspendLayout();

@@ -69,6 +71,7 @@
       this.splitContainer2.Panel2.SuspendLayout();

       this.splitContainer2.SuspendLayout();

       this.menuStrip1.SuspendLayout();

+      this.contextMenuStrip1.SuspendLayout();

       this.SuspendLayout();

       // 

       // currentStateView

@@ -241,6 +244,7 @@
             this.columnHeader3,

             this.columnHeader1,

             this.columnHeader2});

+      this.stateList.ContextMenuStrip = this.contextMenuStrip1;

       this.stateList.Dock = System.Windows.Forms.DockStyle.Fill;

       this.stateList.FullRowSelect = true;

       this.stateList.GridLines = true;

@@ -291,6 +295,13 @@
       this.fileToolStripMenuItem.Size = new System.Drawing.Size(37, 20);

       this.fileToolStripMenuItem.Text = "&File";

       // 

+      // reloadModelFileToolStripMenuItem

+      // 

+      this.reloadModelFileToolStripMenuItem.Name = "reloadModelFileToolStripMenuItem";

+      this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(166, 22);

+      this.reloadModelFileToolStripMenuItem.Text = "&Reload model file";

+      this.reloadModelFileToolStripMenuItem.Click += new System.EventHandler(this.reloadModelFileToolStripMenuItem_Click);

+      // 

       // exitToolStripMenuItem

       // 

       this.exitToolStripMenuItem.Name = "exitToolStripMenuItem";

@@ -359,12 +370,19 @@
       this.modelsToolStripMenuItem.Size = new System.Drawing.Size(58, 20);

       this.modelsToolStripMenuItem.Text = "&Models";

       // 

-      // reloadModelFileToolStripMenuItem

+      // contextMenuStrip1

       // 

-      this.reloadModelFileToolStripMenuItem.Name = "reloadModelFileToolStripMenuItem";

-      this.reloadModelFileToolStripMenuItem.Size = new System.Drawing.Size(166, 22);

-      this.reloadModelFileToolStripMenuItem.Text = "&Reload model file";

-      this.reloadModelFileToolStripMenuItem.Click += new System.EventHandler(this.reloadModelFileToolStripMenuItem_Click);

+      this.contextMenuStrip1.Items.AddRange(new System.Windows.Forms.ToolStripItem[] {

+            this.showSourceToolStripMenuItem});

+      this.contextMenuStrip1.Name = "contextMenuStrip1";

+      this.contextMenuStrip1.Size = new System.Drawing.Size(153, 48);

+      // 

+      // showSourceToolStripMenuItem

+      // 

+      this.showSourceToolStripMenuItem.Name = "showSourceToolStripMenuItem";

+      this.showSourceToolStripMenuItem.Size = new System.Drawing.Size(152, 22);

+      this.showSourceToolStripMenuItem.Text = "Show source";

+      this.showSourceToolStripMenuItem.Click += new System.EventHandler(this.showSourceToolStripMenuItem_Click);

       // 

       // Main

       // 

@@ -388,6 +406,7 @@
       this.splitContainer2.ResumeLayout(false);

       this.menuStrip1.ResumeLayout(false);

       this.menuStrip1.PerformLayout();

+      this.contextMenuStrip1.ResumeLayout(false);

       this.ResumeLayout(false);

       this.PerformLayout();

 

@@ -425,6 +444,8 @@
     private System.Windows.Forms.ToolStripMenuItem modelsToolStripMenuItem;

     private System.Windows.Forms.ToolStripMenuItem includeTheKitchenSinkToolStripMenuItem;

     private System.Windows.Forms.ToolStripMenuItem reloadModelFileToolStripMenuItem;

+    private System.Windows.Forms.ContextMenuStrip contextMenuStrip1;

+    private System.Windows.Forms.ToolStripMenuItem showSourceToolStripMenuItem;

 

 

   }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index c9b574e8..1df48a29 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -621,6 +621,22 @@ namespace Microsoft.Boogie.ModelViewer
       ReadModels();

       LoadModel(modelId);

     }

+

+    private SourceView sourceView;

+    private void showSourceToolStripMenuItem_Click(object sender, EventArgs e)

+    {

+      if (stateList.SelectedItems.Count == 0) return;

+      var li = stateList.SelectedItems[0] as ListViewItem;

+      if (li != null) {

+        var r = ((IState)li.Tag).ShowSource();

+        if (r != null) {

+          if (sourceView == null) {

+            sourceView = new SourceView();

+          }

+          sourceView.SetSourceLocation(r);

+        }        

+      }

+    }

   }

 

   internal class DisplayItem : ListViewItem

diff --git a/Source/ModelViewer/Main.resx b/Source/ModelViewer/Main.resx
index 2a2997d2..3d27240d 100644
--- a/Source/ModelViewer/Main.resx
+++ b/Source/ModelViewer/Main.resx
@@ -120,6 +120,9 @@
   <metadata name="stateViewMenu.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

     <value>17, 17</value>

   </metadata>

+  <metadata name="contextMenuStrip1.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

+    <value>267, 17</value>

+  </metadata>

   <metadata name="menuStrip1.TrayLocation" type="System.Drawing.Point, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">

     <value>152, 17</value>

   </metadata>

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index d374851f..a78894b1 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -82,6 +82,12 @@
     <Compile Include="Namer.cs" />

     <Compile Include="Program.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="SourceView.cs">

+      <SubType>Form</SubType>

+    </Compile>

+    <Compile Include="SourceView.Designer.cs">

+      <DependentUpon>SourceView.cs</DependentUpon>

+    </Compile>

     <Compile Include="TreeSkeleton.cs" />

     <Compile Include="VccProvider.cs" />

     <EmbeddedResource Include="Main.resx">

@@ -97,6 +103,9 @@
       <DependentUpon>Resources.resx</DependentUpon>

       <DesignTime>True</DesignTime>

     </Compile>

+    <EmbeddedResource Include="SourceView.resx">

+      <DependentUpon>SourceView.cs</DependentUpon>

+    </EmbeddedResource>

     <None Include="Properties\Settings.settings">

       <Generator>SettingsSingleFileGenerator</Generator>

       <LastGenOutput>Settings.Designer.cs</LastGenOutput>

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index 01f0e5c6..9191055b 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -18,6 +18,8 @@ namespace Microsoft.Boogie.ModelViewer
     protected Dictionary<Model.Element, string> canonicalName = new Dictionary<Model.Element, string>();

     protected Dictionary<string, Model.Element> invCanonicalName = new Dictionary<string, Model.Element>();

     protected Dictionary<Model.Element, string> localValue = new Dictionary<Model.Element, string>();

+    protected Dictionary<string, SourceLocation> sourceLocations; // initialized lazily by GetSourceLocation()

+    public readonly Model model;

 

     protected virtual bool UseLocalsForCanonicalNames

     {

@@ -25,8 +27,9 @@ namespace Microsoft.Boogie.ModelViewer
     }

 

     public readonly ViewOptions viewOpts;

-    public LanguageModel(ViewOptions opts)

+    public LanguageModel(Model model, ViewOptions opts)

     {

+      this.model = model;

       viewOpts = opts;

     }

     

@@ -226,6 +229,118 @@ namespace Microsoft.Boogie.ModelViewer
       return fields.Select(f => f.Name);

     }

     #endregion

+

+

+

+    #region Displaying source code

+    class Position : IComparable<Position>

+    {

+      public int Line, Column, Index;

+      public int CharPos;

+      public string Name;

+

+      public int CompareTo(Position other)

+      {

+        if (this.Line == other.Line)

+          return this.Column - other.Column;

+        return this.Line - other.Line;

+      }

+    }

+

+    public SourceLocation GetSourceLocation(Model.CapturedState s)

+    {

+      if (sourceLocations == null) {

+        GenerateSourceLocations();

+      }

+

+      SourceLocation res;

+      sourceLocations.TryGetValue(s.Name, out res);

+      return res;

+    }

+

+    protected virtual bool TryParseSourceLocation(string name, out string filename, out int line, out int column)

+    {

+      filename = name;

+      line = 0;

+      column = 0;

+

+      var par = name.LastIndexOf('(');      

+      if (par <= 0) return false;

+

+      filename = name.Substring(0, par);

+      var words = name.Substring(par + 1).Split(',', ')').Where(x => x != "").ToArray();

+      if (words.Length != 2) return false;

+      if (!int.TryParse(words[0], out line) || !int.TryParse(words[1], out column)) return false;

+

+      return true;

+    }

+

+    protected virtual void GenerateSourceLocations()

+    {

+      sourceLocations = new Dictionary<string, SourceLocation>();

+

+      var files = new Dictionary<string, List<Position>>();

+      var sIdx = -1;

+      foreach (var s in model.States) {

+        sIdx++;

+        int line, col;

+        string fn;

+        if (!TryParseSourceLocation(s.Name, out fn, out line, out col))

+          continue;

+

+        List<Position> positions;

+        if (!files.TryGetValue(fn, out positions)) {

+          positions = new List<Position>();

+          files[fn] = positions;

+        }

+        positions.Add(new Position() { Name = s.Name, Line = line, Column = col, Index = sIdx });

+      }

+

+      foreach (var kv in files) {

+        var positions = kv.Value;

+        positions.Sort();

+

+        string content = "";

+        try {

+          content = System.IO.File.ReadAllText(kv.Key);

+        } catch {

+          continue;

+        }

+

+        var currPosIdx = 0;

+        var currLine = 1;

+        var currColumn = 1;

+        var output = new StringBuilder();

+        var charPos = 0;

+

+        foreach (var c in content) {

+          if (c == '\n') {

+            currColumn = int.MaxValue; // flush remaining positions in this line

+          }

+

+          while (currPosIdx < positions.Count && positions[currPosIdx].Line <= currLine && positions[currPosIdx].Column <= currColumn) {

+            positions[currPosIdx].CharPos = charPos;

+            SourceLocation.RtfAppendStateIdx(output, positions[currPosIdx].Index.ToString(), ref charPos);

+            currPosIdx++;

+          }

+

+          SourceLocation.RtfAppend(output, c, ref charPos);

+

+          if (c == '\n') {

+            currLine++;

+            currColumn = 1;

+          } else {

+            currColumn++;

+          }

+        }

+

+        var resStr = output.ToString();

+        foreach (var pos in positions) {

+          sourceLocations[pos.Name] = new SourceLocation() { Header = pos.Name, Location = pos.CharPos, RichTextContent = resStr };

+        }

+      }

+    }

+    #endregion

   }

 

   public class EdgeName

diff --git a/Source/ModelViewer/SourceView.Designer.cs b/Source/ModelViewer/SourceView.Designer.cs
new file mode 100644
index 00000000..55ca2e37
--- /dev/null
+++ b/Source/ModelViewer/SourceView.Designer.cs
@@ -0,0 +1,63 @@
+namespace Microsoft.Boogie.ModelViewer

+{

+  partial class SourceView

+  {

+    /// <summary>

+    /// Required designer variable.

+    /// </summary>

+    private System.ComponentModel.IContainer components = null;

+

+    /// <summary>

+    /// Clean up any resources being used.

+    /// </summary>

+    /// <param name="disposing">true if managed resources should be disposed; otherwise, false.</param>

+    protected override void Dispose(bool disposing)

+    {

+      if (disposing && (components != null)) {

+        components.Dispose();

+      }

+      base.Dispose(disposing);

+    }

+

+    #region Windows Form Designer generated code

+

+    /// <summary>

+    /// Required method for Designer support - do not modify

+    /// the contents of this method with the code editor.

+    /// </summary>

+    private void InitializeComponent()

+    {

+      this.richTextBox1 = new System.Windows.Forms.RichTextBox();

+      this.SuspendLayout();

+      // 

+      // richTextBox1

+      // 

+      this.richTextBox1.DetectUrls = false;

+      this.richTextBox1.Dock = System.Windows.Forms.DockStyle.Fill;

+      this.richTextBox1.Font = new System.Drawing.Font("Lucida Sans Typewriter", 8.25F, System.Drawing.FontStyle.Regular, System.Drawing.GraphicsUnit.Point, ((byte)(0)));

+      this.richTextBox1.HideSelection = false;

+      this.richTextBox1.Location = new System.Drawing.Point(0, 0);

+      this.richTextBox1.Name = "richTextBox1";

+      this.richTextBox1.ReadOnly = true;

+      this.richTextBox1.Size = new System.Drawing.Size(715, 582);

+      this.richTextBox1.TabIndex = 0;

+      this.richTextBox1.Text = "#include <vcc.h>\n\nint main()\n{\n\\foo\n}";

+      this.richTextBox1.WordWrap = false;

+      // 

+      // SourceView

+      // 

+      this.AutoScaleDimensions = new System.Drawing.SizeF(6F, 13F);

+      this.AutoScaleMode = System.Windows.Forms.AutoScaleMode.Font;

+      this.ClientSize = new System.Drawing.Size(715, 582);

+      this.Controls.Add(this.richTextBox1);

+      this.Name = "SourceView";

+      this.Text = "SourceView";

+      this.ResumeLayout(false);

+

+    }

+

+    #endregion

+

+    private System.Windows.Forms.RichTextBox richTextBox1;

+  }

+}
\ No newline at end of file
diff --git a/Source/ModelViewer/SourceView.cs b/Source/ModelViewer/SourceView.cs
new file mode 100644
index 00000000..94694260
--- /dev/null
+++ b/Source/ModelViewer/SourceView.cs
@@ -0,0 +1,46 @@
+using System;

+using System.Collections.Generic;

+using System.ComponentModel;

+using System.Data;

+using System.Drawing;

+using System.Linq;

+using System.Text;

+using System.Windows.Forms;

+

+namespace Microsoft.Boogie.ModelViewer

+{

+  public partial class SourceView : Form

+  {

+    public SourceView()

+    {

+      InitializeComponent();

+    }

+

+    string prevRtf;

+

+    string prefix =

+        @"{\rtf1\ansi\ansicpg1252\deff0\deflang1033{\fonttbl{\f0\fnil\fcharset0 Lucida Sans Typewriter;}}\r\n" +

+        @"{\colortbl;\red0\green0\blue0;\red255\green0\blue0;\red0\green255\blue0;\red0\green0\blue255;\red255\green255\blue255;}" +

+        @"\viewkind4\uc1\pard\f0\fs17 ";

+

+    internal void SetSourceLocation(SourceLocation r)

+    {      

+      if (r.RichTextContent != prevRtf) {

+        richTextBox1.Rtf = prefix + r.RichTextContent + "\r\n}\r\n";

+        prevRtf = r.RichTextContent;

+      }

+

+      richTextBox1.Select(r.Location, 6);

+

+      this.Text = r.Header;      

+      this.Show();

+    }

+

+    protected override void OnClosing(CancelEventArgs e)

+    {

+      base.OnClosing(e);

+      e.Cancel = true;

+      Hide();

+    }

+  }

+}

diff --git a/Source/ModelViewer/SourceView.resx b/Source/ModelViewer/SourceView.resx
new file mode 100644
index 00000000..29dcb1b3
--- /dev/null
+++ b/Source/ModelViewer/SourceView.resx
@@ -0,0 +1,120 @@
+<?xml version="1.0" encoding="utf-8"?>

+<root>

+  <!-- 

+    Microsoft ResX Schema 

+    

+    Version 2.0

+    

+    The primary goals of this format is to allow a simple XML format 

+    that is mostly human readable. The generation and parsing of the 

+    various data types are done through the TypeConverter classes 

+    associated with the data types.

+    

+    Example:

+    

+    ... ado.net/XML headers & schema ...

+    <resheader name="resmimetype">text/microsoft-resx</resheader>

+    <resheader name="version">2.0</resheader>

+    <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>

+    <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>

+    <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>

+    <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>

+    <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">

+        <value>[base64 mime encoded serialized .NET Framework object]</value>

+    </data>

+    <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">

+        <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>

+        <comment>This is a comment</comment>

+    </data>

+                

+    There are any number of "resheader" rows that contain simple 

+    name/value pairs.

+    

+    Each data row contains a name, and value. The row also contains a 

+    type or mimetype. Type corresponds to a .NET class that support 

+    text/value conversion through the TypeConverter architecture. 

+    Classes that don't support this are serialized and stored with the 

+    mimetype set.

+    

+    The mimetype is used for serialized objects, and tells the 

+    ResXResourceReader how to depersist the object. This is currently not 

+    extensible. For a given mimetype the value must be set accordingly:

+    

+    Note - application/x-microsoft.net.object.binary.base64 is the format 

+    that the ResXResourceWriter will generate, however the reader can 

+    read any of the formats listed below.

+    

+    mimetype: application/x-microsoft.net.object.binary.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter

+            : and then encoded with base64 encoding.

+    

+    mimetype: application/x-microsoft.net.object.soap.base64

+    value   : The object must be serialized with 

+            : System.Runtime.Serialization.Formatters.Soap.SoapFormatter

+            : and then encoded with base64 encoding.

+

+    mimetype: application/x-microsoft.net.object.bytearray.base64

+    value   : The object must be serialized into a byte array 

+            : using a System.ComponentModel.TypeConverter

+            : and then encoded with base64 encoding.

+    -->

+  <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">

+    <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />

+    <xsd:element name="root" msdata:IsDataSet="true">

+      <xsd:complexType>

+        <xsd:choice maxOccurs="unbounded">

+          <xsd:element name="metadata">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" />

+              </xsd:sequence>

+              <xsd:attribute name="name" use="required" type="xsd:string" />

+              <xsd:attribute name="type" type="xsd:string" />

+              <xsd:attribute name="mimetype" type="xsd:string" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="assembly">

+            <xsd:complexType>

+              <xsd:attribute name="alias" type="xsd:string" />

+              <xsd:attribute name="name" type="xsd:string" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="data">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+                <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />

+              <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />

+              <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />

+              <xsd:attribute ref="xml:space" />

+            </xsd:complexType>

+          </xsd:element>

+          <xsd:element name="resheader">

+            <xsd:complexType>

+              <xsd:sequence>

+                <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />

+              </xsd:sequence>

+              <xsd:attribute name="name" type="xsd:string" use="required" />

+            </xsd:complexType>

+          </xsd:element>

+        </xsd:choice>

+      </xsd:complexType>

+    </xsd:element>

+  </xsd:schema>

+  <resheader name="resmimetype">

+    <value>text/microsoft-resx</value>

+  </resheader>

+  <resheader name="version">

+    <value>2.0</value>

+  </resheader>

+  <resheader name="reader">

+    <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+  <resheader name="writer">

+    <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>

+  </resheader>

+</root>
\ No newline at end of file
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 91a76d72..58395385 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -34,7 +34,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

   class VccModel : LanguageModel

   {

-    public readonly Model model;

     public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,

                                f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t, f_select_ptr,

                                f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,

@@ -49,9 +48,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();

 

     public VccModel(Model m, ViewOptions opts)

-      : base(opts)

+      : base(m, opts)

     {

-      model = m;

       f_ptr_to = m.MkFunc("$ptr_to", 1);

       f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);

       f_phys_ptr_cast = m.MkFunc("$phys_ptr_cast", 2);

@@ -931,7 +929,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     internal VccModel vm;

     internal List<VariableNode> vars;

     internal List<ElementNode> commons;

-    internal int index;

+    internal int index;    

     

     public StateNode(int i, VccModel parent, Model.CapturedState s)

     {

@@ -990,6 +988,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       }

     }

 

+    public SourceLocation ShowSource()

+    {

+      return vm.GetSourceLocation(state);

+    }

+

   }

 

   class ElementNode : DisplayNode