/***** spin: spinlex.c *****/ /* Copyright (c) 1991,1995 by AT&T Corporation.  All Rights Reserved.     *//* This software is for educational purposes only.                        *//* Permission is given to distribute this code provided that this intro-  *//* ductory message is not removed and no monies are exchanged.            *//* No guarantee is expressed or implied by the distribution of this code. *//* Software written by Gerard J. Holzmann as part of the book:            *//* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4,     *//* Prentice Hall, Englewood Cliffs, NJ, 07632.                            *//* Send bug-reports and/or questions to: gerard@research.att.com          */ #include "spin.h"#include "y.tab.h" int		lineno=1;unsigned char	in_comment=0;char		yytext[512];FILE		*yyin  = {stdin};FILE		*yyout = {stdout}; extern Symbol	*Fname;extern YYSTYPE	yylval;extern int	has_last; extern int	isdigit(int);extern int	isalpha(int);extern int	isalnum(int); #define Token(y)	{ yylval = nn(ZN,0,ZN,ZN); \			if (!in_comment) return y; else goto again; } #define ValToken(x, y)	{ yylval = nn(ZN,0,ZN,ZN); yylval->val = x; \			if (!in_comment) return y; else goto again; } #define SymToken(x, y)	{ yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; \			if (!in_comment) return y; else goto again; } #define Getchar()	getc(yyin)#define Ungetch(c)	ungetc(c, yyin) intnotquote(int c){	return (c != '\"' && c != '\n');} intisalnum_(int c){	return (isalnum(c) || c == '_');} voidgetword(int first, int (*tst)(int)){	int i=0; char c; 	yytext[i++]= first;	while (tst(c = Getchar()))		yytext[i++] = c;	yytext[i] = '\0';	Ungetch(c);} intfollow(int tok, int ifyes, int ifno){	int c; 	if ((c = Getchar()) == tok)		return ifyes;	Ungetch(c); 	return ifno;} intlex(void){	int c; again:	c = Getchar();	yytext[0] = c;	yytext[1] = '\0';	switch (c) {	case '\n':		/* newline */		lineno++;		goto again; 	case  ' ': case '\t':	/* white space */		goto again; 	case '#':		/* preprocessor directive */		getword(c, isalpha);		if (Getchar() != ' ')			fatal("malformed preprocessor directive - # .", 0);		if (!isdigit(c = Getchar()))			fatal("malformed preprocessor directive - # .lineno", 0);		getword(c, isdigit);		lineno = atoi(yytext);		/* removed -1 */		c = Getchar();		if (c == '\n') goto again;	/* no filename */ 		if (c != ' ')			fatal("malformed preprocessor directive - .fname", 0);		if ((c = Getchar()) != '\"')			fatal("malformed preprocessor directive - .fname", 0);		getword(c, notquote);		if (Getchar() != '\"')			fatal("malformed preprocessor directive - fname.", 0);		strcat(yytext, "\"");		Fname = lookup(yytext);		while (Getchar() != '\n')			;		goto again; 	case '\"':		getword(c, notquote);		if (Getchar() != '\"')			fatal("string not terminated", yytext);		strcat(yytext, "\"");		SymToken(lookup(yytext), STRING); 	default:		break;	} 	if (isdigit(c))	{	getword(c, isdigit);		ValToken(atoi(yytext), CONST);	} 	if (isalpha(c) || c == '_')	{	getword(c, isalnum_);		if (!in_comment)			return check_name(yytext);		else goto again;	} 	switch (c) {	case '/': c = follow('*', 0, '/');		  if (!c) { in_comment = 1; goto again; }		  break;	case '*': c = follow('/', 0, '*');		  if (!c) { in_comment = 0; goto again; }		  break;	case ':': c = follow(':', SEP, ':'); break;	case '-': c = follow('>', SEMI, follow('-', DECR, '-')); break;	case '+': c = follow('+', INCR, '+'); break;	case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break;	case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break;	case '=': c = follow('=', EQ, ASGN); break;	case '!': c = follow('=', NE, follow('!', O_SND, SND)); break;	case '?': c = follow('?', R_RCV, RCV); break;	case '&': c = follow('&', AND, '&'); break;	case '|': c = follow('|', OR, '|'); break;	case ';': c = SEMI; break;	default : break;	}	Token(c);} static struct {	char *s;	int tok;	int val;	char *sym;} Names[] = {	"active",	ACTIVE,		0,		0,	"assert",	ASSERT,		0,		0,	"atomic",	ATOMIC,		0,		0,	"bit",		TYPE,		BIT,		0,	"bool",		TYPE,		BIT,		0,	"break",	BREAK,		0,		0,	"byte",		TYPE,		BYTE,		0,	"do",		DO,		0,		0,	"chan",		TYPE,		CHAN,		0,	"else", 	ELSE,		0,		0,	"empty",	EMPTY,		0,		0,	"enabled",	ENABLED,	0,		0,	"fi",		FI,		0,		0,	"full",		FULL,		0,		0,	"goto",		GOTO,		0,		0,	"hidden",	HIDDEN,		0,		0,	"if",		IF,		0,		0,	"init",		INIT,		0,		":init:",	"int",		TYPE,		INT,		0,	"len",		LEN,		0,		0,	"mtype",	MTYPE,		0,		0,	"nempty",	NEMPTY,		0,		0,	"never",	CLAIM,		0,		":never:",	"nfull",	NFULL,		0,		0,	"od",		OD,		0,		0,	"of",		OF,		0,		0,	"pc_value",	PC_VAL,		0,		0,	"printf",	PRINT,		0,		0,	"proctype",	PROCTYPE,	0,		0,	"run",		RUN,		0,		0,	"d_step",	D_STEP,		0,		0,	"short",	TYPE,		SHORT,		0,	"skip",		CONST,		1,		0,	"timeout",	TIMEOUT,	0,		0,	"typedef",	TYPEDEF,	0,		0,	"unless",	UNLESS,		0,		0,	"xr",		XU,		XR,		0,	"xs",		XU,		XS,		0,	0, 		0,		0,		0,}; intcheck_name(char *s){	register int i; 	yylval = nn(ZN, 0, ZN, ZN);	for (i = 0; Names[i].s; i++)		if (strcmp(s, Names[i].s) == 0)		{	yylval->val = Names[i].val;			if (Names[i].sym)				yylval->sym = lookup(Names[i].sym);			return Names[i].tok;		} 	if (yylval->val = ismtype(s))	{	yylval->ismtyp = 1;		return CONST;	} 	if (strcmp(s, "_last") == 0)		has_last++; 	yylval->sym = lookup(s);	/* symbol table */ 	if (isutype(s))		return UNAME;	if (isproctype(s))		return PNAME; 	return NAME;} intyylex(void){	static int last = 0;	static int hold = 0;	int c; 	/*	 * repair two common syntax mistakes with	 * semi-colons before or after a '}'	 */ 	if (hold)	{	c = hold;		hold = 0;	} else	{	c = lex();		if (last == ELSE		&&  c != SEMI		&&  c != FI)		{	hold = c;			last = 0;			return SEMI;		}		if (last == '}'		&&  c != PROCTYPE		&&  c != INIT		&&  c != CLAIM		&&  c != SEP		&&  c != FI		&&  c != OD		&&  c != '}'		&&  c != UNLESS		&&  c != SEMI		&&  c != EOF)		{	hold = c;			last = 0;			return SEMI;	/* insert ';' */		}		if (c == SEMI)		{	extern Symbol *context, *owner;			/* if context, we're not in a typedef			 * because they're global.			 * if owner, we're at the end of a ref			 * to a struct field -- prevent that the			 * lookahead is interpreted as a field of			 * the same struct...			 */			if (context) owner = ZS;			hold = lex();	/* look ahead */			if (hold == '}'			||  hold == SEMI)			{	c = hold; /* omit ';' */				hold = 0;			}		}	}	last = c;	return c;}