revert previous change: DROPPING THE GRUNGE HAMMER. :)

diff --git a/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java b/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java
index 79a4414bdf07876bee45ba3c57e7d5d1442b2b80..7211dd9905c95a20e92a404dbb729c993c62914c 100644 (file)
--- a/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java
+++ b/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java
@@ -9,6 +9,14 @@ public class FlatIRGraph {
 
   private State state;
 
+  private BufferedWriter flatbw;
+
+  private HashSet<FlatNode> visited;
+  private HashSet<FlatNode> toVisit;
+
+  private int labelindex;
+  private Hashtable<FlatNode, Integer> flatnodetolabel;
+
   public FlatIRGraph(State state, boolean tasks, boolean usermethods, boolean libmethods) throws java.io.IOException {
     this.state=state;
 
@@ -38,21 +46,7 @@ public class FlatIRGraph {
     }
   }
 
-
-
-  static BufferedWriter flatbw;
-
-  static HashSet<FlatNode> visited;
-  static HashSet<FlatNode> toVisit;
-
-  static int labelindex;
-  static Hashtable<FlatNode, Integer> flatnodetolabel;
-
-  
-  static public void writeFlatIRGraph(FlatMethod fm, String graphname) throws java.io.IOException {
-
-
-
+  private void writeFlatIRGraph(FlatMethod fm, String graphname) throws java.io.IOException {
     // give every node in the flat IR graph a unique label
     // so a human being can inspect the graph and verify
     // correctness
@@ -97,8 +91,7 @@ public class FlatIRGraph {
     flatbw.close();
   }
 
-
-  static private void labelFlatNodes(FlatNode fn) {
+  private void labelFlatNodes(FlatNode fn) {
     visited.add(fn);
     flatnodetolabel.put(fn,new Integer(labelindex++));
     for(int i=0; i<fn.numNext(); i++) {
@@ -109,13 +102,12 @@ public class FlatIRGraph {
     }
   }
 
-
-  static private String makeNodeName(String graphname, Integer id, String type) {
+  private String makeNodeName(String graphname, Integer id, String type) {
     String s = String.format("%05d", id);
     return "FN"+s+"_"+type;
   }
 
-  static private String makeDotNodeDec(String graphname, Integer id, String type, String details) {
+  private String makeDotNodeDec(String graphname, Integer id, String type, String details) {
     if( details == null ) {
       return "  node"+id+"[label=\""+makeNodeName(graphname,id,type)+"\"];\n";
     } else {