pangen1.h

对软件进行可达性测试的软件

	"			sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
	"			goto try_again;",
	"		}",
	"		printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
	"		pan_exit(1);",
	"	}",
	"#if NCORE>1 && defined(SEP_STATE)",
	"	{	void set_root(void); /* for partial traces from local root */",
	"		set_root();",
	"	}",
	"#endif",
	"	return fd;",
	"}",
	"",
	"uchar do_transit(Trans *, short);",
	"",
	"void",
	"getrail(void)",
	"{	FILE *fd;",
	"	char *q;",
	"	int i, t_id, lastnever=-1; short II;",
	"	Trans *t;",
	"	P0 *z;",
	"",
	"	fd = findtrail();	/* exits if unsuccessful */",
	"	while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
	"	{	if (depth == -1)",
	"			printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
	"		if (depth < 0)",
	"			continue;",
	"		if (i > now._nr_pr)",
	"		{	printf(\"pan: Error, proc %%d invalid pid \", i);",
	"			printf(\"transition %%d\\n\", t_id);",
	"			break;",
	"		}",
	"		II = i;",
	"		z = (P0 *)pptr(II);",
	"		for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
	"			if (t->t_id == (T_ID) t_id)",
	"				break;",
	"		if (!t)",
	"		{	for (i = 0; i < NrStates[z->_t]; i++)",
	"			{	t = trans[z->_t][i];",
	"				if (t && t->t_id == (T_ID) t_id)",
	"				{	printf(\"	Recovered at state %%d\\n\", i);",
	"					z->_p = i;",
	"					goto recovered;",
	"			}	}",
	"			printf(\"pan: Error, proc %%d type %%d state %%d: \",",
	"				II, z->_t, z->_p);",
	"			printf(\"transition %%d not found\\n\", t_id);",
	"			printf(\"pan: list of possible transitions in this process:\\n\");",
	"			if (z->_t >= 0 && z->_t <= _NP_)",
	"			for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
	"				printf(\"	t_id %%d -- case %%d, [%%s]\\n\",",
	"					t->t_id, t->forw, t->tp);",
	"			break; /* pan_exit(1); */",
	"		}",
	"recovered:",
	"		q = transmognify(t->tp);",
	"		if (gui) simvals[0] = \'\\0\';",

	"		this = pptr(II);",
	"		trpt->tau |= 1;",	/* timeout always possible */
	"		if (!do_transit(t, II))",
	"		{	if (onlyproc >= 0 && II != onlyproc)",
	"				goto moveon;",
	"			printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
	"			printf(\"     most likely causes: missing c_track statements\\n\");",
	"			printf(\"       or illegal side-effects in c_expr statements\\n\");",
	"		}",

	"		if (onlyproc >= 0 && II != onlyproc)",
	"			goto moveon;",

	"		if (verbose)",
	"		{	printf(\"%%3ld: proc %%2d (%%s) \", depth, II, procname[z->_t]);",

	"			for (i = 0; src_all[i].src; i++)",
	"				if (src_all[i].tp == (int) z->_t)",
	"				{	printf(\" line %%3d \\\"%%s\\\" \",",
	"						src_all[i].src[z->_p], PanSource);",
	"					break;",
	"				}",

	"			printf(\"(state %%d) trans {%%d,%%d} [%%s]\\n\",",
	"				z->_p, t_id, t->forw, q?q:\"\");",

	"			c_globals();",
	"			for (i = 0; i < now._nr_pr; i++)",
	"			{	c_locals(i, ((P0 *)pptr(i))->_t);",
	"			}",
	"		} else",
	"		if (strcmp(procname[z->_t], \":never:\") == 0)",
	"		{	if (lastnever != (int) z->_p)",
	"			{	for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\"MSC: ~G %%d\\n\",",
	"							src_all[i].src[z->_p]);",
	"						break;",
	"					}",
	"				if (!src_all[i].src)",
	"					printf(\"MSC: ~R %%d\\n\", z->_p);",
	"			}",
	"			lastnever = z->_p;",
	"			goto sameas;",
	"		} else",
	"		if (strcmp(procname[z->_t], \":np_:\") != 0)",
	"		{",
	"sameas:		if (no_rck) goto moveon;",
	"			if (coltrace)",
	"			{	printf(\"%%ld: \", depth);",
	"				for (i = 0; i < II; i++)",
	"					printf(\"\\t\\t\");",
	"				printf(\"%%s(%%d):\", procname[z->_t], II);",
	"				printf(\"[%%s]\\n\", q?q:\"\");",
	"			} else if (!silent)",
	"			{	if (strlen(simvals) > 0) {",
	"				printf(\"%%3ld:	proc %%2d (%%s)\", ",
	"					depth, II, procname[z->_t]);",
	"				for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\" line %%3d \\\"%%s\\\" \",",
	"							src_all[i].src[z->_p], PanSource);",
	"						break;",
	"					}",
	"				printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
	"				}",
	"				printf(\"%%3ld:	proc %%2d (%%s)\", ",
	"					depth, II, procname[z->_t]);",
	"				for (i = 0; src_all[i].src; i++)",
	"					if (src_all[i].tp == (int) z->_t)",
	"					{	printf(\" line %%3d \\\"%%s\\\" \",",
	"							src_all[i].src[z->_p], PanSource);",
	"						break;",
	"					}",
	"				printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
	"			/*	printf(\"\\n\");	*/",
	"		}	}",
	"moveon:	z->_p = t->st;",
	"	}",
	"	wrap_trail();",
	"}",
	"#endif",
	"int",
	"f_pid(int pt)",
	"{	int i;",
	"	P0 *z;",
	"	for (i = 0; i < now._nr_pr; i++)",
	"	{	z = (P0 *)pptr(i);",
	"		if (z->_t == (unsigned) pt)",
	"			return BASE+z->_pid;",
	"	}",
	"	return -1;",
	"}",
	"#ifdef VERI",
	"void check_claim(int);",
	"#endif",
	"",
	"#if defined(SFH) && !defined(HASH64) && !defined(NOCOMP)",
	"	#define NOCOMP	/* go for speed */",
	"#endif",
	"",
	"#ifdef BITSTATE",
