ref: dab539cd14726de15932b0310532212f8da29bf7
dir: /sys/src/cmd/spin/pangen3.h/
/***** spin: pangen3.h *****/ /* 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: [email protected] */ static char *Head0[] = { "#if defined(BFS) && defined(REACH)", "#undef REACH", /* redundant with bfs */ "#endif", "#ifdef VERI", "#define BASE 1", "#else", "#define BASE 0", "#endif", "typedef struct Trans {", " short atom; /* if &2 = atomic trans; if &8 local */", "#ifdef HAS_UNLESS", " short escp[HAS_UNLESS]; /* lists the escape states */", " short e_trans; /* if set, this is an escp-trans */", "#endif", " short tpe[2]; /* class of operation (for reduction) */", " short qu[6]; /* for conditional selections: qid's */", " uchar ty[6]; /* ditto: type's */", "#ifdef NIBIS", " short om; /* completion status of preselects */", "#endif", " char *tp; /* src txt of statement */", " int st; /* the nextstate */", " int t_id; /* transition id, unique within proc */", " int forw; /* index forward transition */", " int back; /* index return transition */", " struct Trans *nxt;", "} Trans;\n", "#define qptr(x) (((uchar *)&now)+(int)q_offset[x])", "#define pptr(x) (((uchar *)&now)+(int)proc_offset[x])", /* "#define Pptr(x) ((proc_offset[x])?pptr(x):noptr)", */ "extern uchar *Pptr(int);", "#define q_sz(x) (((Q0 *)qptr(x))->Qlen)\n", "#ifndef VECTORSZ", "#define VECTORSZ 1024 /* sv size in bytes */", "#endif\n", 0, }; static char *Header[] = { "#ifdef VERBOSE", "#ifndef CHECK", "#define CHECK", "#endif", "#ifndef DEBUG", "#define DEBUG", "#endif", "#endif", "#ifdef SAFETY", "#ifndef NOFAIR", "#define NOFAIR", "#endif", "#endif", "#ifdef NOREDUCE", "#ifndef XUSAFE", "#define XUSAFE", "#endif", "#if !defined(SAFETY) && !defined(MA)", "#define FULLSTACK", "#endif", "#else", "#ifdef BITSTATE", "#ifdef SAFETY && !defined(HASH64)", "#define CNTRSTACK", "#else", "#define FULLSTACK", "#endif", "#else", "#define FULLSTACK", "#endif", "#endif", "#ifdef BITSTATE", "#ifndef NOCOMP", "#define NOCOMP", "#endif", "#if !defined(LC) && defined(SC)", "#define LC", "#endif", "#endif", "#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)", "/* accept the above for backward compatibility */", "#define COLLAPSE", "#endif", "#ifdef HC", "#undef HC", "#define HC4", "#endif", "#ifdef HC0", /* 32 bits */ "#define HC 0", "#endif", "#ifdef HC1", /* 32+8 bits */ "#define HC 1", "#endif", "#ifdef HC2", /* 32+16 bits */ "#define HC 2", "#endif", "#ifdef HC3", /* 32+24 bits */ "#define HC 3", "#endif", "#ifdef HC4", /* 32+32 bits - combine with -DMA=8 */ "#define HC 4", "#endif", "#ifdef COLLAPSE", "unsigned long ncomps[256+2];", "#endif", "#define MAXQ 255", "#define MAXPROC 255", "#define WS sizeof(long) /* word size in bytes */", "typedef struct Stack { /* for queues and processes */", "#if VECTORSZ>32000", " int o_delta;", " int o_offset;", " int o_skip;", " int o_delqs;", "#else", " short o_delta;", " short o_offset;", " short o_skip;", " short o_delqs;", "#endif", " short o_boq;", "#ifndef XUSAFE", " char *o_name;", "#endif", " char *body;", " struct Stack *nxt;", " struct Stack *lst;", "} Stack;\n", "typedef struct Svtack { /* for complete state vector */", "#if VECTORSZ>32000", " int o_delta;", " int m_delta;", "#else", " short o_delta; /* current size of frame */", " short m_delta; /* maximum size of frame */", "#endif", "#if SYNC", " short o_boq;", "#endif", 0, }; static char *Header0[] = { " char *body;", " struct Svtack *nxt;", " struct Svtack *lst;", "} Svtack;\n", "Trans ***trans; /* 1 ptr per state per proctype */\n", "#if defined(FULLSTACK) || defined(BFS)", "struct H_el *Lstate;", "#endif", "int depthfound = -1; /* loop detection */", "#if VECTORSZ>32000", "int proc_offset[MAXPROC];", "int q_offset[MAXQ];", "#else", "short proc_offset[MAXPROC];", "short q_offset[MAXQ];", "#endif", "uchar proc_skip[MAXPROC];", "uchar q_skip[MAXQ];", "unsigned long vsize; /* vector size in bytes */", "#ifdef SVDUMP", "int vprefix=0, svfd; /* runtime option -pN */", "#endif", "char *tprefix = \"trail\"; /* runtime option -tsuffix */", "short boq = -1; /* blocked_on_queue status */", 0, }; static char *Head1[] = { "typedef struct State {", " uchar _nr_pr;", " uchar _nr_qs;", " uchar _a_t; /* cycle detection */", #if 0 in _a_t: bits 0,4, and 5 =(1|16|32) are set during a 2nd dfs bit 1 is used as the A-bit for fairness bit 7 (128) is the proviso bit, for reduced 2nd dfs (acceptance) #endif "#ifndef NOFAIR", " uchar _cnt[NFAIR]; /* counters, weak fairness */", "#endif", "#ifndef NOVSZ", #ifdef SOLARIS "#if 0", /* v3.4 * noticed alignment problems with some Solaris * compilers, if widest field isn't wordsized */ #else "#if VECTORSZ<65536", #endif " unsigned short _vsz;", "#else", " unsigned long _vsz;", "#endif", "#endif", "#ifdef HAS_LAST", /* cannot go before _cnt - see hstore() */ " uchar _last; /* pid executed in last step */", "#endif", "#ifdef EVENT_TRACE", "#if nstates_event<256", " uchar _event;", "#else", " unsigned short _event;", "#endif", "#endif", 0, }; static char *Addp0[] = { /* addproc(....parlist... */ ")", "{ int j, h = now._nr_pr;", "#ifndef NOCOMP", " int k;", "#endif", " uchar *o_this = this;\n", "#ifndef INLINE", " if (TstOnly) return (h < MAXPROC);", "#endif", "#ifndef NOBOUNDCHECK", "/* redefine Index only within this procedure */", "#undef Index", "#define Index(x, y) Boundcheck(x, y, 0, 0, 0)", "#endif", " if (h >= MAXPROC)", " Uerror(\"too many processes\");", " switch (n) {", " case 0: j = sizeof(P0); break;", 0, }; static char *Addp1[] = { " default: Uerror(\"bad proc - addproc\");", " }", " if (vsize%%WS)", " proc_skip[h] = WS-(vsize%%WS);", " else", " proc_skip[h] = 0;", "#ifndef NOCOMP", " for (k = vsize + (int) proc_skip[h]; k > vsize; k--)", " Mask[k-1] = 1; /* align */", "#endif", " vsize += (int) proc_skip[h];", " proc_offset[h] = vsize;", "#ifdef SVDUMP", " if (vprefix > 0)", " { int dummy = 0;", " write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */", " write(svfd, (uchar *) &h, sizeof(int));", " write(svfd, (uchar *) &n, sizeof(int));", "#if VECTORSZ>32000", " write(svfd, (uchar *) &proc_offset[h], sizeof(int));", "#else", " write(svfd, (uchar *) &proc_offset[h], sizeof(short));", "#endif", " write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */", " }", "#endif", " now._nr_pr += 1;", " if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))", " { printf(\"pan: error: too many processes -- current\");", " printf(\" max is %%d procs (-DNFAIR=%%d)\\n\",", " (8*NFAIR)/2 - 2, NFAIR);", " printf(\"\\trecompile with -DNFAIR=%%d\\n\",", " NFAIR+1);", " pan_exit(1);", " }", " vsize += j;", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", "#ifndef NOCOMP", " for (k = 1; k <= Air[n]; k++)", " Mask[vsize - k] = 1; /* pad */", " Mask[vsize-j] = 1; /* _pid */", "#endif", " hmax = max(hmax, vsize);", " if (vsize >= VECTORSZ)", " { printf(\"pan: error, VECTORSZ too small, recompile pan.c\");", " printf(\" with -DVECTORSZ=N with N>%%d\\n\", vsize);", " Uerror(\"aborting\");", " }", " memset((char *)pptr(h), 0, j);", " this = pptr(h);", " if (BASE > 0 && h > 0)", " ((P0 *)this)->_pid = h-BASE;", " else", " ((P0 *)this)->_pid = h;", " switch (n) {", 0, }; static char *Addq0[] = { "int", "addqueue(int n, int is_rv)", "{ int j=0, i = now._nr_qs;", "#ifndef NOCOMP", " int k;", "#endif", " if (i >= MAXQ)", " Uerror(\"too many queues\");", " switch (n) {", 0, }; static char *Addq1[] = { " default: Uerror(\"bad queue - addqueue\");", " }", " if (vsize%%WS)", " q_skip[i] = WS-(vsize%%WS);", " else", " q_skip[i] = 0;", "#ifndef NOCOMP", " k = vsize;", "#ifndef BFS", " if (is_rv) k += j;", "#endif", " for (k += (int) q_skip[i]; k > vsize; k--)", " Mask[k-1] = 1;", "#endif", " vsize += (int) q_skip[i];", " q_offset[i] = vsize;", " now._nr_qs += 1;", " vsize += j;", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", " hmax = max(hmax, vsize);", " if (vsize >= VECTORSZ)", " Uerror(\"VECTORSZ is too small, edit pan.h\");", " memset((char *)qptr(i), 0, j);", " ((Q0 *)qptr(i))->_t = n;", " return i+1;", "}\n", 0, }; static char *Addq11[] = { "{ int j; uchar *z;\n", "#ifdef HAS_SORTED", " int k;", "#endif", " if (!into--)", " uerror(\"ref to uninitialized chan name (sending)\");", " if (into >= (int) now._nr_qs || into < 0)", " Uerror(\"qsend bad queue#\");", " z = qptr(into);", " j = ((Q0 *)qptr(into))->Qlen;", " switch (((Q0 *)qptr(into))->_t) {", 0, }; static char *Addq2[] = { " case 0: printf(\"queue %%d was deleted\\n\", into+1);", " default: Uerror(\"bad queue - qsend\");", " }", "#ifdef EVENT_TRACE", " if (in_s_scope(into+1))", " require('s', into);", "#endif", "}", "#endif\n", "#if SYNC", "int", "q_zero(int from)", "{ if (!from--)", " { uerror(\"ref to uninitialized chan name (q_zero)\");", " return 0;", " }", " switch(((Q0 *)qptr(from))->_t) {", 0, }; static char *Addq3[] = { " case 0: printf(\"queue %%d was deleted\\n\", from+1);", " }", " Uerror(\"bad queue q-zero\");", " return -1;", "}", "int", "not_RV(int from)", "{ if (q_zero(from))", " { printf(\"==>> a test of the contents of a rv \");", " printf(\"channel always returns FALSE\\n\");", " uerror(\"error to poll rendezvous channel\");", " }", " return 1;", "}", "#endif", "#ifndef XUSAFE", "void", "setq_claim(int x, int m, char *s, int y, char *p)", "{ if (x == 0)", " uerror(\"x[rs] claim on uninitialized channel\");", " if (x < 0 || x > MAXQ)", " Uerror(\"cannot happen setq_claim\");", " q_claim[x] |= m;", " p_name[y] = p;", " q_name[x] = s;", " if (m&2) q_S_check(x, y);", " if (m&1) q_R_check(x, y);", "}", "short q_sender[MAXQ+1];", "int", "q_S_check(int x, int who)", "{ if (!q_sender[x])", " { q_sender[x] = who+1;", "#if SYNC", " if (q_zero(x))", " { printf(\"chan %%s (%%d), \",", " q_name[x], x-1);", " printf(\"sndr proc %%s (%%d)\\n\",", " p_name[who], who);", " uerror(\"xs chans cannot be used for rv\");", " }", "#endif", " } else", " if (q_sender[x] != who+1)", " { printf(\"pan: xs assertion violated: \");", " printf(\"access to chan <%%s> (%%d)\\npan: by \",", " q_name[x], x-1);", " if (q_sender[x] > 0 && p_name[q_sender[x]-1])", " printf(\"%%s (proc %%d) and by \",", " p_name[q_sender[x]-1], q_sender[x]-1);", " printf(\"%%s (proc %%d)\\n\",", " p_name[who], who);", " uerror(\"error, partial order reduction invalid\");", " }", " return 1;", "}", "short q_recver[MAXQ+1];", "int", "q_R_check(int x, int who)", "{ if (!q_recver[x])", " { q_recver[x] = who+1;", "#if SYNC", " if (q_zero(x))", " { printf(\"chan %%s (%%d), \",", " q_name[x], x-1);", " printf(\"recv proc %%s (%%d)\\n\",", " p_name[who], who);", " uerror(\"xr chans cannot be used for rv\");", " }", "#endif", " } else", " if (q_recver[x] != who+1)", " { printf(\"pan: xr assertion violated: \");", " printf(\"access to chan %%s (%%d)\\npan: \",", " q_name[x], x-1);", " if (q_recver[x] > 0 && p_name[q_recver[x]-1])", " printf(\"by %%s (proc %%d) and \",", " p_name[q_recver[x]-1], q_recver[x]-1);", " printf(\"by %%s (proc %%d)\\n\",", " p_name[who], who);", " uerror(\"error, partial order reduction invalid\");", " }", " return 1;", "}", "#endif", "int", "q_len(int x)", "{ if (!x--)", " uerror(\"ref to uninitialized chan name (len)\");", " return ((Q0 *)qptr(x))->Qlen;", "}\n", "int", "q_full(int from)", "{ if (!from--)", " uerror(\"ref to uninitialized chan name (qfull)\");", " switch(((Q0 *)qptr(from))->_t) {", 0, }; static char *Addq4[] = { " case 0: printf(\"queue %%d was deleted\\n\", from+1);", " }", " Uerror(\"bad queue - q_full\");", " return 0;", "}\n", "#ifdef HAS_UNLESS", "int", "q_e_f(int from)", "{ /* empty or full */", " return !q_len(from) || q_full(from);", "}", "#endif", "#if NQS>0", "int", "qrecv(int from, int slot, int fld, int done)", "{ uchar *z;", " int j, k, r=0;\n", " if (!from--)", " uerror(\"ref to uninitialized chan name (receiving)\");", " if (from >= (int) now._nr_qs || from < 0)", " Uerror(\"qrecv bad queue#\");", " z = qptr(from);", "#ifdef EVENT_TRACE", " if (done && (in_r_scope(from+1)))", " require('r', from);", "#endif", " switch (((Q0 *)qptr(from))->_t) {", 0, }; static char *Addq5[] = { " case 0: printf(\"queue %%d was deleted\\n\", from+1);", " default: Uerror(\"bad queue - qrecv\");", " }", " return r;", "}", "#endif\n", "#ifndef BITSTATE", "#ifdef COLLAPSE", "long", "col_q(int i, char *z)", "{ int j=0, k;", " char *x, *y;", " Q0 *ptr = (Q0 *) qptr(i);", " switch (ptr->_t) {", 0, }; static char *Code0[] = { "void", "run(void)", "{ /* int i; */", " memset((char *)&now, 0, sizeof(State));", " vsize = (unsigned long) (sizeof(State) - VECTORSZ);", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", "/* optional provisioning statements, e.g. to */", "/* set hidden variables, used as constants */", "#ifdef PROV", "#include PROV", "#endif", " settable();", 0, }; static char *R0[] = { " Maxbody = max(Maxbody, sizeof(P%d));", " reached[%d] = reached%d;", " accpstate[%d] = (uchar *) emalloc(nstates%d);", " progstate[%d] = (uchar *) emalloc(nstates%d);", " stopstate[%d] = (uchar *) emalloc(nstates%d);", " visstate[%d] = (uchar *) emalloc(nstates%d);", " mapstate[%d] = (short *) emalloc(nstates%d * sizeof(short));", "#ifdef HAS_CODE", " NrStates[%d] = nstates%d;", "#endif", " stopstate[%d][endstate%d] = 1;", 0, }; static char *R0a[] = { " retrans(%d, nstates%d, start%d, src_ln%d, reached%d);", 0, }; static char *R0b[] = { " if (state_tables)", " { printf(\"\\nTransition Type: \");", " printf(\"A=atomic; D=d_step; L=local; G=global\\n\");", " printf(\"Source-State Labels: \");", " printf(\"p=progress; e=end; a=accept;\\n\");", "#ifdef MERGED", " printf(\"Note: statement merging was used. Only the first\\n\");", " printf(\" stmnt executed in each merge sequence is shown\\n\");", " printf(\" (use spin -a -o3 to disable statement merging)\\n\");", "#endif", " pan_exit(0);", " }", 0, }; static char *Code1[] = { "#ifdef NP", "#define ACCEPT_LAB 1 /* at least 1 in np_ */", "#else", "#define ACCEPT_LAB %d /* user-defined accept labels */", "#endif", 0, }; static char *Code3[] = { "#define PROG_LAB %d /* progress labels */", 0, }; static char *R2[] = { "uchar *accpstate[%d];", "uchar *progstate[%d];", "uchar *reached[%d];", "uchar *stopstate[%d];", "uchar *visstate[%d];", "short *mapstate[%d];", "#ifdef HAS_CODE", "int NrStates[%d];", "#endif", 0, }; static char *R3[] = { " Maxbody = max(Maxbody, sizeof(Q%d));", 0, }; static char *R4[] = { " r_ck(reached%d, nstates%d, %d, src_ln%d, src_file%d);", 0, }; static char *R5[] = { " case %d: j = sizeof(P%d); break;", 0, }; static char *R6[] = { " }", " this = o_this;", " return h-BASE;", "#ifndef NOBOUNDCHECK", "#undef Index", "#define Index(x, y) Boundcheck(x, y, II, tt, t)", "#endif", "}\n", "#if defined(BITSTATE) && defined(COLLAPSE)", "/* just to allow compilation, to generate the error */", "long col_p(int i, char *z) { return 0; }", "long col_q(int i, char *z) { return 0; }", "#endif", "#ifndef BITSTATE", "#ifdef COLLAPSE", "long", "col_p(int i, char *z)", "{ int j, k; unsigned long ordinal(char *, long, short);", " char *x, *y;", " P0 *ptr = (P0 *) pptr(i);", " switch (ptr->_t) {", " case 0: j = sizeof(P0); break;", 0, }; static char *R8a[] = { " default: Uerror(\"bad proctype - collapse\");", " }", " if (z) x = z; else x = scratch;", " y = (char *) ptr; k = proc_offset[i];", " for ( ; j > 0; j--, y++)", " if (!Mask[k++]) *x++ = *y;", " for (j = 0; j < WS-1; j++)", " *x++ = 0;", " x -= j;", " if (z) return (long) (x - z);", " return ordinal(scratch, x-scratch, (short) (2+ptr->_t));", "}", "#endif", "#endif", 0, }; static char *R8b[] = { " default: Uerror(\"bad qtype - collapse\");", " }", " if (z) x = z; else x = scratch;", " y = (char *) ptr; k = q_offset[i];", " /* no need to store the empty slots at the end */", " j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);", " for ( ; j > 0; j--, y++)", " if (!Mask[k++]) *x++ = *y;", " for (j = 0; j < WS-1; j++)", " *x++ = 0;", " x -= j;", " if (z) return (long) (x - z);", " return ordinal(scratch, x-scratch, 1); /* chan */", "}", "#endif", "#endif", 0, }; static char *R12[] = { "\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;", 0, }; char *R13[] = { "int ", "unsend(int into)", "{ int _m=0, j; uchar *z;\n", "#ifdef HAS_SORTED", " int k;", "#endif", " if (!into--)", " uerror(\"ref to uninitialized chan (unsend)\");", " z = qptr(into);", " j = ((Q0 *)z)->Qlen;", " ((Q0 *)z)->Qlen = --j;", " switch (((Q0 *)qptr(into))->_t) {", 0, }; char *R14[] = { " default: Uerror(\"bad queue - unsend\");", " }", " return _m;", "}\n", "void", "unrecv(int from, int slot, int fld, int fldvar, int strt)", "{ int j; uchar *z;\n", " if (!from--)", " uerror(\"ref to uninitialized chan (unrecv)\");", " z = qptr(from);", " j = ((Q0 *)z)->Qlen;", " if (strt) ((Q0 *)z)->Qlen = j+1;", " switch (((Q0 *)qptr(from))->_t) {", 0, }; char *R15[] = { " default: Uerror(\"bad queue - qrecv\");", " }", "}", 0, }; static char *Proto[] = { "", "/** function prototypes **/", "char *emalloc(unsigned long);", "char *Malloc(unsigned long);", "int Boundcheck(int, int, int, int, Trans *);", "int addqueue(int, int);", "/* int atoi(char *); */", "/* int abort(void); */", "int close(int);", /* should probably remove this */ #if 0 "#ifndef SC", "int creat(char *, unsigned short);", "int write(int, void *, unsigned);", "#endif", #endif "int delproc(int, int);", "int endstate(void);", "int hstore(char *, int);", "#ifdef MA", "int gstore(char *, int, uchar);", "#endif", "int q_cond(short, Trans *);", "int q_full(int);", "int q_len(int);", "int q_zero(int);", "int qrecv(int, int, int, int);", "int unsend(int);", "/* void *sbrk(int); */", "void Uerror(char *);", "void assert(int, char *, int, int, Trans *);", "void c_chandump(int);", "void c_globals(void);", "void c_locals(int, int);", "void checkcycles(void);", "void crack(int, int, Trans *, short *);", "void d_hash(uchar *, int);", "void s_hash(uchar *, int);", "void r_hash(uchar *, int);", "void delq(int);", "void do_reach(void);", "void pan_exit(int);", "void exit(int);", "void hinit(void);", "void imed(Trans *, int, int, int);", "void new_state(void);", "void p_restor(int);", "void putpeg(int, int);", "void putrail(void);", "void q_restor(void);", "void retrans(int, int, int, short *, uchar *);", "void settable(void);", "void setq_claim(int, int, char *, int, char *);", "void sv_restor(void);", "void sv_save(void);", "void tagtable(int, int, int, short *, uchar *);", "void uerror(char *);", "void unrecv(int, int, int, int, int);", "void usage(FILE *);", "void wrap_stats(void);", "#if defined(FULLSTACK) && defined(BITSTATE)", "int onstack_now(void);", "void onstack_init(void);", "void onstack_put(void);", "void onstack_zap(void);", "#endif", "#ifndef XUSAFE", "int q_S_check(int, int);", "int q_R_check(int, int);", "uchar q_claim[MAXQ+1];", "char *q_name[MAXQ+1];", "char *p_name[MAXPROC+1];", "#endif", 0, }; static char *SvMap[] = { "void", "to_compile(void)", "{ char ctd[1024], carg[64];", "#ifdef BITSTATE", " strcpy(ctd, \"-DBITSTATE \");", "#else", " strcpy(ctd, \"\");", "#endif", "#ifdef NOVSZ", " strcat(ctd, \"-DNOVSZ \");", "#endif", "#ifdef MEMLIM", " sprintf(carg, \"-DMEMLIM=%%d \", MEMLIM);", " strcat(ctd, carg);", "#else", "#ifdef MEMCNT", " sprintf(carg, \"-DMEMCNT=%%d \", MEMCNT);", " strcat(ctd, carg);", "#endif", "#endif", "#ifdef NOCLAIM", " strcat(ctd, \"-DNOCLAIM \");", "#endif", "#ifdef SAFETY", " strcat(ctd, \"-DSAFETY \");", "#else", "#ifdef NOFAIR", " strcat(ctd, \"-DNOFAIR \");", "#else", "#ifdef NFAIR", " if (NFAIR != 2)", " { sprintf(carg, \"-DNFAIR=%%d \", NFAIR);", " strcat(ctd, carg);", " }", "#endif", "#endif", "#endif", "#ifdef NOREDUCE", " strcat(ctd, \"-DNOREDUCE \");", "#else", "#ifdef XUSAFE", " strcat(ctd, \"-DXUSAFE \");", "#endif", "#endif", "#ifdef NP", " strcat(ctd, \"-DNP \");", "#endif", "#ifdef PEG", " strcat(ctd, \"-DPEG \");", "#endif", "#ifdef VAR_RANGES", " strcat(ctd, \"-DVAR_RANGES \");", "#endif", "#ifdef HC0", " strcat(ctd, \"-DHC0 \");", "#endif", "#ifdef HC1", " strcat(ctd, \"-DHC1 \");", "#endif", "#ifdef HC2", " strcat(ctd, \"-DHC2 \");", "#endif", "#ifdef HC3", " strcat(ctd, \"-DHC3 \");", "#endif", "#ifdef HC4", " strcat(ctd, \"-DHC4 \");", "#endif", "#ifdef CHECK", " strcat(ctd, \"-DCHECK \");", "#endif", "#ifdef CTL", " strcat(ctd, \"-DCTL \");", "#endif", "#ifdef NIBIS", " strcat(ctd, \"-DNIBIS \");", "#endif", "#ifdef NOBOUNDCHECK", " strcat(ctd, \"-DNOBOUNDCHECK \");", "#endif", "#ifdef NOSTUTTER", " strcat(ctd, \"-DNOSTUTTER \");", "#endif", "#ifdef REACH", " strcat(ctd, \"-DREACH \");", "#endif", "#ifdef PRINTF", " strcat(ctd, \"-DPRINTF \");", "#endif", "#ifdef OTIM", " strcat(ctd, \"-DOTIM \");", "#endif", "#ifdef COLLAPSE", " strcat(ctd, \"-DCOLLAPSE \");", "#endif", "#ifdef MA", " sprintf(carg, \"-DMA=%%d \", MA);", " strcat(ctd, carg);", "#endif", "#ifdef SVDUMP", " strcat(ctd, \"-DSVDUMP \");", "#endif", "#ifdef VECTORSZ", " if (VECTORSZ != 1024)", " { sprintf(carg, \"-DVECTORSZ=%%d \", VECTORSZ);", " strcat(ctd, carg);", " }", "#endif", "#ifdef VERBOSE", " strcat(ctd, \"-DVERBOSE \");", "#endif", "#ifdef CHECK", " strcat(ctd, \"-DCHECK \");", "#endif", "#ifdef SDUMP", " strcat(ctd, \"-DSDUMP \");", "#endif", "#ifdef COVEST", " strcat(ctd, \"-DCOVEST \");", "#endif", " printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);", "}", 0, };