001 package escjava.vcGeneration;
002
003 import javafe.ast.*;
004 import javafe.tc.*;
005 import javafe.util.*;
006 import escjava.ast.*;
007 import escjava.translate.*;
008 import escjava.ast.TagConstants;
009 import escjava.prover.Atom;
010
011 import java.io.*;
012
013 public class VcGenerator {
014
015 /**
016 * README :
017 *
018 * This class is an interface to the vc generation suite
019 * (this is done this way to be able to put all the other classes in a new package.)
020 *
021 * Usage :
022 * You have to supply the root node of the vc tree you want to translate.
023 * Then you can call any of the public finction to get what you want.
024 * It has been designed in a way that makes sure we won't do the work
025 * two times. I.e., if you call the constructor and never call old2Dot(),
026 * we never compute the dot file.
027 * Most of the time (ie except for development and debugging), you have
028 * to do :
029 * 1/ vcg = new VcGenerator(p,e,..); // p is the prover type and e is the root node of the vc tree
030 * 2/ vcg.getProof(vc); // return, as a string, proof script for the given vc
031 */
032
033 private/*@ spec_public @*/ProverType prover = null;
034
035 private/*@ spec_public non_null @*/ASTNode oldRootNode = null;
036
037 private/*@ spec_public non_null @*/TNode newRootNode = null;
038
039 private/*@ spec_public @*/StringBuffer oldDot = null;
040
041 private/*@ spec_public @*/boolean computationDone = false;
042
043 /*@
044 @ public invariant computationDone ==> newRootNode != null &&
045 @ (newRootNode != null ==> (newRootNode instanceof TRoot));
046 @*/
047
048 /**
049 * @param e the root node of the gc tree.
050 *
051 * @return The VcGenerator on which you can call method to get
052 * vcs for different syntax
053 */
054 public VcGenerator(/*@ non_null @*/ProverType p, /*@ non_null @*/ASTNode e, boolean err, boolean warn, boolean info, boolean colors) {
055 prover = p;
056 oldRootNode = e;
057
058 /*
059 * Set different output (or not);
060 */
061 TDisplay.init(err, warn, info, colors);
062
063 /*
064 * Reset static initialization for TNode.
065 */
066 TNode.init(prover);
067 }
068
069 public void getProof(Writer out, String proofName) throws IOException {
070
071 if (!computationDone) {
072 generateIfpTree(oldRootNode, false);
073 newRootNode.typeTree();
074 }
075
076 newRootNode = prover.rewrite(newRootNode);
077
078 prover.getProof(out, proofName, newRootNode);
079 }
080
081 /*@
082 @ ensures computationDone && oldDot != null;
083 @*/
084 public String old2Dot() {
085 if (oldDot == null) {
086
087 /* call to the fonction that does the job,
088 indicating with the second parameter that we want the
089 dot representation as well */
090 generateIfpTree(oldRootNode, true);
091
092 computationDone = true;
093 }
094
095 return oldDot.toString();
096 }
097
098 /*@
099 @ ensures computationDone;
100 @*/
101 public String toDot() throws IOException {
102 if (!computationDone)
103 generateIfpTree(oldRootNode, false);
104
105 TDotVisitor v = new TDotVisitor();
106
107 newRootNode.accept(v);
108
109 return v.out.toString();
110 }
111
112 /**
113 * This attribute is used by the next function to save the current parent of the node
114 * we may create. Before any call to generateIfpTree, and after the last call has returned
115 * this field is always null. This is bizarre, but avoids to add a parameter to this function
116 * and makes the code more concise.
117 */
118 private TFunction currentParent = null;
119
120 // boolean to skip first not
121 // Clement's experiment
122 private boolean firstNotSkipped = true;
123
124 /**
125 * The main goal of this method is to translate the
126 * gc tree (which is still independant from simplify) to a new tree
127 * (classes of this new tree are in escjava/vcGeneration which is, by far,
128 * easier to manipulate that the one which is given here (parameter e).
129 *
130 * The code is divided in this way :
131 *
132 * 1/ declarations
133 * 2/ switch on the type of the node currently looked at
134 * 3/ a/ depending on the type, create a new node for the translation of the tree
135 * b/ if dot output is asked (ie parameter dot != null), do the job
136 *
137 * 4/ call the method on the sons of the current node.
138 *
139 * @param p the node (of the old tree) you're visiting.
140 * @param dot if true, generate the dot representation of the old tree.
141 */
142 private void generateIfpTree(/*@ non_null @*/ASTNode n, boolean dot) {
143
144 // declarations & instancations
145 int nbChilds = n.childCount();
146 Object o = null;
147
148 ASTNode nodeTemp = null;
149 boolean outputDot = false;
150 StringBuffer name = null;
151
152 if (oldDot == null)
153 oldDot = new StringBuffer();
154
155 TFunction saveParent = currentParent;
156
157 /* happen at first call */
158 if (currentParent == null)
159 currentParent = new TRoot();
160 // /declarations & instancations
161
162 if (dot) {
163 name = new StringBuffer(getNameASTNode(n));
164 name.append(n.dotId);
165
166 /* declaration of the node in dot */
167 oldDot.append(name);
168 /* label = "xxxx" <- notice the " */
169 oldDot.append(" [label = \"" + getNameASTNode(n));
170 }
171
172 // if(e.getStartLoc() != Location.NULL)
173 // dot.append(" "+e.getStartLoc()+"|"+e.getEndLoc());
174
175 // all types checked are in alphabetical order
176 if (n instanceof ArrayType) {
177
178 ArrayType m = (ArrayType) n;
179 // this represents a type
180
181 String s = m.toString();
182
183 TDisplay.err(this, "generateIfpTree", s);
184
185 // TName newNode = new TName(s);
186 // // we put it as a variable name with type %Type
187 // TNode.addName(s, "%Type");
188
189 // // we put as a type too
190 // TNode.addType(s);
191
192 // currentParent.addSon(newNode);
193
194 if (dot)
195 // fixme, not precise enough maybe
196 oldDot.append("\\n" + s + "\"");
197 } else if (n instanceof LiteralExpr) {
198 LiteralExpr m = (LiteralExpr) n;
199
200 switch (m.getTag()) {
201 case TagConstants.STRINGLIT: {
202 TString newNode = new TString(null);
203 currentParent.addSon(newNode);
204 break;
205 }
206 case TagConstants.BOOLEANLIT: {
207 TBoolean newNode = null;
208
209 if (((Boolean) m.value).booleanValue())
210 newNode = new TBoolean(true);
211 else
212 newNode = new TBoolean(false);
213
214 currentParent.addSon(newNode);
215 break;
216 }
217 case TagConstants.CHARLIT: {
218 TChar newNode = new TChar(((Integer) m.value).intValue());
219 currentParent.addSon(newNode);
220 break;
221 }
222 case TagConstants.INTLIT: {
223 TInt newNode = new TInt(((Integer) m.value).intValue());
224 currentParent.addSon(newNode);
225 break;
226 }
227 case TagConstants.FLOATLIT: {
228 TFloat newNode = new TFloat(((Float) m.value).floatValue());
229 currentParent.addSon(newNode);
230 break;
231 }
232 case TagConstants.DOUBLELIT: {
233 TDouble newNode = new TDouble(((Double) m.value).doubleValue());
234 currentParent.addSon(newNode);
235 break;
236 }
237 case TagConstants.NULLLIT: {
238 TNull newNode = new TNull();
239 currentParent.addSon(newNode);
240 break;
241 }
242 case TagConstants.SYMBOLLIT: {
243 //error.println("SYMBOLLIT "+(String)m.value );
244
245 // pass here for ecReturn and ecThrow
246 String s = (String) m.value;
247
248 // fixme am I right ?
249 TName newNode = new TName(s);
250 TNode.addName(s, null);
251 currentParent.addSon(newNode);
252 break;
253 }
254 default:
255 TDisplay.err(this, "generateIfpTree",
256 "Instanceof LiteralExpr, case missed :"
257 + TagConstants.toString(m.getTag()));
258 break;
259 }
260
261 if (dot)
262 oldDot.append("\\n" + TagConstants.toString(m.getTag()) + "\"");
263 }
264 // name of a method
265 else if (n instanceof NaryExpr) {
266 NaryExpr m = (NaryExpr) n;
267
268 String methodName = TagConstants.toString(m.getTag());
269
270 switch (m.getTag()) {
271 // boolean operations
272 case TagConstants.BOOLIMPLIES: {
273 TBoolImplies newNode = new TBoolImplies();
274 currentParent.addSon(newNode);
275 currentParent = newNode;
276 break;
277 }
278 case TagConstants.BOOLAND:
279 case TagConstants.BOOLANDX: {
280 TBoolAnd newNode = new TBoolAnd();
281 currentParent.addSon(newNode);
282 currentParent = newNode;
283 break;
284 }
285 case TagConstants.BOOLOR: {
286 TBoolOr newNode = new TBoolOr();
287 currentParent.addSon(newNode);
288 currentParent = newNode;
289 break;
290 }
291 case TagConstants.BOOLNOT: {
292 //FIXME: I am sorry Clement but I can't prove anything with
293 // your experiment...
294 if (firstNotSkipped) {
295 TBoolNot newNode = new TBoolNot();
296 currentParent.addSon(newNode);
297 currentParent = newNode;
298 } else
299 firstNotSkipped = true;
300
301 break;
302 }
303 case TagConstants.BOOLEQ: {
304 TBoolEQ newNode = new TBoolEQ();
305 currentParent.addSon(newNode);
306 currentParent = newNode;
307 break;
308 }
309 case TagConstants.BOOLNE: {
310 TBoolNE newNode = new TBoolNE();
311 currentParent.addSon(newNode);
312 currentParent = newNode;
313 break;
314 }
315 case TagConstants.METHODCALL: {
316 // FIXME I think it is fixed... needs further testing
317 //TDisplay.err(this, "generateIfpTree", TagConstants.toString(m.getTag()));
318 TMethodCall newNode = new TMethodCall(m.methodName.toString());
319 currentParent.addSon(newNode);
320 currentParent = newNode;
321 break;
322 }
323 // allocation comparisons
324 case TagConstants.ALLOCLT: {
325 TAllocLT newNode = new TAllocLT();
326 currentParent.addSon(newNode);
327 currentParent = newNode;
328 break;
329 }
330 case TagConstants.ALLOCLE: {
331 TAllocLE newNode = new TAllocLE();
332 currentParent.addSon(newNode);
333 currentParent = newNode;
334 break;
335 }
336
337 // references
338 case TagConstants.ANYEQ: {
339 TAnyEQ newNode = new TAnyEQ();
340 currentParent.addSon(newNode);
341 currentParent = newNode;
342 break;
343 }
344 case TagConstants.ANYNE: {
345 TAnyNE newNode = new TAnyNE();
346 currentParent.addSon(newNode);
347 currentParent = newNode;
348 break;
349 }
350
351 // integral comparisons
352 case TagConstants.INTEGRALEQ: {
353 TIntegralEQ newNode = new TIntegralEQ();
354 currentParent.addSon(newNode);
355 currentParent = newNode;
356 break;
357 }
358 case TagConstants.INTEGRALGE: {
359 TIntegralGE newNode = new TIntegralGE();
360 currentParent.addSon(newNode);
361 currentParent = newNode;
362 break;
363 }
364 case TagConstants.INTEGRALGT: {
365 TIntegralGT newNode = new TIntegralGT();
366 currentParent.addSon(newNode);
367 currentParent = newNode;
368 break;
369 }
370 case TagConstants.INTEGRALLE: {
371 TIntegralLE newNode = new TIntegralLE();
372 currentParent.addSon(newNode);
373 currentParent = newNode;
374 break;
375 }
376 case TagConstants.INTEGRALLT: {
377 TIntegralLT newNode = new TIntegralLT();
378 currentParent.addSon(newNode);
379 currentParent = newNode;
380 break;
381 }
382 case TagConstants.INTEGRALNE: {
383 TIntegralNE newNode = new TIntegralNE();
384 currentParent.addSon(newNode);
385 currentParent = newNode;
386 break;
387 } // integral operation // fixme some missing
388 case TagConstants.INTEGRALADD: {
389 TIntegralAdd newNode = new TIntegralAdd();
390 currentParent.addSon(newNode);
391 currentParent = newNode;
392 break;
393 }
394 case TagConstants.INTEGRALDIV: {
395 TIntegralDiv newNode = new TIntegralDiv();
396 currentParent.addSon(newNode);
397 currentParent = newNode;
398 break;
399 }
400 case TagConstants.INTEGRALMOD: {
401 TIntegralMod newNode = new TIntegralMod();
402 currentParent.addSon(newNode);
403 currentParent = newNode;
404 break;
405 }
406 case TagConstants.INTEGRALMUL: {
407 TIntegralMul newNode = new TIntegralMul();
408 currentParent.addSon(newNode);
409 currentParent = newNode;
410 break;
411 }
412 case TagConstants.INTEGRALSUB: {
413 TIntegralSub newNode = new TIntegralSub();
414 currentParent.addSon(newNode);
415 currentParent = newNode;
416 break;
417 }
418 // real comparisons
419 case TagConstants.FLOATINGEQ: {
420 TFloatEQ newNode = new TFloatEQ();
421 currentParent.addSon(newNode);
422 currentParent = newNode;
423 break;
424 }
425 case TagConstants.FLOATINGGE: {
426 TFloatGE newNode = new TFloatGE();
427 currentParent.addSon(newNode);
428 currentParent = newNode;
429 break;
430 }
431 case TagConstants.FLOATINGGT: {
432 TFloatGT newNode = new TFloatGT();
433 currentParent.addSon(newNode);
434 currentParent = newNode;
435 break;
436 }
437 case TagConstants.FLOATINGLE: {
438 TFloatLE newNode = new TFloatLE();
439 currentParent.addSon(newNode);
440 currentParent = newNode;
441 break;
442 }
443 case TagConstants.FLOATINGLT: {
444 TFloatLT newNode = new TFloatLT();
445 currentParent.addSon(newNode);
446 currentParent = newNode;
447 break;
448 }
449 case TagConstants.FLOATINGNE: {
450 TFloatNE newNode = new TFloatNE();
451 currentParent.addSon(newNode);
452 currentParent = newNode;
453 break;
454 }
455 // integral operation // fixme some missing
456 case TagConstants.FLOATINGADD: {
457 TFloatAdd newNode = new TFloatAdd();
458 currentParent.addSon(newNode);
459 currentParent = newNode;
460 break;
461 }
462 case TagConstants.FLOATINGDIV: {
463 TFloatDiv newNode = new TFloatDiv();
464 currentParent.addSon(newNode);
465 currentParent = newNode;
466 break;
467 }
468 case TagConstants.FLOATINGMOD: {
469 TFloatMod newNode = new TFloatMod();
470 currentParent.addSon(newNode);
471 currentParent = newNode;
472 break;
473 }
474 case TagConstants.FLOATINGMUL: {
475 TFloatMul newNode = new TFloatMul();
476 currentParent.addSon(newNode);
477 currentParent = newNode;
478 break;
479 }
480 // lock comparisons
481 case TagConstants.LOCKLE: {
482 TLockLE newNode = new TLockLE();
483 currentParent.addSon(newNode);
484 currentParent = newNode;
485 break;
486 }
487 case TagConstants.LOCKLT: {
488 TLockLT newNode = new TLockLT();
489 currentParent.addSon(newNode);
490 currentParent = newNode;
491 break;
492 } // reference comparisons
493 case TagConstants.REFEQ: {
494 TRefEQ newNode = new TRefEQ();
495 currentParent.addSon(newNode);
496 currentParent = newNode;
497 break;
498 }
499 case TagConstants.REFNE: {
500 TRefNE newNode = new TRefNE();
501 currentParent.addSon(newNode);
502 currentParent = newNode;
503 break;
504 } // type comparison
505 case TagConstants.TYPEEQ: {
506 TTypeEQ newNode = new TTypeEQ();
507 currentParent.addSon(newNode);
508 currentParent = newNode;
509 break;
510 }
511 case TagConstants.TYPENE: {
512 TTypeNE newNode = new TTypeNE();
513 currentParent.addSon(newNode);
514 currentParent = newNode;
515 break;
516 }
517 case TagConstants.TYPELE: {
518 TTypeLE newNode = new TTypeLE();
519 currentParent.addSon(newNode);
520 currentParent = newNode;
521 break;
522 } // usual functions, cast is select store typeof
523 case TagConstants.CAST: {
524 TCast newNode = new TCast();
525 currentParent.addSon(newNode);
526 currentParent = newNode;
527 break;
528 }
529 case TagConstants.IS: {
530 TIs newNode = new TIs();
531 currentParent.addSon(newNode);
532 currentParent = newNode;
533 break;
534 }
535 case TagConstants.SELECT: {
536 TSelect newNode = new TSelect();
537 currentParent.addSon(newNode);
538 currentParent = newNode;
539 break;
540 }
541 case TagConstants.STORE: {
542 TStore newNode = new TStore();
543 currentParent.addSon(newNode);
544 currentParent = newNode;
545 break;
546 }
547 case TagConstants.UNSET: {
548 TUnset newNode = new TUnset();
549 currentParent.addSon(newNode);
550 currentParent = newNode;
551 break;
552 }
553 case TagConstants.TYPEOF: {
554 TTypeOf newNode = new TTypeOf();
555 currentParent.addSon(newNode);
556 currentParent = newNode;
557 break;
558 }
559 // allocation
560 case TagConstants.ISALLOCATED: {
561 TIsAllocated newNode = new TIsAllocated();
562 currentParent.addSon(newNode);
563 currentParent = newNode;
564 break;
565 }
566 case TagConstants.ECLOSEDTIME: {
567 TEClosedTime newNode = new TEClosedTime();
568 currentParent.addSon(newNode);
569 currentParent = newNode;
570 break;
571 }
572 case TagConstants.FCLOSEDTIME: {
573 TFClosedTime newNode = new TFClosedTime();
574 currentParent.addSon(newNode);
575 currentParent = newNode;
576 break;
577 } // as trick : asElems asField asLockset
578 case TagConstants.ASELEMS: {
579 TAsElems newNode = new TAsElems();
580 currentParent.addSon(newNode);
581 currentParent = newNode;
582 break;
583 }
584 case TagConstants.SUM: {
585 TSum newNode = new TSum();
586 currentParent.addSon(newNode);
587 currentParent = newNode;
588 }
589 case TagConstants.ASFIELD: {
590 TAsField newNode = new TAsField();
591 currentParent.addSon(newNode);
592 currentParent = newNode;
593 break;
594 }
595 case TagConstants.ASLOCKSET: {
596 TAsLockSet newNode = new TAsLockSet();
597 currentParent.addSon(newNode);
598 currentParent = newNode;
599 break;
600 } // array
601 case TagConstants.ARRAYFRESH: {
602 TArrayFresh newNode = new TArrayFresh();
603 currentParent.addSon(newNode);
604 currentParent = newNode;
605 break;
606 }
607 case TagConstants.ARRAYSHAPEONE: {
608 TArrayShapeOne newNode = new TArrayShapeOne();
609 currentParent.addSon(newNode);
610 currentParent = newNode;
611 break;
612 }
613 case TagConstants.ARRAYSHAPEMORE: {
614 TArrayShapeMore newNode = new TArrayShapeMore();
615 currentParent.addSon(newNode);
616 currentParent = newNode;
617 break;
618 }
619 case TagConstants.ISNEWARRAY: {
620 TIsNewArray newNode = new TIsNewArray();
621 currentParent.addSon(newNode);
622 currentParent = newNode;
623 break;
624 }
625 case TagConstants.ARRAYLENGTH: {
626 TArrayLength newNode = new TArrayLength();
627 currentParent.addSon(newNode);
628 currentParent = newNode;
629 break;
630 }
631 default:
632 TDisplay.err(this, "generateIfpTree",
633 "translating old gc tree, methodName not recognized "
634 + methodName);
635 }
636
637 if (dot)
638 /* fixme maybe this call can return "?" which means
639 * the name of the function isn't in the original tree
640 */
641 oldDot.append("\\n" + TagConstants.toString(m.getTag()) + "\"");
642
643 } else if (n instanceof PrimitiveType) { // javafe/Type
644 PrimitiveType m = (PrimitiveType) n;
645 String s = javafe.ast.TagConstants.toString(m.getTag());
646
647 // this means this variable represent a type like
648 // Java.x.Vector or Java.lang.Object etc...
649 TName newNode = new TName(s);
650 TNode.addName(s, "%Type");
651
652 currentParent.addSon(newNode);
653
654 if (dot)
655 oldDot.append("\\n" + s + "\"");
656
657 } else if (n instanceof QuantifiedExpr) {
658 QuantifiedExpr m = (QuantifiedExpr) n;
659 String s = TagConstants.toString(m.getTag());
660
661 if (s.equals("\\forall")) {
662 TForAll newNode = new TForAll();
663 currentParent.addSon(newNode);
664 currentParent = newNode;
665 } else if (s.equals("\\exist")) {
666 TExist newNode = new TExist();
667 currentParent.addSon(newNode);
668 currentParent = newNode;
669 } else
670 TDisplay.err(this, "generateIfpTree",
671 "QuantifiedExpr, unhandled tag : " + s);
672
673 if (dot)
674 oldDot.append("\\n" + s + "\"");
675
676 } else if (n instanceof SimpleName) {
677 SimpleName m = (SimpleName) n;
678
679 // it seems that this node is under a TypeName node all the time
680 // and that all the information is in the TypeName node.
681 // that's why we don't create a new node here.
682
683 if (dot)
684 oldDot.append("\\n" + m.printName() + "\"");
685 } else if (n instanceof SubstExpr) {
686 SubstExpr m = (SubstExpr) n;
687
688 TDisplay.err(this, "generateIfpTree",
689 "SubstExpr viewed and not handled");
690 } else if (n instanceof TypeDecl) {
691
692 TypeDecl m = (TypeDecl) n;
693 // this represents a type
694
695 String s = new String(m.id.chars);
696
697 TName newNode = new TName(s);
698 // we put it as a variable name with type %Type
699 TNode.addName(s, "%Type");
700
701 // we put as a type too
702 TNode.addType(s);
703
704 currentParent.addSon(newNode);
705
706 if (dot)
707 // fixme, not precise enough maybe
708 oldDot.append("\\n" + s + "\"");
709 } else if (n instanceof TypeExpr) {
710 /* It seems that this kind always has a son that contains
711 the information we want (like TypeSig).
712 However from previoius experiment it seems that sometimes
713 the sons contains (but is it harmful since name
714 have been resoluted during compilation and we know there
715 is no ambiguity)
716 'Object' and that this one contains
717 'java.lang.Object' so maybe something has to be fixed.
718
719 corrected since by adding the double instanceof switch,
720 the class avoided here are handled in other else if
721 */
722 TypeExpr m = (TypeExpr) n;
723
724 if (!(m.type instanceof TypeName || m.type instanceof PrimitiveType || m.type instanceof ArrayType)) {
725 String s = m.type.toString(); // here we get the type
726
727 TName newNode = new TName(s);
728 TNode.addName(s, "%Type");
729
730 TNode.addType(s);
731
732 currentParent.addSon(newNode);
733 }
734
735 if (dot)
736 oldDot.append("\\n \"");
737 } else if (n instanceof TypeName) { // javafe/Type
738 // this represents a type
739
740 TypeName m = (TypeName) n;
741 String s = m.name.printName();
742
743 if (s == null)
744 TDisplay
745 .err(this, "generateIfpTree",
746 "case n instanceof TypeName, warning null reference not expected");
747
748 // we say that this name represents a type
749 TName newNode = new TName(s);
750 TNode.addName(s, "%Type");
751 currentParent.addSon(newNode);
752
753 if (dot)
754 oldDot.append("\\n" + s + "\"");
755 } else if (n instanceof TypeSig) {
756 TypeSig m = (TypeSig) n;
757 // // this represents a type
758
759 // String s = m.simpleName;
760
761 // TName newNode = new TName(s, TNode.$Type);
762 // // we put as a variable name
763 // TNode.addName(s, "%Type");
764
765 // // we put as a type too
766 // TNode.addType(s);
767
768 // currentParent.addSon(newNode);
769
770 if (dot)
771 // fixme, not precise enough maybe
772 oldDot.append("\\n" + m.simpleName + "\"");
773
774 } else if (n instanceof VariableAccess) {
775 VariableAccess m = (VariableAccess) n;
776
777 String sTemp = Atom.printableVersion(UniqName.variable(m.decl));
778
779 //String sTemp = new String(m.id.chars);
780
781 // fixme the two are not the same all the time
782 // error.println("\n");
783 // error.println(m.id.chars);
784 // error.println(m.decl.id.chars);
785 // error.println("\n");
786
787 // if(m.loc != 0)
788 // sTemp = sTemp+":"+UniqName.locToSuffix(m.loc);
789
790 // add it to the global map containg all variables name
791 TNode.addName(sTemp, null);
792
793 /* we don't know the type, so null */
794 TName nTemp = new TName(sTemp);
795 currentParent.addSon(nTemp);
796
797 if (dot) {
798 /* display a square box for variable
799 * + name of the variable
800 */
801
802 oldDot.append("\\n" + sTemp);
803
804 // append line & column in the old format
805 if (m.loc != Location.NULL)
806 oldDot.append(":" + UniqName.locToSuffix(m.loc));
807
808 oldDot.append("\"");
809
810 oldDot.append(", shape = box");
811 }
812 } else /* add the " */
813 if (dot)
814 oldDot.append("\"");
815
816 if (dot) {
817 oldDot.append("];\n");
818
819 /* declaration of the sons */
820 for (int i = 0; i < nbChilds; i++) {
821 o = (Object) n.childAt(i);
822
823 if (o instanceof ASTNode) {
824 oldDot.append(name);
825 oldDot.append(" -> ");
826 nodeTemp = (ASTNode) o;
827 oldDot.append(getNameASTNode(nodeTemp));
828 oldDot.append(nodeTemp.dotId);
829
830 /* red arrow for variables */
831 if (nodeTemp instanceof VariableAccess) {
832 VariableAccess va = (VariableAccess) nodeTemp;
833 oldDot.append(" [color = red]");
834 // error.println(va.id);
835 // error.println(va.loc);
836 // error.println(va.decl);
837
838 }
839
840 oldDot.append(";\n");
841 }
842 }
843
844 }
845
846 /* call on all the sons */
847
848 for (int i = 0; i < nbChilds; i++) {
849 o = (Object) n.childAt(i);
850
851 if (o instanceof ASTNode) {
852 nodeTemp = (ASTNode) o;
853
854 generateIfpTree(nodeTemp, dot);
855 }
856 }
857
858 if (saveParent == null) { // end of the first call
859 newRootNode = currentParent;
860
861 if (newRootNode == null)
862 TDisplay.err(this, "generateIfpTree", "root node is null");
863
864 if (!(newRootNode instanceof TRoot))
865 TDisplay.err(this, "generateIfpTree",
866 "root node doesn't have type TRoot");
867
868 //
869 //firstNotSkipped = false;
870
871 // we type the tree.
872 newRootNode.typeTree();
873
874 TDisplay.info(this, "generateIfpTree", "tree has been typed");
875
876 }
877
878 // restore the parent
879 currentParent = saveParent;
880
881 }
882
883 /**
884 * Utility method for creating dot representation of gc tree
885 *
886 * @return transform escjava.prover.sammy to sammy, ie escjava.x.y to y
887 */
888 private static String getNameASTNode(ASTNode e) {
889
890 String s = e.getClass().getName();
891 int lastDotIndex = s.lastIndexOf('.');
892
893 /* truncate to the class name without package before */
894 if (lastDotIndex != -1)
895 s = s.substring(lastDotIndex + 1, s.length());
896
897 return s;
898
899 }
900
901 /**
902 * Debugging purpose only.
903 */
904 public void printInfo() {
905 if (!computationDone) {
906 generateIfpTree(oldRootNode, true);
907
908 computationDone = true;
909 }
910
911 TNode nTemp = (TNode) newRootNode;
912 nTemp.printInfo();
913 }
914
915 }