Before writing a dot file, remove all symbols that confuse

the dot syntax from the graph's name.

diff --git a/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java b/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java
index fac5e59b6dab3e1fcdcc87356f840c08ee26dd95..ac816503a60754069266f1438e9034e5fd475c59 100644 (file)
--- a/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java
+++ b/Robust/src/Analysis/FlatIRGraph/FlatIRGraph.java
@@ -55,6 +55,9 @@ public class FlatIRGraph {
        labelindex=0;
        labelFlatNodes( fm );
 
+       // take symbols out of graphname that cause dot to fail
+       graphname = graphname.replaceAll( "[\\W]", "" );
+
        flatbw=new BufferedWriter( new FileWriter( graphname+"_flatIRGraph.dot" ) );
        flatbw.write("digraph "+graphname+" {\n");