1 /***** spin: pangen3.c *****/
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
16 extern int claimnr
, eventmapnr
;
19 short ln
, st
; /* linenr, statenr */
20 Symbol
*fn
; /* filename */
25 static Symbol
*lastfnm
;
26 static Symbol lastdef
;
28 static SRC
*frst
= (SRC
*) 0;
29 static SRC
*skip
= (SRC
*) 0;
31 extern void sr_mesg(FILE *, int, int);
37 { fprintf(th
, "\n\t");
40 fprintf(th
, "%3d, ", n
);
44 putfnm(int j
, Symbol
*s
)
46 if (lastfnm
&& lastfnm
== s
&& j
!= -1)
50 fprintf(th
, "{ %s, %d, %d },\n\t",
62 fprintf(th
, "{ %s, %d, %d }\n",
68 putskip(int m
) /* states that need not be reached */
71 for (tmp
= skip
; tmp
; tmp
= tmp
->nxt
)
74 tmp
= (SRC
*) emalloc(sizeof(SRC
));
81 unskip(int m
) /* a state that needs to be reached after all */
82 { SRC
*tmp
, *lst
=(SRC
*)0;
84 for (tmp
= skip
; tmp
; lst
= tmp
, tmp
= tmp
->nxt
)
88 else if (lst
) /* always true, but helps coverity */
95 putsrc(Element
*e
) /* match states to source lines */
99 if (!e
|| !e
->n
) return;
104 for (tmp
= frst
; tmp
; tmp
= tmp
->nxt
)
106 { if (tmp
->ln
!= n
|| tmp
->fn
!= e
->n
->fn
)
107 printf("putsrc mismatch %d - %d, file %s\n", n
,
108 tmp
->ln
, tmp
->fn
->name
);
111 tmp
= (SRC
*) emalloc(sizeof(SRC
));
120 dumpskip(int n
, int m
)
124 fprintf(th
, "uchar reached%d [] = {\n\t", m
);
125 for (j
= 0, col
= 0; j
<= n
; j
++)
127 for (tmp
= skip
; tmp
; lst
= tmp
, tmp
= tmp
->nxt
)
141 fprintf(th
, "uchar *loopstate%d;\n", m
);
144 fprintf(th
, "#define reached_claim reached%d\n", m
);
146 fprintf(th
, "#define reached_event reached%d\n", m
);
152 dumpsrc(int n
, int m
)
156 fprintf(th
, "short src_ln%d [] = {\n\t", m
);
157 for (j
= 0, col
= 0; j
<= n
; j
++)
159 for (tmp
= frst
; tmp
; lst
= tmp
, tmp
= tmp
->nxt
)
169 lastfnm
= (Symbol
*) 0;
170 lastdef
.name
= "\"-\"";
171 fprintf(th
, "S_F_MAP src_file%d [] = {\n\t", m
);
172 for (j
= 0, col
= 0; j
<= n
; j
++)
174 for (tmp
= frst
; tmp
; lst
= tmp
, tmp
= tmp
->nxt
)
176 { putfnm(j
, tmp
->fn
);
190 fprintf(th
, "#define src_claim src_ln%d\n", m
);
192 fprintf(th
, "#define src_event src_ln%d\n", m
);
198 #define Cat0(x) comwork(fd,now->lft,m); fprintf(fd, x); \
199 comwork(fd,now->rgt,m)
200 #define Cat1(x) fprintf(fd,"("); Cat0(x); fprintf(fd,")")
201 #define Cat2(x,y) fprintf(fd,x); comwork(fd,y,m)
202 #define Cat3(x,y,z) fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z)
205 symbolic(FILE *fd
, Lextok
*tv
)
206 { Lextok
*n
; extern Lextok
*Mtype
;
210 for (n
= Mtype
; n
; n
= n
->rgt
, cnt
++)
212 { fprintf(fd
, "%s", n
->lft
->sym
->name
);
219 comwork(FILE *fd
, Lextok
*now
, int m
)
223 if (!now
) { fprintf(fd
, "0"); return; }
225 case CONST
: sr_mesg(fd
, now
->val
, now
->ismtyp
); break;
226 case '!': Cat3("!(", now
->lft
, ")"); break;
227 case UMIN
: Cat3("-(", now
->lft
, ")"); break;
228 case '~': Cat3("~(", now
->lft
, ")"); break;
230 case '/': Cat1("/"); break;
231 case '*': Cat1("*"); break;
232 case '-': Cat1("-"); break;
233 case '+': Cat1("+"); break;
234 case '%': Cat1("%%"); break;
235 case '&': Cat1("&"); break;
236 case '^': Cat1("^"); break;
237 case '|': Cat1("|"); break;
238 case LE
: Cat1("<="); break;
239 case GE
: Cat1(">="); break;
240 case GT
: Cat1(">"); break;
241 case LT
: Cat1("<"); break;
242 case NE
: Cat1("!="); break;
243 case EQ
: Cat1("=="); break;
244 case OR
: Cat1("||"); break;
245 case AND
: Cat1("&&"); break;
246 case LSHIFT
: Cat1("<<"); break;
247 case RSHIFT
: Cat1(">>"); break;
249 case RUN
: fprintf(fd
, "run %s(", now
->sym
->name
);
250 for (v
= now
->lft
; v
; v
= v
->rgt
)
252 { comwork(fd
, v
->lft
, m
);
259 case LEN
: putname(fd
, "len(", now
->lft
, m
, ")");
261 case FULL
: putname(fd
, "full(", now
->lft
, m
, ")");
263 case EMPTY
: putname(fd
, "empty(", now
->lft
, m
, ")");
265 case NFULL
: putname(fd
, "nfull(", now
->lft
, m
, ")");
267 case NEMPTY
: putname(fd
, "nempty(", now
->lft
, m
, ")");
270 case 's': putname(fd
, "", now
->lft
, m
, now
->val
?"!!":"!");
271 for (v
= now
->rgt
, i
=0; v
; v
= v
->rgt
, i
++)
272 { if (v
!= now
->rgt
) fprintf(fd
,",");
273 if (!symbolic(fd
, v
->lft
))
274 comwork(fd
,v
->lft
,m
);
277 case 'r': putname(fd
, "", now
->lft
, m
, "?");
280 case 1: fprintf(fd
, "?"); break;
281 case 2: fprintf(fd
, "<"); break;
282 case 3: fprintf(fd
, "?<"); break;
284 for (v
= now
->rgt
, i
=0; v
; v
= v
->rgt
, i
++)
285 { if (v
!= now
->rgt
) fprintf(fd
,",");
286 if (!symbolic(fd
, v
->lft
))
287 comwork(fd
,v
->lft
,m
);
292 case 'R': putname(fd
, "", now
->lft
, m
, now
->val
?"??[":"?[");
293 for (v
= now
->rgt
, i
=0; v
; v
= v
->rgt
, i
++)
294 { if (v
!= now
->rgt
) fprintf(fd
,",");
295 if (!symbolic(fd
, v
->lft
))
296 comwork(fd
,v
->lft
,m
);
301 case ENABLED
: Cat3("enabled(", now
->lft
, ")");
304 case EVAL
: Cat3("eval(", now
->lft
, ")");
311 case PC_VAL
: Cat3("pc_value(", now
->lft
, ")");
314 case 'c': Cat3("(", now
->lft
, ")");
317 case '?': if (now
->lft
)
318 { Cat3("( (", now
->lft
, ") -> ");
321 { Cat3("(", now
->rgt
->lft
, ") : ");
322 Cat3("(", now
->rgt
->rgt
, ") )");
326 case ASGN
: comwork(fd
,now
->lft
,m
);
328 comwork(fd
,now
->rgt
,m
);
331 case PRINT
: { char c
, buf
[512];
332 strncpy(buf
, now
->sym
->name
, 510);
333 for (i
= j
= 0; i
< 510; i
++, j
++)
334 { c
= now
->sym
->name
[i
];
336 if (c
== '\\') buf
[++j
] = c
;
337 if (c
== '\"') buf
[j
] = '\'';
338 if (c
== '\0') break;
340 if (now
->ntyp
== PRINT
)
341 fprintf(fd
, "printf");
343 fprintf(fd
, "annotate");
344 fprintf(fd
, "(%s", buf
);
346 for (v
= now
->lft
; v
; v
= v
->rgt
)
351 case PRINTM
: fprintf(fd
, "printm(");
352 comwork(fd
, now
->lft
, m
);
355 case NAME
: putname(fd
, "", now
, m
, "");
357 case 'p': putremote(fd
, now
, m
);
359 case 'q': fprintf(fd
, "%s", now
->sym
->name
);
362 case C_CODE
: fprintf(fd
, "{%s}", now
->sym
->name
);
364 case ASSERT
: Cat3("assert(", now
->lft
, ")");
366 case '.': fprintf(fd
, ".(goto)"); break;
367 case GOTO
: fprintf(fd
, "goto %s", now
->sym
->name
); break;
368 case BREAK
: fprintf(fd
, "break"); break;
369 case ELSE
: fprintf(fd
, "else"); break;
370 case '@': fprintf(fd
, "-end-"); break;
372 case D_STEP
: fprintf(fd
, "D_STEP"); break;
373 case ATOMIC
: fprintf(fd
, "ATOMIC"); break;
374 case NON_ATOMIC
: fprintf(fd
, "sub-sequence"); break;
375 case IF
: fprintf(fd
, "IF"); break;
376 case DO
: fprintf(fd
, "DO"); break;
377 case UNLESS
: fprintf(fd
, "unless"); break;
378 case TIMEOUT
: fprintf(fd
, "timeout"); break;
379 default: if (isprint(now
->ntyp
))
380 fprintf(fd
, "'%c'", now
->ntyp
);
382 fprintf(fd
, "%d", now
->ntyp
);
388 comment(FILE *fd
, Lextok
*now
, int m
)
389 { extern short terse
, nocast
;
This page took 0.055033 seconds and 4 git commands to generate.