#ifndef POWOW
	"int",
	"bstore_mod(char *v, int n)	/* hasharray size not a power of two */",
	"{	unsigned long x, y;",
	"	unsigned int i = 1;",
	"",
	"#if defined(SFH) && !defined(HASH64)",
	"	d_sfh((const char *) v, n);",
	"#else",
	"	d_hash((uchar *) v, n); /* sets j3, j4, K1, K2 */",
	"#endif",
	"	x = K1; y = j3;",	/* was K2 before 5.1.1 */
	"	for (;;)",
	"	{	if (!(SS[x%%udmem]&(1<<y))) break;",	/* take the hit in speed */
	"		if (i == hfns) {",
				"#ifdef DEBUG",
	"			printf(\"Old bitstate\\n\");",
				"#endif",
	"			return 1;",
	"		}",
	"		x = (x + K2 + i);",	/* no mask, using mod - was K1 before 5.1.1 */
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef RANDSTOR",
	"	if (rand()%%100 > RANDSTOR) return 0;",
		"#endif",
	"	for (;;)",
	"	{	SS[x%%udmem] |= (1<<y);",
	"		if (i == hfns) break;",	/* done */
	"		x = (x + K2 + i);",	/* no mask - was K1 before 5.1.1 */
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef DEBUG",
	"	printf(\"New bitstate\\n\");",
		"#endif",
	"	if (now._a_t&1)",
	"	{	nShadow++;",
	"	}",
	"	return 0;",
	"}",
