/***** 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 <sys/types.h>#include <sys/stat.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);extern char	CurScope[MAXSCOPESZ]; 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	old_scope_rules;	/* use pre 5.3.0 rules */int	split_decl = 1, product, Strict; int	merger = 1, deadvar = 1;int	ccache = 0; /* oyvind teig: 5.2.0 case caching off by default */ static int preprocessonly, SeedUsed;static int seedy;	/* be verbose about chosen seed */static int inlineonly;	/* show inlined code */static int dataflow = 1; #if 0meaning 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	*ltl_claims = (char *) 0;static FILE	*fd_ltl = (FILE *) 0;static char	*PreArg[64];static int	PreCnt = 0;static char	out1[64]; char	**trailfilename;	/* new option 'k' */ void	explain(int); 	/* to use visual C++:		#define CPP	"CL -E/E"	   or call spin as:	"spin -PCL  -E/E" 	   on OS2:		#define CPP	"icc -E/Pd+ -E/Q+"	   or call spin as:	"spin -Picc -E/Pd+ -E/Q+"	*/#ifndef CPP	#if defined(PC) || defined(MAC)		#define CPP	"gcc -E -x c"	/* most systems have gcc or cpp */		/* if gcc-4 is available, this setting is modified below */	#else		#ifdef SOLARIS			#define CPP	"/usr/ccs/lib/cpp"		#else			#if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__)				#define CPP	"cpp"			#else				#define CPP	"/bin/cpp"	/* classic Unix systems */			#endif		#endif	#endif#endif static char	*PreProc = CPP;extern int	depth; /* at least some steps were made */ voidalldone(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);} voidpreprocess(char *a, char *b, int a_tmp){	char precmd[1024], cmd[2048]; int i;#if defined(WIN32) || defined(WIN64)	struct _stat x;/*	struct stat x;	*/#endif#ifdef PC	extern int try_zpp(char *, char *);	if (PreCnt == 0 && try_zpp(a, b))	{	goto out;	}#endif#if defined(WIN32) || defined(WIN64)	if (strncmp(PreProc, "gcc -E -x c", strlen("gcc -E -x c")) == 0)	{	if (stat("/bin/gcc-4.exe", (struct stat *)&x) == 0	/* for PCs with cygwin */		||  stat("c:/cygwin/bin/gcc-4.exe", (struct stat *)&x) == 0)		{	PreProc = "gcc-4 -E -x c";		} else if (stat("/bin/gcc-3.exe", (struct stat *)&x) == 0		       ||  stat("c:/cygwin/bin/gcc-3.exe", (struct stat *)&x) == 0)		{	PreProc = "gcc-3 -E -x c";	}	}#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 PCout:#endif	if (a_tmp) (void) unlink((const char *) a);} voidusage(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-e compute synchronous product of multiple never claims (modified by -L)\n");	printf("\t-f \"..formula..\"  translate LTL ");	printf("into never claim\n");	printf("\t-F file  like -f, but with the LTL 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-k fname use the trailfile stored in file fname, see also -t\n");	printf("\t-L when using -e, use strict language intersection\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 fname use never claim stored in file fname\n");	printf("\t-nN seed for random nr generator\n");	printf("\t-O use old scope rules (pre 5.3.0)\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-o4 turn on rendezvous optiomizations in verifier\n");	printf("\t-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)\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, see also -k\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);} voidoptimizations(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;	}} intmain(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;	strcpy(CurScope, "_"); 	/* unused flags: y, z, G, L, Q, R, 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 'e': product++; break; /* see also 'L' */		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 'k': s_trail = 1;			  trailfilename = (char **) (argv+2);			  argc--; argv++; break;		case 'L': Strict++; break; /* modified -e */		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': old_scope_rules = 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((int) 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((int)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;#if 0		case 'x': split_decl = 0; break;	/* experimental */#endif		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);		}		if (!fgets(formula, 4096, tl_out))		{	printf("spin: cannot read %s\n", *ltl_file);		}		fclose(tl_out);		tl_out = stdout;		*ltl_file = (char *) formula;	}	if (argc > 1)	{	FILE *fd = stdout;		char cmd[512], out2[512]; 		/* must remain in current dir */		strcpy(out1, "pan.pre"); 		if (add_ltl || nvr_file)		{	sprintf(out2, "%s.nvr", argv[1]);			if ((fd = fopen(out2, MFLAGS)) == NULL)			{	printf("spin: cannot create tmp file %s\n",					out2);				alldone(1);			}			fprintf(fd, "#include \"%s\"\n", argv[1]);		} 		if (add_ltl)		{	tl_out = fd;			nr_errs = tl_main(2, add_ltl);			fclose(fd);			preprocess(out2, out1, 1);		} else if (nvr_file)		{	fprintf(fd, "#include \"%s\"\n", *nvr_file);			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);		fprintf(stderr, "spin: error, no filename specified");		fflush(stdout);		alldone(1);	}	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); 	if (ltl_claims)	{	Symbol *r;		fclose(fd_ltl);		if (!(yyin = fopen(ltl_claims, "r")))		{	fatal("cannot open %s", ltl_claims);		}		r = oFname;		oFname = Fname = lookup(ltl_claims);		lineno = 0;		yyparse();		fclose(yyin);		oFname = Fname = r;		if (0)		{	(void) unlink(ltl_claims);	}	} 	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;

Lines 1–500 of 860. Load more