001 package escjava.vcGeneration;
002
003 import java.io.StringWriter;
004
005 class TDotVisitor extends TVisitor {
006
007 TDotVisitor() {
008 super(new StringWriter());
009 }
010
011 /*
012 * Generic functions used by different visit* functions
013 */
014
015 public void visitTFunction(/*@ non_null @*/ TFunction n) throws java.io.IOException{
016
017 /* declaration of the node */
018 out.write(n.dotId()); /* unique */
019
020 out.write(" [label = \""+n.getShortName());
021
022 // write the type (if exists)
023 if(n.type!=null){
024 /* the old type is contained into the 'type' field which has
025 type 'typeInfo' ouf! */
026
027 out.write("\\n\\["+n.getType()+"\\]");
028 }
029
030 out.write("\"];\n");
031
032 TNode nTemp = null;
033
034 /* add all the sons */
035 for(int i = 0; i <= n.sons.size() - 1; i++){
036
037 out.write(n.dotId()+" -> ");
038
039 nTemp = n.getChildAt(i);
040 out.write(nTemp.dotId());
041
042 /* red arrow for variables, green one for value */
043 if(nTemp instanceof TName)
044 out.write(" [color = red]");
045 else if(nTemp instanceof TLiteral)
046 out.write(" [color = green]");
047
048 out.write(";\n");
049
050 /* recursive call on the sons */
051 nTemp.accept(this);
052 }
053
054 }
055
056 public void visitTVariable(/*@ non_null @*/ TVariable n) throws java.io.IOException{
057
058 out.write(n.dotId());
059
060 /* add fancy stuff, like square box o_O */
061 out.write(" [shape=box, label=\"");
062
063 // write the type (if exists)
064 if(n.type!=null){
065 /* the old type is contained into the 'type' field which has
066 type 'typeInfo' ouf! */
067
068 out.write("\\["+n.getType()+"\\]");
069 }
070
071 //out.write("\"];\n");
072 }
073
074 /*
075 * non automatic generated class
076 */
077 public void visitTName(/*@ non_null @*/ TName n) throws java.io.IOException{
078
079 out.write(n.dotId());
080
081 /* add fancy stuff, like square box o_O */
082 out.write(" [shape=box, label=\"");
083
084 out.write("\\["+n.getType()+"\\]");
085
086 /* append the name of the variable */
087 out.write("\\n"+n.name);
088
089 out.write("\"];\n");
090 }
091
092 public void visitTRoot(/*@ non_null @*/ TRoot n) throws java.io.IOException{
093
094 TNode nTemp = null;
095
096 for(int i = 0; i <= n.sons.size() - 1; i++){
097
098 nTemp = n.getChildAt(i);
099
100 /* recursive call on the sons */
101 nTemp.accept(this);
102
103 }
104 }
105
106 /*
107 * class created using the perl script
108 */
109 public void visitTBoolImplies(/*@ non_null @*/ TBoolImplies n) throws java.io.IOException{
110 visitTFunction(n);
111 }
112
113 public void visitTBoolAnd(/*@ non_null @*/ TBoolAnd n) throws java.io.IOException{
114 visitTFunction(n);
115 }
116
117 public void visitTBoolOr(/*@ non_null @*/ TBoolOr n) throws java.io.IOException{
118 visitTFunction(n);
119 }
120
121 public void visitTBoolNot(/*@ non_null @*/ TBoolNot n) throws java.io.IOException{
122 visitTFunction(n);
123 }
124
125 public void visitTBoolEQ(/*@ non_null @*/ TBoolEQ n) throws java.io.IOException{
126 visitTFunction(n);
127 }
128
129 public void visitTBoolNE(/*@ non_null @*/ TBoolNE n) throws java.io.IOException{
130 visitTFunction(n);
131 }
132
133 public void visitTAllocLT(/*@ non_null @*/ TAllocLT n) throws java.io.IOException{
134 visitTFunction(n);
135 }
136
137 public void visitTAllocLE(/*@ non_null @*/ TAllocLE n) throws java.io.IOException{
138 visitTFunction(n);
139 }
140
141 public void visitTAnyEQ(/*@ non_null @*/ TAnyEQ n) throws java.io.IOException{
142 visitTFunction(n);
143 }
144
145 public void visitTAnyNE(/*@ non_null @*/ TAnyNE n) throws java.io.IOException{
146 visitTFunction(n);
147 }
148
149 public void visitTIntegralEQ(/*@ non_null @*/ TIntegralEQ n) throws java.io.IOException{
150 visitTFunction(n);
151 }
152
153 public void visitTIntegralGE(/*@ non_null @*/ TIntegralGE n) throws java.io.IOException{
154 visitTFunction(n);
155 }
156
157 public void visitTIntegralGT(/*@ non_null @*/ TIntegralGT n) throws java.io.IOException{
158 visitTFunction(n);
159 }
160
161 public void visitTIntegralLE(/*@ non_null @*/ TIntegralLE n) throws java.io.IOException{
162 visitTFunction(n);
163 }
164
165 public void visitTIntegralLT(/*@ non_null @*/ TIntegralLT n) throws java.io.IOException{
166 visitTFunction(n);
167 }
168
169 public void visitTIntegralNE(/*@ non_null @*/ TIntegralNE n) throws java.io.IOException{
170 visitTFunction(n);
171 }
172
173 public void visitTIntegralAdd(/*@ non_null @*/ TIntegralAdd n) throws java.io.IOException{
174 visitTFunction(n);
175 }
176
177 public void visitTIntegralDiv(/*@ non_null @*/ TIntegralDiv n) throws java.io.IOException{
178 visitTFunction(n);
179 }
180
181 public void visitTIntegralMod(/*@ non_null @*/ TIntegralMod n) throws java.io.IOException{
182 visitTFunction(n);
183 }
184
185 public void visitTIntegralMul(/*@ non_null @*/ TIntegralMul n) throws java.io.IOException{
186 visitTFunction(n);
187 }
188
189 public void visitTFloatEQ(/*@ non_null @*/ TFloatEQ n) throws java.io.IOException{
190 visitTFunction(n);
191 }
192
193 public void visitTFloatGE(/*@ non_null @*/ TFloatGE n) throws java.io.IOException{
194 visitTFunction(n);
195 }
196
197 public void visitTFloatGT(/*@ non_null @*/ TFloatGT n) throws java.io.IOException{
198 visitTFunction(n);
199 }
200
201 public void visitTFloatLE(/*@ non_null @*/ TFloatLE n) throws java.io.IOException{
202 visitTFunction(n);
203 }
204
205 public void visitTFloatLT(/*@ non_null @*/ TFloatLT n) throws java.io.IOException{
206 visitTFunction(n);
207 }
208
209 public void visitTFloatNE(/*@ non_null @*/ TFloatNE n) throws java.io.IOException{
210 visitTFunction(n);
211 }
212
213 public void visitTFloatAdd(/*@ non_null @*/ TFloatAdd n) throws java.io.IOException{
214 visitTFunction(n);
215 }
216
217 public void visitTFloatDiv(/*@ non_null @*/ TFloatDiv n) throws java.io.IOException{
218 visitTFunction(n);
219 }
220
221 public void visitTFloatMod(/*@ non_null @*/ TFloatMod n) throws java.io.IOException{
222 visitTFunction(n);
223 }
224
225 public void visitTFloatMul(/*@ non_null @*/ TFloatMul n) throws java.io.IOException{
226 visitTFunction(n);
227 }
228
229 public void visitTLockLE(/*@ non_null @*/ TLockLE n) throws java.io.IOException{
230 visitTFunction(n);
231 }
232
233 public void visitTLockLT(/*@ non_null @*/ TLockLT n) throws java.io.IOException{
234 visitTFunction(n);
235 }
236
237 public void visitTRefEQ(/*@ non_null @*/ TRefEQ n) throws java.io.IOException{
238 visitTFunction(n);
239 }
240
241 public void visitTRefNE(/*@ non_null @*/ TRefNE n) throws java.io.IOException{
242 visitTFunction(n);
243 }
244
245 public void visitTTypeEQ(/*@ non_null @*/ TTypeEQ n) throws java.io.IOException{
246 visitTFunction(n);
247 }
248
249 public void visitTTypeNE(/*@ non_null @*/ TTypeNE n) throws java.io.IOException{
250 visitTFunction(n);
251 }
252
253 public void visitTTypeLE(/*@ non_null @*/ TTypeLE n) throws java.io.IOException{
254 visitTFunction(n);
255 }
256
257 public void visitTCast(/*@ non_null @*/ TCast n) throws java.io.IOException{
258 visitTFunction(n);
259 }
260
261 public void visitTIs(/*@ non_null @*/ TIs n) throws java.io.IOException{
262 visitTFunction(n);
263 }
264
265 public void visitTSelect(/*@ non_null @*/ TSelect n) throws java.io.IOException{
266 visitTFunction(n);
267 }
268
269 public void visitTStore(/*@ non_null @*/ TStore n) throws java.io.IOException{
270 visitTFunction(n);
271 }
272
273 public void visitTTypeOf(/*@ non_null @*/ TTypeOf n) throws java.io.IOException{
274 visitTFunction(n);
275 }
276
277 public void visitTForAll(/*@ non_null @*/ TForAll n) throws java.io.IOException{
278 visitTFunction(n);
279 }
280
281 public void visitTExist(/*@ non_null @*/ TExist n) throws java.io.IOException{
282 visitTFunction(n);
283 }
284
285 public void visitTIsAllocated(/*@ non_null @*/ TIsAllocated n) throws java.io.IOException{
286 visitTFunction(n);
287 }
288
289 public void visitTEClosedTime(/*@ non_null @*/ TEClosedTime n) throws java.io.IOException{
290 visitTFunction(n);
291 }
292
293 public void visitTFClosedTime(/*@ non_null @*/ TFClosedTime n) throws java.io.IOException{
294 visitTFunction(n);
295 }
296
297 public void visitTAsElems(/*@ non_null @*/ TAsElems n) throws java.io.IOException{
298 visitTFunction(n);
299 }
300
301 public void visitTAsField(/*@ non_null @*/ TAsField n) throws java.io.IOException{
302 visitTFunction(n);
303 }
304
305 public void visitTAsLockSet(/*@ non_null @*/ TAsLockSet n) throws java.io.IOException{
306 visitTFunction(n);
307 }
308
309 public void visitTArrayLength(/*@ non_null @*/ TArrayLength n) throws java.io.IOException{
310 visitTFunction(n);
311 }
312
313 public void visitTArrayFresh(/*@ non_null @*/ TArrayFresh n) throws java.io.IOException{
314 visitTFunction(n);
315 }
316
317 public void visitTArrayShapeOne(/*@ non_null @*/ TArrayShapeOne n) throws java.io.IOException{
318 visitTFunction(n);
319 }
320
321 public void visitTArrayShapeMore(/*@ non_null @*/ TArrayShapeMore n) throws java.io.IOException{
322 visitTFunction(n);
323 }
324
325 public void visitTIsNewArray(/*@ non_null @*/ TIsNewArray n) throws java.io.IOException{
326 visitTFunction(n);
327 }
328
329 public void visitTString(/*@ non_null @*/ TString n) throws java.io.IOException{
330 visitTVariable(n);
331
332 out.write("\\n"+n.value);
333 out.write("\"];\n");
334 }
335
336 public void visitTBoolean(/*@ non_null @*/ TBoolean n) throws java.io.IOException{
337 visitTVariable(n);
338
339 out.write("\\n"+Boolean.toString(n.value));
340 out.write("\"];\n");
341 }
342
343 public void visitTChar(/*@ non_null @*/ TChar n) throws java.io.IOException{
344 visitTVariable(n);
345
346 out.write("\\n"+Character.toString(n.value));
347 out.write("\"];\n");
348 }
349
350 public void visitTInt(/*@ non_null @*/ TInt n) throws java.io.IOException{
351 visitTVariable(n);
352
353 out.write("\\n"+Integer.toString(n.value));
354 out.write("\"];\n");
355 }
356
357 public void visitTFloat(/*@ non_null @*/ TFloat n) throws java.io.IOException{
358 visitTVariable(n);
359
360 out.write("\\n"+Float.toString(n.value));
361 out.write("\"];\n");
362 }
363
364 public void visitTDouble(/*@ non_null @*/ TDouble n) throws java.io.IOException{
365 visitTVariable(n);
366
367 out.write("\\n"+Double.toString(n.value));
368 out.write("\"];\n");
369 }
370
371 public void visitTNull(/*@ non_null @*/ TNull n) throws java.io.IOException{
372 visitTVariable(n);
373
374 out.write("\\nnull\"];\n");
375 }
376
377 public void visitTMethodCall(/*@non_null*/TMethodCall call) throws java.io.IOException{
378 // TODO Auto-generated method stub
379
380 }
381
382 public void visitTUnset(/*@non_null*/TUnset n) throws java.io.IOException {
383 // TODO Auto-generated method stub
384
385 }
386
387 public void visitTIntegralSub(/*@non_null*/TIntegralSub sub) throws java.io.IOException {
388 // TODO Auto-generated method stub
389
390 }
391
392 public void visitTSum(TSum s) {
393 // TODO Auto-generated method stub
394
395 }
396 }