diff options
author | Bryan Parno <parno@microsoft.com> | 2015-07-01 11:53:59 -0700 |
---|---|---|
committer | Bryan Parno <parno@microsoft.com> | 2015-07-01 11:53:59 -0700 |
commit | f057d2ec10bdf93bb8ef73cbb3ea80d56159faeb (patch) | |
tree | 6a5614c01600993197394ce049ada2e9999bd50f /Source/Dafny/SccGraph.cs | |
parent | 9e0c60f26bc3c228447154f0d2f9cbeaee9c1974 (diff) |
Add code to calculate various interesting statistics about Dafny files.
Diffstat (limited to 'Source/Dafny/SccGraph.cs')
-rw-r--r-- | Source/Dafny/SccGraph.cs | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs index 01a72fc5..20b4f65e 100644 --- a/Source/Dafny/SccGraph.cs +++ b/Source/Dafny/SccGraph.cs @@ -6,8 +6,8 @@ namespace Microsoft.Dafny { public class Graph<Node> where Node : class
{
- enum VisitedStatus { Unvisited, OnStack, Visited }
- class Vertex {
+ public enum VisitedStatus { Unvisited, OnStack, Visited }
+ public class Vertex {
public readonly Node N;
public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();
public List<Vertex/*!*/> SccMembers; // non-null only for the representative of the SCC
@@ -65,6 +65,10 @@ namespace Microsoft.Dafny { {
}
+ public IEnumerable<Vertex> GetVertices() {
+ return vertices.Values;
+ }
+
/// <summary>
/// Idempotently adds a vertex 'n' to the graph.
/// </summary>
@@ -97,7 +101,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Returns the vertex for 'n' if 'n' is in the graph. Otherwise, returns null.
/// </summary>
- Vertex FindVertex(Node n) {
+ public Vertex FindVertex(Node n) {
Vertex v;
if (vertices.TryGetValue(n, out v)) {
Contract.Assert(v != null); // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!)
|