/***** 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] */
/* (c) 2007: small additions for V5.0 to support multi-core verifications */
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",
"#ifdef TRIX",
" #define qptr(x) (channels[x]->body)",
" #define pptr(x) (processes[x]->body)",
"#else",
" #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)", */
"#endif",
"extern uchar *Pptr(int);",
"extern uchar *Qptr(int);",
"#define q_sz(x) (((Q0 *)qptr(x))->Qlen)",
"",
"#ifdef TRIX",
" #ifdef VECTORSZ",
" #undef VECTORSZ", /* backward compatibility */
" #endif",
" #if WS==4",
" #define VECTORSZ 2056 /* ((MAXPROC+MAXQ+4)*sizeof(uchar *)) */",
" #else",
" #define VECTORSZ 4112 /* the formula causes probs in preprocessing */",
" #endif",
"#else",
" #ifndef VECTORSZ",
" #define VECTORSZ 1024 /* sv size in bytes */",
" #endif",
"#endif\n",
"#define MAXQ 255",
"#define MAXPROC 255",
"",
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",
#if 0
NOREDUCE BITSTATE SAFETY MA WS>4
CNTRSTACK: - + + d -
FULLSTACK: + d - - d
- + d d d
- + + d +
- - d d d
Neither: + d + d d
+ d d + d
#endif
"#ifdef NOREDUCE",
" #ifndef XUSAFE",
" #define XUSAFE",
" #endif",
" #if !defined(SAFETY) && !defined(MA)",
" #define FULLSTACK", /* => NOREDUCE && !SAFETY && !MA */
" #endif",
"#else",
" #ifdef BITSTATE",
" #if defined(SAFETY) && WS<=4",
" #define CNTRSTACK", /* => !NOREDUCE && BITSTATE && SAFETY && WS<=4 */
" #else",
" #define FULLSTACK", /* => !NOREDUCE && BITSTATE && (!SAFETY || WS>4) */
" #endif",
" #else",
" #define FULLSTACK", /* => !NOREDUCE && !BITSTATE */
" #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",
"#if defined(HC0) || defined(HC1) || defined(HC2) || defined(HC3) || defined(HC4)",
" #define HC 4", /* 2x32 bits */
"#endif", /* really only one hashcompact mode, not 5 */
"",
"typedef struct _Stack { /* for queues and processes */",
"#if VECTORSZ>32000",
" int o_delta;",
" #ifndef TRIX",
" int o_offset;",
" int o_skip;",
" #endif",
" int o_delqs;",
"#else",
" short o_delta;",
" #ifndef TRIX",
" short o_offset;",
" short o_skip;",
" #endif",
" short o_delqs;",
"#endif",
" short o_boq;",
"#ifdef TRIX",
" short parent;",
" char *b_ptr;", /* used in delq/q_restor and delproc/p_restor */
"#else",
" char *body;", /* full copy of state vector in non-trix mode */
"#endif",
"#ifndef XUSAFE",
" char *o_name;",
"#endif",
" 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",
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",
" ulong _vsz;",
"#endif",
"#endif",
"#ifdef HAS_LAST", /* cannot go before _cnt - see h_store() */
" uchar _last; /* pid executed in last step */",
"#endif",
"#if defined(BITSTATE) && defined(BCS) && defined(STORE_CTX)",
" uchar _ctx; /* nr of context switches so far */",
"#endif",
"#if defined(BFS_PAR) && defined(L_BOUND)",
" uchar _l_bnd; /* bounded liveness */",
" uchar *_l_sds; /* seed state */",
"#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\");",
"#ifdef V_TRIX",
" printf(\"%%4d: add process %%d\\n\", depth, h);",
"#endif",
" switch (n) {",
" case 0: j = sizeof(P0); break;",
0,
};
static char *Addp1[] = {
" default: Uerror(\"bad proc - addproc\");",
" }",
" #ifdef BFS_PAR",
" bfs_prepmask(1); /* addproc */",
" #endif",
"#ifdef TRIX",
" vsize += sizeof(H_el *);",
"#else",
" if (vsize%%WS)",
" proc_skip[h] = WS-(vsize%%WS);",
" else",
" proc_skip[h] = 0;",
" #if !defined(NOCOMP) && !defined(HC)",
" 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;",
" vsize += j;",
" #if defined(SVDUMP) && defined(VERBOSE)",
" 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));",
" write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",
" #else",
" write(svfd, (uchar *) &proc_offset[h], sizeof(short));",
" write(svfd, (uchar *) &now, vprefix-3*sizeof(int)-sizeof(short)); /* padd */",
" #endif",
" }",
" #endif",
"#endif",
" now._nr_pr += 1;",
"#if defined(BCS) && defined(CONSERVATIVE)",
" if (now._nr_pr >= CONSERVATIVE*8)",
" { printf(\"pan: error: too many processes -- recompile with \");",
" printf(\"-DCONSERVATIVE=%%d\\n\", CONSERVATIVE+1);",
" pan_exit(1);",
" }",
"#endif",
" 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);",
" }",
"#ifndef NOVSZ",
" now._vsz = vsize;",
"#endif",
" hmax = max(hmax, vsize);",
"#ifdef TRIX",
" #ifndef BFS",
" if (freebodies)",
" { processes[h] = freebodies;",
" freebodies = freebodies->nxt;",
" } else",
" { processes[h] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
" processes[h]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
" }",
" processes[h]->modified = 1; /* addproc */",
" #endif",
" processes[h]->psize = j;",
" processes[h]->parent_pid = calling_pid;",
" processes[h]->nxt = (TRIX_v6 *) 0;",
"#else",
" #if !defined(NOCOMP) && !defined(HC)",
" for (k = 1; k <= Air[n]; k++)",
" Mask[vsize - k] = 1; /* pad */",
" Mask[vsize-j] = 1; /* _pid */",
" #endif",
" #ifdef BFS_PAR",
" bfs_fixmask(1); /* addproc */",
" #endif",
" if (vsize >= VECTORSZ)",
" { printf(\"pan: error, VECTORSZ too small, recompile pan.c\");",
" printf(\" with -DVECTORSZ=N with N>%%d\\n\", (int) vsize);",
" Uerror(\"aborting\");",
" }",
"#endif",
" 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 calling_pid, int n, int is_rv)",
"{ int j=0, i = now._nr_qs;",
"#if !defined(NOCOMP) && !defined(TRIX)",
" int k;",
"#endif",
" if (i >= MAXQ)",
" Uerror(\"too many queues\");",
"#ifdef V_TRIX",
" printf(\"%%4d: add queue %%d\\n\", depth, i);",
"#endif",
" switch (n) {",
0,
};
static char *Addq1[] = {
" default: Uerror(\"bad queue - addqueue\");",
" }",
" #ifdef BFS_PAR",
" bfs_prepmask(2); /* addqueue */",
" #endif",
"#ifdef TRIX",
" vsize += sizeof(H_el *);",
"#else",
" if (vsize%%WS)",
" q_skip[i] = WS-(vsize%%WS);",
" else",
" q_skip[i] = 0;",
" #if !defined(NOCOMP) && !defined(HC)",
" 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;",
" vsize += j;",
" #ifdef BFS_PAR",
" bfs_fixmask(2); /* addqueue */",
" #endif",
"#endif",
" now._nr_qs += 1;",
"#ifndef NOVSZ",
" now._vsz = vsize;",
"#endif",
" hmax = max(hmax, vsize);",
"#ifdef TRIX",
" #ifndef BFS",
" if (freebodies)",
" { channels[i] = freebodies;",
" freebodies = freebodies->nxt;",
" } else",
" { channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
" channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
" }",
" channels[i]->modified = 1; /* addq */",
" #endif",
" channels[i]->psize = j;",
" channels[i]->parent_pid = calling_pid;",
" channels[i]->nxt = (TRIX_v6 *) 0;",
"#else",
" if (vsize >= VECTORSZ)",
" Uerror(\"VECTORSZ is too small, edit pan.h\");",
"#endif",
" if (j > 0)", /* zero if there are no queues */
" { 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#\");",
"#if defined(TRIX) && !defined(BFS)",
" #ifndef TRIX_ORIG",
" (trpt+1)->q_bup = now._ids_[now._nr_pr+into];",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d s save %%p from %%d\\n\",",
" depth, into, (trpt+1)->q_bup, now._nr_pr+into);",
" #endif",
" #endif",
" channels[into]->modified = 1; /* qsend */",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d modified\\n\", depth, into);",
" #endif",
"#endif",
" 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 defined(TRIX) && !defined(BFS)",
" #ifndef TRIX_ORIG",
" (trpt+1)->q_bup = now._ids_[now._nr_pr+from];",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d r save %%p from %%d\\n\",",
" depth, from, (trpt+1)->q_bup, now._nr_pr+from);",
" #endif",
" #endif",
" channels[from]->modified = 1; /* qrecv */",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d modified\\n\", depth, from);",
" #endif",
"#endif",
" 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 = (ulong) (sizeof(State) - VECTORSZ);",
"#ifndef NOVSZ",
" now._vsz = vsize;",
"#endif",
"#ifdef TRIX",
" if (VECTORSZ != sizeof(now._ids_))",
" { printf(\"VECTORSZ is %%d, but should be %%d in this mode\\n\",",
" VECTORSZ, (int) sizeof(now._ids_));",
" Uerror(\"VECTORSZ set incorrectly, recompile Spin (not pan.c)\");",
" }",
"#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, ((int) sizeof(P%d)));",
" reached[%d] = reached%d;",
" accpstate[%d] = (uchar *) emalloc(nstates%d);",
" progstate[%d] = (uchar *) emalloc(nstates%d);",
" loopstate%d = loopstate[%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));",
" stopstate[%d][endstate%d] = 1;",
0,
};
static char *R00[] = {
" NrStates[%d] = nstates%d;",
0,
};
static char *R0a[] = {
" retrans(%d, nstates%d, start%d, src_ln%d, reached%d, loopstate%d);",
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",
"#ifdef MEMCNT",
" #ifdef MEMLIM",
" #warning -DMEMLIM takes precedence over -DMEMCNT",
" #undef MEMCNT",
" #else",
" #if MEMCNT<20",
" #warning using minimal value -DMEMCNT=20 (=1MB)",
" #define MEMLIM (1)",
" #undef MEMCNT",
" #else",
" #if MEMCNT==20",
" #define MEMLIM (1)",
" #undef MEMCNT",
" #else",
" #if MEMCNT>=50",
" #error excessive value for MEMCNT",
" #else",
" #define MEMLIM (1<<(MEMCNT-20))",
" #endif",
" #endif",
" #endif",
" #endif",
"#endif",
"#if NCORE>1 && !defined(MEMLIM)",
" #define MEMLIM (2048) /* need a default, using 2 GB */",
"#endif",
0,
};
static char *Code3[] = {
"#define PROG_LAB %d /* progress labels */",
0,
};
static char *R2[] = {
"uchar *accpstate[%d];",
"uchar *progstate[%d];",
"uchar *loopstate[%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, ((int) 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;",
"#ifdef TRIX",
" re_mark_all(1); /* addproc */",
"#endif",
" 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; ulong ordinal(char *, long, short);",
" char *x, *y;",
" P0 *ptr = (P0 *) pptr(i);",
" switch (ptr->_t) {",
" case 0: j = sizeof(P0); break;",
0,
};
static char *R7a[] = {
"void\nre_mark_all(int whichway)",
"{ int j;",
" #ifdef V_TRIX",
" printf(\"%%d: re_mark_all channels %%d\\n\", depth, whichway);",
" #endif",
" #ifndef BFS",
" for (j = 0; j < now._nr_qs; j++)",
" channels[j]->modified = 1; /* channel index moved */",
" #endif",
" #ifndef TRIX_ORIG",
" if (whichway > 0)",
" { for (j = now._nr_pr + now._nr_qs - 1; j >= now._nr_pr; j--)",
" now._ids_[j] = now._ids_[j-1];",
" } else",
" { for (j = now._nr_pr; j < now._nr_pr + now._nr_qs; j++)",
" now._ids_[j] = now._ids_[j+1];",
" }",
" #endif",
"}",
0,
};
static char *R7b[] = {
"#ifdef BFS_PAR",
"inline void",
"bfs_prepmask(int caller)",
"{",
"#if !defined(NOCOMP) && !defined(HC)",
" memcpy((char *) &tmp_msk, (const char *) Mask, sizeof(State));",
" Mask = (uchar *) &tmp_msk;",
"#endif",
" switch (caller) {",
" case 1: /* addproc */",
"#if VECTORSZ>32000",
" memcpy((char *) P_o_tmp, (const char *) proc_offset, MAXPROC*sizeof(int));",
"#else",
" memcpy((char *) P_o_tmp, (const char *) proc_offset, MAXPROC*sizeof(short));",
"#endif",
" memcpy((char *) P_s_tmp, (const char *) proc_skip, MAXPROC*sizeof(uchar));",
" proc_offset = P_o_tmp;",
" proc_skip = (uchar *) &P_s_tmp[0];",
" break;",
" case 2: /* addqueue */",
"#if VECTORSZ>32000",
" memcpy((char *) Q_o_tmp, (const char *) q_offset, MAXQ*sizeof(int));",
"#else",
" memcpy((char *) Q_o_tmp, (const char *) q_offset, MAXQ*sizeof(short));",
"#endif",
" memcpy((char *) Q_s_tmp, (const char *) q_skip, MAXQ*sizeof(uchar));",
" q_offset = Q_o_tmp;",
" q_skip = (uchar *) &Q_s_tmp[0];",
" break;",
" case 3: /* no nothing */",
" break;",
" default: /* cannot happen */",
" Uerror(\"no good\");",
" break;",
" }",
"}",
"",
"typedef struct BFS_saves BFS_saves;",
"struct BFS_saves {",
" char *m;",
" BFS_saves *nxt;",
"} *bfs_save_po,",
" *bfs_save_ps,",
"#if !defined(NOCOMP) && !defined(HC)",
" *bfs_save_mask,",
"#endif",
" *bfs_save_qo,",
" *bfs_save_qs;",
"",
"extern volatile uchar *sh_malloc(ulong);",
"static int bfs_runs; /* 0 before local heaps are initialized */",
"",
"void",
"bfs_swoosh(BFS_saves **where, char **what, int howmuch)",
"{ BFS_saves *m;",
" for (m = *where; m; m = m->nxt)",
" { if (memcmp(m->m, *what, howmuch) == 0)",
" { *what = m->m;",
" return;",
" } }",
" m = (BFS_saves *) emalloc(sizeof(BFS_saves));",
" if (bfs_runs)",
" { m->m = (char *) sh_malloc(howmuch);",
" } else",
" { m->m = (char *) sh_pre_malloc(howmuch);",
" }",
" memcpy(m->m, *what, howmuch);",
" m->nxt = *where;",
" *where = m;",
" *what = m->m;",
"}",
"",
"void",
"bfs_fixmask(int caller)", /* 1=addproc, 2=addqueue */
"{",
"#if !defined(NOCOMP) && !defined(HC)",
" bfs_swoosh(&bfs_save_mask, (char **) &Mask, sizeof(State));",
"#endif",
"#ifndef TRIX",
" switch (caller) {",
" case 1: /* addproc */",
" #if VECTORSZ>32000",
" bfs_swoosh(&bfs_save_po, (char **) &proc_offset, MAXPROC*sizeof(int));",
" #else",
" bfs_swoosh(&bfs_save_po, (char **) &proc_offset, MAXPROC*sizeof(short));",
" #endif",
" bfs_swoosh(&bfs_save_ps, (char **) &proc_skip, MAXPROC*sizeof(uchar));",
" break;",
" case 2: /* addqueue */",
" #if VECTORSZ>32000",
" bfs_swoosh(&bfs_save_qo, (char **) &q_offset, MAXQ*sizeof(int));",
" #else",
" bfs_swoosh(&bfs_save_qo, (char **) &q_offset, MAXQ*sizeof(short));",
" #endif",
" bfs_swoosh(&bfs_save_qs, (char **) &q_skip, MAXQ*sizeof(uchar));",
" break;",
" case 3: /* do nothing */",
" break;",
" default:",
" Uerror(\"double plus ungood\");",
" break;",
" }",
"#endif",
"}",
"#endif",
0,
};
static char *R8a[] = {
" default: Uerror(\"bad proctype - collapse\");",
" }",
" if (z) x = z; else x = scratch;",
" y = (char *) ptr; k = proc_offset[i];",
"",
"#if !defined(NOCOMP) && !defined(HC)",
" for ( ; j > 0; j--, y++)",
" if (!Mask[k++]) *x++ = *y;",
"#else",
" memcpy(x, y, j);",
" x += j;",
"#endif",
" 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];",
"#if NQS > 0",
" /* no need to store the empty slots at the end */",
" j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);",
"#endif",
"",
"#if !defined(NOCOMP) && !defined(HC)",
" for ( ; j > 0; j--, y++)",
" if (!Mask[k++]) *x++ = *y;",
"#else",
" memcpy(x, y, j);",
" x += j;",
"#endif",
" 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)\");",
"#if defined(TRIX) && !defined(BFS)",
" #ifndef TRIX_ORIG",
" now._ids_[now._nr_pr+into] = trpt->q_bup;",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d s restore %%p into %%d\\n\",",
" depth, into, trpt->q_bup, now._nr_pr+into);",
" #endif",
" #else",
" channels[into]->modified = 1; /* unsend */",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d unmodify\\n\", depth, into);",
" #endif",
" #endif",
"#endif",
" 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)\");",
"#if defined(TRIX) && !defined(BFS)",
" #ifndef TRIX_ORIG",
" now._ids_[now._nr_pr+from] = trpt->q_bup;",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d r restore %%p into %%d\\n\",",
" depth, from, trpt->q_bup, now._nr_pr+from);",
" #endif",
" #else",
" channels[from]->modified = 1; /* unrecv */",
" #ifdef V_TRIX",
" printf(\"%%4d: channel %%d unmodify\\n\", depth, from);",
" #endif",
" #endif",
"#endif",
" 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(ulong);",
"char *Malloc(ulong);",
"int Boundcheck(int, int, int, int, Trans *);",
"int addqueue(int, 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 find_claim(char *);",
"int h_store(char *, int);",
"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 spin_assert(int, char *, int, int, Trans *);",
"#ifdef BFS_PAR",
"void bfs_printf(const char *, ...);",
"volatile uchar *sh_pre_malloc(ulong);",
"#endif",
"void c_chandump(int);",
"void c_globals(void);",
"void c_locals(int, int);",
"void checkcycles(void);",
"void crack(int, int, Trans *, short *);",
"void d_sfh(uchar *, int);",
"void d_hash(uchar *, int);",
"void s_hash(uchar *, int);",
"void delq(int);",
"void dot_crack(int, int, Trans *);",
"void do_reach(void);",
"void pan_exit(int);",
"void exit(int);",
"#ifdef BFS_PAR",
" void bfs_setup_mem(void);",
"#endif",
"#ifdef BITSTATE",
" void sinit(void);",
"#else",
" void hinit(void);",
"#endif",
"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 *, uchar *);",
"void select_claim(int);",
"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 do_dfs(int, int, int, short *, uchar *, uchar *);",
"void unrecv(int, int, int, int, int);",
"void usage(FILE *);",
"void wrap_stats(void);\n",
"#ifdef MA",
" int g_store(char *, int, uchar);",
"#endif",
"#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",
"",
"#ifndef NO_V_PROVISO",
" #define V_PROVISO",
"#endif",
"#if !defined(NO_RESIZE) && !defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(SPACE) && !defined(USE_TDH) && NCORE==1",
" #define AUTO_RESIZE",
"#endif",
"",
"typedef struct Trail Trail;",
"typedef struct H_el H_el;",
"",
"struct H_el {",
" H_el *nxt;",
" #ifdef FULLSTACK",
" unsigned int tagged;",
" #if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)",
" unsigned int proviso;", /* uses just 1 bit 0/1 */
" #endif",
" #endif",
" #if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))",
" ulong st_id;",
" #endif",
" #if !defined(SAFETY) || defined(REACH)",
" uint D;",
" #endif",
" #ifdef BCS",
" #ifndef CONSERVATIVE",
" #define CONSERVATIVE 1 /* good for up to 8 processes */",
" #endif",
" #ifdef CONSERVATIVE",
" #if CONSERVATIVE <= 0 || CONSERVATIVE>32",
" #error sensible values for CONSERVATIVE are 1..32 (256/8 = 32)",
" #endif",
" uchar ctx_pid[CONSERVATIVE];", /* pids setting lowest value */
" #endif",
" uchar ctx_low;", /* lowest nr of context switches seen so far */
" #endif",
" #if NCORE>1",
" /* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */",
" #ifdef V_PROVISO",
" uchar cpu_id; /* id of cpu that created the state */",
" #endif",
" #endif",
" #ifdef COLLAPSE",
" #if VECTORSZ<65536",
" ushort ln;", /* length of vector */
" #else",
" ulong ln;", /* length of vector */
" #endif",
" #endif",
" #if defined(AUTO_RESIZE) && !defined(BITSTATE)",
" ulong m_K1;",
" #endif",
" ulong state;",
"};",
"",
"#ifdef BFS_PAR",
"typedef struct BFS_Trail BFS_Trail;",
"struct BFS_Trail {",
" H_el *ostate;",
" int st;",
" int o_tt;",
" T_ID t_id;", /* could be uint, ushort, or uchar */
" uchar pr;",
" uchar o_pm;",
" uchar tau;",
"};",
" #if SYNC>0",
" #undef BFS_NOTRAIL", /* just in case it was used */
" #endif",
"#endif",
"",
"struct Trail {",
" int st; /* current state */",
" int o_tt;",
" uchar pr; /* process id */",
" uchar tau; /* 8 bit-flags */",
" uchar o_pm; /* 8 more bit-flags */",
" #if 0",
" Meaning of bit-flags:",
" tau&1 -> timeout enabled",
" tau&2 -> request to enable timeout 1 level up (in claim)",
" tau&4 -> current transition is a claim move",
" tau&8 -> current transition is an atomic move",
" tau&16 -> last move was truncated on stack",
" tau&32 -> current transition is a preselected move",
" tau&64 -> at least one next state is not on the stack",
" tau&128 -> current transition is a stutter move",
" o_pm&1 -> the current pid moved -- implements else",
" o_pm&2 -> this is an acceptance state",
" o_pm&4 -> this is a progress state",
" o_pm&8 -> fairness alg rule 1 undo mark",
" o_pm&16 -> fairness alg rule 3 undo mark",
" o_pm&32 -> fairness alg rule 2 undo mark",
" o_pm&64 -> the current proc applied rule2",
" o_pm&128 -> a fairness, dummy move - all procs blocked",
" #endif",
" #ifdef NSUCC",
" uchar n_succ; /* nr of successor states */",
" #endif",
" #if defined(FULLSTACK) && defined(MA) && !defined(BFS)",
" uchar proviso;",
" #endif",
" #ifndef BFS",
" uchar o_n, o_ot; /* to save locals */",
" #endif",
" uchar o_m;",
" #ifdef EVENT_TRACE",
" #if nstates_event<256",
" uchar o_event;",
" #else",
" unsigned short o_event;",
" #endif",
" #endif",
" #ifndef BFS",
" short o_To;",
" #ifdef T_RAND",
" short oo_i;",
" #endif",
" #endif",
" #if defined(HAS_UNLESS) && !defined(BFS)",
" int e_state; /* if escape trans - state of origin */",
" #endif",
" #if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)",
" H_el *ostate; /* pointer to stored state */",
" #endif",
/* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY && WS<=4, uses LL[] */
" #if defined(CNTRSTACK) && !defined(BFS)",
" long j6, j7;",
" #endif",
" Trans *o_t;", /* transition fct, next state */
" #if !defined(BFS) && !defined(TRIX_ORIG)",
" char *p_bup;",
" char *q_bup;",
" #endif",
" #ifdef BCS",
" unsigned short sched_limit;",
" unsigned char bcs; /* phase 1 or 2, or forced 4 */",
" unsigned char b_pno; /* preferred pid */",
" #endif",
" #ifdef P_RAND", /* process scheduling randomization */
" unsigned char p_left; /* nr of procs left to explore */",
" short p_skip; /* to find starting point in list */",
" #endif",
" #ifdef HAS_SORTED",
" short ipt;", /* insertion slot in q */
" #endif",
" union {",
" int oval;", /* single backup value of variable */
" int *ovals;", /* ptr to multiple values */
" } bup;",
"}; /* end of struct Trail */",
"",
"#ifdef BFS", /* breadth-first search */
" #if !defined(NOREDUCE) || !defined(BFS_PAR)",
" #define Q_PROVISO",
" #endif",
" #ifndef INLINE_REV",
" #define INLINE_REV",
" #endif",
"",
"typedef struct SV_Hold {",
" State *sv;",
" #ifndef BFS_PAR",
" int sz;",
" #endif",
" struct SV_Hold *nxt;",
"} SV_Hold;",
"#if !defined(BFS_PAR) || NRUNS>0",
" typedef struct EV_Hold {",
" #if !defined(BFS_PAR) || (!defined(NOCOMP) && !defined(HC) && NRUNS>0)",
" char *sv; /* Mask */",
" #endif",
" #if VECTORSZ<65536",
" ushort sz; /* vsize */",
" #else",
" ulong sz;",
" #endif",
" #ifdef BFS_PAR",
" uchar owner;",
" #endif",
" uchar nrpr;",
" uchar nrqs;",
" #if !defined(BFS_PAR) || (!defined(TRIX) && NRUNS>0)",
" char *po, *qo;",
" char *ps, *qs;",
" #endif",
" struct EV_Hold *nxt;",
" } EV_Hold;",
"#endif",
"typedef struct BFS_State {",
" #ifdef BFS_PAR",
" BFS_Trail *t_info;",
" State *osv;",
" #else",
" Trail *frame;",
" SV_Hold *onow;",
" #endif",
" #if !defined(BFS_PAR) || NRUNS>0",
" EV_Hold *omask;",
" #endif",
" #ifdef Q_PROVISO",
" H_el *lstate;",
" #endif",
" #if !defined(BFS_PAR) || SYNC>0",
" short boq;",
" #endif",
" #ifdef VERBOSE",
" ulong nr;",
" #endif",
" #ifndef BFS_PAR", /* new 6.2.4, 3 dec 2012 */
" struct BFS_State *nxt;",
" #endif",
"} BFS_State;",
"#endif\n",
0,
};
static char *SvMap[] = {
"void",
"to_compile(void)",
"{ char ctd[1024], carg[64];",
"#ifdef BITSTATE",
" strcpy(ctd, \"-DBITSTATE \");",
"#else",
" strcpy(ctd, \"\");",
"#endif",
"#ifdef BFS_PAR",
" strcat(ctd, \"-DBFS_PAR \");",
"#endif",
"#ifdef NOVSZ",
" strcat(ctd, \"-DNOVSZ \");",
"#endif",
"#ifdef REVERSE",
" strcat(ctd, \"-DREVERSE \");",
"#endif",
" if (t_reverse)",
" { strcat(ctd, \"-DT_REVERSE \");",
" }",
"#ifdef T_RAND",
" #if T_RAND>0",
" sprintf(carg, \"-DT_RAND=%%d \", T_RAND);",
" strcat(ctd, carg);",
" #else",
" strcat(ctd, \"-DT_RAND \");",
" #endif",
"#endif",
"#ifdef P_RAND",
" #if P_RAND>0",
" sprintf(carg, \"-DP_RAND=%%d \", P_RAND);",
" strcat(ctd, carg);",
" #else",
" strcat(ctd, \"-DP_RAND \");",
" #endif",
"#endif",
"#ifdef BCS",
" sprintf(carg, \"-DBCS=%%d \", BCS);",
" strcat(ctd, carg);",
"#endif",
"#ifdef BFS",
" strcat(ctd, \"-DBFS \");",
"#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 HC",
" strcat(ctd, \"-DHC \");",
"#endif",
"#ifdef CHECK",
" strcat(ctd, \"-DCHECK \");",
"#endif",
"#ifdef CTL",
" strcat(ctd, \"-DCTL \");",
"#endif",
"#ifdef TRIX",
" strcat(ctd, \"-DTRIX \");",
"#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 COLLAPSE",
" strcat(ctd, \"-DCOLLAPSE \");",
"#endif",
"#ifdef MA",
" sprintf(carg, \"-DMA=%%d \", MA);",
" strcat(ctd, carg);",
"#endif",
"#ifdef SVDUMP",
" strcat(ctd, \"-DSVDUMP \");",
"#endif",
"#if defined(VECTORSZ) && !defined(TRIX)",
" 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",
"#if NCORE>1",
" sprintf(carg, \"-DNCORE=%%d \", NCORE);",
" strcat(ctd, carg);",
"#endif",
"#ifdef VMAX",
" if (VMAX != 256)",
" { sprintf(carg, \"-DVMAX=%%d \", VMAX);",
" strcat(ctd, carg);",
" }",
"#endif",
"#ifdef PMAX",
" if (PMAX != 16)",
" { sprintf(carg, \"-DPMAX=%%d \", PMAX);",
" strcat(ctd, carg);",
" }",
"#endif",
"#ifdef QMAX",
" if (QMAX != 16)",
" { sprintf(carg, \"-DQMAX=%%d \", QMAX);",
" strcat(ctd, carg);",
" }",
"#endif",
"#ifdef SET_WQ_SIZE",
" sprintf(carg, \"-DSET_WQ_SIZE=%%d \", SET_WQ_SIZE);",
" strcat(ctd, carg);",
"#endif",
" printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);",
"}",
0,
};
|
