xref: /plan9-contrib/sys/src/cmd/spin/spin.y (revision de2caf28f9ba1a56e70be94a699435d36eb50311)
1 /***** spin: spin.y *****/
2 
3 /*
4  * This file is part of the public release of Spin. It is subject to the
5  * terms in the LICENSE file that is included in this source directory.
6  * Tool documentation is available at http://spinroot.com
7  */
8 
9 %{
10 #include "spin.h"
11 #include <sys/types.h>
12 #ifndef PC
13 #include <unistd.h>
14 #endif
15 #include <stdarg.h>
16 
17 #define YYMAXDEPTH	20000	/* default is 10000 */
18 #define YYDEBUG		0
19 #define Stop	nn(ZN,'@',ZN,ZN)
20 #define PART0	"place initialized declaration of "
21 #define PART1	"place initialized chan decl of "
22 #define PART2	" at start of proctype "
23 
24 static	Lextok *ltl_to_string(Lextok *);
25 
26 extern  Symbol	*context, *owner;
27 extern	Lextok *for_body(Lextok *, int);
28 extern	void for_setup(Lextok *, Lextok *, Lextok *);
29 extern	Lextok *for_index(Lextok *, Lextok *);
30 extern	Lextok *sel_index(Lextok *, Lextok *, Lextok *);
31 extern  void    keep_track_off(Lextok *);
32 extern	void	safe_break(void);
33 extern	void	restore_break(void);
34 extern  int	u_sync, u_async, dumptab, scope_level;
35 extern	int	initialization_ok;
36 extern	short	has_sorted, has_random, has_enabled, has_pcvalue, has_np, has_priority;
37 extern	short	has_code, has_state, has_ltl, has_io;
38 extern	void	check_mtypes(Lextok *, Lextok *);
39 extern	void	count_runs(Lextok *);
40 extern	void	no_internals(Lextok *);
41 extern	void	any_runs(Lextok *);
42 extern	void	explain(int);
43 extern	void	ltl_list(char *, char *);
44 extern	void	validref(Lextok *, Lextok *);
45 extern  void	sanity_check(Lextok *);
46 extern	char	yytext[];
47 
48 int	Mpars = 0;	/* max nr of message parameters  */
49 int	nclaims = 0;	/* nr of never claims */
50 int	ltl_mode = 0;	/* set when parsing an ltl formula */
51 int	Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
52 int	in_for = 0, in_seq = 0, par_cnt = 0;
53 int	dont_simplify = 0;
54 char	*claimproc = (char *) 0;
55 char	*eventmap = (char *) 0;
56 
57 static	char *ltl_name;
58 static	int  Embedded = 0, inEventMap = 0, has_ini = 0;
59 
60 %}
61 
62 %token	ASSERT PRINT PRINTM PREPROC
63 %token	C_CODE C_DECL C_EXPR C_STATE C_TRACK
64 %token	RUN LEN ENABLED SET_P GET_P EVAL PC_VAL
65 %token	TYPEDEF MTYPE INLINE RETURN LABEL OF
66 %token	GOTO BREAK ELSE SEMI ARROW
67 %token	IF FI DO OD FOR SELECT IN SEP DOTDOT
68 %token	ATOMIC NON_ATOMIC D_STEP UNLESS
69 %token  TIMEOUT NONPROGRESS
70 %token	ACTIVE PROCTYPE D_PROCTYPE
71 %token	HIDDEN SHOW ISLOCAL
72 %token	PRIORITY PROVIDED
73 %token	FULL EMPTY NFULL NEMPTY
74 %token	CONST TYPE XU			/* val */
75 %token	NAME UNAME PNAME INAME		/* sym */
76 %token	STRING CLAIM TRACE INIT	LTL	/* sym */
77 
78 %right	ASGN
79 %left	SND O_SND RCV R_RCV /* SND doubles as boolean negation */
80 %left	IMPLIES EQUIV			/* ltl */
81 %left	OR
82 %left	AND
83 %left	ALWAYS EVENTUALLY		/* ltl */
84 %left	UNTIL WEAK_UNTIL RELEASE	/* ltl */
85 %right	NEXT				/* ltl */
86 %left	'|'
87 %left	'^'
88 %left	'&'
89 %left	EQ NE
90 %left	GT LT GE LE
91 %left	LSHIFT RSHIFT
92 %left	'+' '-'
93 %left	'*' '/' '%'
94 %left	INCR DECR
95 %right	'~' UMIN NEG
96 %left	DOT
97 %%
98 
99 /** PROMELA Grammar Rules **/
100 
101 program	: units		{ yytext[0] = '\0'; }
102 	;
103 
104 units	: unit
105 	| units unit
106 	;
107 
108 unit	: proc		/* proctype { }       */
109 	| init		/* init { }           */
110 	| claim		/* never claim        */
111 	| ltl		/* ltl formula        */
112 	| events	/* event assertions   */
113 	| one_decl	/* variables, chans   */
114 	| utype		/* user defined types */
115 	| c_fcts	/* c functions etc.   */
116 	| ns		/* named sequence     */
117 	| semi		/* optional separator */
118 	| error
119 	;
120 
121 l_par	: '('		{ par_cnt++; }
122 	;
123 
124 r_par	: ')'		{ par_cnt--; }
125 	;
126 
127 
128 proc	: inst		/* optional instantiator */
129 	  proctype NAME	{
130 			  setptype(ZN, $3, PROCTYPE, ZN);
131 			  setpname($3);
132 			  context = $3->sym;
133 			  context->ini = $2; /* linenr and file */
134 			  Expand_Ok++; /* expand struct names in decl */
135 			  has_ini = 0;
136 			}
137 	  l_par decl r_par	{ Expand_Ok--;
138 			  if (has_ini)
139 			  fatal("initializer in parameter list", (char *) 0);
140 			}
141 	  Opt_priority
142 	  Opt_enabler
143 	  body		{ ProcList *rl;
144 			  if ($1 != ZN && $1->val > 0)
145 			  {	int j;
146 				rl = mk_rdy($3->sym, $6, $11->sq, $2->val, $10, A_PROC);
147 			  	for (j = 0; j < $1->val; j++)
148 				{	runnable(rl, $9?$9->val:1, 1);
149 					announce(":root:");
150 				}
151 				if (dumptab) $3->sym->ini = $1;
152 			  } else
153 			  {	rl = mk_rdy($3->sym, $6, $11->sq, $2->val, $10, P_PROC);
154 			  }
155 			  if (rl && has_ini == 1) /* global initializations, unsafe */
156 			  {	/* printf("proctype %s has initialized data\n",
157 					$3->sym->name);
158 				 */
159 				rl->unsafe = 1;
160 			  }
161 			  context = ZS;
162 			}
163 	;
164 
165 proctype: PROCTYPE	{ $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
166 	| D_PROCTYPE	{ $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
167 	;
168 
169 inst	: /* empty */	{ $$ = ZN; }
170 	| ACTIVE	{ $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
171 	| ACTIVE '[' const_expr ']' {
172 			  $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
173 			  if ($3->val > 255)
174 				non_fatal("max nr of processes is 255\n", "");
175 			}
176 	| ACTIVE '[' NAME ']' {
177 			  $$ = nn(ZN,CONST,ZN,ZN);
178 			  $$->val = 0;
179 			  if (!$3->sym->type)
180 				fatal("undeclared variable %s",
181 					$3->sym->name);
182 			  else if ($3->sym->ini->ntyp != CONST)
183 				fatal("need constant initializer for %s\n",
184 					$3->sym->name);
185 			  else
186 				$$->val = $3->sym->ini->val;
187 			}
188 	;
189 
190 init	: INIT		{ context = $1->sym; }
191 	  Opt_priority
192 	  body		{ ProcList *rl;
193 			  rl = mk_rdy(context, ZN, $4->sq, 0, ZN, I_PROC);
194 			  runnable(rl, $3?$3->val:1, 1);
195 			  announce(":root:");
196 			  context = ZS;
197         		}
198 	;
199 
200 ltl	: LTL optname2	{ ltl_mode = 1; ltl_name = $2->sym->name; }
201 	  ltl_body	{ if ($4) ltl_list($2->sym->name, $4->sym->name);
202 			  ltl_mode = 0; has_ltl = 1;
203 			}
204 	;
205 
206 ltl_body: '{' full_expr OS '}' { $$ = ltl_to_string($2); }
207 	| error		{ $$ = NULL; }
208 	;
209 
210 claim	: CLAIM	optname	{ if ($2 != ZN)
211 			  {	$1->sym = $2->sym;	/* new 5.3.0 */
212 			  }
213 			  nclaims++;
214 			  context = $1->sym;
215 			  if (claimproc && !strcmp(claimproc, $1->sym->name))
216 			  {	fatal("claim %s redefined", claimproc);
217 			  }
218 			  claimproc = $1->sym->name;
219 			}
220 	  body		{ (void) mk_rdy($1->sym, ZN, $4->sq, 0, ZN, N_CLAIM);
221         		  context = ZS;
222         		}
223 	;
224 
225 optname : /* empty */	{ char tb[32];
226 			  memset(tb, 0, 32);
227 			  sprintf(tb, "never_%d", nclaims);
228 			  $$ = nn(ZN, NAME, ZN, ZN);
229 			  $$->sym = lookup(tb);
230 			}
231 	| NAME		{ $$ = $1; }
232 	;
233 
234 optname2 : /* empty */ { char tb[32]; static int nltl = 0;
235 			  memset(tb, 0, 32);
236 			  sprintf(tb, "ltl_%d", nltl++);
237 			  $$ = nn(ZN, NAME, ZN, ZN);
238 			  $$->sym = lookup(tb);
239 			}
240 	| NAME		{ $$ = $1; }
241 	;
242 
243 events : TRACE		{ context = $1->sym;
244 			  if (eventmap)
245 				non_fatal("trace %s redefined", eventmap);
246 			  eventmap = $1->sym->name;
247 			  inEventMap++;
248 			}
249 	  body		{
250 			  if (strcmp($1->sym->name, ":trace:") == 0)
251 			  {	(void) mk_rdy($1->sym, ZN, $3->sq, 0, ZN, E_TRACE);
252 			  } else
253 			  {	(void) mk_rdy($1->sym, ZN, $3->sq, 0, ZN, N_TRACE);
254 			  }
255         		  context = ZS;
256 			  inEventMap--;
257 			}
258 	;
259 
260 utype	: TYPEDEF NAME '{' 	{  if (context)
261 				   { fatal("typedef %s must be global",
262 					$2->sym->name);
263 				   }
264 				   owner = $2->sym;
265 				   in_seq = $1->ln;
266 				}
267 	  decl_lst '}'		{ setuname($5);
268 				  owner = ZS;
269 				  in_seq = 0;
270 				}
271 	;
272 
273 nm	: NAME			{ $$ = $1; }
274 	| INAME			{ $$ = $1;
275 				  if (IArgs)
276 				  fatal("invalid use of '%s'", $1->sym->name);
277 				}
278 	;
279 
280 ns	: INLINE nm l_par		{ NamesNotAdded++; }
281 	  args r_par		{ prep_inline($2->sym, $5);
282 				  NamesNotAdded--;
283 				}
284 	;
285 
286 c_fcts	: ccode			{ /* leaves pseudo-inlines with sym of
287 				   * type CODE_FRAG or CODE_DECL in global context
288 				   */
289 				}
290 	| cstate
291 	;
292 
293 cstate	: C_STATE STRING STRING	{
294 				  c_state($2->sym, $3->sym, ZS);
295 				  has_code = has_state = 1;
296 				}
297 	| C_TRACK STRING STRING {
298 				  c_track($2->sym, $3->sym, ZS);
299 				  has_code = has_state = 1;
300 				}
301 	| C_STATE STRING STRING	STRING {
302 				  c_state($2->sym, $3->sym, $4->sym);
303 				  has_code = has_state = 1;
304 				}
305 	| C_TRACK STRING STRING STRING {
306 				  c_track($2->sym, $3->sym, $4->sym);
307 				  has_code = has_state = 1;
308 				}
309 	;
310 
311 ccode	: C_CODE		{ Symbol *s;
312 				  NamesNotAdded++;
313 				  s = prep_inline(ZS, ZN);
314 				  NamesNotAdded--;
315 				  $$ = nn(ZN, C_CODE, ZN, ZN);
316 				  $$->sym = s;
317 				  $$->ln = $1->ln;
318 				  $$->fn = $1->fn;
319 				  has_code = 1;
320 				}
321 	| C_DECL		{ Symbol *s;
322 				  NamesNotAdded++;
323 				  s = prep_inline(ZS, ZN);
324 				  NamesNotAdded--;
325 				  s->type = CODE_DECL;
326 				  $$ = nn(ZN, C_CODE, ZN, ZN);
327 				  $$->sym = s;
328 				  $$->ln = $1->ln;
329 				  $$->fn = $1->fn;
330 				  has_code = 1;
331 				}
332 	;
333 cexpr	: C_EXPR		{ Symbol *s;
334 				  NamesNotAdded++;
335 				  s = prep_inline(ZS, ZN);
336 /* if context is 0 this was inside an ltl formula
337    mark the last inline added to seqnames */
338 				  if (!context)
339 				  {	mark_last();
340 				  }
341 				  NamesNotAdded--;
342 				  $$ = nn(ZN, C_EXPR, ZN, ZN);
343 				  $$->sym = s;
344 				  $$->ln = $1->ln;
345 				  $$->fn = $1->fn;
346 				  no_side_effects(s->name);
347 				  has_code = 1;
348 				}
349 	;
350 
351 body	: '{'			{ open_seq(1); in_seq = $1->ln; }
352           sequence OS		{ add_seq(Stop); }
353           '}'			{ $$->sq = close_seq(0); in_seq = 0;
354 				  if (scope_level != 0)
355 				  {	non_fatal("missing '}' ?", 0);
356 					scope_level = 0;
357 				  }
358 				}
359 	;
360 
361 sequence: step			{ if ($1) add_seq($1); }
362 	| sequence MS step	{ if ($3) add_seq($3); }
363 	;
364 
365 step    : one_decl		{ $$ = ZN; }
366 	| XU vref_lst		{ setxus($2, $1->val); $$ = ZN; }
367 	| NAME ':' one_decl	{ fatal("label preceding declaration,", (char *)0); }
368 	| NAME ':' XU		{ fatal("label preceding xr/xs claim,", 0); }
369 	| stmnt			{ $$ = $1; }
370 	| stmnt UNLESS		{ if ($1->ntyp == DO) { safe_break(); } }
371 	  stmnt			{ if ($1->ntyp == DO) { restore_break(); }
372 				  $$ = do_unless($1, $4);
373 				}
374 	| error
375 	;
376 
377 vis	: /* empty */		{ $$ = ZN; }
378 	| HIDDEN		{ $$ = $1; }
379 	| SHOW			{ $$ = $1; }
380 	| ISLOCAL		{ $$ = $1; }
381 	;
382 
383 asgn	: /* empty */		{ $$ = ZN; }
384 	| ':' NAME ASGN		{ $$ = $2; /* mtype decl */ }
385 	| ASGN			{ $$ = ZN; /* mtype decl */ }
386 	;
387 
388 osubt	: /* empty */		{ $$ = ZN; }
389 	| ':' NAME		{ $$ = $2; }
390 	;
391 
392 one_decl: vis TYPE osubt var_list { setptype($3, $4, $2->val, $1);
393 				  $4->val = $2->val;
394 				  $$ = $4;
395 				}
396 	| vis UNAME var_list	{ setutype($3, $2->sym, $1);
397 				  $$ = expand($3, Expand_Ok);
398 				}
399 	| vis TYPE asgn '{' nlst '}' {
400 				  if ($2->val != MTYPE)
401 					fatal("malformed declaration", 0);
402 				  setmtype($3, $5);
403 				  if ($1)
404 					non_fatal("cannot %s mtype (ignored)",
405 						$1->sym->name);
406 				  if (context != ZS)
407 					fatal("mtype declaration must be global", 0);
408 				}
409 	;
410 
411 decl_lst: one_decl       	{ $$ = nn(ZN, ',', $1, ZN); }
412 	| one_decl SEMI
413 	  decl_lst		{ $$ = nn(ZN, ',', $1, $3); }
414 	;
415 
416 decl    : /* empty */		{ $$ = ZN; }
417 	| decl_lst      	{ $$ = $1; }
418 	;
419 
420 vref_lst: varref		{ $$ = nn($1, XU, $1, ZN); }
421 	| varref ',' vref_lst	{ $$ = nn($1, XU, $1, $3); }
422 	;
423 
424 var_list: ivar           	{ $$ = nn($1, TYPE, ZN, ZN); }
425 	| ivar ',' var_list	{ $$ = nn($1, TYPE, ZN, $3); }
426 	;
427 
428 c_list	: CONST			{ $1->ntyp = CONST; $$ = $1; }
429 	| CONST ',' c_list	{ $1->ntyp = CONST; $$ = nn($1, ',', $1, $3); }
430 	;
431 
432 ivar    : vardcl           	{ $$ = $1;
433 				  $1->sym->ini = nn(ZN,CONST,ZN,ZN);
434 				  $1->sym->ini->val = 0;
435 				  if (!initialization_ok)
436 				  {	Lextok *zx, *xz;
437 					zx = nn(ZN, NAME, ZN, ZN);
438 					zx->sym = $1->sym;
439 					xz = nn(zx, ASGN, zx, $1->sym->ini);
440 					keep_track_off(xz);
441 					/* make sure zx doesnt turn out to be a STRUCT later */
442 					add_seq(xz);
443 				  }
444 				}
445 	| vardcl ASGN '{' c_list '}'	{	/* array initialization */
446 				  if (!$1->sym->isarray)
447 					fatal("%s must be an array", $1->sym->name);
448 				  $$ = $1;
449 				  $1->sym->ini = $4;
450 				  has_ini = 1;
451 				  $1->sym->hidden |= (4|8);	/* conservative */
452 				  if (!initialization_ok)
453 				  {	Lextok *zx = nn(ZN, NAME, ZN, ZN);
454 					zx->sym = $1->sym;
455 					add_seq(nn(zx, ASGN, zx, $4));
456 				  }
457 				}
458 	| vardcl ASGN expr   	{ $$ = $1;	/* initialized scalar */
459 				  $1->sym->ini = $3;
460 				  if ($3->ntyp == CONST
461 				  || ($3->ntyp == NAME && $3->sym->context))
462 				  {	has_ini = 2; /* local init */
463 				  } else
464 				  {	has_ini = 1; /* possibly global */
465 				  }
466 				  trackvar($1, $3);
467 				  if (any_oper($3, RUN))
468 				  {	fatal("cannot use 'run' in var init, saw", (char *) 0);
469 				  }
470 				  nochan_manip($1, $3, 0);
471 				  no_internals($1);
472 				  if (!initialization_ok)
473 				  {	Lextok *zx = nn(ZN, NAME, ZN, ZN);
474 					zx->sym = $1->sym;
475 					add_seq(nn(zx, ASGN, zx, $3));
476 					$1->sym->ini = 0;	/* Patrick Trentlin */
477 				  }
478 				}
479 	| vardcl ASGN ch_init	{ $1->sym->ini = $3;	/* channel declaration */
480 				  $$ = $1; has_ini = 1;
481 				  if (!initialization_ok)
482 				  {	non_fatal(PART1 "'%s'" PART2, $1->sym->name);
483 				  }
484 				}
485 	;
486 
487 ch_init : '[' const_expr ']' OF
488 	  '{' typ_list '}'	{ if ($2->val)
489 					u_async++;
490 				  else
491 					u_sync++;
492         			  {	int i = cnt_mpars($6);
493 					Mpars = max(Mpars, i);
494 				  }
495         			  $$ = nn(ZN, CHAN, ZN, $6);
496 				  $$->val = $2->val;
497 				  $$->ln = $1->ln;
498 				  $$->fn = $1->fn;
499         			}
500 	;
501 
502 vardcl  : NAME  		{ $1->sym->nel = 1; $$ = $1; }
503 	| NAME ':' CONST	{ $1->sym->nbits = $3->val;
504 				  if ($3->val >= 8*sizeof(long))
505 				  {	non_fatal("width-field %s too large",
506 						$1->sym->name);
507 					$3->val = 8*sizeof(long)-1;
508 				  }
509 				  $1->sym->nel = 1; $$ = $1;
510 				}
511 	| NAME '[' const_expr ']'	{ $1->sym->nel = $3->val; $1->sym->isarray = 1; $$ = $1; }
512 	| NAME '[' NAME ']'	{	/* make an exception for an initialized scalars */
513 					$$ = nn(ZN, CONST, ZN, ZN);
514 					fprintf(stderr, "spin: %s:%d, warning: '%s' in array bound ",
515 						$1->fn->name, $1->ln, $3->sym->name);
516 					if ($3->sym->ini
517 					&&  $3->sym->ini->val > 0)
518 					{	fprintf(stderr, "evaluated as %d\n", $3->sym->ini->val);
519 						$$->val = $3->sym->ini->val;
520 					} else
521 					{	fprintf(stderr, "evaluated as 1 by default (to avoid zero)\n");
522 						$$->val = 1;
523 					}
524 					$1->sym->nel = $$->val;
525 					$1->sym->isarray = 1;
526 					$$ = $1;
527 				}
528 	;
529 
530 varref	: cmpnd			{ $$ = mk_explicit($1, Expand_Ok, NAME); }
531 	;
532 
533 pfld	: NAME			{ $$ = nn($1, NAME, ZN, ZN);
534 				  if ($1->sym->isarray && !in_for)
535 				  {	non_fatal("missing array index for '%s'",
536 						$1->sym->name);
537 				  }
538 				}
539 	| NAME			{ owner = ZS; }
540 	  '[' expr ']'		{ $$ = nn($1, NAME, $4, ZN); }
541 	;
542 
543 cmpnd	: pfld			{ Embedded++;
544 				  if ($1->sym->type == STRUCT)
545 					owner = $1->sym->Snm;
546 				}
547 	  sfld			{ $$ = $1; $$->rgt = $3;
548 				  if ($3 && $1->sym->type != STRUCT)
549 					$1->sym->type = STRUCT;
550 				  Embedded--;
551 				  if (!Embedded && !NamesNotAdded
552 				  &&  !$1->sym->type)
553 				   fatal("undeclared variable: %s",
554 						$1->sym->name);
555 				  if ($3) validref($1, $3->lft);
556 				  owner = ZS;
557 				}
558 	;
559 
560 sfld	: /* empty */		{ $$ = ZN; }
561 	| '.' cmpnd %prec DOT	{ $$ = nn(ZN, '.', $2, ZN); }
562 	;
563 
564 stmnt	: Special		{ $$ = $1; initialization_ok = 0; }
565 	| Stmnt			{ $$ = $1; initialization_ok = 0;
566 				  if (inEventMap) non_fatal("not an event", (char *)0);
567 				}
568 	;
569 
570 for_pre : FOR l_par		{ in_for = 1; }
571 	  varref		{ trapwonly($4 /*, "for" */);
572 				  pushbreak(); /* moved up */
573 				  $$ = $4;
574 				}
575 	;
576 
577 for_post: '{' sequence OS '}'
578 	| SEMI '{' sequence OS '}'
579 
580 Special : varref RCV		{ Expand_Ok++; }
581 	  rargs			{ Expand_Ok--; has_io++;
582 				  $$ = nn($1,  'r', $1, $4);
583 				  trackchanuse($4, ZN, 'R');
584 				}
585 	| varref SND		{ Expand_Ok++; }
586 	  margs			{ Expand_Ok--; has_io++;
587 				  $$ = nn($1, 's', $1, $4);
588 				  $$->val=0; trackchanuse($4, ZN, 'S');
589 				  any_runs($4);
590 				}
591 	| for_pre ':' expr DOTDOT expr r_par	{
592 				  for_setup($1, $3, $5); in_for = 0;
593 				}
594 	  for_post		{ $$ = for_body($1, 1);
595 				}
596 	| for_pre IN varref r_par	{ $$ = for_index($1, $3); in_for = 0;
597 				}
598 	  for_post		{ $$ = for_body($5, 1);
599 				}
600 	| SELECT l_par varref ':' expr DOTDOT expr r_par {
601 				  trapwonly($3 /*, "select" */);
602 				  $$ = sel_index($3, $5, $7);
603 				}
604 	| IF options FI 	{ $$ = nn($1, IF, ZN, ZN);
605         			  $$->sl = $2->sl;
606 				  $$->ln = $1->ln;
607 				  $$->fn = $1->fn;
608 				  prune_opts($$);
609         			}
610 	| DO    		{ pushbreak(); }
611           options OD    	{ $$ = nn($1, DO, ZN, ZN);
612         			  $$->sl = $3->sl;
613 				  $$->ln = $1->ln;
614 				  $$->fn = $1->fn;
615 				  prune_opts($$);
616         			}
617 	| BREAK  		{ $$ = nn(ZN, GOTO, ZN, ZN);
618 				  $$->sym = break_dest();
619 				}
620 	| GOTO NAME		{ $$ = nn($2, GOTO, ZN, ZN);
621 				  if ($2->sym->type != 0
622 				  &&  $2->sym->type != LABEL) {
623 				  	non_fatal("bad label-name %s",
624 					$2->sym->name);
625 				  }
626 				  $2->sym->type = LABEL;
627 				}
628 	| NAME ':' stmnt	{ $$ = nn($1, ':',$3, ZN);
629 				  if ($1->sym->type != 0
630 				  &&  $1->sym->type != LABEL) {
631 				  	non_fatal("bad label-name %s",
632 					$1->sym->name);
633 				  }
634 				  $1->sym->type = LABEL;
635 				}
636 	| NAME ':'		{ $$ = nn($1, ':',ZN,ZN);
637 				  if ($1->sym->type != 0
638 				  &&  $1->sym->type != LABEL) {
639 				  	non_fatal("bad label-name %s",
640 					$1->sym->name);
641 				  }
642 				  $$->lft = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
643 				  $$->lft->lft->val = 1; /* skip */
644 				  $1->sym->type = LABEL;
645 				}
646 	| error			{ $$ = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
647 				  $$->lft->val = 1; /* skip */
648 				}
649 	;
650 
651 Stmnt	: varref ASGN full_expr	{ $$ = nn($1, ASGN, $1, $3);	/* assignment */
652 				  trackvar($1, $3);
653 				  nochan_manip($1, $3, 0);
654 				  no_internals($1);
655 				}
656 	| varref INCR		{ $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
657 				  $$ = nn(ZN,  '+', $1, $$);
658 				  $$ = nn($1, ASGN, $1, $$);
659 				  trackvar($1, $1);
660 				  no_internals($1);
661 				  if ($1->sym->type == CHAN)
662 				   fatal("arithmetic on chan", (char *)0);
663 				}
664 	| varref DECR		{ $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
665 				  $$ = nn(ZN,  '-', $1, $$);
666 				  $$ = nn($1, ASGN, $1, $$);
667 				  trackvar($1, $1);
668 				  no_internals($1);
669 				  if ($1->sym->type == CHAN)
670 				   fatal("arithmetic on chan id's", (char *)0);
671 				}
672 	| SET_P l_par two_args r_par	{ $$ = nn(ZN, SET_P, $3, ZN); has_priority++; }
673 	| PRINT	l_par STRING	{ realread = 0; }
674 	  prargs r_par		{ $$ = nn($3, PRINT, $5, ZN); realread = 1; }
675 	| PRINTM l_par varref r_par	{ $$ = nn(ZN, PRINTM, $3, ZN); }
676 	| PRINTM l_par CONST r_par	{ $$ = nn(ZN, PRINTM, $3, ZN); }
677 	| ASSERT full_expr    	{ $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
678 	| ccode			{ $$ = $1; }
679 	| varref R_RCV		{ Expand_Ok++; }
680 	  rargs			{ Expand_Ok--; has_io++;
681 				  $$ = nn($1,  'r', $1, $4);
682 				  $$->val = has_random = 1;
683 				  trackchanuse($4, ZN, 'R');
684 				}
685 	| varref RCV		{ Expand_Ok++; }
686 	  LT rargs GT		{ Expand_Ok--; has_io++;
687 				  $$ = nn($1, 'r', $1, $5);
688 				  $$->val = 2;	/* fifo poll */
689 				  trackchanuse($5, ZN, 'R');
690 				}
691 	| varref R_RCV		{ Expand_Ok++; }
692 	  LT rargs GT		{ Expand_Ok--; has_io++;	/* rrcv poll */
693 				  $$ = nn($1, 'r', $1, $5);
694 				  $$->val = 3; has_random = 1;
695 				  trackchanuse($5, ZN, 'R');
696 				}
697 	| varref O_SND		{ Expand_Ok++; }
698 	  margs			{ Expand_Ok--; has_io++;
699 				  $$ = nn($1, 's', $1, $4);
700 				  $$->val = has_sorted = 1;
701 				  trackchanuse($4, ZN, 'S');
702 				  any_runs($4);
703 				}
704 	| full_expr		{ $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
705 	| ELSE  		{ $$ = nn(ZN,ELSE,ZN,ZN);
706 				}
707 	| ATOMIC   '{'   	{ open_seq(0); }
708           sequence OS '}'   	{ $$ = nn($1, ATOMIC, ZN, ZN);
709         			  $$->sl = seqlist(close_seq(3), 0);
710 				  $$->ln = $1->ln;
711 				  $$->fn = $1->fn;
712 				  make_atomic($$->sl->this, 0);
713         			}
714 	| D_STEP '{'		{ open_seq(0);
715 				  rem_Seq();
716 				}
717           sequence OS '}'   	{ $$ = nn($1, D_STEP, ZN, ZN);
718         			  $$->sl = seqlist(close_seq(4), 0);
719 				  $$->ln = $1->ln;
720 				  $$->fn = $1->fn;
721         			  make_atomic($$->sl->this, D_ATOM);
722 				  unrem_Seq();
723         			}
724 	| '{'			{ open_seq(0); }
725 	  sequence OS '}'	{ $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
726         			  $$->sl = seqlist(close_seq(5), 0);
727 				  $$->ln = $1->ln;
728 				  $$->fn = $1->fn;
729         			}
730 	| INAME			{ IArgs++; }
731 	  l_par args r_par	{ initialization_ok = 0;
732 				  pickup_inline($1->sym, $4, ZN);
733 				  IArgs--;
734 				}
735 	  Stmnt			{ $$ = $7; }
736 
737 	| varref ASGN INAME	{ IArgs++; /* inline call */ }
738 	  l_par args r_par	{ initialization_ok = 0;
739 				  pickup_inline($3->sym, $6, $1);
740 				  IArgs--;
741 				}
742 	  Stmnt			{ $$ = $9; }
743 	| RETURN full_expr	{ $$ = return_statement($2); }
744 	;
745 
746 options : option		{ $$->sl = seqlist($1->sq, 0); }
747 	| option options	{ $$->sl = seqlist($1->sq, $2->sl); }
748 	;
749 
750 option  : SEP   		{ open_seq(0); }
751           sequence OS		{ $$ = nn(ZN,0,ZN,ZN);
752 				  $$->sq = close_seq(6);
753 				  $$->ln = $1->ln;
754 				  $$->fn = $1->fn;
755 				}
756 	;
757 
758 OS	: /* empty */
759 	| semi			{ /* redundant semi at end of sequence */ }
760 	;
761 
762 semi	: SEMI
763 	| ARROW
764 	;
765 
766 MS	: semi			{ /* at least one semi-colon */ }
767 	| MS semi		{ /* but more are okay too   */ }
768 	;
769 
770 aname	: NAME			{ $$ = $1; }
771 	| PNAME			{ $$ = $1; }
772 	;
773 
774 const_expr:	CONST			{ $$ = $1; }
775 	| '-' const_expr %prec UMIN	{ $$ = $2; $$->val = -($2->val); }
776 	| l_par const_expr r_par		{ $$ = $2; }
777 	| const_expr '+' const_expr	{ $$ = $1; $$->val = $1->val + $3->val; }
778 	| const_expr '-' const_expr	{ $$ = $1; $$->val = $1->val - $3->val; }
779 	| const_expr '*' const_expr	{ $$ = $1; $$->val = $1->val * $3->val; }
780 	| const_expr '/' const_expr	{ $$ = $1;
781 					  if ($3->val == 0)
782 					  { fatal("division by zero", (char *) 0);
783 					  }
784 					  $$->val = $1->val / $3->val;
785 					}
786 	| const_expr '%' const_expr	{ $$ = $1;
787 					  if ($3->val == 0)
788 					  { fatal("attempt to take modulo of zero", (char *) 0);
789 					  }
790 					  $$->val = $1->val % $3->val;
791 					}
792 	;
793 
794 expr    : l_par expr r_par		{ $$ = $2; }
795 	| expr '+' expr		{ $$ = nn(ZN, '+', $1, $3); }
796 	| expr '-' expr		{ $$ = nn(ZN, '-', $1, $3); }
797 	| expr '*' expr		{ $$ = nn(ZN, '*', $1, $3); }
798 	| expr '/' expr		{ $$ = nn(ZN, '/', $1, $3); }
799 	| expr '%' expr		{ $$ = nn(ZN, '%', $1, $3); }
800 	| expr '&' expr		{ $$ = nn(ZN, '&', $1, $3); }
801 	| expr '^' expr		{ $$ = nn(ZN, '^', $1, $3); }
802 	| expr '|' expr		{ $$ = nn(ZN, '|', $1, $3); }
803 	| expr GT expr		{ $$ = nn(ZN,  GT, $1, $3); }
804 	| expr LT expr		{ $$ = nn(ZN,  LT, $1, $3); }
805 	| expr GE expr		{ $$ = nn(ZN,  GE, $1, $3); }
806 	| expr LE expr		{ $$ = nn(ZN,  LE, $1, $3); }
807 	| expr EQ expr		{ $$ = nn(ZN,  EQ, $1, $3); }
808 	| expr NE expr		{ $$ = nn(ZN,  NE, $1, $3); }
809 	| expr AND expr		{ $$ = nn(ZN, AND, $1, $3); }
810 	| expr OR  expr		{ $$ = nn(ZN,  OR, $1, $3); }
811 	| expr LSHIFT expr	{ $$ = nn(ZN, LSHIFT,$1, $3); }
812 	| expr RSHIFT expr	{ $$ = nn(ZN, RSHIFT,$1, $3); }
813 	| '~' expr		{ $$ = nn(ZN, '~', $2, ZN); }
814 	| '-' expr %prec UMIN	{ $$ = nn(ZN, UMIN, $2, ZN); }
815 	| SND expr %prec NEG	{ $$ = nn(ZN, '!', $2, ZN); }
816 
817 	| l_par expr ARROW expr ':' expr r_par {
818 				  $$ = nn(ZN,  OR, $4, $6);
819 				  $$ = nn(ZN, '?', $2, $$);
820 				}
821 
822 	| RUN aname		{ Expand_Ok++;
823 				  if (!context)
824 				   fatal("used 'run' outside proctype", (char *) 0);
825 				}
826 	  l_par args r_par
827 	  Opt_priority		{ Expand_Ok--;
828 				  $$ = nn($2, RUN, $5, ZN);
829 				  $$->val = ($7) ? $7->val : 0;
830 				  trackchanuse($5, $2, 'A'); trackrun($$);
831 				}
832 	| LEN l_par varref r_par	{ $$ = nn($3, LEN, $3, ZN); }
833 	| ENABLED l_par expr r_par	{ $$ = nn(ZN, ENABLED, $3, ZN); has_enabled++; }
834 	| GET_P l_par expr r_par	{ $$ = nn(ZN, GET_P, $3, ZN); has_priority++; }
835 	| varref RCV		{ Expand_Ok++; }
836 	  '[' rargs ']'		{ Expand_Ok--; has_io++;
837 				  $$ = nn($1, 'R', $1, $5);
838 				}
839 	| varref R_RCV		{ Expand_Ok++; }
840 	  '[' rargs ']'		{ Expand_Ok--; has_io++;
841 				  $$ = nn($1, 'R', $1, $5);
842 				  $$->val = has_random = 1;
843 				}
844 	| varref		{ $$ = $1; trapwonly($1 /*, "varref" */); }
845 	| cexpr			{ $$ = $1; }
846 	| CONST 		{ $$ = nn(ZN,CONST,ZN,ZN);
847 				  $$->ismtyp = $1->ismtyp;
848 				  $$->sym = $1->sym;
849 				  $$->val = $1->val;
850 				}
851 	| TIMEOUT		{ $$ = nn(ZN,TIMEOUT, ZN, ZN); }
852 	| NONPROGRESS		{ $$ = nn(ZN,NONPROGRESS, ZN, ZN);
853 				  has_np++;
854 				}
855 	| PC_VAL l_par expr r_par	{ $$ = nn(ZN, PC_VAL, $3, ZN);
856 				  has_pcvalue++;
857 				}
858 	| PNAME '[' expr ']' '@' NAME
859 	  			{ $$ = rem_lab($1->sym, $3, $6->sym); }
860 	| PNAME '[' expr ']' ':' pfld
861 	  			{ $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
862 	| PNAME '@' NAME	{ $$ = rem_lab($1->sym, ZN, $3->sym); }
863 	| PNAME ':' pfld	{ $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
864 	| ltl_expr		{ $$ = $1; /* sanity_check($1); */ }
865 	;
866 
867 Opt_priority:	/* none */	{ $$ = ZN; }
868 	| PRIORITY CONST	{ $$ = $2; has_priority++; }
869 	;
870 
871 full_expr:	expr		{ $$ = $1; }
872 	| Expr			{ $$ = $1; }
873 	;
874 
875 ltl_expr: expr UNTIL expr	{ $$ = nn(ZN, UNTIL,   $1, $3); }
876 	| expr RELEASE expr	{ $$ = nn(ZN, RELEASE, $1, $3); }
877 	| expr WEAK_UNTIL expr	{ $$ = nn(ZN, ALWAYS, $1, ZN);
878 				  $$ = nn(ZN, OR, $$, nn(ZN, UNTIL, $1, $3));
879 				}
880 	| expr IMPLIES expr	{ $$ = nn(ZN, '!', $1, ZN);
881 				  $$ = nn(ZN, OR,  $$, $3);
882 				}
883 	| expr EQUIV expr	{ $$ = nn(ZN, EQUIV,   $1, $3); }
884 	| NEXT expr       %prec NEG { $$ = nn(ZN, NEXT,  $2, ZN); }
885 	| ALWAYS expr     %prec NEG { $$ = nn(ZN, ALWAYS,$2, ZN); }
886 	| EVENTUALLY expr %prec NEG { $$ = nn(ZN, EVENTUALLY, $2, ZN); }
887 	;
888 
889 	/* an Expr cannot be negated - to protect Probe expressions */
890 Expr	: Probe			{ $$ = $1; }
891 	| l_par Expr r_par	{ $$ = $2; }
892 	| Expr AND Expr		{ $$ = nn(ZN, AND, $1, $3); }
893 	| Expr AND expr		{ $$ = nn(ZN, AND, $1, $3); }
894 	| expr AND Expr		{ $$ = nn(ZN, AND, $1, $3); }
895 	| Expr OR  Expr		{ $$ = nn(ZN,  OR, $1, $3); }
896 	| Expr OR  expr		{ $$ = nn(ZN,  OR, $1, $3); }
897 	| expr OR  Expr		{ $$ = nn(ZN,  OR, $1, $3); }
898 	;
899 
900 Probe	: FULL l_par varref r_par	{ $$ = nn($3,  FULL, $3, ZN); }
901 	| NFULL l_par varref r_par	{ $$ = nn($3, NFULL, $3, ZN); }
902 	| EMPTY l_par varref r_par	{ $$ = nn($3, EMPTY, $3, ZN); }
903 	| NEMPTY l_par varref r_par	{ $$ = nn($3,NEMPTY, $3, ZN); }
904 	;
905 
906 Opt_enabler:	/* none */	{ $$ = ZN; }
907 	| PROVIDED l_par full_expr r_par {
908 				   if (!proper_enabler($3))
909 				   { non_fatal("invalid PROVIDED clause", (char *)0);
910 				     $$ = ZN;
911 				   } else
912 				   { $$ = $3;
913 				 } }
914 	| PROVIDED error	 { $$ = ZN;
915 				   non_fatal("usage: provided ( ..expr.. )", (char *)0);
916 				 }
917 	;
918 
919 oname	: /* empty */		{ $$ = ZN; }
920 	| ':' NAME		{ $$ = $2; }
921 	;
922 
923 basetype: TYPE oname		{ if ($2)
924 				  {	if ($1->val != MTYPE)
925 					{	explain($1->val);
926 						fatal("unexpected type", (char *) 0);
927 				  }	}
928 				  $$->sym = $2 ? $2->sym : ZS;
929 				  $$->val = $1->val;
930 				  if ($$->val == UNSIGNED)
931 				  fatal("unsigned cannot be used as mesg type", 0);
932 				}
933 	| UNAME			{ $$->sym = $1->sym;
934 				  $$->val = STRUCT;
935 				}
936 	| error			/* e.g., unsigned ':' const */
937 	;
938 
939 typ_list: basetype		{ $$ = nn($1, $1->val, ZN, ZN); }
940 	| basetype ',' typ_list	{ $$ = nn($1, $1->val, ZN, $3); }
941 	;
942 
943 two_args:	expr ',' expr	{ $$ = nn(ZN, ',', $1, $3); }
944 	;
945 
946 args    : /* empty */		{ $$ = ZN; }
947 	| arg			{ $$ = $1; }
948 	;
949 
950 prargs  : /* empty */		{ $$ = ZN; }
951 	| ',' arg		{ $$ = $2; }
952 	;
953 
954 margs   : arg			{ $$ = $1; }
955 	| expr l_par arg r_par	{ if ($1->ntyp == ',')
956 					$$ = tail_add($1, $3);
957 				  else
958 				  	$$ = nn(ZN, ',', $1, $3);
959 				}
960 	;
961 
962 arg     : expr			{ if ($1->ntyp == ',')
963 					$$ = $1;
964 				  else
965 				  	$$ = nn(ZN, ',', $1, ZN);
966 				}
967 	| expr ',' arg		{ if ($1->ntyp == ',')
968 					$$ = tail_add($1, $3);
969 				  else
970 				  	$$ = nn(ZN, ',', $1, $3);
971 				}
972 	;
973 
974 rarg	: varref		{ $$ = $1; trackvar($1, $1);
975 				  trapwonly($1 /*, "rarg" */); }
976 	| EVAL l_par expr r_par	{ $$ = nn(ZN,EVAL,$3,ZN);
977 				  trapwonly($1 /*, "eval rarg" */); }
978 	| CONST 		{ $$ = nn(ZN,CONST,ZN,ZN);
979 				  $$->ismtyp = $1->ismtyp;
980 				  $$->sym = $1->sym;
981 				  $$->val = $1->val;
982 				}
983 	| '-' CONST %prec UMIN	{ $$ = nn(ZN,CONST,ZN,ZN);
984 				  $$->val = - ($2->val);
985 				}
986 	;
987 
988 rargs	: rarg			{ if ($1->ntyp == ',')
989 					$$ = $1;
990 				  else
991 				  	$$ = nn(ZN, ',', $1, ZN);
992 				}
993 	| rarg ',' rargs	{ if ($1->ntyp == ',')
994 					$$ = tail_add($1, $3);
995 				  else
996 				  	$$ = nn(ZN, ',', $1, $3);
997 				}
998 	| rarg l_par rargs r_par	{ if ($1->ntyp == ',')
999 					$$ = tail_add($1, $3);
1000 				  else
1001 				  	$$ = nn(ZN, ',', $1, $3);
1002 				}
1003 	| l_par rargs r_par		{ $$ = $2; }
1004 	;
1005 
1006 nlst	: NAME			{ $$ = nn($1, NAME, ZN, ZN);
1007 				  $$ = nn(ZN, ',', $$, ZN); }
1008 	| nlst NAME 		{ $$ = nn($2, NAME, ZN, ZN);
1009 				  $$ = nn(ZN, ',', $$, $1);
1010 				}
1011 	| nlst ','		{ $$ = $1; /* commas optional */ }
1012 	;
1013 %%
1014 
1015 #define binop(n, sop)	fprintf(fd, "("); recursive(fd, n->lft); \
1016 			fprintf(fd, ") %s (", sop); recursive(fd, n->rgt); \
1017 			fprintf(fd, ")");
1018 #define unop(n, sop)	fprintf(fd, "%s (", sop); recursive(fd, n->lft); \
1019 			fprintf(fd, ")");
1020 
1021 static void
1022 recursive(FILE *fd, Lextok *n)
1023 {
1024 	if (n)
1025 	switch (n->ntyp) {
1026 	case NEXT:
1027 		unop(n, "X");
1028 		break;
1029 	case ALWAYS:
1030 		unop(n, "[]");
1031 		break;
1032 	case EVENTUALLY:
1033 		unop(n, "<>");
1034 		break;
1035 	case '!':
1036 		unop(n, "!");
1037 		break;
1038 	case UNTIL:
1039 		binop(n, "U");
1040 		break;
1041 	case WEAK_UNTIL:
1042 		binop(n, "W");
1043 		break;
1044 	case RELEASE: /* see http://en.wikipedia.org/wiki/Linear_temporal_logic */
1045 		binop(n, "V");
1046 		break;
1047 	case OR:
1048 		binop(n, "||");
1049 		break;
1050 	case AND:
1051 		binop(n, "&&");
1052 		break;
1053 	case IMPLIES:
1054 		binop(n, "->");
1055 		break;
1056 	case EQUIV:
1057 		binop(n, "<->");
1058 		break;
1059 	case C_EXPR:
1060 		fprintf(fd, "c_expr { %s }", put_inline(fd, n->sym->name));
1061 		break;
1062 	default:
1063 		comment(fd, n, 0);
1064 		break;
1065 	}
1066 }
1067 
1068 #ifdef __MINGW32__
1069 extern ssize_t getline(char **, size_t *, FILE *); /* see main.c */
1070 #endif
1071 
1072 static Lextok *
ltl_to_string(Lextok * n)1073 ltl_to_string(Lextok *n)
1074 {	Lextok *m = nn(ZN, 0, ZN, ZN);
1075 	ssize_t retval;
1076 	char *ltl_formula = NULL;
1077 	FILE *tf = fopen(TMP_FILE1, "w+"); /* tmpfile() fails on Windows 7 */
1078 
1079 	/* convert the parsed ltl to a string
1080 	   by writing into a file, using existing functions,
1081 	   and then passing it to the existing interface for
1082 	   conversion into a never claim
1083 	  (this means parsing everything twice, which is
1084 	   a little redundant, but adds only miniscule overhead)
1085 	 */
1086 
1087 	if (!tf)
1088 	{	fatal("cannot create temporary file", (char *) 0);
1089 	}
1090 	dont_simplify = 1;
1091 	recursive(tf, n);
1092 	dont_simplify = 0;
1093 	(void) fseek(tf, 0L, SEEK_SET);
1094 
1095 	size_t linebuffsize = 0;
1096 	retval = getline(&ltl_formula, &linebuffsize, tf);
1097 	fclose(tf);
1098 
1099 	(void) unlink(TMP_FILE1);
1100 
1101 	if (!retval)
1102 	{	printf("%ld\n", (long int) retval);
1103 		fatal("could not translate ltl ltl_formula", 0);
1104 	}
1105 
1106 	if (1) printf("ltl %s: %s\n", ltl_name, ltl_formula);
1107 
1108 	m->sym = lookup(ltl_formula);
1109 #ifndef __MINGW32__
1110 	free(ltl_formula);
1111 #endif
1112 	return m;
1113 }
1114 
1115 int
is_temporal(int t)1116 is_temporal(int t)
1117 {
1118 	return (t == EVENTUALLY || t == ALWAYS || t == UNTIL
1119 	     || t == WEAK_UNTIL || t == RELEASE);
1120 }
1121 
1122 int
is_boolean(int t)1123 is_boolean(int t)
1124 {
1125 	return (t == AND || t == OR || t == IMPLIES || t == EQUIV);
1126 }
1127 
1128 #if 0
1129 /* flags correct formula like: ltl { true U (true U true) } */
1130 void
1131 sanity_check(Lextok *t)	/* check proper embedding of ltl_expr */
1132 {
1133 	if (!t) return;
1134 	sanity_check(t->lft);
1135 	sanity_check(t->rgt);
1136 
1137 	if (t->lft && t->rgt)
1138 	{	if (!is_boolean(t->ntyp)
1139 		&&  (is_temporal(t->lft->ntyp)
1140 		||   is_temporal(t->rgt->ntyp)))
1141 		{	printf("spin: attempt to apply '");
1142 			explain(t->ntyp);
1143 			printf("' to '");
1144 			explain(t->lft->ntyp);
1145 			printf("' and '");
1146 			explain(t->rgt->ntyp);
1147 			printf("'\n");
1148 	/*		non_fatal("missing parentheses?", (char *)0); */
1149 	}	}
1150 }
1151 #endif
1152 
1153 void
yyerror(char * fmt,...)1154 yyerror(char *fmt, ...)
1155 {
1156 	non_fatal(fmt, (char *) 0);
1157 }
1158