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