--- /dev/null
+/***** spin: main.c *****/
+
+/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
+/* All Rights Reserved. This software is for educational purposes only. */
+/* No guarantee whatsoever is expressed or implied by the distribution of */
+/* this code. Permission is given to distribute this code provided that */
+/* this introductory message is not removed and no monies are exchanged. */
+/* Software written by Gerard J. Holzmann. For tool documentation see: */
+/* http://spinroot.com/ */
+/* Send all bug-reports and/or questions to: bugs@spinroot.com */
+
+#include <stdlib.h>
+#include "spin.h"
+#include "version.h"
+#include <signal.h>
+/* #include <malloc.h> */
+#include <time.h>
+#ifdef PC
+#include <io.h>
+extern int unlink(const char *);
+#else
+#include <unistd.h>
+#endif
+#include "y.tab.h"
+
+extern int DstepStart, lineno, tl_terse;
+extern FILE *yyin, *yyout, *tl_out;
+extern Symbol *context;
+extern char *claimproc;
+extern void repro_src(void);
+extern void qhide(int);
+
+Symbol *Fname, *oFname;
+
+int Etimeouts; /* nr timeouts in program */
+int Ntimeouts; /* nr timeouts in never claim */
+int analyze, columns, dumptab, has_remote, has_remvar;
+int interactive, jumpsteps, m_loss, nr_errs, cutoff;
+int s_trail, ntrail, verbose, xspin, notabs, rvopt;
+int no_print, no_wrapup, Caccess, limited_vis, like_java;
+int separate; /* separate compilation */
+int export_ast; /* pangen5.c */
+
+int merger = 1, deadvar = 1, ccache = 1;
+
+static int preprocessonly, SeedUsed;
+static int seedy; /* be verbose about chosen seed */
+static int inlineonly; /* show inlined code */
+static int dataflow = 1;
+
+#if 0
+meaning of flags on verbose:
+ 1 -g global variable values
+ 2 -l local variable values
+ 4 -p all process actions
+ 8 -r receives
+ 16 -s sends
+ 32 -v verbose
+ 64 -w very verbose
+#endif
+
+static char Operator[] = "operator: ";
+static char Keyword[] = "keyword: ";
+static char Function[] = "function-name: ";
+static char **add_ltl = (char **)0;
+static char **ltl_file = (char **)0;
+static char **nvr_file = (char **)0;
+static char *PreArg[64];
+static int PreCnt = 0;
+static char out1[64];
+void explain(int);
+
+#ifndef CPP
+ /* OS2: "spin -Picc -E/Pd+ -E/Q+" */
+ /* Visual C++: "spin -PCL -E/E */
+#ifdef PC
+#define CPP "gcc -E -x c" /* most systems have gcc anyway */
+ /* else use "cpp" */
+#else
+#ifdef SOLARIS
+#define CPP "/usr/ccs/lib/cpp"
+#else
+#if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__)
+#define CPP "cpp"
+#else
+#define CPP "/lib/cpp" /* classic Unix systems */
+#endif
+#endif
+#endif
+
+#endif
+static char *PreProc = CPP;
+extern int depth; /* at least some steps were made */
+
+void
+alldone(int estatus)
+{
+ if (preprocessonly == 0
+ && strlen(out1) > 0)
+ (void) unlink((const char *)out1);
+
+ if (seedy && !analyze && !export_ast
+ && !s_trail && !preprocessonly && depth > 0)
+ printf("seed used: %d\n", SeedUsed);
+
+ if (xspin && (analyze || s_trail))
+ { if (estatus)
+ printf("spin: %d error(s) - aborting\n",
+ estatus);
+ else
+ printf("Exit-Status 0\n");
+ }
+ exit(estatus);
+}
+
+void
+preprocess(char *a, char *b, int a_tmp)
+{ char precmd[1024], cmd[2048]; int i;
+#ifdef PC
+ extern int try_zpp(char *, char *);
+ if (PreCnt == 0 && try_zpp(a, b)) goto out;
+#endif
+ strcpy(precmd, PreProc);
+ for (i = 1; i <= PreCnt; i++)
+ { strcat(precmd, " ");
+ strcat(precmd, PreArg[i]);
+ }
+ if (strlen(precmd) > sizeof(precmd))
+ { fprintf(stdout, "spin: too many -D args, aborting\n");
+ alldone(1);
+ }
+ sprintf(cmd, "%s %s > %s", precmd, a, b);
+ if (system((const char *)cmd))
+ { (void) unlink((const char *) b);
+ if (a_tmp) (void) unlink((const char *) a);
+ fprintf(stdout, "spin: preprocessing failed\n"); /* 4.1.2 was stderr */
+ alldone(1); /* no return, error exit */
+ }
+#ifdef PC
+out:
+#endif
+ if (a_tmp) (void) unlink((const char *) a);
+}
+
+FILE *
+cpyfile(char *src, char *tgt)
+{ FILE *inp, *out;
+ char buf[1024];
+
+ inp = fopen(src, "r");
+ out = fopen(tgt, "w");
+ if (!inp || !out)
+ { printf("spin: cannot cp %s to %s\n", src, tgt);
+ alldone(1);
+ }
+ while (fgets(buf, 1024, inp))
+ fprintf(out, "%s", buf);
+ fclose(inp);
+ return out;
+}
+
+void
+usage(void)
+{
+ printf("use: spin [-option] ... [-option] file\n");
+ printf("\tNote: file must always be the last argument\n");
+ printf("\t-A apply slicing algorithm\n");
+ printf("\t-a generate a verifier in pan.c\n");
+ printf("\t-B no final state details in simulations\n");
+ printf("\t-b don't execute printfs in simulation\n");
+ printf("\t-C print channel access info (combine with -g etc.)\n");
+ printf("\t-c columnated -s -r simulation output\n");
+ printf("\t-d produce symbol-table information\n");
+ printf("\t-Dyyy pass -Dyyy to the preprocessor\n");
+ printf("\t-Eyyy pass yyy to the preprocessor\n");
+ printf("\t-f \"..formula..\" translate LTL ");
+ printf("into never claim\n");
+ printf("\t-F file like -f, but with the LTL ");
+ printf("formula stored in a 1-line file\n");
+ printf("\t-g print all global variables\n");
+ printf("\t-h at end of run, print value of seed for random nr generator used\n");
+ printf("\t-i interactive (random simulation)\n");
+ printf("\t-I show result of inlining and preprocessing\n");
+ printf("\t-J reverse eval order of nested unlesses\n");
+ printf("\t-jN skip the first N steps ");
+ printf("in simulation trail\n");
+ printf("\t-l print all local variables\n");
+ printf("\t-M print msc-flow in Postscript\n");
+ printf("\t-m lose msgs sent to full queues\n");
+ printf("\t-N file use never claim stored in file\n");
+ printf("\t-nN seed for random nr generator\n");
+ printf("\t-o1 turn off dataflow-optimizations in verifier\n");
+ printf("\t-o2 don't hide write-only variables in verifier\n");
+ printf("\t-o3 turn off statement merging in verifier\n");
+ printf("\t-Pxxx use xxx for preprocessing\n");
+ printf("\t-p print all statements\n");
+ printf("\t-qN suppress io for queue N in printouts\n");
+ printf("\t-r print receive events\n");
+ printf("\t-S1 and -S2 separate pan source for claim and model\n");
+ printf("\t-s print send events\n");
+ printf("\t-T do not indent printf output\n");
+ printf("\t-t[N] follow [Nth] simulation trail\n");
+ printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
+ printf("\t-uN stop a simulation run after N steps\n");
+ printf("\t-v verbose, more warnings\n");
+ printf("\t-w very verbose (when combined with -l or -g)\n");
+ printf("\t-[XYZ] reserved for use by xspin interface\n");
+ printf("\t-V print version number and exit\n");
+ alldone(1);
+}
+
+void
+optimizations(int nr)
+{
+ switch (nr) {
+ case '1':
+ dataflow = 1 - dataflow; /* dataflow */
+ if (verbose&32)
+ printf("spin: dataflow optimizations turned %s\n",
+ dataflow?"on":"off");
+ break;
+ case '2':
+ /* dead variable elimination */
+ deadvar = 1 - deadvar;
+ if (verbose&32)
+ printf("spin: dead variable elimination turned %s\n",
+ deadvar?"on":"off");
+ break;
+ case '3':
+ /* statement merging */
+ merger = 1 - merger;
+ if (verbose&32)
+ printf("spin: statement merging turned %s\n",
+ merger?"on":"off");
+ break;
+
+ case '4':
+ /* rv optimization */
+ rvopt = 1 - rvopt;
+ if (verbose&32)
+ printf("spin: rendezvous optimization turned %s\n",
+ rvopt?"on":"off");
+ break;
+ case '5':
+ /* case caching */
+ ccache = 1 - ccache;
+ if (verbose&32)
+ printf("spin: case caching turned %s\n",
+ ccache?"on":"off");
+ break;
+ default:
+ printf("spin: bad or missing parameter on -o\n");
+ usage();
+ break;
+ }
+}
+
+#if 0
+static int
+Rename(const char *old, char *new)
+{ FILE *fo, *fn;
+ char buf[1024];
+
+ if ((fo = fopen(old, "r")) == NULL)
+ { printf("spin: cannot open %s\n", old);
+ return 1;
+ }
+ if ((fn = fopen(new, "w")) == NULL)
+ { printf("spin: cannot create %s\n", new);
+ fclose(fo);
+ return 2;
+ }
+ while (fgets(buf, 1024, fo))
+ fputs(buf, fn);
+
+ fclose(fo);
+ fclose(fn);
+
+ return 0; /* success */
+}
+#endif
+
+int
+main(int argc, char *argv[])
+{ Symbol *s;
+ int T = (int) time((time_t *)0);
+ int usedopts = 0;
+ extern void ana_src(int, int);
+
+ yyin = stdin;
+ yyout = stdout;
+ tl_out = stdout;
+
+ /* unused flags: e, w, x, y, z, A, G, I, L, O, Q, R, S, T, W */
+ while (argc > 1 && argv[1][0] == '-')
+ { switch (argv[1][1]) {
+
+ /* generate code for separate compilation: S1 or S2 */
+ case 'S': separate = atoi(&argv[1][2]);
+ /* fall through */
+ case 'a': analyze = 1; break;
+
+ case 'A': export_ast = 1; break;
+ case 'B': no_wrapup = 1; break;
+ case 'b': no_print = 1; break;
+ case 'C': Caccess = 1; break;
+ case 'c': columns = 1; break;
+ case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];
+ break; /* define */
+ case 'd': dumptab = 1; break;
+ case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];
+ break;
+ case 'F': ltl_file = (char **) (argv+2);
+ argc--; argv++; break;
+ case 'f': add_ltl = (char **) argv;
+ argc--; argv++; break;
+ case 'g': verbose += 1; break;
+ case 'h': seedy = 1; break;
+ case 'i': interactive = 1; break;
+ case 'I': inlineonly = 1; break;
+ case 'J': like_java = 1; break;
+ case 'j': jumpsteps = atoi(&argv[1][2]); break;
+ case 'l': verbose += 2; break;
+ case 'M': columns = 2; break;
+ case 'm': m_loss = 1; break;
+ case 'N': nvr_file = (char **) (argv+2);
+ argc--; argv++; break;
+ case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;
+ case 'o': optimizations(argv[1][2]);
+ usedopts = 1; break;
+ case 'P': PreProc = (char *) &argv[1][2]; break;
+ case 'p': verbose += 4; break;
+ case 'q': if (isdigit(argv[1][2]))
+ qhide(atoi(&argv[1][2]));
+ break;
+ case 'r': verbose += 8; break;
+ case 's': verbose += 16; break;
+ case 'T': notabs = 1; break;
+ case 't': s_trail = 1;
+ if (isdigit(argv[1][2]))
+ ntrail = atoi(&argv[1][2]);
+ break;
+ case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
+ break; /* undefine */
+ case 'u': cutoff = atoi(&argv[1][2]); break; /* new 3.4.14 */
+ case 'v': verbose += 32; break;
+ case 'V': printf("%s\n", SpinVersion);
+ alldone(0);
+ break;
+ case 'w': verbose += 64; break;
+ case 'X': xspin = notabs = 1;
+#ifndef PC
+ signal(SIGPIPE, alldone); /* not posix... */
+#endif
+ break;
+ case 'Y': limited_vis = 1; break; /* used by xspin */
+ case 'Z': preprocessonly = 1; break; /* used by xspin */
+
+ default : usage(); break;
+ }
+ argc--; argv++;
+ }
+ if (usedopts && !analyze)
+ printf("spin: warning -o[123] option ignored in simulations\n");
+
+ if (ltl_file)
+ { char formula[4096];
+ add_ltl = ltl_file-2; add_ltl[1][1] = 'f';
+ if (!(tl_out = fopen(*ltl_file, "r")))
+ { printf("spin: cannot open %s\n", *ltl_file);
+ alldone(1);
+ }
+ fgets(formula, 4096, tl_out);
+ fclose(tl_out);
+ tl_out = stdout;
+ *ltl_file = (char *) formula;
+ }
+ if (argc > 1)
+ { char cmd[128], out2[64];
+
+ /* must remain in current dir */
+ strcpy(out1, "pan.pre");
+
+ if (add_ltl || nvr_file)
+ strcpy(out2, "pan.___");
+
+ if (add_ltl)
+ { tl_out = cpyfile(argv[1], out2);
+ nr_errs = tl_main(2, add_ltl); /* in tl_main.c */
+ fclose(tl_out);
+ preprocess(out2, out1, 1);
+ } else if (nvr_file)
+ { FILE *fd; char buf[1024];
+
+ if ((fd = fopen(*nvr_file, "r")) == NULL)
+ { printf("spin: cannot open %s\n",
+ *nvr_file);
+ alldone(1);
+ }
+ tl_out = cpyfile(argv[1], out2);
+ while (fgets(buf, 1024, fd))
+ fprintf(tl_out, "%s", buf);
+ fclose(tl_out);
+ fclose(fd);
+ preprocess(out2, out1, 1);
+ } else
+ preprocess(argv[1], out1, 0);
+
+ if (preprocessonly)
+ alldone(0);
+
+ if (!(yyin = fopen(out1, "r")))
+ { printf("spin: cannot open %s\n", out1);
+ alldone(1);
+ }
+
+ if (strncmp(argv[1], "progress", (size_t) 8) == 0
+ || strncmp(argv[1], "accept", (size_t) 6) == 0)
+ sprintf(cmd, "_%s", argv[1]);
+ else
+ strcpy(cmd, argv[1]);
+ oFname = Fname = lookup(cmd);
+ if (oFname->name[0] == '\"')
+ { int i = (int) strlen(oFname->name);
+ oFname->name[i-1] = '\0';
+ oFname = lookup(&oFname->name[1]);
+ }
+ } else
+ { oFname = Fname = lookup("<stdin>");
+ if (add_ltl)
+ { if (argc > 0)
+ exit(tl_main(2, add_ltl));
+ printf("spin: missing argument to -f\n");
+ alldone(1);
+ }
+ printf("%s\n", SpinVersion);
+ printf("reading input from stdin:\n");
+ fflush(stdout);
+ }
+ if (columns == 2)
+ { extern void putprelude(void);
+ if (xspin || verbose&(1|4|8|16|32))
+ { printf("spin: -c precludes all flags except -t\n");
+ alldone(1);
+ }
+ putprelude();
+ }
+ if (columns && !(verbose&8) && !(verbose&16))
+ verbose += (8+16);
+ if (columns == 2 && limited_vis)
+ verbose += (1+4);
+ Srand((unsigned int) T); /* defined in run.c */
+ SeedUsed = T;
+ s = lookup("_"); s->type = PREDEF; /* write-only global var */
+ s = lookup("_p"); s->type = PREDEF;
+ s = lookup("_pid"); s->type = PREDEF;
+ s = lookup("_last"); s->type = PREDEF;
+ s = lookup("_nr_pr"); s->type = PREDEF; /* new 3.3.10 */
+
+ yyparse();
+ fclose(yyin);
+ loose_ends();
+
+ if (inlineonly)
+ { repro_src();
+ return 0;
+ }
+
+ chanaccess();
+ if (!Caccess)
+ { if (!s_trail && (dataflow || merger))
+ ana_src(dataflow, merger);
+ sched();
+ alldone(nr_errs);
+ }
+ return 0;
+}
+
+int
+yywrap(void) /* dummy routine */
+{
+ return 1;
+}
+
+void
+non_fatal(char *s1, char *s2)
+{ extern int yychar; extern char yytext[];
+
+ printf("spin: line %3d %s, Error: ",
+ lineno, Fname?Fname->name:"nofilename");
+ if (s2)
+ printf(s1, s2);
+ else
+ printf(s1);
+ if (yychar != -1 && yychar != 0)
+ { printf(" saw '");
+ explain(yychar);
+ printf("'");
+ }
+ if (strlen(yytext)>1)
+ printf(" near '%s'", yytext);
+ printf("\n");
+ nr_errs++;
+}
+
+void
+fatal(char *s1, char *s2)
+{
+ non_fatal(s1, s2);
+ alldone(1);
+}
+
+char *
+emalloc(size_t n)
+{ char *tmp;
+
+ if (n == 0)
+ return NULL; /* robert shelton 10/20/06 */
+
+ if (!(tmp = (char *) malloc(n)))
+ fatal("not enough memory", (char *)0);
+ memset(tmp, 0, n);
+ return tmp;
+}
+
+void
+trapwonly(Lextok *n /* , char *unused */)
+{ extern int realread;
+ short i = (n->sym)?n->sym->type:0;
+
+ if (i != MTYPE
+ && i != BIT
+ && i != BYTE
+ && i != SHORT
+ && i != INT
+ && i != UNSIGNED)
+ return;
+
+ if (realread)
+ n->sym->hidden |= 128; /* var is read at least once */
+}
+
+void
+setaccess(Symbol *sp, Symbol *what, int cnt, int t)
+{ Access *a;
+
+ for (a = sp->access; a; a = a->lnk)
+ if (a->who == context
+ && a->what == what
+ && a->cnt == cnt
+ && a->typ == t)
+ return;
+
+ a = (Access *) emalloc(sizeof(Access));
+ a->who = context;
+ a->what = what;
+ a->cnt = cnt;
+ a->typ = t;
+ a->lnk = sp->access;
+ sp->access = a;
+}
+
+Lextok *
+nn(Lextok *s, int t, Lextok *ll, Lextok *rl)
+{ Lextok *n = (Lextok *) emalloc(sizeof(Lextok));
+ static int warn_nn = 0;
+
+ n->ntyp = (short) t;
+ if (s && s->fn)
+ { n->ln = s->ln;
+ n->fn = s->fn;
+ } else if (rl && rl->fn)
+ { n->ln = rl->ln;
+ n->fn = rl->fn;
+ } else if (ll && ll->fn)
+ { n->ln = ll->ln;
+ n->fn = ll->fn;
+ } else
+ { n->ln = lineno;
+ n->fn = Fname;
+ }
+ if (s) n->sym = s->sym;
+ n->lft = ll;
+ n->rgt = rl;
+ n->indstep = DstepStart;
+
+ if (t == TIMEOUT) Etimeouts++;
+
+ if (!context) return n;
+
+ if (t == 'r' || t == 's')
+ setaccess(n->sym, ZS, 0, t);
+ if (t == 'R')
+ setaccess(n->sym, ZS, 0, 'P');
+
+ if (context->name == claimproc)
+ { int forbidden = separate;
+ switch (t) {
+ case ASGN:
+ printf("spin: Warning, never claim has side-effect\n");
+ break;
+ case 'r': case 's':
+ non_fatal("never claim contains i/o stmnts",(char *)0);
+ break;
+ case TIMEOUT:
+ /* never claim polls timeout */
+ if (Ntimeouts && Etimeouts)
+ forbidden = 0;
+ Ntimeouts++; Etimeouts--;
+ break;
+ case LEN: case EMPTY: case FULL:
+ case 'R': case NFULL: case NEMPTY:
+ /* status becomes non-exclusive */
+ if (n->sym && !(n->sym->xu&XX))
+ { n->sym->xu |= XX;
+ if (separate == 2) {
+ printf("spin: warning, make sure that the S1 model\n");
+ printf(" also polls channel '%s' in its claim\n",
+ n->sym->name);
+ } }
+ forbidden = 0;
+ break;
+ case 'c':
+ AST_track(n, 0); /* register as a slice criterion */
+ /* fall thru */
+ default:
+ forbidden = 0;
+ break;
+ }
+ if (forbidden)
+ { printf("spin: never, saw "); explain(t); printf("\n");
+ fatal("incompatible with separate compilation",(char *)0);
+ }
+ } else if ((t == ENABLED || t == PC_VAL) && !(warn_nn&t))
+ { printf("spin: Warning, using %s outside never claim\n",
+ (t == ENABLED)?"enabled()":"pc_value()");
+ warn_nn |= t;
+ } else if (t == NONPROGRESS)
+ { fatal("spin: Error, using np_ outside never claim\n", (char *)0);
+ }
+ return n;
+}
+
+Lextok *
+rem_lab(Symbol *a, Lextok *b, Symbol *c) /* proctype name, pid, label name */
+{ Lextok *tmp1, *tmp2, *tmp3;
+
+ has_remote++;
+ c->type = LABEL; /* refered to in global context here */
+ fix_dest(c, a); /* in case target of rem_lab is jump */
+ tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
+ tmp1 = nn(ZN, 'p', tmp1, ZN);
+ tmp1->sym = lookup("_p");
+ tmp2 = nn(ZN, NAME, ZN, ZN); tmp2->sym = a;
+ tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c;
+ return nn(ZN, EQ, tmp1, tmp3);
+#if 0
+ .---------------EQ-------.
+ / \
+ 'p' -sym-> _p 'q' -sym-> c (label name)
+ / /
+ '?' -sym-> a (proctype) NAME -sym-> a (proctype name)
+ /
+ b (pid expr)
+#endif
+}
+
+Lextok *
+rem_var(Symbol *a, Lextok *b, Symbol *c, Lextok *ndx)
+{ Lextok *tmp1;
+
+ has_remote++;
+ has_remvar++;
+ dataflow = 0; /* turn off dead variable resets 4.2.5 */
+ tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
+ tmp1 = nn(ZN, 'p', tmp1, ndx);
+ tmp1->sym = c;
+ return tmp1;
+#if 0
+ cannot refer to struct elements
+ only to scalars and arrays
+
+ 'p' -sym-> c (variable name)
+ / \______ possible arrayindex on c
+ /
+ '?' -sym-> a (proctype)
+ /
+ b (pid expr)
+#endif
+}
+
+void
+explain(int n)
+{ FILE *fd = stdout;
+ switch (n) {
+ default: if (n > 0 && n < 256)
+ fprintf(fd, "'%c' = '", n);
+ fprintf(fd, "%d'", n);
+ break;
+ case '\b': fprintf(fd, "\\b"); break;
+ case '\t': fprintf(fd, "\\t"); break;
+ case '\f': fprintf(fd, "\\f"); break;
+ case '\n': fprintf(fd, "\\n"); break;
+ case '\r': fprintf(fd, "\\r"); break;
+ case 'c': fprintf(fd, "condition"); break;
+ case 's': fprintf(fd, "send"); break;
+ case 'r': fprintf(fd, "recv"); break;
+ case 'R': fprintf(fd, "recv poll %s", Operator); break;
+ case '@': fprintf(fd, "@"); break;
+ case '?': fprintf(fd, "(x->y:z)"); break;
+ case ACTIVE: fprintf(fd, "%sactive", Keyword); break;
+ case AND: fprintf(fd, "%s&&", Operator); break;
+ case ASGN: fprintf(fd, "%s=", Operator); break;
+ case ASSERT: fprintf(fd, "%sassert", Function); break;
+ case ATOMIC: fprintf(fd, "%satomic", Keyword); break;
+ case BREAK: fprintf(fd, "%sbreak", Keyword); break;
+ case C_CODE: fprintf(fd, "%sc_code", Keyword); break;
+ case C_DECL: fprintf(fd, "%sc_decl", Keyword); break;
+ case C_EXPR: fprintf(fd, "%sc_expr", Keyword); break;
+ case C_STATE: fprintf(fd, "%sc_state",Keyword); break;
+ case C_TRACK: fprintf(fd, "%sc_track",Keyword); break;
+ case CLAIM: fprintf(fd, "%snever", Keyword); break;
+ case CONST: fprintf(fd, "a constant"); break;
+ case DECR: fprintf(fd, "%s--", Operator); break;
+ case D_STEP: fprintf(fd, "%sd_step", Keyword); break;
+ case D_PROCTYPE: fprintf(fd, "%sd_proctype", Keyword); break;
+ case DO: fprintf(fd, "%sdo", Keyword); break;
+ case DOT: fprintf(fd, "."); break;
+ case ELSE: fprintf(fd, "%selse", Keyword); break;
+ case EMPTY: fprintf(fd, "%sempty", Function); break;
+ case ENABLED: fprintf(fd, "%senabled",Function); break;
+ case EQ: fprintf(fd, "%s==", Operator); break;
+ case EVAL: fprintf(fd, "%seval", Function); break;
+ case FI: fprintf(fd, "%sfi", Keyword); break;
+ case FULL: fprintf(fd, "%sfull", Function); break;
+ case GE: fprintf(fd, "%s>=", Operator); break;
+ case GOTO: fprintf(fd, "%sgoto", Keyword); break;
+ case GT: fprintf(fd, "%s>", Operator); break;
+ case HIDDEN: fprintf(fd, "%shidden", Keyword); break;
+ case IF: fprintf(fd, "%sif", Keyword); break;
+ case INCR: fprintf(fd, "%s++", Operator); break;
+ case INAME: fprintf(fd, "inline name"); break;
+ case INLINE: fprintf(fd, "%sinline", Keyword); break;
+ case INIT: fprintf(fd, "%sinit", Keyword); break;
+ case ISLOCAL: fprintf(fd, "%slocal", Keyword); break;
+ case LABEL: fprintf(fd, "a label-name"); break;
+ case LE: fprintf(fd, "%s<=", Operator); break;
+ case LEN: fprintf(fd, "%slen", Function); break;
+ case LSHIFT: fprintf(fd, "%s<<", Operator); break;
+ case LT: fprintf(fd, "%s<", Operator); break;
+ case MTYPE: fprintf(fd, "%smtype", Keyword); break;
+ case NAME: fprintf(fd, "an identifier"); break;
+ case NE: fprintf(fd, "%s!=", Operator); break;
+ case NEG: fprintf(fd, "%s! (not)",Operator); break;
+ case NEMPTY: fprintf(fd, "%snempty", Function); break;
+ case NFULL: fprintf(fd, "%snfull", Function); break;
+ case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
+ case NONPROGRESS: fprintf(fd, "%snp_", Function); break;
+ case OD: fprintf(fd, "%sod", Keyword); break;
+ case OF: fprintf(fd, "%sof", Keyword); break;
+ case OR: fprintf(fd, "%s||", Operator); break;
+ case O_SND: fprintf(fd, "%s!!", Operator); break;
+ case PC_VAL: fprintf(fd, "%spc_value",Function); break;
+ case PNAME: fprintf(fd, "process name"); break;
+ case PRINT: fprintf(fd, "%sprintf", Function); break;
+ case PRINTM: fprintf(fd, "%sprintm", Function); break;
+ case PRIORITY: fprintf(fd, "%spriority", Keyword); break;
+ case PROCTYPE: fprintf(fd, "%sproctype",Keyword); break;
+ case PROVIDED: fprintf(fd, "%sprovided",Keyword); break;
+ case RCV: fprintf(fd, "%s?", Operator); break;
+ case R_RCV: fprintf(fd, "%s??", Operator); break;
+ case RSHIFT: fprintf(fd, "%s>>", Operator); break;
+ case RUN: fprintf(fd, "%srun", Operator); break;
+ case SEP: fprintf(fd, "token: ::"); break;
+ case SEMI: fprintf(fd, ";"); break;
+ case SHOW: fprintf(fd, "%sshow", Keyword); break;
+ case SND: fprintf(fd, "%s!", Operator); break;
+ case STRING: fprintf(fd, "a string"); break;
+ case TRACE: fprintf(fd, "%strace", Keyword); break;
+ case TIMEOUT: fprintf(fd, "%stimeout",Keyword); break;
+ case TYPE: fprintf(fd, "data typename"); break;
+ case TYPEDEF: fprintf(fd, "%stypedef",Keyword); break;
+ case XU: fprintf(fd, "%sx[rs]", Keyword); break;
+ case UMIN: fprintf(fd, "%s- (unary minus)", Operator); break;
+ case UNAME: fprintf(fd, "a typename"); break;
+ case UNLESS: fprintf(fd, "%sunless", Keyword); break;
+ }
+}
projects / lttv.git / blobdiff