[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools StateSpaceDot.java,1.1.1.1,1.2

[Masoud Mansouri-S. <mas...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv714/src/gov/nasa/jpf/tools

Modified Files:
	StateSpaceDot.java 
Log Message:
* Fixed a bug which appears when the show_source option is used. The
  Java source line may contain dot-specific special characters. We need
  to precede those (e.g., ']' and '"') with the '\' escape character. There
  seems to be a bug in Java String's replaceAll() method which does not
  allow us to use it so I used the more combersome StringBuffer's replace
  method to do this.


Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- StateSpaceDot.java	26 Apr 2005 19:44:22 -0000	1.1.1.1
+++ StateSpaceDot.java	14 Jun 2005 19:43:08 -0000	1.2
@@ -172,7 +172,42 @@
       String source_line=last_trans_step.getSourceRef().getLineString();
       if ((source_line != null) && !source_line.equals("")) {
         result.append("\\n");
-        result.append(source_line.replaceAll("\\n", ""));
+
+        StringBuffer sb=new StringBuffer(source_line);
+        
+        // We need to precede the dot-specific special characters which appear
+        // in the Java source line, such as ']' and '"', with the '\' escape
+        // characters and also to remove any new lines. There seems to be a bug
+        // in Java String's replaceAll() method which does not allow us to use
+        // it to replace the special chars in the source_line string, so here
+        // I am using StringBuffer's replace method to do this - masoud
+        
+        int indexOfNewLine=0;
+        while (indexOfNewLine!=-1) {
+          indexOfNewLine=sb.indexOf("\\n");
+          if (indexOfNewLine!=-1)
+        	  sb.replace(indexOfNewLine, indexOfNewLine+2, "");
+        }
+        
+        int indexOfBracket=0, lastIndex=0;
+        while (indexOfBracket!=-1) {
+          indexOfBracket=sb.indexOf("]", lastIndex);
+          if (indexOfBracket!=-1) {
+            sb.replace(indexOfBracket, indexOfBracket+1, "\\]");
+            lastIndex=indexOfBracket+2;
+          }
+        }
+        
+        int indexOfQuote=0, lastIndexOfQueote=0;
+        while (indexOfQuote!=-1) {
+          indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
+          if (indexOfQuote!=-1) {
+            sb.replace(indexOfQuote, indexOfQuote+1, "\\\"");
+            lastIndexOfQueote=indexOfQuote+2;
+          }
+        }
+        
+        result.append(sb.toString());
       }
     }