#endif
	"int",
	"bstore_reg(char *v, int n)	/* extended hashing, Peter Dillinger, 2004 */",
	"{	unsigned long x, y;",
	"	unsigned int i = 1;",
	"",
	"#if defined(SFH) && !defined(HASH64)",
	"	d_sfh((const char *) v, n);",
	"#else",
	"	d_hash((uchar *) v, n); /* sets j1-j4 */",
	"#endif",
	"	x = j2; y = j3;",
	"	for (;;)",
	"	{	if (!(SS[x]&(1<<y))) break;",	/* at least one bit not set */
	"		if (i == hfns) {",
				"#ifdef DEBUG",
	"			printf(\"Old bitstate\\n\");",
				"#endif",
	"			return 1;",
	"		}",
	"		x = (x + j1 + i) & nmask;",
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef RANDSTOR",
	"	if (rand()%%100 > RANDSTOR) return 0;",
		"#endif",
	"	for (;;)",
	"	{	SS[x] |= (1<<y);",
	"		if (i == hfns) break;",		/* done */
	"		x = (x + j1 + i) & nmask;",
	"		y = (y + j4) & 7;",
	"		i++;",
	"	}",
		"#ifdef DEBUG",
	"	printf(\"New bitstate\\n\");",
		"#endif",
	"	if (now._a_t&1)",
	"	{	nShadow++;",
	"	}",
	"	return 0;",
	"}",
	"#endif",
	"unsigned long TMODE = 0666; /* file permission bits for trail files */",
	"",
	"int trcnt=1;",
	"char snap[64], fnm[512];",
	"",
	"int",
	"make_trail(void)",
	"{	int fd;",
	"	char *q;",
	"	char MyFile[512];",
	"",
	"	q = strrchr(TrailFile, \'/\');",
	"	if (q == NULL) q = TrailFile; else q++;",
	"	strcpy(MyFile, q); /* TrailFile is not a writable string */",
	"",
	"	if (iterative == 0 && Nr_Trails++ > 0)",
	"		sprintf(fnm, \"%%s%%d.%%s\",",
	"			MyFile, Nr_Trails-1, tprefix);",
	"	else",
	"		sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"",
	"	if ((fd = creat(fnm, TMODE)) < 0)",
	"	{	if ((q = strchr(MyFile, \'.\')))",
	"		{	*q = \'\\0\';",		/* strip .pml */
	"			if (iterative == 0 && Nr_Trails-1 > 0)",
	"				sprintf(fnm, \"%%s%%d.%%s\",",
	"					MyFile, Nr_Trails-1, tprefix);",
	"			else",
	"				sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
	"			*q = \'.\';",
	"			fd = creat(fnm, TMODE);",
	"	}	}",
	"	if (fd < 0)",
	"	{	printf(\"pan: cannot create %%s\\n\", fnm);",
	"		perror(\"cause\");",
	"	} else",
	"	{",
	"#if NCORE>1 && (defined(SEP_STATE) || !defined(FULL_TRAIL))",
	"	void write_root(void); ",
	"	write_root();",
	"#else",
	"		printf(\"pan: wrote %%s\\n\", fnm);",
	"#endif",
	"	}",
	"	return fd;",
	"}",
	0
};

