1 /***** spin: main.c *****/ 2 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 */ 11 12 #include <stdlib.h> 13 #include "spin.h" 14 #include "version.h" 15 #include <signal.h> 16 /* #include <malloc.h> */ 17 #include <time.h> 18 #ifdef PC 19 #include <io.h> 20 extern int unlink(const char *); 21 #else 22 #include <unistd.h> 23 #endif 24 #include "y.tab.h" 25 26 extern int DstepStart, lineno, tl_terse; 27 extern FILE *yyin, *yyout, *tl_out; 28 extern Symbol *context; 29 extern char *claimproc; 30 extern void repro_src(void); 31 extern void qhide(int); 32 33 Symbol *Fname, *oFname; 34 35 int Etimeouts; /* nr timeouts in program */ 36 int Ntimeouts; /* nr timeouts in never claim */ 37 int analyze, columns, dumptab, has_remote, has_remvar; 38 int interactive, jumpsteps, m_loss, nr_errs, cutoff; 39 int s_trail, ntrail, verbose, xspin, notabs, rvopt; 40 int no_print, no_wrapup, Caccess, limited_vis, like_java; 41 int separate; /* separate compilation */ 42 int export_ast; /* pangen5.c */ 43 int inlineonly; /* show inlined code */ 44 int seedy; /* be verbose about chosen seed */ 45 46 int dataflow = 1, merger = 1, deadvar = 1, ccache = 1; 47 48 static int preprocessonly, SeedUsed; 49 50 #if 0 51 meaning of flags on verbose: 52 1 -g global variable values 53 2 -l local variable values 54 4 -p all process actions 55 8 -r receives 56 16 -s sends 57 32 -v verbose 58 64 -w very verbose 59 #endif 60 61 static char Operator[] = "operator: "; 62 static char Keyword[] = "keyword: "; 63 static char Function[] = "function-name: "; 64 static char **add_ltl = (char **)0; 65 static char **ltl_file = (char **)0; 66 static char **nvr_file = (char **)0; 67 static char *PreArg[64]; 68 static int PreCnt = 0; 69 static char out1[64]; 70 static void explain(int); 71 72 #ifndef CPP 73 /* OS2: "spin -Picc -E/Pd+ -E/Q+" */ 74 /* Visual C++: "spin -PCL -E/E */ 75 #ifdef PC 76 #define CPP "gcc -E -x c" /* most systems have gcc anyway */ 77 /* else use "cpp" */ 78 #else 79 #ifdef SOLARIS 80 #define CPP "/usr/ccs/lib/cpp" 81 #else 82 #if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__) 83 #define CPP "cpp" 84 #else 85 #define CPP "/bin/cpp" /* classic Unix systems */ 86 #endif 87 #endif 88 #endif 89 90 #endif 91 static char *PreProc = CPP; 92 extern int depth; /* at least some steps were made */ 93 94 void 95 alldone(int estatus) 96 { 97 if (preprocessonly == 0 98 && strlen(out1) > 0) 99 (void) unlink((const char *)out1); 100 101 if (seedy && !analyze && !export_ast 102 && !s_trail && !preprocessonly && depth > 0) 103 printf("seed used: %d\n", SeedUsed); 104 105 if (xspin && (analyze || s_trail)) 106 { if (estatus) 107 printf("spin: %d error(s) - aborting\n", 108 estatus); 109 else 110 printf("Exit-Status 0\n"); 111 } 112 exit(estatus); 113 } 114 115 void 116 preprocess(char *a, char *b, int a_tmp) 117 { char precmd[512], cmd[1024]; int i; 118 #ifdef PC 119 extern int try_zpp(char *, char *); 120 if (PreCnt == 0 && try_zpp(a, b)) goto out; 121 #endif 122 strcpy(precmd, PreProc); 123 for (i = 1; i <= PreCnt; i++) 124 { strcat(precmd, " "); 125 strcat(precmd, PreArg[i]); 126 } 127 sprintf(cmd, "%s %s > %s", precmd, a, b); 128 if (system((const char *)cmd)) 129 { (void) unlink((const char *) b); 130 if (a_tmp) (void) unlink((const char *) a); 131 fprintf(stdout, "spin: preprocessing failed\n"); /* 4.1.2 was stderr */ 132 alldone(1); /* no return, error exit */ 133 } 134 #ifdef PC 135 out: 136 #endif 137 if (a_tmp) (void) unlink((const char *) a); 138 } 139 140 FILE * 141 cpyfile(char *src, char *tgt) 142 { FILE *inp, *out; 143 char buf[1024]; 144 145 inp = fopen(src, "r"); 146 out = fopen(tgt, "w"); 147 if (!inp || !out) 148 { printf("spin: cannot cp %s to %s\n", src, tgt); 149 alldone(1); 150 } 151 while (fgets(buf, 1024, inp)) 152 fprintf(out, "%s", buf); 153 fclose(inp); 154 return out; 155 } 156 157 void 158 usage(void) 159 { 160 printf("use: spin [-option] ... [-option] file\n"); 161 printf("\tNote: file must always be the last argument\n"); 162 printf("\t-A apply slicing algorithm\n"); 163 printf("\t-a generate a verifier in pan.c\n"); 164 printf("\t-B no final state details in simulations\n"); 165 printf("\t-b don't execute printfs in simulation\n"); 166 printf("\t-C print channel access info (combine with -g etc.)\n"); 167 printf("\t-c columnated -s -r simulation output\n"); 168 printf("\t-d produce symbol-table information\n"); 169 printf("\t-Dyyy pass -Dyyy to the preprocessor\n"); 170 printf("\t-Eyyy pass yyy to the preprocessor\n"); 171 printf("\t-f \"..formula..\" translate LTL "); 172 printf("into never claim\n"); 173 printf("\t-F file like -f, but with the LTL "); 174 printf("formula stored in a 1-line file\n"); 175 printf("\t-g print all global variables\n"); 176 printf("\t-h at end of run, print value of seed for random nr generator used\n"); 177 printf("\t-i interactive (random simulation)\n"); 178 printf("\t-I show result of inlining and preprocessing\n"); 179 printf("\t-J reverse eval order of nested unlesses\n"); 180 printf("\t-jN skip the first N steps "); 181 printf("in simulation trail\n"); 182 printf("\t-l print all local variables\n"); 183 printf("\t-M print msc-flow in Postscript\n"); 184 printf("\t-m lose msgs sent to full queues\n"); 185 printf("\t-N file use never claim stored in file\n"); 186 printf("\t-nN seed for random nr generator\n"); 187 printf("\t-o1 turn off dataflow-optimizations in verifier\n"); 188 printf("\t-o2 don't hide write-only variables in verifier\n"); 189 printf("\t-o3 turn off statement merging in verifier\n"); 190 printf("\t-Pxxx use xxx for preprocessing\n"); 191 printf("\t-p print all statements\n"); 192 printf("\t-qN suppress io for queue N in printouts\n"); 193 printf("\t-r print receive events\n"); 194 printf("\t-S1 and -S2 separate pan source for claim and model\n"); 195 printf("\t-s print send events\n"); 196 printf("\t-T do not indent printf output\n"); 197 printf("\t-t[N] follow [Nth] simulation trail\n"); 198 printf("\t-Uyyy pass -Uyyy to the preprocessor\n"); 199 printf("\t-uN stop a simulation run after N steps\n"); 200 printf("\t-v verbose, more warnings\n"); 201 printf("\t-w very verbose (when combined with -l or -g)\n"); 202 printf("\t-[XYZ] reserved for use by xspin interface\n"); 203 printf("\t-V print version number and exit\n"); 204 alldone(1); 205 } 206 207 void 208 optimizations(char nr) 209 { 210 switch (nr) { 211 case '1': 212 dataflow = 1 - dataflow; /* dataflow */ 213 if (verbose&32) 214 printf("spin: dataflow optimizations turned %s\n", 215 dataflow?"on":"off"); 216 break; 217 case '2': 218 /* dead variable elimination */ 219 deadvar = 1 - deadvar; 220 if (verbose&32) 221 printf("spin: dead variable elimination turned %s\n", 222 deadvar?"on":"off"); 223 break; 224 case '3': 225 /* statement merging */ 226 merger = 1 - merger; 227 if (verbose&32) 228 printf("spin: statement merging turned %s\n", 229 merger?"on":"off"); 230 break; 231 232 case '4': 233 /* rv optimization */ 234 rvopt = 1 - rvopt; 235 if (verbose&32) 236 printf("spin: rendezvous optimization turned %s\n", 237 rvopt?"on":"off"); 238 break; 239 case '5': 240 /* case caching */ 241 ccache = 1 - ccache; 242 if (verbose&32) 243 printf("spin: case caching turned %s\n", 244 ccache?"on":"off"); 245 break; 246 default: 247 printf("spin: bad or missing parameter on -o\n"); 248 usage(); 249 break; 250 } 251 } 252 253 #if 0 254 static int 255 Rename(const char *old, char *new) 256 { FILE *fo, *fn; 257 char buf[1024]; 258 259 if ((fo = fopen(old, "r")) == NULL) 260 { printf("spin: cannot open %s\n", old); 261 return 1; 262 } 263 if ((fn = fopen(new, "w")) == NULL) 264 { printf("spin: cannot create %s\n", new); 265 fclose(fo); 266 return 2; 267 } 268 while (fgets(buf, 1024, fo)) 269 fputs(buf, fn); 270 271 fclose(fo); 272 fclose(fn); 273 274 return 0; /* success */ 275 } 276 #endif 277 278 int 279 main(int argc, char *argv[]) 280 { Symbol *s; 281 int T = (int) time((time_t *)0); 282 int usedopts = 0; 283 extern void ana_src(int, int); 284 285 yyin = stdin; 286 yyout = stdout; 287 tl_out = stdout; 288 289 /* unused flags: e, w, x, y, z, A, G, I, L, O, Q, R, S, T, W */ 290 while (argc > 1 && argv[1][0] == '-') 291 { switch (argv[1][1]) { 292 293 /* generate code for separate compilation: S1 or S2 */ 294 case 'S': separate = atoi(&argv[1][2]); 295 /* fall through */ 296 case 'a': analyze = 1; break; 297 298 case 'A': export_ast = 1; break; 299 case 'B': no_wrapup = 1; break; 300 case 'b': no_print = 1; break; 301 case 'C': Caccess = 1; break; 302 case 'c': columns = 1; break; 303 case 'D': PreArg[++PreCnt] = (char *) &argv[1][0]; 304 break; /* define */ 305 case 'd': dumptab = 1; break; 306 case 'E': PreArg[++PreCnt] = (char *) &argv[1][2]; 307 break; 308 case 'F': ltl_file = (char **) (argv+2); 309 argc--; argv++; break; 310 case 'f': add_ltl = (char **) argv; 311 argc--; argv++; break; 312 case 'g': verbose += 1; break; 313 case 'h': seedy = 1; break; 314 case 'i': interactive = 1; break; 315 case 'I': inlineonly = 1; break; 316 case 'J': like_java = 1; break; 317 case 'j': jumpsteps = atoi(&argv[1][2]); break; 318 case 'l': verbose += 2; break; 319 case 'M': columns = 2; break; 320 case 'm': m_loss = 1; break; 321 case 'N': nvr_file = (char **) (argv+2); 322 argc--; argv++; break; 323 case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break; 324 case 'o': optimizations(argv[1][2]); 325 usedopts = 1; break; 326 case 'P': PreProc = (char *) &argv[1][2]; break; 327 case 'p': verbose += 4; break; 328 case 'q': if (isdigit(argv[1][2])) 329 qhide(atoi(&argv[1][2])); 330 break; 331 case 'r': verbose += 8; break; 332 case 's': verbose += 16; break; 333 case 'T': notabs = 1; break; 334 case 't': s_trail = 1; 335 if (isdigit(argv[1][2])) 336 ntrail = atoi(&argv[1][2]); 337 break; 338 case 'U': PreArg[++PreCnt] = (char *) &argv[1][0]; 339 break; /* undefine */ 340 case 'u': cutoff = atoi(&argv[1][2]); break; /* new 3.4.14 */ 341 case 'v': verbose += 32; break; 342 case 'V': printf("%s\n", Version); 343 alldone(0); 344 break; 345 case 'w': verbose += 64; break; 346 case 'X': xspin = notabs = 1; 347 #ifndef PC 348 signal(SIGPIPE, alldone); /* not posix... */ 349 #endif 350 break; 351 case 'Y': limited_vis = 1; break; /* used by xspin */ 352 case 'Z': preprocessonly = 1; break; /* used by xspin */ 353 354 default : usage(); break; 355 } 356 argc--; argv++; 357 } 358 if (usedopts && !analyze) 359 printf("spin: warning -o[123] option ignored in simulations\n"); 360 361 if (ltl_file) 362 { char formula[4096]; 363 add_ltl = ltl_file-2; add_ltl[1][1] = 'f'; 364 if (!(tl_out = fopen(*ltl_file, "r"))) 365 { printf("spin: cannot open %s\n", *ltl_file); 366 alldone(1); 367 } 368 fgets(formula, 4096, tl_out); 369 fclose(tl_out); 370 tl_out = stdout; 371 *ltl_file = (char *) formula; 372 } 373 if (argc > 1) 374 { char cmd[128], out2[64]; 375 376 /* must remain in current dir */ 377 strcpy(out1, "pan.pre"); 378 379 if (add_ltl || nvr_file) 380 strcpy(out2, "pan.___"); 381 382 if (add_ltl) 383 { tl_out = cpyfile(argv[1], out2); 384 nr_errs = tl_main(2, add_ltl); /* in tl_main.c */ 385 fclose(tl_out); 386 preprocess(out2, out1, 1); 387 } else if (nvr_file) 388 { FILE *fd; char buf[1024]; 389 390 if ((fd = fopen(*nvr_file, "r")) == NULL) 391 { printf("spin: cannot open %s\n", 392 *nvr_file); 393 alldone(1); 394 } 395 tl_out = cpyfile(argv[1], out2); 396 while (fgets(buf, 1024, fd)) 397 fprintf(tl_out, "%s", buf); 398 fclose(tl_out); 399 fclose(fd); 400 preprocess(out2, out1, 1); 401 } else 402 preprocess(argv[1], out1, 0); 403 404 if (preprocessonly) 405 alldone(0); 406 407 if (!(yyin = fopen(out1, "r"))) 408 { printf("spin: cannot open %s\n", out1); 409 alldone(1); 410 } 411 412 if (strncmp(argv[1], "progress", 8) == 0 413 || strncmp(argv[1], "accept", 6) == 0) 414 sprintf(cmd, "_%s", argv[1]); 415 else 416 strcpy(cmd, argv[1]); 417 oFname = Fname = lookup(cmd); 418 if (oFname->name[0] == '\"') 419 { int i = (int) strlen(oFname->name); 420 oFname->name[i-1] = '\0'; 421 oFname = lookup(&oFname->name[1]); 422 } 423 } else 424 { oFname = Fname = lookup("<stdin>"); 425 if (add_ltl) 426 { if (argc > 0) 427 exit(tl_main(2, add_ltl)); 428 printf("spin: missing argument to -f\n"); 429 alldone(1); 430 } 431 printf("%s\n", Version); 432 printf("reading input from stdin:\n"); 433 fflush(stdout); 434 } 435 if (columns == 2) 436 { extern void putprelude(void); 437 if (xspin || verbose&(1|4|8|16|32)) 438 { printf("spin: -c precludes all flags except -t\n"); 439 alldone(1); 440 } 441 putprelude(); 442 } 443 if (columns && !(verbose&8) && !(verbose&16)) 444 verbose += (8+16); 445 if (columns == 2 && limited_vis) 446 verbose += (1+4); 447 Srand(T); /* defined in run.c */ 448 SeedUsed = T; 449 s = lookup("_"); s->type = PREDEF; /* write-only global var */ 450 s = lookup("_p"); s->type = PREDEF; 451 s = lookup("_pid"); s->type = PREDEF; 452 s = lookup("_last"); s->type = PREDEF; 453 s = lookup("_nr_pr"); s->type = PREDEF; /* new 3.3.10 */ 454 455 yyparse(); 456 fclose(yyin); 457 loose_ends(); 458 459 if (inlineonly) 460 { repro_src(); 461 return 0; 462 } 463 464 chanaccess(); 465 if (!Caccess) 466 { if (!s_trail && (dataflow || merger)) 467 ana_src(dataflow, merger); 468 sched(); 469 alldone(nr_errs); 470 } 471 return 0; 472 } 473 474 int 475 yywrap(void) /* dummy routine */ 476 { 477 return 1; 478 } 479 480 void 481 non_fatal(char *s1, char *s2) 482 { extern char yytext[]; 483 484 printf("spin: line %3d %s, Error: ", 485 lineno, Fname?Fname->name:"nofilename"); 486 if (s2) 487 printf(s1, s2); 488 else 489 printf(s1); 490 if (yytext && strlen(yytext)>1) 491 printf(" near '%s'", yytext); 492 printf("\n"); 493 nr_errs++; 494 } 495 496 void 497 fatal(char *s1, char *s2) 498 { 499 non_fatal(s1, s2); 500 alldone(1); 501 } 502 503 char * 504 emalloc(int n) 505 { char *tmp; 506 507 if (n == 0) 508 return NULL; /* robert shelton 10/20/06 */ 509 510 if (!(tmp = (char *) malloc(n))) 511 fatal("not enough memory", (char *)0); 512 memset(tmp, 0, n); 513 return tmp; 514 } 515 516 void 517 trapwonly(Lextok *n, char *unused) 518 { extern int realread; 519 short i = (n->sym)?n->sym->type:0; 520 521 if (i != MTYPE 522 && i != BIT 523 && i != BYTE 524 && i != SHORT 525 && i != INT 526 && i != UNSIGNED) 527 return; 528 529 if (realread) 530 n->sym->hidden |= 128; /* var is read at least once */ 531 } 532 533 void 534 setaccess(Symbol *sp, Symbol *what, int cnt, int t) 535 { Access *a; 536 537 for (a = sp->access; a; a = a->lnk) 538 if (a->who == context 539 && a->what == what 540 && a->cnt == cnt 541 && a->typ == t) 542 return; 543 544 a = (Access *) emalloc(sizeof(Access)); 545 a->who = context; 546 a->what = what; 547 a->cnt = cnt; 548 a->typ = t; 549 a->lnk = sp->access; 550 sp->access = a; 551 } 552 553 Lextok * 554 nn(Lextok *s, int t, Lextok *ll, Lextok *rl) 555 { Lextok *n = (Lextok *) emalloc(sizeof(Lextok)); 556 static int warn_nn = 0; 557 558 n->ntyp = (short) t; 559 if (s && s->fn) 560 { n->ln = s->ln; 561 n->fn = s->fn; 562 } else if (rl && rl->fn) 563 { n->ln = rl->ln; 564 n->fn = rl->fn; 565 } else if (ll && ll->fn) 566 { n->ln = ll->ln; 567 n->fn = ll->fn; 568 } else 569 { n->ln = lineno; 570 n->fn = Fname; 571 } 572 if (s) n->sym = s->sym; 573 n->lft = ll; 574 n->rgt = rl; 575 n->indstep = DstepStart; 576 577 if (t == TIMEOUT) Etimeouts++; 578 579 if (!context) return n; 580 581 if (t == 'r' || t == 's') 582 setaccess(n->sym, ZS, 0, t); 583 if (t == 'R') 584 setaccess(n->sym, ZS, 0, 'P'); 585 586 if (context->name == claimproc) 587 { int forbidden = separate; 588 switch (t) { 589 case ASGN: 590 printf("spin: Warning, never claim has side-effect\n"); 591 break; 592 case 'r': case 's': 593 non_fatal("never claim contains i/o stmnts",(char *)0); 594 break; 595 case TIMEOUT: 596 /* never claim polls timeout */ 597 if (Ntimeouts && Etimeouts) 598 forbidden = 0; 599 Ntimeouts++; Etimeouts--; 600 break; 601 case LEN: case EMPTY: case FULL: 602 case 'R': case NFULL: case NEMPTY: 603 /* status becomes non-exclusive */ 604 if (n->sym && !(n->sym->xu&XX)) 605 { n->sym->xu |= XX; 606 if (separate == 2) { 607 printf("spin: warning, make sure that the S1 model\n"); 608 printf(" also polls channel '%s' in its claim\n", 609 n->sym->name); 610 } } 611 forbidden = 0; 612 break; 613 case 'c': 614 AST_track(n, 0); /* register as a slice criterion */ 615 /* fall thru */ 616 default: 617 forbidden = 0; 618 break; 619 } 620 if (forbidden) 621 { printf("spin: never, saw "); explain(t); printf("\n"); 622 fatal("incompatible with separate compilation",(char *)0); 623 } 624 } else if ((t == ENABLED || t == PC_VAL) && !(warn_nn&t)) 625 { printf("spin: Warning, using %s outside never claim\n", 626 (t == ENABLED)?"enabled()":"pc_value()"); 627 warn_nn |= t; 628 } else if (t == NONPROGRESS) 629 { fatal("spin: Error, using np_ outside never claim\n", (char *)0); 630 } 631 return n; 632 } 633 634 Lextok * 635 rem_lab(Symbol *a, Lextok *b, Symbol *c) /* proctype name, pid, label name */ 636 { Lextok *tmp1, *tmp2, *tmp3; 637 638 has_remote++; 639 c->type = LABEL; /* refered to in global context here */ 640 fix_dest(c, a); /* in case target of rem_lab is jump */ 641 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a; 642 tmp1 = nn(ZN, 'p', tmp1, ZN); 643 tmp1->sym = lookup("_p"); 644 tmp2 = nn(ZN, NAME, ZN, ZN); tmp2->sym = a; 645 tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c; 646 return nn(ZN, EQ, tmp1, tmp3); 647 #if 0 648 .---------------EQ-------. 649 / \ 650 'p' -sym-> _p 'q' -sym-> c (label name) 651 / / 652 '?' -sym-> a (proctype) NAME -sym-> a (proctype name) 653 / 654 b (pid expr) 655 #endif 656 } 657 658 Lextok * 659 rem_var(Symbol *a, Lextok *b, Symbol *c, Lextok *ndx) 660 { Lextok *tmp1; 661 662 has_remote++; 663 has_remvar++; 664 dataflow = 0; /* turn off dead variable resets 4.2.5 */ 665 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a; 666 tmp1 = nn(ZN, 'p', tmp1, ndx); 667 tmp1->sym = c; 668 return tmp1; 669 #if 0 670 cannot refer to struct elements 671 only to scalars and arrays 672 673 'p' -sym-> c (variable name) 674 / \______ possible arrayindex on c 675 / 676 '?' -sym-> a (proctype) 677 / 678 b (pid expr) 679 #endif 680 } 681 682 static void 683 explain(int n) 684 { FILE *fd = stdout; 685 switch (n) { 686 default: if (n > 0 && n < 256) 687 fprintf(fd, "'%c' = '", n); 688 fprintf(fd, "%d'", n); 689 break; 690 case '\b': fprintf(fd, "\\b"); break; 691 case '\t': fprintf(fd, "\\t"); break; 692 case '\f': fprintf(fd, "\\f"); break; 693 case '\n': fprintf(fd, "\\n"); break; 694 case '\r': fprintf(fd, "\\r"); break; 695 case 'c': fprintf(fd, "condition"); break; 696 case 's': fprintf(fd, "send"); break; 697 case 'r': fprintf(fd, "recv"); break; 698 case 'R': fprintf(fd, "recv poll %s", Operator); break; 699 case '@': fprintf(fd, "@"); break; 700 case '?': fprintf(fd, "(x->y:z)"); break; 701 case ACTIVE: fprintf(fd, "%sactive", Keyword); break; 702 case AND: fprintf(fd, "%s&&", Operator); break; 703 case ASGN: fprintf(fd, "%s=", Operator); break; 704 case ASSERT: fprintf(fd, "%sassert", Function); break; 705 case ATOMIC: fprintf(fd, "%satomic", Keyword); break; 706 case BREAK: fprintf(fd, "%sbreak", Keyword); break; 707 case C_CODE: fprintf(fd, "%sc_code", Keyword); break; 708 case C_DECL: fprintf(fd, "%sc_decl", Keyword); break; 709 case C_EXPR: fprintf(fd, "%sc_expr", Keyword); break; 710 case C_STATE: fprintf(fd, "%sc_state",Keyword); break; 711 case C_TRACK: fprintf(fd, "%sc_track",Keyword); break; 712 case CLAIM: fprintf(fd, "%snever", Keyword); break; 713 case CONST: fprintf(fd, "a constant"); break; 714 case DECR: fprintf(fd, "%s--", Operator); break; 715 case D_STEP: fprintf(fd, "%sd_step", Keyword); break; 716 case D_PROCTYPE: fprintf(fd, "%sd_proctype", Keyword); break; 717 case DO: fprintf(fd, "%sdo", Keyword); break; 718 case DOT: fprintf(fd, "."); break; 719 case ELSE: fprintf(fd, "%selse", Keyword); break; 720 case EMPTY: fprintf(fd, "%sempty", Function); break; 721 case ENABLED: fprintf(fd, "%senabled",Function); break; 722 case EQ: fprintf(fd, "%s==", Operator); break; 723 case EVAL: fprintf(fd, "%seval", Function); break; 724 case FI: fprintf(fd, "%sfi", Keyword); break; 725 case FULL: fprintf(fd, "%sfull", Function); break; 726 case GE: fprintf(fd, "%s>=", Operator); break; 727 case GOTO: fprintf(fd, "%sgoto", Keyword); break; 728 case GT: fprintf(fd, "%s>", Operator); break; 729 case HIDDEN: fprintf(fd, "%shidden", Keyword); break; 730 case IF: fprintf(fd, "%sif", Keyword); break; 731 case INCR: fprintf(fd, "%s++", Operator); break; 732 case INAME: fprintf(fd, "inline name"); break; 733 case INLINE: fprintf(fd, "%sinline", Keyword); break; 734 case INIT: fprintf(fd, "%sinit", Keyword); break; 735 case ISLOCAL: fprintf(fd, "%slocal", Keyword); break; 736 case LABEL: fprintf(fd, "a label-name"); break; 737 case LE: fprintf(fd, "%s<=", Operator); break; 738 case LEN: fprintf(fd, "%slen", Function); break; 739 case LSHIFT: fprintf(fd, "%s<<", Operator); break; 740 case LT: fprintf(fd, "%s<", Operator); break; 741 case MTYPE: fprintf(fd, "%smtype", Keyword); break; 742 case NAME: fprintf(fd, "an identifier"); break; 743 case NE: fprintf(fd, "%s!=", Operator); break; 744 case NEG: fprintf(fd, "%s! (not)",Operator); break; 745 case NEMPTY: fprintf(fd, "%snempty", Function); break; 746 case NFULL: fprintf(fd, "%snfull", Function); break; 747 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break; 748 case NONPROGRESS: fprintf(fd, "%snp_", Function); break; 749 case OD: fprintf(fd, "%sod", Keyword); break; 750 case OF: fprintf(fd, "%sof", Keyword); break; 751 case OR: fprintf(fd, "%s||", Operator); break; 752 case O_SND: fprintf(fd, "%s!!", Operator); break; 753 case PC_VAL: fprintf(fd, "%spc_value",Function); break; 754 case PNAME: fprintf(fd, "process name"); break; 755 case PRINT: fprintf(fd, "%sprintf", Function); break; 756 case PRINTM: fprintf(fd, "%sprintm", Function); break; 757 case PRIORITY: fprintf(fd, "%spriority", Keyword); break; 758 case PROCTYPE: fprintf(fd, "%sproctype",Keyword); break; 759 case PROVIDED: fprintf(fd, "%sprovided",Keyword); break; 760 case RCV: fprintf(fd, "%s?", Operator); break; 761 case R_RCV: fprintf(fd, "%s??", Operator); break; 762 case RSHIFT: fprintf(fd, "%s>>", Operator); break; 763 case RUN: fprintf(fd, "%srun", Operator); break; 764 case SEP: fprintf(fd, "token: ::"); break; 765 case SEMI: fprintf(fd, ";"); break; 766 case SHOW: fprintf(fd, "%sshow", Keyword); break; 767 case SND: fprintf(fd, "%s!", Operator); break; 768 case STRING: fprintf(fd, "a string"); break; 769 case TRACE: fprintf(fd, "%strace", Keyword); break; 770 case TIMEOUT: fprintf(fd, "%stimeout",Keyword); break; 771 case TYPE: fprintf(fd, "data typename"); break; 772 case TYPEDEF: fprintf(fd, "%stypedef",Keyword); break; 773 case XU: fprintf(fd, "%sx[rs]", Keyword); break; 774 case UMIN: fprintf(fd, "%s- (unary minus)", Operator); break; 775 case UNAME: fprintf(fd, "a typename"); break; 776 case UNLESS: fprintf(fd, "%sunless", Keyword); break; 777 } 778 } 779