static char *Code2b[] = {	/* breadth-first search option */
	"#ifdef BFS",
	"#define Q_PROVISO",
	"#ifndef INLINE_REV",
	"#define INLINE_REV",
	"#endif",
	"",
	"typedef struct SV_Hold {",
	"	State *sv;",
	"	int  sz;",
	"	struct SV_Hold *nxt;",
	"} SV_Hold;",
	"",
	"typedef struct EV_Hold {",
	"	char *sv;",	/* Mask */
	"	int  sz;",	/* vsize */
	"	int nrpr;",
	"	int nrqs;",
	"	char *po;",
	"	char *qo;",
	"	char *ps, *qs;",
	"	struct EV_Hold *nxt;",
	"} EV_Hold;",
	"",
	"typedef struct BFS_Trail {",
	"	Trail	*frame;",
	"	SV_Hold *onow;",
	"	EV_Hold *omask;",
	"#ifdef Q_PROVISO",
	"	struct H_el *lstate;",
	"#endif",
	"	short boq;",
	"	struct BFS_Trail *nxt;",
	"} BFS_Trail;",
	"",
	"BFS_Trail *bfs_trail, *bfs_bot, *bfs_free;",
	"",
	"SV_Hold *svhold, *svfree;",
	"",
	"uchar do_reverse(Trans *, short, uchar);",
	"void snapshot(void);",
	"",
	"SV_Hold *",
	"getsv(int n)",
	"{	SV_Hold *h = (SV_Hold *) 0, *oh;",
	"",
	"	oh = (SV_Hold *) 0;",
	"	for (h = svfree; h; oh = h, h = h->nxt)",
	"	{	if (n == h->sz)",
	"		{	if (!oh)",
	"				svfree = h->nxt;",
	"			else",
	"				oh->nxt = h->nxt;",
	"			h->nxt = (SV_Hold *) 0;",
	"			break;",
	"		}",
	"		if (n < h->sz)",
	"		{	h = (SV_Hold *) 0;",
	"			break;",
	"		}",
	"		/* else continue */",
	"	}",
	"",
	"	if (!h)",
	"	{	h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
	"		h->sz = n;",
	"		h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
	"	}",
	"	return h;",
	"}",
	"",
	"EV_Hold *",
	"getsv_mask(int n)",
	"{	EV_Hold *h;",
	"	static EV_Hold *kept = (EV_Hold *) 0;",
	"",
	"	for (h = kept; h; h = h->nxt)",
	"		if (n == h->sz",
	"		&&  (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
	"		&&  (now._nr_pr == h->nrpr)",
	"		&&  (now._nr_qs == h->nrqs)",
	"#if VECTORSZ>32000",
	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
	"#else",
	"		&&  (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
	"		&&  (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
	"#endif",
	"		&&  (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
	"		&&  (memcmp((char *) q_skip,    (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
	"			break;",
	"	if (!h)",
	"	{	h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
	"		h->sz = n;",
	"		h->nrpr = now._nr_pr;",
	"		h->nrqs = now._nr_qs;",
	"",
	"		h->sv = (char *) emalloc(n * sizeof(char));",
	"		memcpy((char *) h->sv, (char *) Mask, n);",
	"",
	"		if (now._nr_pr > 0)",
	"		{	h->ps = (char *) emalloc(now._nr_pr * sizeof(int));",
	"			memcpy((char *) h->ps, (char *) proc_skip,   now._nr_pr * sizeof(uchar));",
	"#if VECTORSZ>32000",
	"			h->po = (char *) emalloc(now._nr_pr * sizeof(int));",
	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
	"#else",
	"			h->po = (char *) emalloc(now._nr_pr * sizeof(short));",
	"			memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
	"#endif",
	"		}",
	"		if (now._nr_qs > 0)",
	"		{	h->qs = (char *) emalloc(now._nr_qs * sizeof(int));",
	"			memcpy((char *) h->qs, (char *) q_skip,   now._nr_qs * sizeof(uchar));",
	"#if VECTORSZ>32000",
	"			h->qo = (char *) emalloc(now._nr_qs * sizeof(int));",
	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
	"#else",
	"			h->qo = (char *) emalloc(now._nr_qs * sizeof(short));",
	"			memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
	"#endif",
	"		}",
	"",
	"		h->nxt = kept;",
	"		kept = h;",
	"	}",
	"	return h;",
	"}",
	"",
	"void",
	"freesv(SV_Hold *p)",
	"{	SV_Hold *h, *oh;",
	"",
	"	oh = (SV_Hold *) 0;",
	"	for (h = svfree; h; oh = h, h = h->nxt)",
	"		if (h->sz >= p->sz)",
	"			break;",
	"",
	"	if (!oh)",
	"	{	p->nxt = svfree;",
	"		svfree = p;",
	"	} else",
	"	{	p->nxt = h;",
	"		oh->nxt = p;",
	"	}",
	"}",
	"",
	"BFS_Trail *",
	"get_bfs_frame(void)",
	"{	BFS_Trail *t;",
	"",
	"	if (bfs_free)",
	"	{	t = bfs_free;",
	"		bfs_free = bfs_free->nxt;",
	"		t->nxt = (BFS_Trail *) 0;",
	"	} else",
	"	{	t = (BFS_Trail *) emalloc(sizeof(BFS_Trail));",
	"	}",
	"	t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
	"	return t;",
	"}",
	"",
	"void",
	"push_bfs(Trail *f, int d)",
	"{	BFS_Trail *t;",
	"",
	"	t = get_bfs_frame();",
	"	memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
	"	t->frame->o_tt = d;	/* depth */",
	"",
	"	t->boq = boq;",
	"	t->onow = getsv(vsize);",
	"	memcpy((char *)t->onow->sv, (char *)&now, vsize);",
	"	t->omask = getsv_mask(vsize);",
	"#if defined(FULLSTACK) && defined(Q_PROVISO)",
	"	t->lstate = Lstate;",
	"#endif",
	"	if (!bfs_bot)",
	"	{	bfs_bot = bfs_trail = t;",
	"	} else",
	"	{	bfs_bot->nxt = t;",
	"		bfs_bot = t;",
	"	}",
	"#ifdef CHECK",
	"	printf(\"PUSH %%u (%%d)\\n\", t->frame, d);",
	"#endif",
	"}",
	"",
	"Trail *",
	"pop_bfs(void)",
	"{	BFS_Trail *t;",
	"",
	"	if (!bfs_trail)",
	"		return (Trail *) 0;",
	"",