]> andersk Git - splint.git/blame - src/abstract.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Updated README version number. (Testing sourceforge)
[splint.git] / src / abstract.c
CommitLineData
616915dd 1/*
2** LCLint - annotation-assisted static program checker
28bf4b0b 3** Copyright (C) 1994-2001 University of Virginia,
616915dd 4** Massachusetts Institute of Technology
5**
6** This program is free software; you can redistribute it and/or modify it
7** under the terms of the GNU General Public License as published by the
8** Free Software Foundation; either version 2 of the License, or (at your
9** option) any later version.
10**
11** This program is distributed in the hope that it will be useful, but
12** WITHOUT ANY WARRANTY; without even the implied warranty of
13** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14** General Public License for more details.
15**
16** The GNU General Public License is available from http://www.gnu.org/ or
17** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18** MA 02111-1307, USA.
19**
20** For information on lclint: lclint-request@cs.virginia.edu
21** To report a bug: lclint-bug@cs.virginia.edu
22** For more information: http://lclint.cs.virginia.edu
23*/
24/*
25** abstract.c
26**
27** Module for building abstract syntax trees for LCL.
28**
29** This module is too close to the surface syntax of LCL.
30** Suffices for now.
31**
32** AUTHOR:
33** Yang Meng Tan,
34** Massachusetts Institute of Technology
35*/
36
37# include "lclintMacros.nf"
38# include "llbasic.h"
39# include "lslparse.h"
40# include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
41# include "lclscan.h"
42# include "lh.h"
43# include "imports.h"
44
45static lsymbol lsymbol_Bool;
46static lsymbol lsymbol_bool;
47static lsymbol lsymbol_TRUE;
48static lsymbol lsymbol_FALSE;
49
50static void lclPredicateNode_free (/*@only@*/ /*@null@*/ lclPredicateNode p_x) ;
51static void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode p_x) ;
52static void CTypesNode_free (/*@null@*/ /*@only@*/ CTypesNode p_x);
53static /*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode p_x) /*@*/ ;
54static void
55 constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode p_x);
56static void claimNode_free (/*@only@*/ /*@null@*/ claimNode p_x);
57static void iterNode_free (/*@only@*/ /*@null@*/ iterNode p_x);
58static void abstBodyNode_free (/*@only@*/ /*@null@*/ abstBodyNode p_n);
59static void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode p_x);
60static void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode p_x);
61static void typeNode_free (/*@only@*/ /*@null@*/ typeNode p_t);
62static /*@null@*/ strOrUnionNode
63 strOrUnionNode_copy (/*@null@*/ strOrUnionNode p_n) /*@*/ ;
64static void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode p_n)
65 /*@modifies *p_n @*/ ;
66
67static void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode p_x);
68static /*@only@*/ /*@null@*/ enumSpecNode
69 enumSpecNode_copy (/*@null@*/ enumSpecNode p_x) /*@*/ ;
70static /*@only@*/ lclTypeSpecNode
71 lclTypeSpecNode_copySafe (lclTypeSpecNode p_n) /*@*/ ;
72static void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode p_n);
73static void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack p_x);
74static void opFormNode_free (/*@only@*/ /*@null@*/ opFormNode p_op);
75static quantifiedTermNode quantifiedTermNode_copy (quantifiedTermNode p_q) /*@*/ ;
76static void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode p_x);
77static void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode p_x);
78static void exportNode_free (/*@null@*/ /*@only@*/ exportNode p_x);
79static void privateNode_free (/*@only@*/ /*@null@*/ privateNode p_x);
80static /*@null@*/ termNode termNode_copy (/*@null@*/ termNode p_t) /*@*/ ;
81static void
82 stmtNode_free (/*@only@*/ /*@null@*/ stmtNode p_x) /*@modifies *p_x@*/ ;
83static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr p_x) /*@*/ ;
84
85static lsymbol ConditionalSymbol;
86static lsymbol equalSymbol;
87static lsymbol eqSymbol;
88static lclTypeSpecNode exposedType;
89
90static /*@only@*/ cstring abstDeclaratorNode_unparse (abstDeclaratorNode p_x);
91static pairNodeList extractParams (/*@null@*/ typeExpr p_te);
92static sort extractReturnSort (lclTypeSpecNode p_t, declaratorNode p_d);
93static void checkAssociativity (termNode p_x, ltoken p_op);
94static void LCLBootstrap (void);
95static cstring printMiddle (int p_j);
96static void paramNode_checkQualifiers (lclTypeSpecNode p_t, typeExpr p_d);
97
98void
99resetImports (cstring current)
100{
101 lsymbolSet_free (g_currentImports);
102
103 g_currentImports = lsymbolSet_new (); /* equal_symbol; */
104 (void) lsymbolSet_insert (g_currentImports,
28bf4b0b 105 lsymbol_fromString (current));
616915dd 106}
107
108void
109abstract_init ()
110{
111 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
112 nameNode nn;
113 ltoken dom, range;
114 sigNode sign;
115 opFormNode opform;
116 ltokenList domain = ltokenList_new ();
117 ltokenList domain2;
118
119 equalSymbol = lsymbol_fromChars ("=");
120 eqSymbol = lsymbol_fromChars ("\\eq");
121
122 /*
123 ** not: cstring_toCharsSafe (context_getBoolName ())
124 ** we use the hard wired "bool" name.
125 */
126
127 lsymbol_bool = lsymbol_fromChars ("bool");
128 lsymbol_Bool = lsymbol_fromChars ("Bool");
129
130 lsymbol_TRUE = lsymbol_fromChars ("TRUE");
131 lsymbol_FALSE = lsymbol_fromChars ("FALSE");
132
133 ConditionalSymbol = lsymbol_fromChars ("if__then__else__");
134
135 /* generate operators for
136 ** __ \not, __ \implies __ , __ \and __, __ \or __
137 */
138
139 range = ltoken_create (simpleId, lsymbol_bool);
140 dom = ltoken_create (simpleId, lsymbol_bool);
141
142 ltokenList_addh (domain, ltoken_copy (dom));
143
144 domain2 = ltokenList_copy (domain); /* moved this here (before release) */
145
146 sign = makesigNode (ltoken_undefined, domain, ltoken_copy (range));
147
148 opform = makeOpFormNode (ltoken_undefined, OPF_ANYOPM,
149 opFormUnion_createAnyOp (ltoken_not),
150 ltoken_undefined);
151 nn = makeNameNodeForm (opform);
152 symtable_enterOp (g_symtab, nn, sign);
153
154 ltokenList_addh (domain2, dom);
155
156 sign = makesigNode (ltoken_undefined, domain2, range);
157
158 opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM,
159 opFormUnion_createAnyOp (ltoken_and),
160 ltoken_undefined);
161
162 nn = makeNameNodeForm (opform);
163 symtable_enterOp (g_symtab, nn, sigNode_copy (sign));
164
165 opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM,
166 opFormUnion_createAnyOp (ltoken_or),
167 ltoken_undefined);
168
169 nn = makeNameNodeForm (opform);
170 symtable_enterOp (g_symtab, nn, sigNode_copy (sign));
171
172 opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM,
173 opFormUnion_createAnyOp (ltoken_implies),
174 ltoken_undefined);
175 nn = makeNameNodeForm (opform);
176 symtable_enterOp (g_symtab, nn, sign);
177
178 /* from lclscanline.c's init procedure */
179 /* comment out so we can add in lclinit.lci: synonym double float */
180 /* ReserveToken (FLOAT, "float"); */
181 /* But we need to make the scanner parse "float" not as a simpleId, but
182 as a TYPEDEF_NAME. This is done later in abstract_init */
183
184 ti->id = ltoken_createType (LLT_TYPEDEF_NAME, SID_TYPE, lsymbol_fromChars ("float"));
185
186 ti->modifiable = FALSE;
187 ti->abstract = FALSE;
188 ti->export = FALSE; /* this is implicit, not exported */
189 ti->basedOn = sort_float;
190 symtable_enterType (g_symtab, ti);
191}
192
193void
194declareForwardType (declaratorNode declare)
195{
196 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
197 sort tsort, handle;
198 lsymbol typedefname;
199
200 typedefname = ltoken_getText (declare->id);
201 ti->id = ltoken_copy (declare->id);
202
203 ltoken_setCode (ti->id, LLT_TYPEDEF_NAME);
204 ltoken_setIdType (ti->id, SID_TYPE);
205
206 ti->modifiable = FALSE;
207 ti->abstract = FALSE;
208 tsort = lclTypeSpecNode2sort (exposedType);
209 handle = typeExpr2ptrSort (tsort, declare->type);
210 ti->basedOn = sort_makeSyn (declare->id, handle, typedefname);
211 ti->export = FALSE;
212
213 symtable_enterType (g_symtab, ti);
214}
215
216void LCLBuiltins (void)
217{
218 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
219 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
220
221 /* immutable type bool;
222 uses CTrait;
223 constant bool FALSE = false;
224 constant bool TRUE = true; */
225
226 /* the following defines the builtin LSL sorts and operators */
227 LCLBootstrap ();
228
229 /* now LCL builtin proper */
230 /* do "immutable type bool;" */
231
232 ti->id = ltoken_copy (ltoken_bool);
233
234 ltoken_setCode (ti->id, LLT_TYPEDEF_NAME);
235 ltoken_setIdType (ti->id, SID_TYPE);
236
237 ti->modifiable = FALSE;
238 ti->abstract = TRUE;
239 ti->basedOn = sort_bool;
240 ti->export = FALSE; /* this wasn't set (detected by lclint) */
241 symtable_enterType (g_symtab, ti);
242
243 /* do "constant bool FALSE = false;" */
244 vi->id = ltoken_createType (simpleId, SID_VAR, lsymbol_fromChars ("FALSE"));
245
246 vi->kind = VRK_CONST;
247 vi->sort = sort_bool;
248 vi->export = TRUE;
249
250 (void) symtable_enterVar (g_symtab, vi);
251
252 /* do "constant bool TRUE = true;" */
253 /* vi->id = ltoken_copy (vi->id); */
254 ltoken_setText (vi->id, lsymbol_fromChars ("TRUE"));
255 (void) symtable_enterVar (g_symtab, vi);
256
257 varInfo_free (vi);
258
259 importCTrait ();
260}
261
262static void
263LCLBootstrap (void)
264{
265 nameNode nn1, nn2;
266 ltoken range;
267 sigNode sign;
268 sort s;
269
270 /*
271 ** Minimal we need to bootstrap is to provide the sort
272 ** "bool" and 2 bool constants "true" and "false".
273 ** sort_init should already have been called, and hence
274 ** the bool and Bool sorts defined.
275 */
276
277 s = sort_makeImmutable (ltoken_undefined, lsymbol_bool);
278 range = ltoken_create (simpleId, lsymbol_bool);
dfd82dce 279 sign = makesigNode (ltoken_undefined, ltokenList_new (), range);
616915dd 280
281 nn1 = (nameNode) dmalloc (sizeof (*nn1));
282 nn1->isOpId = TRUE;
283
284 nn1->content.opid = ltoken_create (simpleId, lsymbol_fromChars ("true"));
285
286 symtable_enterOp (g_symtab, nn1, sign);
287
288 nn2 = (nameNode) dmalloc (sizeof (*nn2));
289 nn2->isOpId = TRUE;
290 nn2->content.opid = ltoken_create (simpleId, lsymbol_fromChars ("false"));
291
292 symtable_enterOp (g_symtab, nn2, sigNode_copy (sign));
293}
294
295interfaceNodeList
296consInterfaceNode (/*@only@*/ interfaceNode n, /*@returned@*/ interfaceNodeList ns)
297{
298 /* n is never empty, but ns may be empty */
299 interfaceNodeList_addl (ns, n);
300 return (ns);
301}
302
303/*@only@*/ interfaceNode
304makeInterfaceNodeImports (/*@only@*/ importNodeList x)
305{
306 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
307 lsymbol importSymbol;
308
309 i->kind = INF_IMPORTS;
310 i->content.imports = x; /* an importNodeList */
311
312 importNodeList_elements (x, imp)
313 {
314 importSymbol = ltoken_getRawText (imp->val);
315
316 if (lsymbolSet_member (g_currentImports, importSymbol))
317 {
318 lclerror (imp->val,
319 message ("Circular imports: %s",
320 cstring_fromChars (lsymbol_toChars (importSymbol))));
321 }
322 else
323 {
324 processImport (importSymbol, imp->val, imp->kind);
325 }
326 } end_importNodeList_elements;
327
328 lhOutLine (cstring_undefined);
329 return (i);
330}
331
332/*@only@*/ interfaceNode
333makeInterfaceNodeUses (/*@only@*/ traitRefNodeList x)
334{
335 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
336
337 i->kind = INF_USES;
338 i->content.uses = x;
339 /* read in LSL traits */
340
341 return (i);
342}
343
344/*@only@*/ interfaceNode
345interfaceNode_makeConst (/*@only@*/ constDeclarationNode x)
346{
347 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
348 exportNode e = (exportNode) dmalloc (sizeof (*e));
349
350 e->kind = XPK_CONST;
351 e->content.constdeclaration = x;
352 i->kind = INF_EXPORT;
353 i->content.export = e;
354
355 return (i);
356}
357
358/*@only@*/ interfaceNode
359interfaceNode_makeVar (/*@only@*/ varDeclarationNode x)
360{
361 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
362 exportNode e = (exportNode) dmalloc (sizeof (*e));
363
364 e->kind = XPK_VAR;
365 e->content.vardeclaration = x;
366 i->kind = INF_EXPORT;
367 i->content.export = e;
368
369 if (context_msgLh ())
370 {
371 lhOutLine (lhVarDecl (x->type, x->decls, x->qualifier));
372 }
373
374 return (i);
375}
376
377/*@only@*/ interfaceNode
378interfaceNode_makeType (/*@only@*/ typeNode x)
379{
380 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
381 exportNode e = (exportNode) dmalloc (sizeof (*e));
382 e->kind = XPK_TYPE;
383 e->content.type = x;
384 i->kind = INF_EXPORT;
385 i->content.export = e;
386
387 if (context_msgLh ())
388 {
389
390 lhOutLine (lhType (x));
391 }
392
393 return (i);
394}
395
396/*@only@*/ interfaceNode
397interfaceNode_makeFcn (/*@only@*/ fcnNode x)
398{
399 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
400 exportNode e = (exportNode) dmalloc (sizeof (*e));
401
402 e->kind = XPK_FCN;
403 e->content.fcn = x;
404 i->kind = INF_EXPORT;
405 i->content.export = e;
406
407 if (context_msgLh ())
408 {
409 llassert (x->typespec != NULL);
410 llassert (x->declarator != NULL);
411
412 lhOutLine (lhFunction (x->typespec, x->declarator));
413 }
414
415 return (i);
416}
417
418/*@only@*/ interfaceNode
419interfaceNode_makeClaim (/*@only@*/ claimNode x)
420{
421 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
422 exportNode e = (exportNode) dmalloc (sizeof (*e));
423
424 e->kind = XPK_CLAIM;
425 e->content.claim = x;
426 i->kind = INF_EXPORT;
427 i->content.export = e;
428 return (i);
429}
430
431/*@only@*/ interfaceNode
432interfaceNode_makeIter (/*@only@*/ iterNode x)
433{
434 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
435 exportNode e = (exportNode) dmalloc (sizeof (*e));
436
437 e->kind = XPK_ITER;
438 e->content.iter = x;
439 i->kind = INF_EXPORT;
440 i->content.export = e;
441 return (i);
442}
443
444/*@only@*/ interfaceNode
445interfaceNode_makePrivConst (/*@only@*/ constDeclarationNode x)
446{
447 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
448 privateNode e = (privateNode) dmalloc (sizeof (*e));
449
450 e->kind = PRIV_CONST;
451 e->content.constdeclaration = x;
452 i->kind = INF_PRIVATE;
453 i->content.private = e;
454 return (i);
455}
456
457/*@only@*/ interfaceNode
458interfaceNode_makePrivVar (/*@only@*/ varDeclarationNode x)
459{
460 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
461 privateNode e = (privateNode) dmalloc (sizeof (*e));
462
463 e->kind = PRIV_VAR;
464 e->content.vardeclaration = x;
465 i->kind = INF_PRIVATE;
466 i->content.private = e;
467 return (i);
468}
469
470/*@only@*/ interfaceNode
471interfaceNode_makePrivType (/*@only@*/ typeNode x)
472{
473 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
474 privateNode e = (privateNode) dmalloc (sizeof (*e));
475
476 e->kind = PRIV_TYPE;
477 e->content.type = x;
478 i->kind = INF_PRIVATE;
479 i->content.private = e;
480 return (i);
481}
482
483/*@only@*/ interfaceNode
484interfaceNode_makePrivFcn (/*@only@*/ fcnNode x)
485{
486 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
487 privateNode e = (privateNode) dmalloc (sizeof (*e));
488
489 /*
490 ** bug detected by lclint enum checking
491 ** e->kind = XPK_FCN;
492 */
493
494 e->kind = PRIV_FUNCTION;
495 e->content.fcn = x;
496 i->kind = INF_PRIVATE;
497 i->content.private = e;
498 return (i);
499}
500
501/*@only@*/ cstring
502exportNode_unparse (exportNode n)
503{
504 if (n != (exportNode) 0)
505 {
506 switch (n->kind)
507 {
508 case XPK_CONST:
509 return (message
510 ("%q\n",
511 constDeclarationNode_unparse (n->content.constdeclaration)));
512 case XPK_VAR:
513 return (message
514 ("%q\n",
515 varDeclarationNode_unparse (n->content.vardeclaration)));
516 case XPK_TYPE:
517 return (message ("%q\n", typeNode_unparse (n->content.type)));
518 case XPK_FCN:
519 return (fcnNode_unparse (n->content.fcn));
520 case XPK_CLAIM:
521 return (claimNode_unparse (n->content.claim));
522 case XPK_ITER:
523 return (iterNode_unparse (n->content.iter));
524 default:
525 llfatalbug (message ("exportNode_unparse: unknown kind: %d", (int) n->kind));
526 }
527 }
528 return cstring_undefined;
529}
530
531/*@only@*/ cstring
532privateNode_unparse (privateNode n)
533{
534 if (n != (privateNode) 0)
535 {
536 switch (n->kind)
537 {
538 case PRIV_CONST:
539 return (constDeclarationNode_unparse (n->content.constdeclaration));
540 case PRIV_VAR:
541 return (varDeclarationNode_unparse (n->content.vardeclaration));
542 case PRIV_TYPE:
543 return (typeNode_unparse (n->content.type));
544 case PRIV_FUNCTION:
545 return (fcnNode_unparse (n->content.fcn));
546 default:
547 llfatalbug (message ("privateNode_unparse: unknown kind: %d",
548 (int) n->kind));
549 }
550 }
551 return cstring_undefined;
552}
553
554void lclPredicateNode_free (/*@null@*/ /*@only@*/ lclPredicateNode x)
555{
556 if (x != NULL)
557 {
558 termNode_free (x->predicate);
559 ltoken_free (x->tok);
560 sfree (x);
561 }
562}
563
564static /*@only@*/ cstring
565lclPredicateNode_unparse (/*@null@*/ lclPredicateNode p) /*@*/
566{
567 if (p != (lclPredicateNode) 0)
568 {
569 cstring st = cstring_undefined;
570
571 switch (p->kind)
572 {
573 case LPD_REQUIRES:
574 st = cstring_makeLiteral (" requires ");
575 break;
576 case LPD_CHECKS:
577 st = cstring_makeLiteral (" checks ");
578 break;
579 case LPD_ENSURES:
580 st = cstring_makeLiteral (" ensures ");
581 break;
582 case LPD_INTRACLAIM:
583 st = cstring_makeLiteral (" claims ");
584 break;
585 case LPD_CONSTRAINT:
586 st = cstring_makeLiteral ("constraint ");
587 break;
588 case LPD_INITIALLY:
589 st = cstring_makeLiteral ("initially ");
590 break;
591 case LPD_PLAIN:
592 break;
593 default:
594 llfatalbug (message ("lclPredicateNode_unparse: unknown kind: %d",
595 (int) p->kind));
596 }
597 return (message ("%q%q;\n", st, termNode_unparse (p->predicate)));
598 }
599 return cstring_undefined;
600}
601
602bool
603ltoken_similar (ltoken t1, ltoken t2)
604{
605 lsymbol sym1 = ltoken_getText (t1);
606 lsymbol sym2 = ltoken_getText (t2);
607
608 if (sym1 == sym2)
609 {
610 return TRUE;
611 }
612
613 if ((sym1 == eqSymbol && sym2 == equalSymbol) ||
614 (sym2 == eqSymbol && sym1 == equalSymbol))
615 {
616 return TRUE;
617 }
618
619 if ((sym1 == lsymbol_bool && sym2 == lsymbol_Bool) ||
620 (sym2 == lsymbol_bool && sym1 == lsymbol_Bool))
621 {
622 return TRUE;
623 }
624
625 return FALSE;
626}
627
628/*@only@*/ cstring
629iterNode_unparse (/*@null@*/ iterNode i)
630{
631 if (i != (iterNode) 0)
632 {
633 return (message ("iter %s %q", ltoken_unparse (i->name),
634 paramNodeList_unparse (i->params)));
635 }
636 return cstring_undefined;
637}
638
639
640/*@only@*/ cstring
641fcnNode_unparse (/*@null@*/ fcnNode f)
642{
643 if (f != (fcnNode) 0)
644 {
645 return (message ("%q %q%q{\n%q%q%q%q%q%q}\n",
646 lclTypeSpecNode_unparse (f->typespec),
647 declaratorNode_unparse (f->declarator),
648 varDeclarationNodeList_unparse (f->globals),
649 varDeclarationNodeList_unparse (f->inits),
650 letDeclNodeList_unparse (f->lets),
651 lclPredicateNode_unparse (f->require),
652 modifyNode_unparse (f->modify),
653 lclPredicateNode_unparse (f->ensures),
654 lclPredicateNode_unparse (f->claim)));
655 }
656 return cstring_undefined;
657}
658
659/*@only@*/ cstring
660varDeclarationNode_unparse (/*@null@*/ varDeclarationNode x)
661{
662 if (x != (varDeclarationNode) 0)
663 {
664 cstring st;
665
666 if (x->isSpecial)
667 {
668 return (sRef_unparse (x->sref));
669 }
670 else
671 {
672 switch (x->qualifier)
673 {
674 case QLF_NONE:
675 st = cstring_undefined;
676 break;
677 case QLF_CONST:
678 st = cstring_makeLiteral ("const ");
679 break;
680 case QLF_VOLATILE:
681 st = cstring_makeLiteral ("volatile ");
682 break;
683 BADDEFAULT;
684 }
685
686 st = message ("%q%q %q", st, lclTypeSpecNode_unparse (x->type),
687 initDeclNodeList_unparse (x->decls));
688 return (st);
689 }
690 }
691
692 return cstring_undefined;
693}
694
695/*@only@*/ cstring
696typeNode_unparse (/*@null@*/ typeNode t)
697{
698 if (t != (typeNode) 0)
699 {
700 switch (t->kind)
701 {
702 case TK_ABSTRACT:
703 return (abstractNode_unparse (t->content.abstract));
704 case TK_EXPOSED:
705 return (exposedNode_unparse (t->content.exposed));
706 case TK_UNION:
707 return (taggedUnionNode_unparse (t->content.taggedunion));
708 default:
709 llfatalbug (message ("typeNode_unparse: unknown kind: %d", (int)t->kind));
710 }
711 }
712 return cstring_undefined;
713}
714
715/*@only@*/ cstring
716constDeclarationNode_unparse (/*@null@*/ constDeclarationNode x)
717{
718 if (x != (constDeclarationNode) 0)
719 {
720 return (message ("constant %q %q", lclTypeSpecNode_unparse (x->type),
721 initDeclNodeList_unparse (x->decls)));
722 }
723
724 return cstring_undefined;
725}
726
727/*@only@*/ storeRefNode
728makeStoreRefNodeTerm (/*@only@*/ termNode t)
729{
730 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
731
732 x->kind = SRN_TERM;
733 x->content.term = t;
734 return (x);
735}
736
737/*@only@*/ storeRefNode
738makeStoreRefNodeType (/*@only@*/ lclTypeSpecNode t, bool isObj)
739{
740 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
741
742 x->kind = isObj ? SRN_OBJ : SRN_TYPE;
743 x->content.type = t;
744 return (x);
745}
746
747storeRefNode
748makeStoreRefNodeInternal (void)
749{
750 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
751
752 x->kind = SRN_SPECIAL;
753 x->content.ref = sRef_makeInternalState ();
754 return (x);
755}
756
757storeRefNode
758makeStoreRefNodeSystem (void)
759{
760 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
761
762 x->kind = SRN_SPECIAL;
763 x->content.ref = sRef_makeSystemState ();
764 return (x);
765}
766
767/*@only@*/ modifyNode
768makeModifyNodeSpecial (/*@only@*/ ltoken t, bool modifiesNothing)
769{
770 modifyNode x = (modifyNode) dmalloc (sizeof (*x));
771
772 x->tok = t;
773 x->modifiesNothing = modifiesNothing;
774 x->hasStoreRefList = FALSE;
775 return (x);
776}
777
778/*@only@*/ modifyNode
779makeModifyNodeRef (/*@only@*/ ltoken t, /*@only@*/ storeRefNodeList y)
780{
781 modifyNode x = (modifyNode) dmalloc (sizeof (*x));
782 sort sort;
783
784 x->tok = t;
785 x->hasStoreRefList = TRUE;
786 x->modifiesNothing = FALSE;
787 x->list = y;
788 /* check that all storeRef's are modifiable */
789
790 storeRefNodeList_elements (y, sr)
791 {
792 if (storeRefNode_isTerm (sr))
793 {
794 sort = sr->content.term->sort;
795
796 if (!sort_mutable (sort) && sort_isValidSort (sort))
797 {
798 ltoken errtok = termNode_errorToken (sr->content.term);
799 lclerror (errtok,
800 message ("Term denoting immutable object used in modifies list: %q",
801 termNode_unparse (sr->content.term)));
802 }
803 }
804 else
805 {
806 if (!storeRefNode_isSpecial (sr))
807 {
808 sort = lclTypeSpecNode2sort (sr->content.type);
809
810 if (storeRefNode_isObj (sr))
811 {
812 sort = sort_makeObj (sort);
813 }
814
815 if (!sort_mutable (sort))
816 {
817 ltoken errtok = lclTypeSpecNode_errorToken (sr->content.type);
818 lclerror (errtok,
819 message ("Immutable type used in modifies list: %q",
820 sort_unparse (sort)));
821 }
822 }
823 }
824 } end_storeRefNodeList_elements;
825 return (x);
826}
827
828/*@observer@*/ ltoken
829termNode_errorToken (/*@null@*/ termNode n)
830{
831 if (n != (termNode) 0)
832 {
833 switch (n->kind)
834 {
835 case TRM_LITERAL:
836 case TRM_UNCHANGEDALL:
837 case TRM_UNCHANGEDOTHERS:
838 case TRM_SIZEOF:
839 case TRM_CONST:
840 case TRM_VAR:
841 case TRM_ZEROARY: /* also the default kind, when no in symbol table */
842 return n->literal;
843 case TRM_QUANTIFIER:
844 return n->quantified->open;
845 case TRM_APPLICATION:
846 if (n->name != NULL)
847 {
848 if (n->name->isOpId)
849 {
850 return n->name->content.opid;
851 }
852 else
853 {
854 llassert (n->name->content.opform != NULL);
855 return n->name->content.opform->tok;
856 }
857 }
858 else
859 {
860 return ltoken_undefined;
861 }
862 }
863 }
864 return ltoken_undefined;
865}
866
867/*@observer@*/ ltoken
868nameNode_errorToken (/*@null@*/ nameNode nn)
869{
870 if (nn != (nameNode) 0)
871 {
872 if (nn->isOpId)
873 {
874 return nn->content.opid;
875 }
876 else
877 {
878 if (nn->content.opform != NULL)
879 {
880 return nn->content.opform->tok;
881 }
882 }
883 }
884
885 return ltoken_undefined;
886}
887
888/*@observer@*/ ltoken
889lclTypeSpecNode_errorToken (/*@null@*/ lclTypeSpecNode t)
890{
891 if (t != (lclTypeSpecNode) 0)
892 {
893 switch (t->kind)
894 {
895 case LTS_TYPE:
896 {
897 llassert (t->content.type != NULL);
898
899 if (ltokenList_empty (t->content.type->ctypes))
900 break;
901 else
902 return (ltokenList_head (t->content.type->ctypes));
903 }
904 case LTS_STRUCTUNION:
905 llassert (t->content.structorunion != NULL);
906 return t->content.structorunion->tok;
907 case LTS_ENUM:
908 llassert (t->content.enumspec != NULL);
909 return t->content.enumspec->tok;
910 case LTS_CONJ:
911 return (lclTypeSpecNode_errorToken (t->content.conj->a));
912 }
913 }
914
915 return ltoken_undefined;
916}
917
918static bool
919sort_member_modulo_cstring (sort s, /*@null@*/ termNode t)
920{
921
922 if (t != (termNode) 0)
923 {
924 if (t->kind == TRM_LITERAL)
925 { /* allow multiple types */
926 sortNode sn;
927
928 sortSet_elements (t->possibleSorts, el)
929 {
930 if (sort_compatible_modulo_cstring (s, el))
931 {
932 return TRUE;
933 }
934 } end_sortSet_elements;
935
936 sn = sort_lookup (s);
937
28bf4b0b 938 if (sn->kind == SRT_PTR)
616915dd 939 {
940 char *lit = lsymbol_toChars (ltoken_getText (t->literal));
941
942 if (lit != NULL)
943 {
944 long val = 0;
945
946 if (sscanf (lit, "%ld", &val) == 1)
947 {
948 if (val == 0) return TRUE;
949 }
950 }
951 }
952
953 return FALSE;
954 }
955 else
956 {
957 return sort_compatible_modulo_cstring (s, t->sort);
958 }
959 }
960 return FALSE;
961}
962
963/*@only@*/ letDeclNode
964 makeLetDeclNode (ltoken varid, /*@only@*/ /*@null@*/ lclTypeSpecNode t,
965 /*@only@*/ termNode term)
966{
967 letDeclNode x = (letDeclNode) dmalloc (sizeof (*x));
968 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
969 ltoken errtok;
970 sort s, termsort;
971
972 if (t != (lclTypeSpecNode) 0)
973 {
974 /* check varid has the same sort as term */
975 s = lclTypeSpecNode2sort (t);
976 termsort = term->sort;
977 /* should keep the arguments in order */
978 if (!sort_member_modulo_cstring (s, term) &&
979 !term->error_reported)
980 {
981 errtok = termNode_errorToken (term);
982
28bf4b0b 983 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
616915dd 984 /* sprintf (ERRMSG, "expect `%s' type but given term has `%s' type",
985 sort_unparse (s), sort_unparse (termsort)); */
986
987 lclerror (errtok,
988 message ("Let declaration expects type %q", sort_unparse (s)));
989 /* evs --- don't know how to generated this message or what it means? */
990 }
991 }
992 else
993 {
994 s = term->sort;
995 }
996 /* assign variable its type and sort, store in symbol table */
997 vi->id = ltoken_copy (varid);
998 vi->kind = VRK_LET;
999 vi->sort = s;
1000 vi->export = TRUE;
1001
1002 (void) symtable_enterVar (g_symtab, vi);
1003 varInfo_free (vi);
1004
1005 x->varid = varid;
1006 x->sortspec = t;
1007 x->term = term;
1008 x->sort = sort_makeNoSort ();
1009
1010 return (x);
1011}
1012
1013/*@only@*/ programNode
1014makeProgramNodeAction (/*@only@*/ programNodeList x, actionKind k)
1015{
1016 programNode n = (programNode) dmalloc (sizeof (*n));
1017 n->wrapped = 0;
1018 n->kind = k;
1019 n->content.args = x;
1020 return (n);
1021}
1022
1023/*@only@*/ programNode
1024makeProgramNode (/*@only@*/ stmtNode x)
1025{
1026 programNode n = (programNode) dmalloc (sizeof (*n));
1027
1028 n->wrapped = 0;
1029 n->kind = ACT_SELF;
1030 n->content.self = x;
1031 return (n);
1032}
1033
1034/*@only@*/ typeNode
1035makeAbstractTypeNode (/*@only@*/ abstractNode x)
1036{
1037 typeNode n = (typeNode) dmalloc (sizeof (*n));
1038
1039 n->kind = TK_ABSTRACT;
1040 n->content.abstract = x;
1041
1042 return (n);
1043}
1044
1045/*@only@*/ typeNode
1046makeExposedTypeNode (/*@only@*/ exposedNode x)
1047{
1048 typeNode n = (typeNode) dmalloc (sizeof (*n));
1049
1050 n->kind = TK_EXPOSED;
1051 n->content.exposed = x;
1052 return (n);
1053}
1054
1055/*
1056** evs added 8 Sept 1993
1057*/
1058
1059/*@only@*/ importNode
1060importNode_makePlain (/*@only@*/ ltoken t)
1061{
1062 importNode imp = (importNode) dmalloc (sizeof (*imp));
1063
1064 imp->kind = IMPPLAIN;
1065 imp->val = t;
1066 return (imp);
1067}
1068
1069/*@only@*/ importNode
1070importNode_makeBracketed (/*@only@*/ ltoken t)
1071{
1072 importNode imp = (importNode) dmalloc (sizeof (*imp));
1073
1074 imp->kind = IMPBRACKET;
1075 imp->val = t;
1076 return (imp);
1077}
1078
1079static cstring extractQuote (/*@only@*/ cstring s)
1080{
1081 int len = cstring_length (s);
1082 char *sc = cstring_toCharsSafe (s);
1083 cstring t;
1084
1085 llassert (len > 1);
1086 *(sc + len - 1) = '\0';
1087 t = cstring_fromChars (mstring_copy (sc + 1));
1088 cstring_free (s);
1089 return (t);
1090}
1091
1092/*@only@*/ importNode
1093importNode_makeQuoted (/*@only@*/ ltoken t)
1094{
1095 importNode imp = (importNode) dmalloc (sizeof (*imp));
1096 cstring q = extractQuote (cstring_copy (ltoken_getRawString (t)));
1097
1098 imp->kind = IMPQUOTE;
1099
28bf4b0b 1100 ltoken_setRawText (t, lsymbol_fromString (q));
616915dd 1101
1102 imp->val = t;
1103
1104 cstring_free (q);
1105 return (imp);
1106}
1107
1108/*
1109** check that is it '<' and '>'
1110** should probably be in a different file?
1111*/
1112
1113static void cylerror (/*@only@*/ char *s)
1114{
1115 ylerror(s);
1116 sfree (s);
1117}
1118
1119void
1120checkBrackets (ltoken lb, ltoken rb)
1121{
1122 /* no attempt at error recovery...not really necessary */
1123 cstring tname;
1124
1125 tname = ltoken_getRawString (lb);
1126
1127 if (!cstring_equalLit (tname, "<"))
1128 {
1129 cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname)));
1130 }
1131
1132 tname = ltoken_getRawString (rb);
1133
1134 if (!cstring_equalLit (tname, ">"))
1135 {
1136 cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname)));
1137 }
1138}
1139
1140/*@only@*/ traitRefNode
1141makeTraitRefNode (/*@only@*/ ltokenList fl, /*@only@*/ renamingNode r)
1142{
1143 traitRefNode n = (traitRefNode) dmalloc (sizeof (*n));
1144
1145 n->traitid = fl;
1146 n->rename = r;
1147 return (n);
1148}
1149
1150/*
1151** printLeaves: no commas
1152*/
1153
1154static /*@only@*/ cstring
1155printLeaves (ltokenList f)
1156{
1157 bool firstone = TRUE;
1158 cstring s = cstring_undefined;
1159
1160 ltokenList_elements (f, i)
1161 {
1162 if (firstone)
1163 {
1164 s = cstring_copy (ltoken_unparse (i));
1165 firstone = FALSE;
1166 }
1167 else
1168 {
1169 s = message ("%q %s", s, ltoken_unparse (i));
1170 }
1171 } end_ltokenList_elements;
1172
1173 return s;
1174}
1175
1176
1177/*@only@*/ cstring
1178printLeaves2 (ltokenList f)
1179{
1180 return (ltokenList_unparse (f));
1181}
1182
1183/*@only@*/ cstring
1184printRawLeaves2 (ltokenList f)
1185{
1186 bool first = TRUE;
1187 cstring s = cstring_undefined;
1188
1189 ltokenList_elements (f, i)
1190 {
1191 if (first)
1192 {
1193 s = message ("%s", ltoken_getRawString (i));
1194 first = FALSE;
1195 }
1196 else
1197 s = message ("%q, %s", s, ltoken_getRawString (i));
1198 } end_ltokenList_elements;
1199
1200 return s;
1201}
1202
1203/*@only@*/ renamingNode
1204makeRenamingNode (/*@only@*/ typeNameNodeList n, /*@only@*/ replaceNodeList r)
1205{
1206 renamingNode ren = (renamingNode) dmalloc (sizeof (*ren));
1207
1208 if (typeNameNodeList_empty (n))
1209 {
1210 ren->is_replace = TRUE;
1211 ren->content.replace = r;
1212 typeNameNodeList_free (n);
1213 }
1214 else
1215 {
1216 nameAndReplaceNode nr = (nameAndReplaceNode) dmalloc (sizeof (*nr));
1217 nr->replacelist = r;
1218 nr->namelist = n;
1219 ren->is_replace = FALSE;
1220 ren->content.name = nr;
1221 }
1222
1223 return (ren);
1224}
1225
1226/*@only@*/ cstring
1227renamingNode_unparse (/*@null@*/ renamingNode x)
1228{
1229 if (x != (renamingNode) 0)
1230 {
1231 if (x->is_replace)
1232 {
1233 return (replaceNodeList_unparse (x->content.replace));
1234 }
1235 else
1236 {
1237 return (message ("%q%q", typeNameNodeList_unparse (x->content.name->namelist),
1238 replaceNodeList_unparse (x->content.name->replacelist)));
1239 }
1240 }
1241 return cstring_undefined;
1242}
1243
1244/*@only@*/ replaceNode
1245makeReplaceNameNode (ltoken t, typeNameNode tn, nameNode nn)
1246{
1247 replaceNode r = (replaceNode) dmalloc (sizeof (*r));
1248
1249 r->tok = t;
1250 r->isCType = FALSE;
1251 r->typename = tn;
1252 r->content.renamesortname.name = nn;
28bf4b0b 1253 r->content.renamesortname.signature = (sigNode) NULL;
616915dd 1254
1255 return (r);
1256}
1257
1258/*@only@*/ replaceNode
1259makeReplaceNode (ltoken t, typeNameNode tn,
1260 bool is_ctype, ltoken ct,
1261 nameNode nn, sigNode sn)
1262{
1263 replaceNode r = (replaceNode) dmalloc (sizeof (*r));
1264
1265 r->tok = t;
1266 r->isCType = is_ctype;
1267 r->typename = tn;
1268
1269 if (is_ctype)
1270 {
1271 r->content.ctype = ct;
1272 sigNode_free (sn);
1273 nameNode_free (nn);
1274 }
1275 else
1276 {
1277 r->content.renamesortname.name = nn;
1278 r->content.renamesortname.signature = sn;
1279 ltoken_free (ct);
1280 }
1281
1282 return (r);
1283}
1284
1285/*@only@*/ cstring
1286replaceNode_unparse (/*@null@*/ replaceNode x)
1287{
1288 if (x != (replaceNode) 0)
1289 {
1290 cstring st;
1291
1292 st = message ("%q for ", typeNameNode_unparse (x->typename));
1293
1294 if (x->isCType)
1295 {
1296 st = message ("%q%s", st, ltoken_getRawString (x->content.ctype));
1297 }
1298 else
1299 {
1300 st = message ("%q%q%q", st, nameNode_unparse (x->content.renamesortname.name),
1301 sigNode_unparse (x->content.renamesortname.signature));
1302 }
1303 return st;
1304 }
1305 return cstring_undefined;
1306}
1307
1308/*@only@*/ nameNode
1309makeNameNodeForm (/*@only@*/ /*@null@*/ opFormNode opform)
1310{
1311 nameNode nn = (nameNode) dmalloc (sizeof (*nn));
1312
1313 nn->isOpId = FALSE;
1314 nn->content.opform = opform;
1315
1316 return (nn);
1317}
1318
1319/*@only@*/ nameNode
1320makeNameNodeId (/*@only@*/ ltoken opid)
1321{
1322 nameNode nn = (nameNode) dmalloc (sizeof (*nn));
1323
1324 /*
1325 ** current LSL -syms output bug produces "if_then_else_" rather
1326 ** than 6 separate tokens
1327 */
1328
1329 if (ltoken_getText (opid) == ConditionalSymbol)
1330 {
1331 opFormNode opform = makeOpFormNode (ltoken_undefined, OPF_IF,
1332 opFormUnion_createMiddle (0),
1333 ltoken_undefined);
1334 nn->isOpId = FALSE;
1335 nn->content.opform = opform;
1336 ltoken_free (opid);
1337 }
1338 else
1339 {
1340 nn->isOpId = TRUE;
1341 nn->content.opid = opid;
1342 }
1343
1344 return (nn);
1345}
1346
1347/*@only@*/ cstring
1348nameNode_unparse (/*@null@*/ nameNode n)
1349{
1350 if (n != (nameNode) 0)
1351 {
1352 if (n->isOpId)
1353 {
1354 return (cstring_copy (ltoken_getRawString (n->content.opid))); /*!!!*/
1355 }
1356 else
1357 {
1358 return (opFormNode_unparse (n->content.opform));
1359 }
1360 }
1361 return cstring_undefined;
1362}
1363
1364/*@only@*/ sigNode
1365makesigNode (ltoken t, /*@only@*/ ltokenList domain, ltoken range)
1366{
1367 sigNode s = (sigNode) dmalloc (sizeof (*s));
1368 unsigned int key;
1369
1370 /*
1371 ** Assign a hash key here to speed up lookup of operators.
1372 */
1373
1374 s->tok = t;
1375 s->domain = domain;
1376 s->range = range;
1377 key = MASH (0, ltoken_getText (range));
1378
1379 ltokenList_elements (domain, id)
1380 {
1381 lsymbol sym = ltoken_getText (id);
1382 key = MASH (key, sym);
1383 } end_ltokenList_elements;
1384
1385 s->key = key;
1386 return (s);
1387}
1388
1389cstring sigNode_unparse (/*@null@*/ sigNode n)
1390{
1391 if (n != (sigNode) 0)
1392 {
1393 return (message (":%q -> %s", printLeaves2 (n->domain),
1394 ltoken_unparse (n->range)));
1395 }
1396
1397 return cstring_undefined;
1398}
1399
1400void sigNode_markOwned (sigNode n)
1401{
1402 sfreeEventually (n);
1403}
1404
1405/*@only@*/ cstring
1406sigNode_unparseText (/*@null@*/ sigNode n)
1407{
1408 if (n != (sigNode) 0)
1409 {
1410 return (message ("%q -> %s", printLeaves2 (n->domain),
1411 ltoken_unparse (n->range)));
1412 }
1413 return cstring_undefined;
1414}
1415
1416static unsigned int
1417 opFormNode2key (opFormNode op, opFormKind k)
1418{
1419 unsigned int key;
1420
1421 switch (k)
1422 {
1423 case OPF_IF:
1424 /* OPF_IF is the first enum, so it's 0 */
1425
1426 /*@-type@*/
1427 key = MASH (k, k + 1);
1428 /*@=type@*/
1429
1430 break;
1431 case OPF_ANYOP:
1432 case OPF_MANYOP:
1433 case OPF_ANYOPM:
1434 case OPF_MANYOPM:
1435 { /* treat eq and = the same */
1436 lsymbol sym = ltoken_getText (op->content.anyop);
1437
1438 if (sym == equalSymbol)
1439 {
1440 key = MASH (k, eqSymbol);
1441 }
1442 else
1443 {
1444 key = MASH (k, ltoken_getText (op->content.anyop));
1445 }
1446 break;
1447 }
1448 case OPF_MIDDLE:
1449 case OPF_MMIDDLE:
1450 case OPF_MIDDLEM:
1451 case OPF_MMIDDLEM:
1452 case OPF_BMIDDLE:
1453 case OPF_BMMIDDLE:
1454 case OPF_BMIDDLEM:
1455 case OPF_BMMIDDLEM:
1456 key = MASH (k, op->content.middle);
1457 key = MASH (key, ltoken_getRawText (op->tok));
1458 break;
1459 case OPF_SELECT:
1460 case OPF_MAP:
1461 case OPF_MSELECT:
1462 case OPF_MMAP:
1463 key = MASH (k, ltoken_getRawText (op->content.id));
1464 break;
1465 default:
1466 key = 0;
1467 }
1468
1469 return key;
1470}
1471
1472/*@only@*/ opFormNode
1473makeOpFormNode (ltoken t, opFormKind k, opFormUnion u,
1474 ltoken close)
1475{
1476 opFormNode n = (opFormNode) dmalloc (sizeof (*n));
1477 unsigned int key = 0;
1478
1479 /*
1480 ** Assign a hash key here to speed up lookup of operators.
1481 */
1482
1483 n->tok = t;
1484 n->close = close;
1485 n->kind = k;
1486
1487
1488 switch (k)
1489 {
1490 case OPF_IF:
1491 n->content.middle = 0;
1492 /* OPF_IF is the first enum, so it's 0 */
1493 key = MASH /*@+enumint@*/ (k, k + 1) /*@=enumint@*/;
1494 break;
1495 case OPF_ANYOP:
1496 case OPF_MANYOP:
1497 case OPF_ANYOPM:
1498 case OPF_MANYOPM:
1499 { /* treat eq and = the same */
1500 lsymbol sym = ltoken_getText (u.anyop);
1501
1502 if (sym == equalSymbol)
1503 {
1504 key = MASH (k, eqSymbol);
1505 }
1506 else
1507 {
1508 key = MASH (k, ltoken_getText (u.anyop));
1509 }
1510
1511 n->content = u;
1512 break;
1513 }
1514 case OPF_MIDDLE:
1515 case OPF_MMIDDLE:
1516 case OPF_MIDDLEM:
1517 case OPF_MMIDDLEM:
1518 case OPF_BMIDDLE:
1519 case OPF_BMMIDDLE:
1520 case OPF_BMIDDLEM:
1521 case OPF_BMMIDDLEM:
1522 n->content = u;
1523 key = MASH (k, u.middle);
1524 key = MASH (key, ltoken_getRawText (t));
1525 break;
1526 case OPF_SELECT:
1527 case OPF_MAP:
1528 case OPF_MSELECT:
1529 case OPF_MMAP:
1530 key = MASH (k, ltoken_getRawText (u.id));
1531 n->content = u;
1532 break;
1533 default:
1534 {
1535 llbug (message ("makeOpFormNode: unknown opFormKind: %d", (int) k));
1536 }
1537 }
1538 n->key = key;
1539 return (n);
1540}
1541
1542static cstring printMiddle (int j)
1543{
1544 int i;
1545 char *s = mstring_createEmpty ();
1546
1547 for (i = j; i >= 1; i--)
1548 {
1549 s = mstring_concatFree1 (s, "__");
1550
1551 if (i != 1)
1552 {
1553 s = mstring_concatFree1 (s, ", ");
1554 }
1555 }
1556
1557 return cstring_fromCharsO (s);
1558}
1559
1560/*@only@*/ cstring
1561opFormNode_unparse (/*@null@*/ opFormNode n)
1562{
1563 if (n != (opFormNode) 0)
1564 {
1565 switch (n->kind)
1566 {
1567 case OPF_IF:
1568 return (cstring_makeLiteral ("if __ then __ else __ "));
1569 case OPF_ANYOP:
1570 return (cstring_copy (ltoken_getRawString (n->content.anyop)));
1571 case OPF_MANYOP:
1572 return (message ("__ %s", ltoken_getRawString (n->content.anyop)));
1573 case OPF_ANYOPM:
1574 return (message ("%s __ ", ltoken_getRawString (n->content.anyop)));
1575 case OPF_MANYOPM:
1576 return (message ("__ %s __ ", ltoken_getRawString (n->content.anyop)));
1577 case OPF_MIDDLE:
1578 return (message ("%s %q %s",
1579 ltoken_getRawString (n->tok),
1580 printMiddle (n->content.middle),
1581 ltoken_getRawString (n->close)));
1582 case OPF_MMIDDLE:
1583 return (message ("__ %s %q %s",
1584 ltoken_getRawString (n->tok),
1585 printMiddle (n->content.middle),
1586 ltoken_getRawString (n->close)));
1587 case OPF_MIDDLEM:
1588 return (message ("%s %q %s __",
1589 ltoken_getRawString (n->tok),
1590 printMiddle (n->content.middle),
1591 ltoken_getRawString (n->close)));
1592 case OPF_MMIDDLEM:
1593 return (message ("__ %s%q %s __",
1594 ltoken_getRawString (n->tok),
1595 printMiddle (n->content.middle),
1596 ltoken_getRawString (n->close)));
1597 case OPF_BMIDDLE:
1598 return (message ("[%q]", printMiddle (n->content.middle)));
1599 case OPF_BMMIDDLE:
1600 return (message ("__ [%q]", printMiddle (n->content.middle)));
1601 case OPF_BMIDDLEM:
1602 return (message ("[%q] __", printMiddle (n->content.middle)));
1603 case OPF_BMMIDDLEM:
1604 return (message ("__ [%q] __", printMiddle (n->content.middle)));
1605 case OPF_SELECT:
1606 return (message (" \\select %s", ltoken_getRawString (n->content.id)));
1607 case OPF_MAP:
1608 return (message (" \\field_arrow%s", ltoken_getRawString (n->content.id)));
1609 case OPF_MSELECT:
1610 return (message ("__ \\select %s", ltoken_getRawString (n->content.id)));
1611 case OPF_MMAP:
1612 return (message ("__ \\field_arrow %s", ltoken_getRawString (n->content.id)));
1613 default:
1614 llfatalbug (message ("opFormNodeUnparse: unknown kind: %d",
1615 (int) n->kind));
1616 }
1617 }
1618 return cstring_undefined;
1619}
1620
1621/*@only@*/ typeNameNode
1622makeTypeNameNode (bool isObj, lclTypeSpecNode t, abstDeclaratorNode n)
1623{
1624 typeNameNode tn = (typeNameNode) dmalloc (sizeof (*tn));
1625 typeNamePack p = (typeNamePack) dmalloc (sizeof (*p));
1626
1627 tn->isTypeName = TRUE;
1628 p->isObj = isObj;
1629 p->type = t;
1630 p->abst = n;
1631 tn->opform = (opFormNode) 0;
1632 tn->typename = p;
1633 return (tn);
1634}
1635
1636/*@only@*/ typeNameNode
1637makeTypeNameNodeOp (opFormNode n)
1638{
1639 typeNameNode t = (typeNameNode) dmalloc (sizeof (*t));
1640 t->typename = (typeNamePack) 0;
1641 t->opform = n;
1642 t->isTypeName = FALSE;
1643 return (t);
1644}
1645
1646/*@only@*/ cstring
1647typeNameNode_unparse (/*@null@*/ typeNameNode n)
1648{
1649 if (n != (typeNameNode) 0)
1650 {
1651 if (n->isTypeName)
1652 {
1653 cstring st = cstring_undefined;
1654 typeNamePack p = n->typename;
1655
1656 llassert (p != NULL);
1657
1658 if (p->isObj)
1659 st = cstring_makeLiteral ("obj ");
1660
1661 return (message ("%q%q%q", st, lclTypeSpecNode_unparse (p->type),
1662 abstDeclaratorNode_unparse (p->abst)));
1663
1664 }
1665 else
1666 return (opFormNode_unparse (n->opform));
1667 }
1668 return cstring_undefined;
1669}
1670
1671/*@only@*/ lclTypeSpecNode
1672makeLclTypeSpecNodeConj (/*@null@*/ lclTypeSpecNode a, /*@null@*/ lclTypeSpecNode b)
1673{
1674 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1675
1676 n->kind = LTS_CONJ;
1677 n->pointers = 0;
1678 n->quals = qualList_new ();
1679 n->content.conj = (lclconj) dmalloc (sizeof (*n->content.conj));
1680 n->content.conj->a = a;
1681 n->content.conj->b = b;
1682
1683 return (n);
1684}
1685
1686/*@only@*/ lclTypeSpecNode
1687makeLclTypeSpecNodeType (/*@null@*/ CTypesNode x)
1688{
1689 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1690
1691 n->kind = LTS_TYPE;
1692 n->pointers = 0;
1693 n->content.type = x;
1694 n->quals = qualList_new ();
1695 return (n);
1696}
1697
1698/*@only@*/ lclTypeSpecNode
1699makeLclTypeSpecNodeSU (/*@null@*/ strOrUnionNode x)
1700{
1701 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1702
1703 n->kind = LTS_STRUCTUNION;
1704 n->pointers = 0;
1705 n->content.structorunion = x;
1706 n->quals = qualList_new ();
1707 return (n);
1708}
1709
1710/*@only@*/ lclTypeSpecNode
1711makeLclTypeSpecNodeEnum (/*@null@*/ enumSpecNode x)
1712{
1713 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1714
1715 n->quals = qualList_new ();
1716 n->kind = LTS_ENUM;
1717 n->pointers = 0;
1718 n->content.enumspec = x;
1719 return (n);
1720}
1721
1722lclTypeSpecNode
1723lclTypeSpecNode_addQual (lclTypeSpecNode n, qual q)
1724{
1725 llassert (lclTypeSpecNode_isDefined (n));
1726 n->quals = qualList_add (n->quals, q);
1727 return n;
1728}
1729
1730/*@only@*/ cstring
1731lclTypeSpecNode_unparse (/*@null@*/ lclTypeSpecNode n)
1732{
1733 if (n != (lclTypeSpecNode) 0)
1734 {
1735 switch (n->kind)
1736 {
1737 case LTS_TYPE:
1738 llassert (n->content.type != NULL);
1739 return (printLeaves (n->content.type->ctypes));
1740 case LTS_STRUCTUNION:
1741 return (strOrUnionNode_unparse (n->content.structorunion));
1742 case LTS_ENUM:
1743 return (enumSpecNode_unparse (n->content.enumspec));
1744 case LTS_CONJ:
1745 return (lclTypeSpecNode_unparse (n->content.conj->a));
1746 default:
1747 llfatalbug (message ("lclTypeSpecNode_unparse: unknown lclTypeSpec kind: %d",
1748 (int) n->kind));
1749 }
1750 }
1751 return cstring_undefined;
1752}
1753
1754/*@only@*/ enumSpecNode
1755makeEnumSpecNode (ltoken t, ltoken optTagId,
1756 /*@owned@*/ ltokenList enums)
1757{
1758 enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n));
1759 tagInfo ti;
1760 smemberInfo *top = smemberInfo_undefined;
1761
1762 n->tok = t;
1763 n->opttagid = ltoken_copy (optTagId);
1764 n->enums = enums;
1765
1766 /* generate sort for this LCL type */
1767 n->sort = sort_makeEnum (optTagId);
1768
1769 if (!ltoken_isUndefined (optTagId))
1770 {
1771 /* First, check to see if tag is already defined */
1772 ti = symtable_tagInfo (g_symtab, ltoken_getText (optTagId));
1773
1774 if (tagInfo_exists (ti))
1775 {
1776 if (ti->kind == TAG_ENUM)
1777 {
1778 /* 23 Sep 1995 --- had been noting here...is this right? */
1779
1780 ti->content.enums = enums;
1781 ti->sort = n->sort;
1782 ti->imported = context_inImport ();
1783 }
1784 else
1785 {
1786 lclerror (optTagId,
1787 message ("Tag %s previously defined as %q, redefined as enum",
1788 ltoken_getRawString (optTagId),
1789 tagKind_unparse (ti->kind)));
1790
1791 /* evs --- shouldn't they be in different name spaces? */
1792 }
1793
1794 ltoken_free (optTagId);
1795 }
1796 else
1797 {
1798 ti = (tagInfo) dmalloc (sizeof (*ti));
1799
1800 ti->kind = TAG_ENUM;
1801 ti->id = optTagId;
1802 ti->content.enums = enums;
1803 ti->sort = n->sort;
1804 ti->imported = context_inImport ();
1805 /* First, store tag info in symbol table */
1806 (void) symtable_enterTag (g_symtab, ti);
1807 }
1808 }
1809
1810 /* check that enumeration constants are unique */
1811
1812 ltokenList_reset (enums);
1813
1814 while (!ltokenList_isFinished (enums))
1815 {
1816 ltoken c = ltokenList_current (enums);
1817 smemberInfo *ei = (smemberInfo *) dmalloc (sizeof (*ei));
1818
1819 ei->name = ltoken_getText (c);
1820 ei->next = top;
1821 ei->sort = n->sort;
1822 top = ei;
1823
1824 if (!varInfo_exists (symtable_varInfo (g_symtab, ltoken_getText (c))))
1825 { /* put info into symbol table */
1826 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
1827
1828 vi->id = ltoken_copy (c);
1829 vi->kind = VRK_ENUM;
1830 vi->sort = n->sort;
1831 vi->export = TRUE;
1832
1833 (void) symtable_enterVar (g_symtab, vi);
1834 varInfo_free (vi);
1835 }
1836 else
1837 {
1838 lclerror (c, message ("Enumerated value redeclared: %s",
1839 ltoken_getRawString (c)));
1840 ltokenList_removeCurrent (enums);
1841 }
1842 ltokenList_advance (enums);
1843 /*@-branchstate@*/
1844 }
1845 /*@=branchstate@*/
1846
1847 (void) sort_updateEnum (n->sort, top);
1848 return (n);
1849}
1850
1851/*@only@*/ enumSpecNode
1852makeEnumSpecNode2 (ltoken t, ltoken tagid)
1853{
1854 /* a reference, not a definition */
1855 enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n));
1856 tagInfo ti = symtable_tagInfo (g_symtab, ltoken_getText (tagid));
1857
1858 n->tok = t;
1859 n->opttagid = tagid;
1860 n->enums = ltokenList_new ();
1861
1862 if (tagInfo_exists (ti))
1863 {
1864 if (ti->kind == TAG_ENUM)
1865 {
1866 n->sort = ti->sort;
1867 }
1868 else
1869 {
1870 n->sort = sort_makeNoSort ();
1871 lclerror (tagid, message ("Tag %s defined as %q, used as enum",
1872 ltoken_getRawString (tagid),
1873 tagKind_unparse (ti->kind)));
1874 }
1875 }
1876 else
1877 {
1878 n->sort = sort_makeNoSort ();
1879 lclerror (t, message ("Undefined type: enum %s",
1880 ltoken_getRawString (tagid)));
1881 }
1882
1883 return (n);
1884}
1885
1886/*@only@*/ cstring
1887enumSpecNode_unparse (/*@null@*/ enumSpecNode n)
1888{
1889 if (n != (enumSpecNode) 0)
1890 {
1891 cstring s = cstring_makeLiteral ("enum ");
1892
1893 if (!ltoken_isUndefined (n->opttagid))
1894 {
1895 s = message ("%q%s ", s, ltoken_getRawString (n->opttagid));
1896 }
1897
1898 s = message ("%q{%q}", s, printLeaves2 (n->enums));
1899 return s;
1900 }
1901 return cstring_undefined;
1902}
1903
1904/*@only@*/ strOrUnionNode
1905makestrOrUnionNode (ltoken str, suKind k, ltoken opttagid,
1906 /*@only@*/ stDeclNodeList x)
1907{
1908 strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n));
1909 lsymbolSet set = lsymbolSet_new ();
1910 declaratorNodeList declarators;
1911 sort fieldsort, tsort1, tsort2;
1912 smemberInfo *mi, *top = smemberInfo_undefined;
1913 bool doTag = FALSE;
1914 bool isStruct = (k == SU_STRUCT);
1915 tagInfo t;
1916
1917
1918 n->kind = k;
1919 n->tok = str;
1920 n->opttagid = ltoken_copy (opttagid);
1921 n->structdecls = x;
1922 n->sort = isStruct ? sort_makeStr (opttagid) : sort_makeUnion (opttagid);
1923
1924 if (!ltoken_isUndefined (opttagid))
1925 {
1926 /* First, check to see if tag is already defined */
1927 t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid));
1928
1929 if (tagInfo_exists (t))
1930 {
1931 if ((t->kind == TAG_FWDUNION && k == SU_UNION) ||
1932 (t->kind == TAG_FWDSTRUCT && k == SU_STRUCT))
1933 {
1934 /* to allow self-recursive types and forward tag declarations */
1935 t->content.decls = stDeclNodeList_copy (x); /* update tag info */
1936 t->sort = n->sort;
1937 }
1938 else
1939 {
1940 lclerror (opttagid,
1941 message ("Tag %s previously defined as %q, used as %q",
1942 ltoken_getRawString (opttagid),
1943 tagKind_unparse (t->kind),
1944 cstring_makeLiteral (isStruct ? "struct" : "union")));
1945 }
1946 }
1947 else
1948 {
1949 doTag = TRUE;
1950 }
1951 }
1952 else
1953 {
1954 doTag = TRUE;
1955 }
1956
1957 if (doTag && !ltoken_isUndefined (opttagid))
1958 {
1959 t = (tagInfo) dmalloc (sizeof (*t));
1960
1961 /* can either override prev defn or use prev defn */
1962 /* override it so as to detect more errors */
1963
1964 t->kind = (k == SU_STRUCT) ? TAG_STRUCT : TAG_UNION;
1965 t->id = opttagid;
1966 t->content.decls = stDeclNodeList_copy (x);
1967 t->sort = n->sort;
1968 t->imported = FALSE;
1969
1970 /* Next, update tag info in symbol table */
1971 (void) symtable_enterTagForce (g_symtab, t);
1972 }
1973
1974 /* check no duplicate field names */
1975
1976 stDeclNodeList_elements (x, i)
1977 {
1978 fieldsort = lclTypeSpecNode2sort (i->lcltypespec);
1979
1980 /* need the locations, not values */
1981 /* fieldsort = sort_makeObj (fieldsort); */
1982 /* 2/19/93, was
1983 fieldsort = sort_makeGlobal (fieldsort); */
1984
1985 declarators = i->declarators;
1986
1987 declaratorNodeList_elements (declarators, decl)
1988 {
1989 lsymbol fieldname;
1990 mi = (smemberInfo *) dmalloc (sizeof (*mi));
1991 /* need to make dynamic copies */
1992 fieldname = ltoken_getText (decl->id);
1993
1994 /* 2/19/93, added */
1995 tsort1 = typeExpr2ptrSort (fieldsort, decl->type);
1996 tsort2 = sort_makeGlobal (tsort1);
1997
1998 mi->name = fieldname;
1999 mi->sort = tsort2; /* fieldsort; */
2000 mi->next = top;
2001 top = mi;
2002
2003 if (lsymbolSet_member (set, fieldname))
2004 {
2005 lclerror (decl->id,
2006 message ("Field name reused: %s",
2007 ltoken_getRawString (decl->id)));
2008 }
2009 else
2010 {
2011 (void) lsymbolSet_insert (set, fieldname);
2012 }
2013 /*@-branchstate@*/
2014 } end_declaratorNodeList_elements;
2015 /*@=branchstate@*/
2016 } end_stDeclNodeList_elements;
2017
2018 if (k == SU_STRUCT)
2019 {
2020 (void) sort_updateStr (n->sort, top);
2021 }
2022 else
2023 {
2024 (void) sort_updateUnion (n->sort, top);
2025 }
2026
2027 /* We shall keep the info with both tags and types if any
2028 of them are present. */
2029
2030 lsymbolSet_free (set);
2031
2032 return (n);
2033}
2034
2035/*@only@*/ strOrUnionNode
2036makeForwardstrOrUnionNode (ltoken str, suKind k,
2037 ltoken tagid)
2038{
2039 strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n));
2040 sort sort = sort_makeNoSort ();
2041 tagInfo t;
2042
2043 /* a reference, not a definition */
2044
2045 n->kind = k;
2046 n->tok = str;
2047 n->opttagid = tagid;
2048 n->structdecls = stDeclNodeList_new ();
2049
2050 /* get sort for this LCL type */
2051 t = symtable_tagInfo (g_symtab, ltoken_getText (tagid));
2052
2053 if (tagInfo_exists (t))
2054 {
2055 sort = t->sort;
2056
2057 if (!(((t->kind == TAG_STRUCT || t->kind == TAG_FWDSTRUCT) && k == SU_STRUCT)
2058 || ((t->kind == TAG_UNION || t->kind == TAG_FWDUNION) && k == SU_UNION)))
2059 {
2060 lclerror (tagid,
2061 message ("Tag %s previously defined as %q, used as %q",
2062 ltoken_getRawString (tagid),
2063 tagKind_unparse (t->kind),
2064 cstring_makeLiteral ((k == SU_STRUCT) ? "struct" : "union")));
2065 }
2066 }
2067 else
2068 {
2069 /*
2070 ** changed from error: 31 Mar 1994
2071 **
2072 ** lclerror (str, message ("Undefined type: %s %s", s, ltoken_getRawString (tagid));
2073 **
2074 */
2075
2076 /* forward struct's and union's are ok... */
2077
2078 if (k == SU_STRUCT)
2079 {
2080 (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy (tagid));
2081 lhForwardStruct (tagid);
2082 sort = sort_makeStr (tagid);
2083 }
2084 else
2085 {
2086 (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy (tagid));
2087 lhForwardUnion (tagid);
2088 sort = sort_makeUnion (tagid);
2089 }
2090 }
2091
2092 n->sort = sort;
2093 return (n);
2094}
2095
2096/*@only@*/ cstring
2097strOrUnionNode_unparse (/*@null@*/ strOrUnionNode n)
2098{
2099 if (n != (strOrUnionNode) 0)
2100 {
2101 cstring s;
2102 switch (n->kind)
2103 {
2104 case SU_STRUCT:
2105 s = cstring_makeLiteral ("struct ");
2106 break;
2107 case SU_UNION:
2108 s = cstring_makeLiteral ("union ");
2109 break;
2110 BADDEFAULT
2111 }
2112
2113 if (!ltoken_isUndefined (n->opttagid))
2114 {
2115 s = message ("%q%s ", s, ltoken_getRawString (n->opttagid));
2116 }
2117 s = message ("%q{%q}", s, stDeclNodeList_unparse (n->structdecls));
2118 return s;
2119 }
2120 return cstring_undefined;
2121}
2122
2123/*@only@*/ stDeclNode
2124makestDeclNode (lclTypeSpecNode s,
2125 declaratorNodeList x)
2126{
2127 stDeclNode n = (stDeclNode) dmalloc (sizeof (*n));
2128
2129 n->lcltypespec = s;
2130 n->declarators = x;
2131 return n;
2132}
2133
2134/*@only@*/ typeExpr
2135makeFunctionNode (typeExpr x, paramNodeList p)
2136{
2137 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2138
2139 y->wrapped = 0;
2140 y->kind = TEXPR_FCN;
2141 y->content.function.returntype = x;
2142 y->content.function.args = p;
2143 y->sort = sort_makeNoSort ();
2144
2145 return (y);
2146}
2147
2148static /*@observer@*/ ltoken
2149 extractDeclarator (/*@null@*/ typeExpr t)
2150{
2151 if (t != (typeExpr) 0)
2152 {
2153 switch (t->kind)
2154 {
2155 case TEXPR_BASE:
2156 return t->content.base;
2157 case TEXPR_PTR:
2158 return (extractDeclarator (t->content.pointer));
2159 case TEXPR_ARRAY:
2160 return (extractDeclarator (t->content.array.elementtype));
2161 case TEXPR_FCN:
2162 return (extractDeclarator (t->content.function.returntype));
2163 }
2164 }
2165
2166 return ltoken_undefined;
2167}
2168
2169/*@only@*/ typeExpr
2170makeTypeExpr (ltoken t)
2171{
2172 typeExpr x = (typeExpr) dmalloc (sizeof (*x));
2173
2174
2175 x->wrapped = 0;
2176 x->kind = TEXPR_BASE;
2177 x->content.base = t;
2178 x->sort = sort_makeNoSort ();
2179
2180 return (x);
2181}
2182
2183
2184/*@only@*/ declaratorNode
2185makeDeclaratorNode (typeExpr t)
2186{
2187 declaratorNode x = (declaratorNode) dmalloc (sizeof (*x));
2188
2189 x->id = ltoken_copy (extractDeclarator (t));
2190 x->type = t;
2191 x->isRedecl = FALSE;
2192
2193 return (x);
2194}
2195
2196static /*@only@*/ declaratorNode
2197makeUnknownDeclaratorNode (/*@only@*/ ltoken t)
2198{
2199 declaratorNode x = (declaratorNode) dmalloc (sizeof (*x));
2200
2201 x->id = t;
2202 x->type = (typeExpr) 0;
2203 x->isRedecl = FALSE;
2204
2205 return (x);
2206}
2207
2208static /*@only@*/ cstring
2209printTypeExpr2 (/*@null@*/ typeExpr x)
2210{
2211 paramNodeList params;
2212
2213 if (x != (typeExpr) 0)
2214 {
2215 cstring s; /* print out types in reverse order */
2216
2217 switch (x->kind)
2218 {
2219 case TEXPR_BASE:
2220 return (message ("%s ", ltoken_getRawString (x->content.base)));
2221 case TEXPR_PTR:
2222 return (message ("%qptr to ", printTypeExpr2 (x->content.pointer)));
2223 case TEXPR_ARRAY:
2224 return (message ("array[%q] of %q",
2225 termNode_unparse (x->content.array.size),
2226 printTypeExpr2 (x->content.array.elementtype)));
2227 case TEXPR_FCN:
2228 s = printTypeExpr2 (x->content.function.returntype);
2229 params = x->content.function.args;
2230 if (!paramNodeList_empty (params))
2231 {
2232 s = message ("%qfcn with args: (%q)", s,
2233 paramNodeList_unparse (x->content.function.args));
2234 }
2235 else
2236 s = message ("%qfcn with no args", s);
2237 return s;
2238 default:
2239 llfatalbug (message ("printTypeExpr2: unknown typeExprKind: %d", (int) x->kind));
2240 }
2241 }
2242 return cstring_undefined;
2243}
2244
2245/*@only@*/ cstring
2246declaratorNode_unparse (declaratorNode x)
2247{
2248 return (typeExpr_unparse (x->type));
2249}
2250
2251/*@only@*/ declaratorNode
2252 declaratorNode_copy (declaratorNode x)
2253{
2254 declaratorNode ret = (declaratorNode) dmalloc (sizeof (*ret));
2255
2256 ret->type = typeExpr_copy (x->type);
2257 ret->id = ltoken_copy (x->id);
2258 ret->isRedecl = x->isRedecl;
2259
2260 return (ret);
2261}
2262
2263static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr x)
2264{
2265 if (x == NULL)
2266 {
2267 return NULL;
2268 }
2269 else
2270 {
2271 typeExpr ret = (typeExpr) dmalloc (sizeof (*ret));
2272
2273 ret->wrapped = x->wrapped;
2274 ret->kind = x->kind;
2275
2276 switch (ret->kind)
2277 {
2278 case TEXPR_BASE:
2279 ret->content.base = ltoken_copy (x->content.base);
2280 break;
2281 case TEXPR_PTR:
2282 ret->content.pointer = typeExpr_copy (x->content.pointer);
2283 break;
2284 case TEXPR_ARRAY:
2285 ret->content.array.elementtype = typeExpr_copy (x->content.array.elementtype);
2286 ret->content.array.size = termNode_copy (x->content.array.size);
2287 break;
2288 case TEXPR_FCN:
2289 ret->content.function.returntype = typeExpr_copy (x->content.function.returntype);
2290 ret->content.function.args = paramNodeList_copy (x->content.function.args);
2291 break;
2292 }
2293
2294 ret->sort = x->sort;
2295 return ret;
2296 }
2297}
2298
2299static /*@only@*/ cstring
2300 typeExpr_unparseCode (/*@null@*/ typeExpr x)
2301{
2302 /* print out types in order of appearance in source */
2303 cstring s = cstring_undefined;
2304
2305 if (x != (typeExpr) 0)
2306 {
2307 switch (x->kind)
2308 {
2309 case TEXPR_BASE:
2310 return (cstring_copy (ltoken_getRawString (x->content.base)));
2311 case TEXPR_PTR:
2312 return (typeExpr_unparseCode (x->content.pointer));
2313 case TEXPR_ARRAY:
2314 return (typeExpr_unparseCode (x->content.array.elementtype));
2315 case TEXPR_FCN:
2316 return (typeExpr_unparseCode (x->content.function.returntype));
2317 }
2318 }
2319 return s;
2320}
2321
2322void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr x)
2323{
2324 if (x != (typeExpr) 0)
2325 {
2326 switch (x->kind)
2327 {
2328 case TEXPR_BASE:
2329 break;
2330 case TEXPR_PTR:
2331 typeExpr_free (x->content.pointer);
2332 break;
2333 case TEXPR_ARRAY:
2334 typeExpr_free (x->content.array.elementtype);
2335 termNode_free (x->content.array.size);
2336 break;
2337 case TEXPR_FCN:
2338 typeExpr_free (x->content.function.returntype);
2339 paramNodeList_free (x->content.function.args);
2340 break;
2341 /*@-branchstate@*/
2342 }
2343 /*@=branchstate@*/
2344
2345 sfree (x);
2346 }
2347}
2348
2349
2350/*@only@*/ cstring
2351declaratorNode_unparseCode (declaratorNode x)
2352{
2353 return (typeExpr_unparseCode (x->type));
2354}
2355
2356/*@only@*/ cstring
2357typeExpr_unparse (/*@null@*/ typeExpr x)
2358{
2359 cstring s = cstring_undefined; /* print out types in order of appearance in source */
2360 paramNodeList params;
2361 int i;
2362
2363 if (x != (typeExpr) 0)
2364 {
2365 cstring front = cstring_undefined;
2366 cstring back = cstring_undefined;
2367
2368 llassert (x->wrapped < 100);
2369
2370 for (i = x->wrapped; i >= 1; i--)
2371 {
2372 front = cstring_appendChar (front, '(');
2373 back = cstring_appendChar (back, ')');
2374 }
2375
2376 switch (x->kind)
2377 {
2378 case TEXPR_BASE:
2379 s = message ("%q%s", s, ltoken_getRawString (x->content.base));
2380 break;
2381 case TEXPR_PTR:
2382 s = message ("%q*%q", s, typeExpr_unparse (x->content.pointer));
2383 break;
2384 case TEXPR_ARRAY:
2385 s = message ("%q%q[%q]", s,
2386 typeExpr_unparse (x->content.array.elementtype),
2387 termNode_unparse (x->content.array.size));
2388 break;
2389 case TEXPR_FCN:
2390 s = message ("%q%q (", s,
2391 typeExpr_unparse (x->content.function.returntype));
2392 params = x->content.function.args;
2393
2394 if (!paramNodeList_empty (params))
2395 {
2396 s = message ("%q%q", s,
2397 paramNodeList_unparse (x->content.function.args));
2398 }
2399
2400 s = message ("%q)", s);
2401 break;
2402 }
2403 s = message ("%q%q%q", front, s, back);
2404 }
2405 else
2406 {
2407 s = cstring_makeLiteral ("?");
2408 }
2409
2410 return s;
2411}
2412
2413/*@only@*/ cstring
2414typeExpr_unparseNoBase (/*@null@*/ typeExpr x)
2415{
2416 cstring s = cstring_undefined; /* print out types in order of appearance in source */
2417 paramNodeList params;
2418 int i;
2419
2420 if (x != (typeExpr) 0)
2421 {
2422 cstring front = cstring_undefined;
2423 cstring back = cstring_undefined;
2424
2425 llassert (x->wrapped < 100);
2426
2427 for (i = x->wrapped; i >= 1; i--)
2428 {
2429 front = cstring_appendChar (front, '(');
2430 back = cstring_appendChar (back, ')');
2431 }
2432
2433 switch (x->kind)
2434 {
2435 case TEXPR_BASE:
2436 s = message ("%q /* %s */", s, ltoken_getRawString (x->content.base));
2437 break;
2438 case TEXPR_PTR:
2439 s = message ("%q*%q", s, typeExpr_unparseNoBase (x->content.pointer));
2440 break;
2441 case TEXPR_ARRAY:
2442 s = message ("%q%q[%q]", s,
2443 typeExpr_unparseNoBase (x->content.array.elementtype),
2444 termNode_unparse (x->content.array.size));
2445 break;
2446 case TEXPR_FCN:
2447 s = message ("%q%q (", s,
2448 typeExpr_unparseNoBase (x->content.function.returntype));
2449 params = x->content.function.args;
2450
2451 if (!paramNodeList_empty (params))
2452 {
2453 s = message ("%q%q", s,
2454 paramNodeList_unparse (x->content.function.args));
2455 }
2456
2457 s = message ("%q)", s);
2458 break;
2459 }
2460 s = message ("%q%q%q", front, s, back);
2461 }
2462 else
2463 {
2464 s = cstring_makeLiteral ("?");
2465 }
2466
2467 return s;
2468}
2469
2470cstring
2471typeExpr_name (/*@null@*/ typeExpr x)
2472{
2473 if (x != (typeExpr) 0)
2474 {
2475 switch (x->kind)
2476 {
2477 case TEXPR_BASE:
2478 return (cstring_copy (ltoken_getRawString (x->content.base)));
2479 case TEXPR_PTR:
2480 return (typeExpr_name (x->content.pointer));
2481 case TEXPR_ARRAY:
2482 return (typeExpr_name (x->content.array.elementtype));
2483 case TEXPR_FCN:
2484 return (typeExpr_name (x->content.function.returntype));
2485 }
2486 }
2487
2488 /* evs --- 14 Mar 1995
2489 ** not a bug: its okay to have empty parameter names
2490 ** llbug ("typeExpr_name: null");
2491 */
2492
2493 return cstring_undefined;
2494}
2495
2496/*@only@*/ typeExpr
2497 makePointerNode (ltoken star, /*@only@*/ /*@returned@*/ typeExpr x)
2498{
2499 if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0)))
2500 {
2501 x->content.function.returntype = makePointerNode (star, x->content.function.returntype);
2502 return x;
2503 }
2504 else
2505 {
2506 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2507
2508 y->wrapped = 0;
2509 y->kind = TEXPR_PTR;
2510 y->content.pointer = x;
2511 y->sort = sort_makeNoSort ();
2512 ltoken_free (star);
2513
2514 return y;
2515 }
2516}
2517
2518typeExpr makeArrayNode (/*@returned@*/ typeExpr x,
2519 /*@only@*/ arrayQualNode a)
2520{
2521 if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0)))
2522 {
2523 /*
2524 ** Spurious errors reported here, because of referencing
2525 ** in makeArrayNode.
2526 */
2527
2528 /*@i3@*/ x->content.function.returntype = makeArrayNode (x, a);
2529 /*@i1@*/ return x;
2530 }
2531 else
2532 {
2533 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2534 y->wrapped = 0;
2535 y->kind = TEXPR_ARRAY;
2536
2537 if (a == (arrayQualNode) 0)
2538 {
2539 y->content.array.size = (termNode) 0;
2540 }
2541 else
2542 {
2543 y->content.array.size = a->term;
2544 ltoken_free (a->tok);
2545 sfree (a);
2546 }
2547
2548 y->content.array.elementtype = x;
2549 y->sort = sort_makeNoSort ();
2550
2551 return (y);
2552 }
2553}
2554
2555/*@only@*/ constDeclarationNode
2556makeConstDeclarationNode (lclTypeSpecNode t, initDeclNodeList decls)
2557{
2558 constDeclarationNode n = (constDeclarationNode) dmalloc (sizeof (*n));
2559 sort s, s2, initValueSort;
2560 ltoken varid, errtok;
2561 termNode initValue;
2562
2563 s = lclTypeSpecNode2sort (t);
2564
2565 initDeclNodeList_elements (decls, init)
2566 {
2567 declaratorNode vdnode = init->declarator;
2568 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
2569
2570 varid = ltoken_copy (vdnode->id);
2571 s2 = typeExpr2ptrSort (s, vdnode->type);
2572 initValue = init->value;
2573
2574 if (termNode_isDefined (initValue) && !initValue->error_reported)
2575 {
2576 initValueSort = initValue->sort;
2577
2578 /* should keep the arguments in order */
2579 if (!sort_member_modulo_cstring (s2, initValue)
2580 && !initValue->error_reported)
2581 {
2582 errtok = termNode_errorToken (initValue);
2583
2584 lclerror
2585 (errtok,
2586 message ("Constant %s declared type %q, initialized to %q: %q",
2587 ltoken_unparse (varid),
2588 sort_unparse (s2),
2589 sort_unparse (initValueSort),
2590 termNode_unparse (initValue)));
2591 }
2592 }
2593
2594 vi->id = varid;
2595 vi->kind = VRK_CONST;
2596 vi->sort = s2;
2597 vi->export = TRUE;
2598
2599 (void) symtable_enterVar (g_symtab, vi);
2600 varInfo_free (vi);
2601
2602 } end_initDeclNodeList_elements;
2603
2604 n->type = t;
2605 n->decls = decls;
2606
2607 return n;
2608}
2609
2610varDeclarationNode makeInternalStateNode (void)
2611{
2612 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2613
2614 n->isSpecial = TRUE;
2615 n->sref = sRef_makeInternalState ();
2616
2617 /*@-compdef@*/ return n; /*@=compdef@*/
2618}
2619
2620varDeclarationNode makeFileSystemNode (void)
2621{
2622 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2623
2624 n->isSpecial = TRUE;
2625 n->sref = sRef_makeSystemState ();
2626
2627 /*@-compdef@*/ return n; /*@=compdef@*/
2628}
2629
2630/*@only@*/ varDeclarationNode
2631makeVarDeclarationNode (lclTypeSpecNode t, initDeclNodeList x,
2632 bool isGlobal, bool isPrivate)
2633{
2634 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2635 sort s, s2, initValueSort;
2636 ltoken varid, errtok;
2637 termNode initValue;
2638 declaratorNode vdnode;
2639
2640 n->isSpecial = FALSE;
2641 n->qualifier = QLF_NONE;
2642 n->isGlobal = isGlobal;
2643 n->isPrivate = isPrivate;
2644 n->decls = x;
2645
2646 s = lclTypeSpecNode2sort (t);
2647
2648 /* t is an lclTypeSpec, its sort may not be assigned yet */
2649
2650 initDeclNodeList_elements (x, init)
2651 {
2652 vdnode = init->declarator;
2653 varid = vdnode->id;
2654 s2 = typeExpr2ptrSort (s, vdnode->type);
2655 initValue = init->value;
2656
2657 if (termNode_isDefined (initValue) && !initValue->error_reported)
2658 {
2659 initValueSort = initValue->sort;
2660 /* should keep the arguments in order */
2661 if (!sort_member_modulo_cstring (s2, initValue)
2662 && !initValue->error_reported)
2663 {
2664 errtok = termNode_errorToken (initValue);
2665
2666 lclerror (errtok,
2667 message ("Variable %s declared type %q, initialized to %q",
2668 ltoken_unparse (varid),
2669 sort_unparse (s2),
2670 sort_unparse (initValueSort)));
2671 }
2672 }
2673
2674 /*
2675 ** If global, check that it has been declared already, don't push
2676 ** onto symbol table yet (wrong scope, done in enteringFcnScope
2677 */
2678
2679 if (isGlobal)
2680 {
2681 varInfo vi = symtable_varInfo (g_symtab, ltoken_getText (varid));
2682
2683 if (!varInfo_exists (vi))
2684 {
2685 lclerror (varid,
2686 message ("Undeclared global variable: %s",
2687 ltoken_getRawString (varid)));
2688 }
2689 else
2690 {
2691 if (vi->kind == VRK_CONST)
2692 {
2693 lclerror (varid,
2694 message ("Constant used in global list: %s",
2695 ltoken_getRawString (varid)));
2696 }
2697 }
2698 }
2699 else
2700 {
2701 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
2702
2703 vi->id = ltoken_copy (varid);
2704 if (isPrivate)
2705 {
2706 vi->kind = VRK_PRIVATE;
2707 /* check that initValue is not empty */
2708 if (initValue == (termNode) 0)
2709 {
2710 lclerror (varid,
2711 message ("Private variable must have initialization: %s",
2712 ltoken_getRawString (varid)));
2713 }
2714 }
2715 else
2716 {
2717 vi->kind = VRK_VAR;
2718 }
2719
2720 vi->sort = sort_makeGlobal (s2);
2721 vi->export = TRUE;
2722
2723 vdnode->isRedecl = symtable_enterVar (g_symtab, vi);
2724 varInfo_free (vi);
2725 }
2726 } end_initDeclNodeList_elements;
2727
2728 n->type = t;
2729
2730 return n;
2731}
2732
2733/*@only@*/ initDeclNode
2734makeInitDeclNode (declaratorNode d, termNode x)
2735{
2736 initDeclNode n = (initDeclNode) dmalloc (sizeof (*n));
2737
2738 n->declarator = d;
2739 n->value = x;
2740 return n;
2741}
2742
2743/*@only@*/ abstractNode
2744makeAbstractNode (ltoken t, ltoken name,
2745 bool isMutable, bool isRefCounted, abstBodyNode a)
2746{
2747 abstractNode n = (abstractNode) dmalloc (sizeof (*n));
2748 sort handle;
2749 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
2750
2751 n->tok = t;
2752 n->isMutable = isMutable;
2753 n->name = name;
2754 n->body = a;
2755 n->isRefCounted = isRefCounted;
2756
2757 if (isMutable)
2758 handle = sort_makeMutable (name, ltoken_getText (name));
2759 else
2760 handle = sort_makeImmutable (name, ltoken_getText (name));
2761 n->sort = handle;
2762
2763 ti->id = ltoken_createType (ltoken_getCode (ltoken_typename), SID_TYPE,
2764 ltoken_getText (name));
2765 ti->modifiable = isMutable;
2766 ti->abstract = TRUE;
2767 ti->basedOn = handle;
2768 ti->export = TRUE;
2769
2770 symtable_enterType (g_symtab, ti);
2771
2772
2773 return n;
2774}
2775
2776/*@only@*/ cstring
2777abstractNode_unparse (abstractNode n)
2778{
2779 if (n != (abstractNode) 0)
2780 {
2781 cstring s;
2782
2783 if (n->isMutable)
2784 s = cstring_makeLiteral ("mutable");
2785 else
2786 s = cstring_makeLiteral ("immutable");
2787
2788 return (message ("%q type %s%q;", s, ltoken_getRawString (n->name),
2789 abstBodyNode_unparse (n->body)));
2790 }
2791 return cstring_undefined;
2792}
2793
2794void
2795setExposedType (lclTypeSpecNode s)
2796{
2797 exposedType = s;
2798}
2799
2800/*@only@*/ exposedNode
2801makeExposedNode (ltoken t, lclTypeSpecNode s,
2802 declaratorInvNodeList d)
2803{
2804 exposedNode n = (exposedNode) dmalloc (sizeof (*n));
2805
2806 n->tok = t;
2807 n->type = s;
2808 n->decls = d;
2809
2810 return n;
2811}
2812
2813/*@only@*/ cstring
2814exposedNode_unparse (exposedNode n)
2815{
2816 if (n != (exposedNode) 0)
2817 {
2818 return (message ("typedef %q %q;",
2819 lclTypeSpecNode_unparse (n->type),
2820 declaratorInvNodeList_unparse (n->decls)));
2821 }
2822 return cstring_undefined;
2823}
2824
2825/*@only@*/ declaratorInvNode
2826makeDeclaratorInvNode (declaratorNode d, abstBodyNode b)
2827{
2828 declaratorInvNode n = (declaratorInvNode) dmalloc (sizeof (*n));
2829 n->declarator = d;
2830 n->body = b;
2831
2832 return (n);
2833}
2834
2835/*@only@*/ cstring
2836declaratorInvNode_unparse (declaratorInvNode d)
2837{
2838 return (message ("%q%q", declaratorNode_unparse (d->declarator),
2839 abstBodyNode_unparseExposed (d->body)));
2840}
2841
2842/*@only@*/ cstring
2843abstBodyNode_unparse (abstBodyNode n)
2844{
2845 if (n != (abstBodyNode) 0)
2846 {
2847 return (lclPredicateNode_unparse (n->typeinv));
2848 }
2849 return cstring_undefined;
2850}
2851
2852/*@only@*/ cstring
2853abstBodyNode_unparseExposed (abstBodyNode n)
2854{
2855 if (n != (abstBodyNode) 0)
2856 {
2857 return (message ("%q", lclPredicateNode_unparse (n->typeinv)));
2858 }
2859 return cstring_undefined;
2860}
2861
2862/*@only@*/ cstring
2863taggedUnionNode_unparse (taggedUnionNode n)
2864{
2865 if (n != (taggedUnionNode) 0)
2866 {
2867 return (message ("tagged union {%q}%q;\n",
2868 stDeclNodeList_unparse (n->structdecls),
2869 declaratorNode_unparse (n->declarator)));
2870 }
2871 return cstring_undefined;
2872}
2873
2874static /*@observer@*/ paramNodeList
2875 typeExpr_toParamNodeList (/*@null@*/ typeExpr te)
2876{
2877 if (te != (typeExpr) 0)
2878 {
2879 switch (te->kind)
2880 {
2881 case TEXPR_FCN:
2882 return te->content.function.args;
2883 case TEXPR_PTR:
2884 return typeExpr_toParamNodeList (te->content.pointer);
2885 case TEXPR_ARRAY:
2886 /* return typeExpr_toParamNodeList (te->content.array.elementtype); */
2887 case TEXPR_BASE:
2888 return paramNodeList_undefined;
2889 }
2890 }
2891 return paramNodeList_undefined;
2892}
2893
2894/*@only@*/ fcnNode
2895 fcnNode_fromDeclarator (/*@only@*/ /*@null@*/ lclTypeSpecNode t,
2896 /*@only@*/ declaratorNode d)
2897{
dfd82dce 2898 return (makeFcnNode (qual_createUnknown (), t, d,
2899 varDeclarationNodeList_new (),
2900 varDeclarationNodeList_new (),
2901 letDeclNodeList_new (),
616915dd 2902 (lclPredicateNode) 0,
2903 (lclPredicateNode) 0,
2904 (modifyNode) 0,
2905 (lclPredicateNode) 0,
2906 (lclPredicateNode) 0));
2907}
2908
2909/*@only@*/ iterNode
2910makeIterNode (ltoken id, paramNodeList p)
2911{
2912 iterNode x = (iterNode) dmalloc (sizeof (*x));
2913 bool hasYield = FALSE;
2914
2915 x->name = id;
2916 x->params = p;
2917
2918 /* check there is at least one yield param */
2919
2920 paramNodeList_elements (p, pe)
2921 {
2922 if (paramNode_isYield (pe))
2923 {
2924 hasYield = TRUE;
2925 break;
2926 }
2927 } end_paramNodeList_elements
2928
2929 if (!hasYield)
2930 {
2931 lclerror (id, message ("Iterator has no yield parameters: %s",
2932 ltoken_getRawString (id)));
2933 }
2934
2935 return (x);
2936}
2937
2938/*@only@*/ fcnNode
2939makeFcnNode (qual specQual,
2940 /*@null@*/ lclTypeSpecNode t,
2941 declaratorNode d,
2942 /*@null@*/ globalList g,
2943 /*@null@*/ varDeclarationNodeList privateinits,
2944 /*@null@*/ letDeclNodeList lets,
2945 /*@null@*/ lclPredicateNode checks,
2946 /*@null@*/ lclPredicateNode requires,
2947 /*@null@*/ modifyNode m,
2948 /*@null@*/ lclPredicateNode ensures,
2949 /*@null@*/ lclPredicateNode claims)
2950{
2951 fcnNode x = (fcnNode) dmalloc (sizeof (*x));
28bf4b0b 2952
616915dd 2953 if (d->type != (typeExpr)0 && (d->type)->kind != TEXPR_FCN)
2954 {
2955 lclerror (d->id, cstring_makeLiteral
2956 ("Attempt to specify function without parameter list"));
2957 d->type = makeFunctionNode (d->type, paramNodeList_new ());
2958 }
28bf4b0b 2959
616915dd 2960 x->special = specQual;
2961 x->typespec = t;
2962 x->declarator = d;
2963 x->globals = g;
2964 x->inits = privateinits;
2965 x->lets = lets;
2966 x->checks = checks;
2967 x->require = requires;
2968 x->modify = m;
2969 x->ensures = ensures;
2970 x->claim = claims;
2971
2972 /* extract info to fill in x->name =; x->signature =; */
2973 x->name = ltoken_copy (d->id);
2974
2975 return (x);
2976}
2977
2978/*@only@*/ claimNode
2979makeClaimNode (ltoken id, paramNodeList p,
2980 globalList g, letDeclNodeList lets, lclPredicateNode requires,
2981 programNode b, lclPredicateNode ensures)
2982{
2983 claimNode x = (claimNode) dmalloc (sizeof (*x));
2984
2985
2986 x->name = id;
2987 x->params = p;
2988 x->globals = g;
2989 x->lets = lets;
2990 x->require = requires;
2991 x->body = b;
2992 x->ensures = ensures;
2993 return (x);
2994}
2995
2996/*@only@*/ lclPredicateNode
2997makeIntraClaimNode (ltoken t, lclPredicateNode n)
2998{
2999 ltoken_free (n->tok);
3000 n->tok = t;
3001 n->kind = LPD_INTRACLAIM;
3002 return (n);
3003}
3004
3005/*@only@*/ lclPredicateNode
3006makeRequiresNode (ltoken t, lclPredicateNode n)
3007{
3008 ltoken_free (n->tok);
3009 n->tok = t;
3010 n->kind = LPD_REQUIRES;
3011 return (n);
3012}
3013
3014/*@only@*/ lclPredicateNode
3015makeChecksNode (ltoken t, lclPredicateNode n)
3016{
3017 ltoken_free (n->tok);
3018 n->tok = t;
3019 n->kind = LPD_CHECKS;
3020 return (n);
3021}
3022
3023/*@only@*/ lclPredicateNode
3024makeEnsuresNode (ltoken t, lclPredicateNode n)
3025{
3026 ltoken_free (n->tok);
3027 n->tok = t;
3028 n->kind = LPD_ENSURES;
3029 return (n);
3030}
3031
3032/*@only@*/ lclPredicateNode
3033makeLclPredicateNode (ltoken t, termNode n,
3034 lclPredicateKind k)
3035{
3036 lclPredicateNode x = (lclPredicateNode) dmalloc (sizeof (*x));
3037
3038 x->tok = t;
3039 x->predicate = n;
3040 x->kind = k;
3041 return (x);
3042}
3043
3044/*@only@*/ quantifierNode
3045makeQuantifierNode (varNodeList v, ltoken quant)
3046{
3047 quantifierNode x = (quantifierNode) dmalloc (sizeof (*x));
3048
3049 x->quant = quant;
3050 x->vars = v;
3051 x->isForall = cstring_equalLit (ltoken_unparse (quant), "\forall");
3052
3053 return (x);
3054}
3055
3056/*@only@*/ arrayQualNode
3057makeArrayQualNode (ltoken t, termNode term)
3058{
3059 arrayQualNode x = (arrayQualNode) dmalloc (sizeof (*x));
3060
3061 x->tok = t;
3062 x->term = term;
3063 return (x);
3064}
3065
3066/*@only@*/ varNode
3067makeVarNode (/*@only@*/ ltoken varid, bool isObj, lclTypeSpecNode t)
3068{
3069 varNode x = (varNode) dmalloc (sizeof (*x));
3070 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
3071 sort sort;
3072
3073 vi->id = ltoken_copy (varid);
3074 sort = lclTypeSpecNode2sort (t);
3075
3076 /* 9/3/93, The following is needed because we want value sorts to be
3077 the default, object sort is generated only if there is "obj" qualifier.
3078 There are 2 cases: (1) for immutable types (including C primitive types),
3079 we need to generate the object sort if qualifier is present; (2) for
3080 array, struct and union types, they are already in their object sorts.
3081 */
3082
3083 sort = sort_makeVal (sort); /* both cases are now value sorts */
3084
3085 if (isObj)
3086 {
3087 sort = sort_makeObj (sort);
3088 }
3089
3090
3091 vi->sort = sort;
3092 vi->kind = VRK_QUANT;
3093 vi->export = TRUE;
3094
3095 (void) symtable_enterVar (g_symtab, vi);
3096 varInfo_free (vi);
3097
3098 x->varid = varid;
3099 x->isObj = isObj;
3100 x->type = t;
3101 x->sort = sort_makeNoSort ();
3102
3103 return (x);
3104}
3105
3106/*@only@*/ abstBodyNode
3107makeAbstBodyNode (ltoken t, fcnNodeList f)
3108{
3109 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3110
3111 x->tok = t;
3112 x->typeinv = (lclPredicateNode)0;
3113 x->fcns = f;
3114 return (x);
3115}
3116
3117/*@only@*/ abstBodyNode
3118makeExposedBodyNode (ltoken t, lclPredicateNode inv)
3119{
3120 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3121
3122 x->tok = t;
3123 x->typeinv = inv;
3124 x->fcns = fcnNodeList_undefined;
3125 return (x);
3126}
3127
3128/*@only@*/ abstBodyNode
3129makeAbstBodyNode2 (ltoken t, ltokenList ops)
3130{
3131 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3132
3133 x->tok = t;
3134 x->typeinv = (lclPredicateNode) 0;
3135
3136 x->fcns = fcnNodeList_new ();
3137
3138 ltokenList_elements (ops, op)
3139 {
3140 x->fcns = fcnNodeList_add
3141 (x->fcns,
3142 fcnNode_fromDeclarator (lclTypeSpecNode_undefined,
3143 makeUnknownDeclaratorNode (ltoken_copy (op))));
3144 } end_ltokenList_elements;
3145
3146 ltokenList_free (ops);
3147
3148 return (x);
3149}
3150
3151/*@only@*/ stmtNode
3152 makeStmtNode (ltoken varId, ltoken fcnId, /*@only@*/ termNodeList v)
3153{
3154 stmtNode n = (stmtNode) dmalloc (sizeof (*n));
3155
3156 n->lhs = varId;
3157 n->operator = fcnId;
3158 n->args = v;
3159 return (n);
3160}
3161
3162/* printDeclarators -> declaratorNodeList_unparse */
3163
3164static cstring abstDeclaratorNode_unparse (abstDeclaratorNode x)
3165{
3166 return (typeExpr_unparse ((typeExpr) x));
3167}
3168
3169/*@only@*/ paramNode
3170makeParamNode (lclTypeSpecNode t, typeExpr d)
3171{
3172 paramNode x = (paramNode) dmalloc (sizeof (*x));
3173
3174 paramNode_checkQualifiers (t, d);
3175
3176 x->type = t;
3177 x->paramdecl = d;
3178 x->kind = PNORMAL; /*< forgot this! >*/
3179
3180 return (x);
3181}
3182
3183/*@only@*/ paramNode
3184paramNode_elipsis (void)
3185{
3186 paramNode x = (paramNode) dmalloc (sizeof (*x));
3187
3188 x->type = (lclTypeSpecNode) 0;
3189 x->paramdecl = (typeExpr) 0;
3190 x->kind = PELIPSIS;
3191
3192 return (x);
3193}
3194
3195static /*@observer@*/ ltoken typeExpr_getTok (typeExpr d)
3196{
3197 while (d != (typeExpr)0)
3198 {
3199 if (d->kind == TEXPR_BASE)
3200 {
3201 return (d->content.base);
3202 }
3203 else
3204 {
3205 if (d->kind == TEXPR_PTR)
3206 {
3207 d = d->content.pointer;
3208 }
3209 else if (d->kind == TEXPR_ARRAY)
3210 {
3211 d = d->content.array.elementtype;
3212 }
3213 else if (d->kind == TEXPR_FCN)
3214 {
3215 d = d->content.function.returntype;
3216 }
3217 else
3218 {
3219 BADBRANCH;
3220 }
3221 }
3222 }
3223
3224 llfatalerror (cstring_makeLiteral ("typeExpr_getTok: unreachable code"));
3225 BADEXIT;
3226}
3227
3228void
3229paramNode_checkQualifiers (lclTypeSpecNode t, typeExpr d)
3230{
3231 bool isPointer = FALSE;
3232 bool isUser = FALSE;
3233 bool hasAlloc = FALSE;
3234 bool hasAlias = FALSE;
3235
3236 llassert (lclTypeSpecNode_isDefined (t));
3237
3238 if (t->pointers == 0
3239 && (d != (typeExpr)0 && d->kind != TEXPR_PTR) && d->kind != TEXPR_ARRAY)
3240 {
3241 if (t->kind == LTS_TYPE)
3242 {
3243 sortNode sn;
3244
3245 llassert (t->content.type != NULL);
3246
3247 sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort));
3248
28bf4b0b 3249 if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY
3250 || sn->kind == SRT_HOF || sn->kind == SRT_NONE)
616915dd 3251 {
3252 isPointer = TRUE;
3253 }
3254 }
3255 }
3256 else
3257 {
3258 isPointer = TRUE;
3259 }
3260
3261 if (d != (typeExpr)0 && d->kind != TEXPR_BASE)
3262 {
3263 if (t->kind == LTS_TYPE)
3264 {
3265 sortNode sn;
3266
3267 llassert (t->content.type != NULL);
3268 sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort));
3269
28bf4b0b 3270 if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY
3271 || sn->kind == SRT_HOF || sn->kind == SRT_NONE)
616915dd 3272 {
3273 isUser = TRUE;
3274 }
3275 }
3276 }
3277 else
3278 {
3279 isPointer = TRUE;
3280 }
3281
3282 if (d != (typeExpr)NULL)
3283 {
3284 qualList_elements (t->quals, q)
3285 {
3286 if (qual_isAllocQual (q))
3287 {
3288 if (hasAlloc)
3289 {
3290 ltoken tok = typeExpr_getTok (d);
3291 lclerror (tok, message ("Parameter declared with multiple allocation "
3292 "qualifiers: %q", typeExpr_unparse (d)));
3293 }
3294 hasAlloc = TRUE;
3295
3296 if (!isPointer)
3297 {
3298 ltoken tok = typeExpr_getTok (d);
3299 lclerror (tok, message ("Non-pointer declared as %s parameter: %q",
3300 qual_unparse (q),
3301 typeExpr_unparse (d)));
3302 }
3303 }
3304 if (qual_isAliasQual (q))
3305 {
3306 if (hasAlias)
3307 {
3308 ltoken tok = typeExpr_getTok (d);
3309 lclerror (tok, message ("Parameter declared with multiple alias qualifiers: %q",
3310 typeExpr_unparse (d)));
3311 }
3312 hasAlias = TRUE;
3313
3314 if (!(isPointer || isUser))
3315 {
3316 ltoken tok = typeExpr_getTok (d);
3317 lclerror (tok, message ("Unsharable type declared as %s parameter: %q",
3318 qual_unparse (q),
3319 typeExpr_unparse (d)));
3320 }
3321 }
3322 } end_qualList_elements;
3323 }
3324}
3325
3326/*@only@*/ cstring
3327paramNode_unparse (paramNode x)
3328{
3329 if (x != (paramNode) 0)
3330 {
3331 if (x->kind == PELIPSIS)
3332 {
3333 return (cstring_makeLiteral ("..."));
3334 }
3335
3336 if (x->paramdecl != (typeExpr) 0)
3337 { /* handle (void) */
3338 return (message ("%q %q", lclTypeSpecNode_unparse (x->type),
3339 typeExpr_unparse (x->paramdecl)));
3340 }
3341 else
3342 {
3343 return (lclTypeSpecNode_unparse (x->type));
3344 }
3345 }
3346 return cstring_undefined;
3347}
3348
3349static cstring
3350lclTypeSpecNode_unparseAltComments (/*@null@*/ lclTypeSpecNode typespec) /*@*/
3351{
3352 if (typespec != (lclTypeSpecNode) 0)
3353 {
3354 cstring s = qualList_toCComments (typespec->quals);
3355
3356 switch (typespec->kind)
3357 {
3358 case LTS_TYPE:
3359 {
3360 llassert (typespec->content.type != NULL);
3361
3362 return (cstring_concatFree
3363 (s, printLeaves (typespec->content.type->ctypes)));
3364 }
3365 case LTS_ENUM:
3366 {
3367 bool first = TRUE;
3368 enumSpecNode n = typespec->content.enumspec;
3369
3370 s = cstring_concatFree (s, cstring_makeLiteral ("enum"));
3371 llassert (n != NULL);
3372
3373 if (!ltoken_isUndefined (n->opttagid))
3374 {
3375 s = message ("%q %s", s, ltoken_unparse (n->opttagid));
3376 }
3377 s = message ("%q {", s);
3378
3379 ltokenList_elements (n->enums, e)
3380 {
3381 if (first)
3382 {
3383 first = FALSE;
3384 s = message ("%q%s", s, ltoken_getRawString (e));
3385 }
3386 else
3387 s = message ("%q, %s", s, ltoken_getRawString (e));
3388 } end_ltokenList_elements;
3389
3390 return (message ("%q}", s));
3391 }
3392 case LTS_STRUCTUNION:
3393 {
3394 strOrUnionNode n = typespec->content.structorunion;
3395 stDeclNodeList decls;
3396
3397 llassert (n != NULL);
3398
3399 switch (n->kind)
3400 {
3401 case SU_STRUCT:
3402 s = cstring_concatFree (s, cstring_makeLiteral ("struct "));
3403 /*@switchbreak@*/ break;
3404 case SU_UNION:
3405 s = cstring_concatFree (s, cstring_makeLiteral ("union "));
3406 /*@switchbreak@*/ break;
3407 }
3408
3409 if (!ltoken_isUndefined (n->opttagid))
3410 {
3411 if (stDeclNodeList_size (n->structdecls) == 0)
3412 {
3413 return (message ("%q%s", s, ltoken_unparse (n->opttagid)));
3414 }
3415
3416 s = message ("%q%s {\n\2\1", s, ltoken_unparse (n->opttagid));
3417 }
3418 else
3419 {
3420 s = message ("%q{\n\2\1", s);
3421 }
3422
3423 decls = n->structdecls;
3424
3425 stDeclNodeList_elements (decls, f)
3426 {
3427 s = message ("%q%q\1%q;\n\1", s,
3428 lclTypeSpecNode_unparseAltComments (f->lcltypespec),
3429 declaratorNodeList_unparse (f->declarators));
3430 } end_stDeclNodeList_elements;
3431
3432 return (message ("%q\3}", s));
3433 }
3434 case LTS_CONJ:
3435 {
3436 cstring_free (s);
3437
3438 return
3439 (message
3440 ("%q, %q",
3441 lclTypeSpecNode_unparseAltComments (typespec->content.conj->a),
3442 lclTypeSpecNode_unparseAltComments (typespec->content.conj->b)));
3443 }
3444 BADDEFAULT;
3445 }
3446 }
3447 else
3448 {
3449 llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec");
3450
3451 return cstring_undefined;
3452 }
3453
3454 BADEXIT;
3455}
3456
3457cstring lclTypeSpecNode_unparseComments (/*@null@*/ lclTypeSpecNode typespec)
3458{
3459 if (typespec != (lclTypeSpecNode) 0)
3460 {
3461 cstring s = qualList_toCComments (typespec->quals);
3462
3463 switch (typespec->kind)
3464 {
3465 case LTS_TYPE:
3466 {
3467 llassert (typespec->content.type != NULL);
3468
3469 return (cstring_concatFree
3470 (s, printLeaves (typespec->content.type->ctypes)));
3471 }
3472 case LTS_ENUM:
3473 {
3474 bool first = TRUE;
3475 enumSpecNode n = typespec->content.enumspec;
3476
3477 s = cstring_concatFree (s, cstring_makeLiteral ("enum"));
3478 llassert (n != NULL);
3479
3480 if (!ltoken_isUndefined (n->opttagid))
3481 {
3482 s = message ("%q %s", s, ltoken_unparse (n->opttagid));
3483 }
3484 s = message ("%q {", s);
3485
3486 ltokenList_elements (n->enums, e)
3487 {
3488 if (first)
3489 {
3490 first = FALSE;
3491 s = message ("%q%s", s, ltoken_getRawString (e));
3492 }
3493 else
3494 s = message ("%q, %s", s, ltoken_getRawString (e));
3495 } end_ltokenList_elements;
3496
3497 return (message ("%q}", s));
3498 }
3499 case LTS_STRUCTUNION:
3500 {
3501 strOrUnionNode n = typespec->content.structorunion;
3502 stDeclNodeList decls;
3503
3504 llassert (n != NULL);
3505
3506 switch (n->kind)
3507 {
3508 case SU_STRUCT:
3509 s = cstring_concatFree (s, cstring_makeLiteral ("struct "));
3510 /*@switchbreak@*/ break;
3511 case SU_UNION:
3512 s = cstring_concatFree (s, cstring_makeLiteral ("union "));
3513 /*@switchbreak@*/ break;
3514 }
3515
3516 if (!ltoken_isUndefined (n->opttagid))
3517 {
3518 if (stDeclNodeList_size (n->structdecls) == 0)
3519 {
3520 return (message ("%q%s", s, ltoken_unparse (n->opttagid)));
3521 }
3522
3523 s = message ("%q%s {\n\2\1", s, ltoken_unparse (n->opttagid));
3524 }
3525 else
3526 {
3527 s = message ("%q{\n\2\1", s);
3528 }
3529
3530 decls = n->structdecls;
3531
3532 stDeclNodeList_elements (decls, f)
3533 {
3534 s = message ("%q%q\1%q;\n\1", s,
3535 lclTypeSpecNode_unparseComments (f->lcltypespec),
3536 declaratorNodeList_unparse (f->declarators));
3537 } end_stDeclNodeList_elements;
3538
3539 return (message ("%q\3}", s));
3540 }
3541 case LTS_CONJ:
3542 {
3543 cstring_free (s);
3544
3545 return
3546 (message
3547 ("%q /*@alt %q@*/",
3548 lclTypeSpecNode_unparseComments (typespec->content.conj->a),
3549 lclTypeSpecNode_unparseAltComments (typespec->content.conj->b)));
3550 }
3551 BADDEFAULT;
3552 }
3553 }
3554 else
3555 {
3556 llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec");
3557
3558 return cstring_undefined;
3559 }
3560
3561 BADEXIT;
3562}
3563
3564/*@only@*/ cstring
3565paramNode_unparseComments (paramNode x)
3566{
3567 if (x != (paramNode) 0)
3568 {
3569 if (x->kind == PELIPSIS)
3570 {
3571 return (cstring_makeLiteral ("..."));
3572 }
3573
3574 if (x->paramdecl != (typeExpr) 0)
3575 { /* handle (void) */
3576 return (message ("%q %q",
3577 lclTypeSpecNode_unparseComments (x->type),
3578 typeExpr_unparseNoBase (x->paramdecl)));
3579 }
3580 else
3581 {
3582 return (lclTypeSpecNode_unparseComments (x->type));
3583 }
3584 }
3585 return cstring_undefined;
3586}
3587
3588/*@only@*/ termNode
3589makeIfTermNode (ltoken ift, termNode ifn, ltoken thent,
3590 termNode thenn, ltoken elset,
3591 termNode elsen)
3592{
3593 termNode t = (termNode) dmalloc (sizeof (*t));
3594 opFormNode opform = makeOpFormNode (ift, OPF_IF, opFormUnion_createMiddle (0),
3595 ltoken_undefined);
3596 nameNode nn = makeNameNodeForm (opform);
3597 termNodeList args = termNodeList_new ();
3598
3599 t->error_reported = FALSE;
3600 t->wrapped = 0;
3601 termNodeList_addh (args, ifn);
3602 termNodeList_addh (args, thenn);
3603 termNodeList_addh (args, elsen);
3604 t->name = nn;
3605 t->args = args;
3606 t->kind = TRM_APPLICATION;
3607 t->sort = sort_makeNoSort ();
3608 t->given = t->sort;
3609 t->possibleSorts = sortSet_new ();
3610 t->possibleOps = lslOpSet_new ();
3611
3612 ltoken_free (thent);
3613 ltoken_free (elset);
3614
3615 return (t);
3616}
3617
3618static /*@observer@*/ ltoken
3619 nameNode2anyOp (nameNode n)
3620{
3621 if (n != (nameNode) 0)
3622 {
3623 opFormNode opnode = n->content.opform;
3624 opFormKind kind;
3625
3626 llassert (opnode != NULL);
3627
3628 kind = opnode->kind;
3629
3630 if (kind == OPF_MANYOPM || kind == OPF_ANYOP ||
3631 kind == OPF_MANYOP || kind == OPF_ANYOPM)
3632 {
3633 opFormUnion u;
3634
3635 u = opnode->content;
3636 return u.anyop;
3637 }
3638 }
3639 return ltoken_undefined;
3640}
3641
3642/*@only@*/ termNode
3643makeInfixTermNode (termNode x, ltoken op, termNode y)
3644{
3645 termNode t = (termNode) dmalloc (sizeof (*t));
3646 opFormNode opform;
3647 nameNode nn;
3648 termNodeList args = termNodeList_new ();
3649
3650 checkAssociativity (x, op);
3651
3652 opform = makeOpFormNode (op, OPF_MANYOPM,
3653 opFormUnion_createAnyOp (op),
3654 ltoken_undefined);
3655
3656 nn = makeNameNodeForm (opform);
3657
3658 t->error_reported = FALSE;
3659 t->wrapped = 0;
3660 termNodeList_addh (args, x);
3661 termNodeList_addh (args, y);
3662 t->name = nn;
3663 t->args = args;
3664 t->kind = TRM_APPLICATION;
3665 t->sort = sort_makeNoSort ();
3666 t->given = t->sort;
28bf4b0b 3667 t->possibleSorts = sortSet_new (); /* sort_equal */
616915dd 3668 t->possibleOps = lslOpSet_new ();
3669 return (t);
3670}
3671
3672/*@only@*/ quantifiedTermNode
3673 quantifiedTermNode_copy (quantifiedTermNode q)
3674{
3675 quantifiedTermNode ret = (quantifiedTermNode) dmalloc (sizeof (*ret));
3676
3677 ret->quantifiers = quantifierNodeList_copy (q->quantifiers);
3678 ret->open = ltoken_copy (q->open);
3679 ret->close = ltoken_copy (q->close);
3680 ret->body = termNode_copySafe (q->body);
3681
3682 return (ret);
3683}
3684
3685/*@only@*/ termNode
3686makeQuantifiedTermNode (quantifierNodeList qn, ltoken open,
3687 termNode t, ltoken close)
3688{
3689 sort sort;
3690 termNode n = (termNode) dmalloc (sizeof (*n));
3691 quantifiedTermNode q = (quantifiedTermNode) dmalloc (sizeof (*q));
3692
3693 n->name = NULL; /*> missing this --- detected by lclint <*/
3694 n->error_reported = FALSE;
3695 n->wrapped = 0;
3696 n->error_reported = FALSE;
3697 n->kind = TRM_QUANTIFIER;
3698 n->possibleSorts = sortSet_new ();
3699 n->possibleOps = lslOpSet_new ();
3700 n->kind = TRM_UNCHANGEDALL;
3701 n->args = termNodeList_new (); /*< forgot this >*/
3702
3703 termNodeList_free (t->args);
3704 t->args = termNodeList_new ();
3705
3706 sort = sort_bool;
3707 n->sort = sort;
3708 (void) sortSet_insert (n->possibleSorts, sort);
3709
3710 q->quantifiers = qn;
3711 q->open = open;
3712 q->close = close;
3713 q->body = t;
3714
3715 n->quantified = q;
3716 return (n);
3717}
3718
3719/*@only@*/ termNode
3720makePostfixTermNode (/*@returned@*/ /*@only@*/ termNode secondary, ltokenList postfixops)
3721{
3722 termNode top = secondary;
3723
3724 ltokenList_elements (postfixops, op)
3725 {
3726 top = makePostfixTermNode2 (top, ltoken_copy (op));
3727 /*@i@*/ } end_ltokenList_elements;
3728
3729 ltokenList_free (postfixops);
3730
3731 return (top); /* dep as only? */
3732}
3733
3734/*
3735** secondary is returned in the args list
3736*/
3737
3738/*@only@*/ termNode
3739makePostfixTermNode2 (/*@returned@*/ /*@only@*/ termNode secondary,
3740 /*@only@*/ ltoken postfixop)
3741{
3742 termNode t = (termNode) dmalloc (sizeof (*t));
3743
3744 opFormNode opform = makeOpFormNode (postfixop,
3745 OPF_MANYOP, opFormUnion_createAnyOp (postfixop),
3746 ltoken_undefined);
3747 nameNode nn = makeNameNodeForm (opform);
3748 termNodeList args = termNodeList_new ();
3749
3750 t->error_reported = FALSE;
3751 t->wrapped = 0;
3752 termNodeList_addh (args, secondary);
3753 t->name = nn;
3754 t->args = args;
3755 t->kind = TRM_APPLICATION;
3756 t->sort = sort_makeNoSort ();
3757 t->given = t->sort;
3758 t->possibleSorts = sortSet_new ();
3759 t->possibleOps = lslOpSet_new ();
3760 return t;
3761}
3762
3763/*@only@*/ termNode
3764makePrefixTermNode (ltoken op, termNode arg)
3765{
3766 termNode t = (termNode) dmalloc (sizeof (*t));
3767 termNodeList args = termNodeList_new ();
3768 opFormNode opform = makeOpFormNode (op, OPF_ANYOPM, opFormUnion_createAnyOp (op),
3769 ltoken_undefined);
3770 nameNode nn = makeNameNodeForm (opform);
3771
3772 t->error_reported = FALSE;
3773 t->wrapped = 0;
3774 t->name = nn;
3775 termNodeList_addh (args, arg);
3776 t->args = args;
3777 t->kind = TRM_APPLICATION;
3778 t->sort = sort_makeNoSort ();
3779 t->given = t->sort;
3780 t->possibleSorts = sortSet_new ();
3781 t->possibleOps = lslOpSet_new ();
3782 return t;
3783}
3784
3785/*@only@*/ termNode
3786makeOpCallTermNode (ltoken op, ltoken open,
3787 termNodeList args, ltoken close)
3788{
3789 /* like prefixTerm, but with opId LPAR termNodeList RPAR */
3790 termNode t = (termNode) dmalloc (sizeof (*t));
3791 nameNode nn = makeNameNodeId (op);
3792
3793 t->error_reported = FALSE;
3794 t->wrapped = 0;
3795 t->name = nn;
3796 t->args = args;
3797 t->kind = TRM_APPLICATION;
3798 t->sort = sort_makeNoSort ();
3799 t->given = t->sort;
3800 t->possibleSorts = sortSet_new ();
3801 t->possibleOps = lslOpSet_new ();
3802
3803 ltoken_free (open);
3804 ltoken_free (close);
3805
3806 return t;
3807}
3808
3809/*@exposed@*/ termNode
3810CollapseInfixTermNode (/*@returned@*/ termNode secondary, termNodeList infix)
3811{
3812 termNode left = secondary;
3813
3814 termNodeList_elements (infix, node)
3815 {
3816 termNodeList_addl (node->args, termNode_copySafe (left));
3817 left = node;
3818 /* computePossibleSorts (left); */
3819 } end_termNodeList_elements;
3820
3821 return (left);
3822}
3823
3824static void
3825checkAssociativity (termNode x, ltoken op)
3826{
3827 ltoken lastOpToken;
3828
3829 if (x->wrapped == 0 && /* no parentheses */
3830 x->kind == TRM_APPLICATION && x->name != (nameNode) 0 &&
3831 (!x->name->isOpId))
3832 {
3833 lastOpToken = nameNode2anyOp (x->name);
3834
3835 if ((ltoken_getCode (lastOpToken) == logicalOp &&
3836 ltoken_getCode (op) == logicalOp) ||
3837 ((ltoken_getCode (lastOpToken) == simpleOp ||
3838 ltoken_getCode (lastOpToken) == LLT_MULOP) &&
3839 (ltoken_getCode (op) == simpleOp ||
3840 ltoken_getCode (op) == LLT_MULOP)))
3841 if (ltoken_getText (lastOpToken) != ltoken_getText (op))
3842 {
3843 lclerror (op,
3844 message
3845 ("Parentheses needed to specify associativity of %s and %s",
3846 cstring_fromChars (lsymbol_toChars (ltoken_getText (lastOpToken))),
3847 cstring_fromChars (lsymbol_toChars (ltoken_getText (op)))));
3848 }
3849 }
3850}
3851
3852termNodeList
3853pushInfixOpPartNode (/*@returned@*/ termNodeList x, ltoken op,
3854 /*@only@*/ termNode secondary)
3855{
3856 termNode lastLeftTerm;
3857 termNodeList args = termNodeList_new ();
3858 termNode t = (termNode) dmalloc (sizeof (*t));
3859 opFormNode opform;
3860 nameNode nn;
3861
3862 termNodeList_addh (args, secondary);
3863
3864 if (!termNodeList_empty (x))
3865 {
3866 termNodeList_reset (x);
3867 lastLeftTerm = termNodeList_current (x);
3868 checkAssociativity (lastLeftTerm, op);
3869 }
3870
3871 opform = makeOpFormNode (op, OPF_MANYOPM,
3872 opFormUnion_createAnyOp (op), ltoken_undefined);
3873
3874 nn = makeNameNodeForm (opform);
3875
3876 t->error_reported = FALSE;
3877 t->wrapped = 0;
3878 t->name = nn;
3879 t->kind = TRM_APPLICATION;
3880 t->args = args;
3881 t->sort = sort_makeNoSort ();
3882 t->given = t->sort;
3883 t->possibleSorts = sortSet_new ();
3884 t->possibleOps = lslOpSet_new ();
3885 termNodeList_addh (x, t);
3886 /* don't compute sort yet, do it in CollapseInfixTermNode */
3887 return (x);
3888}
3889
3890termNode
3891updateMatchedNode (/*@only@*/ termNode left, /*@returned@*/ termNode t,
3892 /*@only@*/ termNode right)
3893{
3894 opFormNode op;
3895
3896 if ((t == (termNode) 0) || (t->name == NULL) || t->name->isOpId)
3897 {
3898 llbugexitlit ("updateMatchedNode: expect opForm in nameNode");
3899 }
3900
3901 op = t->name->content.opform;
3902 llassert (op != NULL);
3903
3904 if (left == (termNode) 0)
3905 {
3906 if (right == (termNode) 0)
3907 {
3908 /* op->kind is not changed */
3909 termNode_free (right);
3910 }
3911 else
3912 {
3913 op->kind = OPF_MIDDLEM;
3914 op->key = opFormNode2key (op, OPF_MIDDLEM);
3915 termNodeList_addh (t->args, right);
3916 }
3917 }
3918 else
3919 {
3920 termNodeList_addl (t->args, left);
3921 if (right == (termNode) 0)
3922 {
3923 op->kind = OPF_MMIDDLE;
3924 op->key = opFormNode2key (op, OPF_MMIDDLE);
3925 }
3926 else
3927 {
3928 op->kind = OPF_MMIDDLEM;
3929 op->key = opFormNode2key (op, OPF_MMIDDLEM);
3930 termNodeList_addh (t->args, right);
3931 }
3932 }
3933 return t;
3934}
3935
3936/*@only@*/ termNode
3937 updateSqBracketedNode (/*@only@*/ termNode left,
3938 /*@only@*/ /*@returned@*/ termNode t,
3939 /*@only@*/ termNode right)
3940{
3941 opFormNode op;
3942
3943 if ((t == (termNode) 0) || (t->name == NULL) || (t->name->isOpId))
3944 {
3945 llbugexitlit ("updateSqBracketededNode: expect opForm in nameNode");
3946 }
3947
3948 op = t->name->content.opform;
3949 llassert (op != NULL);
3950
3951 if (left == (termNode) 0)
3952 {
3953 if (right == (termNode) 0)
3954 {
3955 /* op->kind is not changed */
3956 }
3957 else
3958 {
3959 op->kind = OPF_BMIDDLEM;
3960 op->key = opFormNode2key (op, OPF_BMIDDLEM);
3961 termNodeList_addh (t->args, right);
3962 }
3963 }
3964 else
3965 {
3966 termNodeList_addl (t->args, left);
3967
3968 if (right == (termNode) 0)
3969 {
3970 op->kind = OPF_BMMIDDLE;
3971 op->key = opFormNode2key (op, OPF_BMMIDDLE);
3972 }
3973 else
3974 {
3975 op->kind = OPF_BMMIDDLEM;
3976 op->key = opFormNode2key (op, OPF_BMMIDDLEM);
3977 termNodeList_addh (t->args, right);
3978 }
3979 }
3980 return t;
3981}
3982
3983/*@only@*/ termNode
3984makeSqBracketedNode (ltoken lbracket,
3985 termNodeList args, ltoken rbracket)
3986{
3987 termNode t = (termNode) dmalloc (sizeof (*t));
3988 int size;
3989 opFormNode opform;
3990 nameNode nn;
3991
3992 t->error_reported = FALSE;
3993 t->wrapped = 0;
3994
3995 size = termNodeList_size (args);
3996 opform = makeOpFormNode (lbracket, OPF_BMIDDLE, opFormUnion_createMiddle (size),
3997 rbracket);
3998 nn = makeNameNodeForm (opform);
3999 t->name = nn;
4000 t->kind = TRM_APPLICATION;
4001 t->args = args;
4002 t->sort = sort_makeNoSort ();
4003 t->given = t->sort;
4004 t->possibleSorts = sortSet_new ();
4005 t->possibleOps = lslOpSet_new ();
4006 /* do sort checking later, not here, incomplete parse */
4007 return (t);
4008}
4009
4010/*@only@*/ termNode
4011makeMatchedNode (ltoken open, termNodeList args, ltoken close)
4012{
4013 /* matched : open args close */
4014 termNode t = (termNode) dmalloc (sizeof (*t));
4015 int size;
4016 opFormNode opform;
4017 nameNode nn;
4018
4019 t->error_reported = FALSE;
4020 t->wrapped = 0;
4021
4022 size = termNodeList_size (args);
4023 opform = makeOpFormNode (open, OPF_MIDDLE, opFormUnion_createMiddle (size), close);
4024 nn = makeNameNodeForm (opform);
4025 t->name = nn;
4026 t->kind = TRM_APPLICATION;
4027 t->args = args;
4028 t->sort = sort_makeNoSort ();
4029 t->given = t->sort;
4030 t->possibleSorts = sortSet_new ();
4031 t->possibleOps = lslOpSet_new ();
4032 /* do sort checking later, not here, incomplete parse */
4033 return (t);
4034}
4035
4036/*@only@*/ termNode
4037makeSimpleTermNode (ltoken varid)
4038{
4039 sort theSort = sort_makeNoSort ();
4040 lsymbol sym;
4041 opInfo oi;
4042 varInfo vi;
4043 termNode n = (termNode) dmalloc (sizeof (*n));
4044
4045 n->error_reported = FALSE;
4046 n->wrapped = 0;
4047 n->name = (nameNode) 0;
4048 n->given = theSort;
4049 n->args = termNodeList_new ();
4050 n->possibleSorts = sortSet_new ();
4051 n->possibleOps = lslOpSet_new ();
4052
4053 sym = ltoken_getText (varid);
4054
4055 /* lookup current scope */
4056 vi = symtable_varInfoInScope (g_symtab, sym);
4057
4058 if (varInfo_exists (vi))
4059 {
4060 theSort = vi->sort;
4061 n->kind = TRM_VAR;
4062 n->sort = theSort;
4063 n->literal = varid;
4064 (void) sortSet_insert (n->possibleSorts, theSort);
4065 }
4066 else
4067 { /* need to handle LCL constants */
4068 vi = symtable_varInfo (g_symtab, sym);
4069
4070 if (varInfo_exists (vi) && vi->kind == VRK_CONST)
4071 {
4072 theSort = vi->sort;
4073 n->kind = TRM_CONST;
4074 n->sort = theSort;
4075 n->literal = varid;
4076 (void) sortSet_insert (n->possibleSorts, theSort);
4077 }
4078 else
4079 { /* and LSL operators (true, false, new, nil, etc) */
4080 nameNode nn = makeNameNodeId (ltoken_copy (varid));
4081 oi = symtable_opInfo (g_symtab, nn);
4082
4083 if (opInfo_exists (oi) && (oi->name->isOpId) &&
4084 !sigNodeSet_isEmpty (oi->signatures))
4085 {
4086 sigNodeSet_elements (oi->signatures, x)
4087 {
4088 if (ltokenList_empty (x->domain))
4089 /* yes, it really is empty, not not empty */
4090 {
4091 lslOp op = (lslOp) dmalloc (sizeof (*op));
4092
4093 op->name = nameNode_copy (nn);
4094 op->signature = x;
4095 (void) sortSet_insert (n->possibleSorts, sigNode_rangeSort (x));
4096 (void) lslOpSet_insert (n->possibleOps, op);
4097 }
4098 } end_sigNodeSet_elements;
4099 }
4100
4101 nameNode_free (nn);
4102
4103 if (sortSet_size (n->possibleSorts) == 0)
4104 {
4105 lclerror
4106 (varid,
4107 message ("Unrecognized identifier (constant, variable or operator): %s",
4108 ltoken_getRawString (varid)));
4109
4110 }
4111
4112 n->sort = sort_makeNoSort ();
4113 n->literal = varid;
4114 n->kind = TRM_ZEROARY;
4115 }
4116 }
4117
4118 return (n);
4119}
4120
4121/*@only@*/ termNode
4122makeSelectTermNode (termNode pri, ltoken select, /*@dependent@*/ ltoken id)
4123{
4124 termNode t = (termNode) dmalloc (sizeof (*t));
4125 opFormNode opform = makeOpFormNode (select,
4126 OPF_MSELECT, opFormUnion_createAnyOp (id),
4127 ltoken_undefined);
4128 nameNode nn = makeNameNodeForm (opform);
4129 termNodeList args = termNodeList_new ();
4130
4131 t->error_reported = FALSE;
4132 t->wrapped = 0;
4133 t->name = nn;
4134 t->kind = TRM_APPLICATION;
4135 termNodeList_addh (args, pri);
4136 t->args = args;
4137 t->kind = TRM_APPLICATION;
4138 t->sort = sort_makeNoSort ();
4139 t->given = t->sort;
4140 t->possibleSorts = sortSet_new ();
4141 t->possibleOps = lslOpSet_new ();
4142
4143 return t;
4144}
4145
4146/*@only@*/ termNode
4147makeMapTermNode (termNode pri, ltoken map, /*@dependent@*/ ltoken id)
4148{
4149 termNode t = (termNode) dmalloc (sizeof (*t));
4150 opFormNode opform = makeOpFormNode (map, OPF_MMAP, opFormUnion_createAnyOp (id),
4151 ltoken_undefined);
4152 nameNode nn = makeNameNodeForm (opform);
4153 termNodeList args = termNodeList_new ();
4154
4155 t->error_reported = FALSE;
4156 t->wrapped = 0;
4157 t->kind = TRM_APPLICATION;
4158 t->name = nn;
4159 termNodeList_addh (args, pri);
4160 t->args = args;
4161 t->kind = TRM_APPLICATION;
4162 t->sort = sort_makeNoSort ();
4163 t->given = t->sort;
4164 t->possibleSorts = sortSet_new ();
4165 t->possibleOps = lslOpSet_new ();
4166 return t;
4167}
4168
4169/*@only@*/ termNode
4170makeLiteralTermNode (ltoken tok, sort s)
4171{
4172 nameNode nn = makeNameNodeId (ltoken_copy (tok));
4173 opInfo oi = symtable_opInfo (g_symtab, nn);
4174 lslOp op = (lslOp) dmalloc (sizeof (*op));
4175 termNode n = (termNode) dmalloc (sizeof (*n));
4176 sigNode sign;
4177 ltoken range;
4178
4179 n->name = nn;
4180 n->error_reported = FALSE;
4181 n->wrapped = 0;
4182 n->kind = TRM_LITERAL;
4183 n->literal = tok;
4184 n->given = sort_makeNoSort ();
4185 n->sort = n->given;
4186 n->args = termNodeList_new ();
4187 n->possibleSorts = sortSet_new ();
4188 n->possibleOps = lslOpSet_new ();
4189
4190 /* look up signatures for this operator too */
4191
4192 range = ltoken_create (simpleId, sort_getLsymbol (s));
dfd82dce 4193 sign = makesigNode (ltoken_undefined, ltokenList_new (),
616915dd 4194 ltoken_copy (range));
4195
4196 if (opInfo_exists (oi) && (oi->name->isOpId)
4197 && (sigNodeSet_size (oi->signatures) > 0))
4198 {
4199 sigNodeSet_elements (oi->signatures, x)
4200 {
4201 if (ltokenList_empty (x->domain))
4202 {
4203 lslOp opn = (lslOp) dmalloc (sizeof (*opn));
4204 sort sort;
4205
4206 opn->name = nameNode_copy (nn);
4207 opn->signature = x;
4208 sort = sigNode_rangeSort (x);
4209 (void) sortSet_insert (n->possibleSorts, sort);
4210 (void) lslOpSet_insert (n->possibleOps, opn);
4211 }
4212 } end_sigNodeSet_elements;
4213 }
4214
4215 /* insert into literal term */
4216 (void) sortSet_insert (n->possibleSorts, s);
4217
4218 op->name = nameNode_copy (nn);
4219 op->signature = sign;
4220 (void) lslOpSet_insert (n->possibleOps, op);
4221
4222 /* enter the literal as an operator into the operator table */
4223 /* 8/9/93. C's char constant 'c' syntax conflicts
4224 with LSL's lslinit.lsi table. Throw out, because it's not
4225 needed anyway. */
4226 /* symtable_enterOp (g_symtab, nn, sign); */
4227
4228 if (s == sort_int)
4229 {
4230 sigNode osign;
4231 lslOp opn = (lslOp) dmalloc (sizeof (*opn));
4232
4233 /* if it is a C int, we should overload it as double too because
4234 C allows you to say "x > 2". */
4235
4236 (void) sortSet_insert (n->possibleSorts, sort_double);
4237
4238 ltoken_setText (range, lsymbol_fromChars ("double"));
4239 osign = makesigNode (ltoken_undefined, ltokenList_new (), range);
4240 opn->name = nameNode_copy (nn);
4241 opn->signature = osign;
4242 (void) lslOpSet_insert (n->possibleOps, opn);
4243
4244 symtable_enterOp (g_symtab, nameNode_copySafe (nn), sigNode_copy (osign));
4245 }
4246 else
4247 {
4248 ltoken_free (range);
4249 }
4250
4251 /* future: could overload cstrings to be both char_Vec as well as
4252 char_ObjPtr */
4253
4254 /*@-mustfree@*/
4255 return n;
4256} /*@=mustfree@*/
4257
4258/*@only@*/ termNode
4259makeUnchangedTermNode1 (ltoken op, /*@unused@*/ ltoken all)
4260{
4261 termNode t = (termNode) dmalloc (sizeof (*t));
4262
4263 t->error_reported = FALSE;
4264 t->wrapped = 0;
4265 t->kind = TRM_UNCHANGEDALL;
4266 t->sort = sort_bool;
4267 t->literal = op;
4268 t->given = sort_makeNoSort ();
4269 t->name = NULL; /*< missing this >*/
4270 t->args = termNodeList_new ();
4271 t->possibleSorts = sortSet_new ();
4272 t->possibleOps = lslOpSet_new ();
4273 (void) sortSet_insert (t->possibleSorts, t->sort);
4274
4275 ltoken_free (all);
4276
4277 return t;
4278}
4279
4280/*@only@*/ termNode
4281makeUnchangedTermNode2 (ltoken op, storeRefNodeList x)
4282{
4283 termNode t = (termNode) dmalloc (sizeof (*t));
4284 ltoken errtok;
4285 sort sort;
4286
4287 t->name = NULL; /*< missing this >*/
4288 t->error_reported = FALSE;
4289 t->wrapped = 0;
4290 t->kind = TRM_UNCHANGEDOTHERS;
4291 t->sort = sort_bool;
4292 t->literal = op;
4293 t->unchanged = x;
4294 t->given = sort_makeNoSort ();
4295 t->possibleSorts = sortSet_new ();
4296 t->possibleOps = lslOpSet_new ();
4297 t->args = termNodeList_new ();
4298
4299 (void) sortSet_insert (t->possibleSorts, t->sort);
4300 /* check storeRefNode's are mutable, uses sort of term */
4301
4302 storeRefNodeList_elements (x, sto)
4303 {
4304 if (storeRefNode_isTerm (sto))
4305 {
4306 sort = sto->content.term->sort;
4307 if (!sort_mutable (sort))
4308 {
4309 errtok = termNode_errorToken (sto->content.term);
4310 lclerror (errtok,
4311 message ("Term denoting immutable object used in unchanged list: %q",
4312 termNode_unparse (sto->content.term)));
4313 }
4314 }
4315 else
4316 {
4317 if (storeRefNode_isType (sto))
4318 {
4319 lclTypeSpecNode type = sto->content.type;
4320 sort = lclTypeSpecNode2sort (type);
4321 if (!sort_mutable (sort))
4322 {
4323 errtok = lclTypeSpecNode_errorToken (type);
4324 lclerror (errtok, message ("Immutable type used in unchanged list: %q",
4325 sort_unparse (sort)));
4326 }
4327 }
4328 }
4329 } end_storeRefNodeList_elements;
4330
4331 return t;
4332}
4333
4334/*@only@*/ termNode
4335 makeSizeofTermNode (ltoken op, lclTypeSpecNode type)
4336{
4337 termNode t = (termNode) dmalloc (sizeof (*t));
4338
4339 t->name = NULL; /*< missing this >*/
4340 t->error_reported = FALSE;
4341 t->wrapped = 0;
4342 t->kind = TRM_SIZEOF;
4343 t->sort = sort_int;
4344 t->literal = op;
4345 t->sizeofField = type;
4346 t->given = sort_makeNoSort ();
4347 t->possibleSorts = sortSet_new ();
4348 t->possibleOps = lslOpSet_new ();
4349 t->args = termNodeList_new ();
4350
4351 (void) sortSet_insert (t->possibleSorts, t->sort);
4352 /* nothing to check */
4353 return (t);
4354}
4355
4356/*@only@*/ cstring
4357claimNode_unparse (claimNode c)
4358{
4359 if (c != (claimNode) 0)
4360 {
4361 cstring s = message ("claims (%q)%q{\n%q",
4362 paramNodeList_unparse (c->params),
4363 varDeclarationNodeList_unparse (c->globals),
4364 lclPredicateNode_unparse (c->require));
4365
4366 if (c->body != NULL)
4367 {
4368 s = message ("%qbody {%q}\n", s, programNode_unparse (c->body));
4369 }
4370 s = message ("%q%q}\n", s, lclPredicateNode_unparse (c->ensures));
4371 return s;
4372 }
4373 return cstring_undefined;
4374}
4375
4376static void
4377WrongArity (ltoken tok, int expect, int size)
4378{
4379 lclerror (tok, message ("Expecting %d arguments but given %d", expect, size));
4380}
4381
4382static cstring
4383printTermNode2 (/*@null@*/ opFormNode op, termNodeList args, sort sort)
4384{
4385 if (op != (opFormNode) 0)
4386 {
4387 cstring s = cstring_undefined;
4388 cstring sortText;
4389 cstring sortSpace;
4390
4391 if (sort != sort_makeNoSort ())
4392 {
4393 sortText = message (": %s", cstring_fromChars (lsymbol_toChars (sort_getLsymbol (sort))));
4394 sortSpace = cstring_makeLiteral (" ");
4395 }
4396 else
4397 {
4398 sortText = cstring_undefined;
4399 sortSpace = cstring_undefined;
4400 }
4401
4402 switch (op->kind)
4403 {
4404 case OPF_IF:
4405 {
4406 int size = termNodeList_size (args);
4407
4408 if (size == 3)
4409 {
4410 s = message ("if %q then %q else %q\n",
4411 termNode_unparse (termNodeList_getN (args, 0)),
4412 termNode_unparse (termNodeList_getN (args, 1)),
4413 termNode_unparse (termNodeList_getN (args, 2)));
4414 }
4415 else
4416 {
4417 WrongArity (op->tok, 3, size);
4418 s = cstring_makeLiteral ("if __ then __ else __");
4419 }
4420 s = message ("%q%s", s, sortText);
4421 break;
4422 }
4423 case OPF_ANYOP:
4424 { /* ymtan ? */
4425 s = message ("%s %s",
4426 ltoken_getRawString (op->content.anyop),
4427 sortText);
4428 break;
4429 }
4430 case OPF_MANYOP:
4431 {
4432 int size = termNodeList_size (args);
4433
4434 if (size == 1)
4435 {
4436 s = message ("%q ", termNode_unparse (termNodeList_head (args)));
4437 }
4438 else
4439 {
4440 WrongArity (op->content.anyop, 1, size);
4441 s = cstring_makeLiteral ("__ ");
4442 }
4443 s = message ("%q%s%s", s, ltoken_getRawString (op->content.anyop),
4444 sortText);
4445 break;
4446 }
4447 case OPF_ANYOPM:
4448 {
4449 int size = termNodeList_size (args);
4450
4451 s = message ("%s ", ltoken_getRawString (op->content.anyop));
4452
4453 if (size == 1)
4454 {
4455 s = message ("%q%q", s, termNode_unparse (termNodeList_head (args)));
4456 }
4457 else
4458 {
4459 WrongArity (op->content.anyop, 1, size);
4460 s = message ("%q__", s);
4461 }
4462 s = message ("%q%s", s, sortText);
4463 break;
4464 }
4465 case OPF_MANYOPM:
4466 {
4467 int size = termNodeList_size (args);
4468
4469 if (size == 2)
4470 {
4471 s = message ("%q %s %q",
4472 termNode_unparse (termNodeList_getN (args, 0)),
4473 ltoken_getRawString (op->content.anyop),
4474 termNode_unparse (termNodeList_getN (args, 1)));
4475 }
4476 else
4477 {
4478 WrongArity (op->content.anyop, 2, size);
4479 s = message ("__ %s __", ltoken_getRawString (op->content.anyop));
4480 }
4481 s = message ("%q%s", s, sortText);
4482 break;
4483 }
4484 case OPF_MIDDLE:
4485 {
4486 int size = termNodeList_size (args);
4487 int expect = op->content.middle;
4488
4489 /* ymtan ? use { or openSym token ? */
4490
4491 if (size == expect)
4492 {
4493 s = message ("{%q}", termNodeList_unparse (args));
4494 }
4495 else
4496 {
4497 WrongArity (op->tok, expect, size);
4498 s = cstring_makeLiteral ("{ * }");
4499 }
4500
4501 s = message ("%q%s", s, sortText);
4502 break; /*** <<<--- bug detected by LCLint ***/
4503 }
4504 case OPF_MMIDDLE:
4505 {
4506 int size = termNodeList_size (args);
4507 int expect = op->content.middle + 1;
4508
4509 if (size == expect)
4510 {
4511 s = message ("%q{%q}",
4512 termNode_unparse (termNodeList_head (args)),
4513 termNodeList_unparseTail (args));
4514 }
4515 else
4516 {
4517 WrongArity (op->tok, expect, size);
4518 s = cstring_makeLiteral ("__ { * }");
4519 }
4520
4521 s = message ("%q%s", s, sortText);
4522 break;
4523 }
4524 case OPF_MIDDLEM:
4525 {
4526 int size = termNodeList_size (args);
4527 int expect = op->content.middle + 1;
4528
4529 if (size == expect)
4530 {
4531 termNodeList_finish (args);
4532
4533 s = message ("{%q}%s%s%q",
4534 termNodeList_unparseToCurrent (args),
4535 sortText, sortSpace,
4536 termNode_unparse (termNodeList_current (args)));
4537 }
4538 else
4539 {
4540 WrongArity (op->tok, expect, size);
4541
4542 s = message ("{ * }%s __", sortText);
4543
4544 /* used to put in extra space! evs 94-01-05 */
4545 }
4546 break;
4547 }
4548 case OPF_MMIDDLEM:
4549 {
4550 int size = termNodeList_size (args);
4551 int expect = op->content.middle + 2;
4552
4553 if (size == expect)
4554 {
4555 termNodeList_finish (args);
4556
4557 s = message ("%q {%q} %s%s%q",
4558 termNode_unparse (termNodeList_head (args)),
4559 termNodeList_unparseSecondToCurrent (args),
4560 sortText, sortSpace,
4561 termNode_unparse (termNodeList_current (args)));
4562 }
4563 else
4564 {
4565 WrongArity (op->tok, expect, size);
4566 s = message ("__ { * } %s __", sortText);
4567
4568 /* also had extra space? */
4569 }
4570 break;
4571 }
4572 case OPF_BMIDDLE:
4573 {
4574 int size = termNodeList_size (args);
4575 int expect = op->content.middle;
4576
4577 if (size == expect)
4578 {
4579 s = message ("[%q]", termNodeList_unparse (args));
4580 }
4581 else
4582 {
4583 WrongArity (op->tok, expect, size);
4584 s = cstring_makeLiteral ("[ * ]");
4585 }
4586 s = message ("%q%s", s, sortText);
4587 break;
4588 }
4589 case OPF_BMMIDDLE:
4590 {
4591 int size = termNodeList_size (args);
4592 int expect = op->content.middle + 1;
4593
4594 if (size == expect)
4595 {
4596 s = message ("%q[%q]",
4597 termNode_unparse (termNodeList_head (args)),
4598 termNodeList_unparseTail (args));
4599 }
4600 else
4601 {
4602 WrongArity (op->tok, expect, size);
4603 s = cstring_makeLiteral ("__ [ * ]");
4604 }
4605
4606 s = message ("%q%s", s, sortText);
4607 break;
4608 }
4609 case OPF_BMMIDDLEM:
4610 {
4611 int size = termNodeList_size (args);
4612 int expect = op->content.middle + 1;
4613
4614 if (size == expect)
4615 {
4616 s = message ("%q[%q] __",
4617 termNode_unparse (termNodeList_head (args)),
4618 termNodeList_unparseTail (args));
4619 }
4620 else
4621 {
4622 WrongArity (op->tok, expect, size);
4623 s = cstring_makeLiteral ("__ [ * ] __");
4624 }
4625 s = message ("%q%s", s, sortText);
4626 break;
4627 }
4628 case OPF_BMIDDLEM:
4629 {
4630 int size = termNodeList_size (args);
4631 int expect = op->content.middle + 1;
4632
4633 if (size == expect)
4634 {
4635 termNodeList_finish (args);
4636
4637 s = message ("[%q]%s%s%q",
4638 termNodeList_unparseToCurrent (args),
4639 sortText, sortSpace,
4640 termNode_unparse (termNodeList_current (args)));
4641 }
4642 else
4643 {
4644 WrongArity (op->tok, expect, size);
4645 s = cstring_makeLiteral ("[ * ] __");
4646 }
4647
4648 break;
4649 }
4650 case OPF_SELECT:
4651 { /* ymtan constant, check args ? */
4652 s = cstring_prependChar ('.', ltoken_getRawString (op->content.id));
4653 break;
4654 }
4655 case OPF_MAP:
4656 s = cstring_concat (cstring_makeLiteralTemp ("->"),
4657 ltoken_getRawString (op->content.id));
4658 break;
4659 case OPF_MSELECT:
4660 {
4661 int size = termNodeList_size (args);
4662
4663 if (size == 1)
4664 {
4665 s = message ("%q.%s", termNode_unparse (termNodeList_head (args)),
4666 ltoken_getRawString (op->content.id));
4667 }
4668 else
4669 {
4670 WrongArity (op->content.id, 1, size);
4671 s = cstring_concat (cstring_makeLiteralTemp ("__."),
4672 ltoken_getRawString (op->content.id));
4673 }
4674 break;
4675 }
4676 case OPF_MMAP:
4677 {
4678 int size = termNodeList_size (args);
4679
4680 if (size == 1)
4681 {
4682 s = message ("%q->%s", termNode_unparse (termNodeList_head (args)),
4683 ltoken_getRawString (op->content.id));
4684 }
4685 else
4686 {
4687 WrongArity (op->content.id, 1, size);
4688 s = cstring_concat (cstring_makeLiteralTemp ("__->"),
4689 ltoken_getRawString (op->content.id));
4690 }
4691 break;
4692 }
4693 }
4694
4695 cstring_free (sortSpace);
4696 cstring_free (sortText);
4697 return s;
4698 }
4699 return cstring_undefined;
4700}
4701
4702/*@only@*/ cstring
4703termNode_unparse (/*@null@*/ termNode n)
4704{
4705 cstring s = cstring_undefined;
4706 cstring back = cstring_undefined;
4707 cstring front = cstring_undefined;
4708 int count;
4709
4710 if (n != (termNode) 0)
4711 {
4712 for (count = n->wrapped; count > 0; count--)
4713 {
4714 front = cstring_appendChar (front, '(');
4715 back = cstring_appendChar (back, ')');
4716 }
4717
4718 switch (n->kind)
4719 {
4720 case TRM_LITERAL:
4721 case TRM_CONST:
4722 case TRM_VAR:
4723 case TRM_ZEROARY:
4724 s = cstring_copy (ltoken_getRawString (n->literal));
4725 break;
4726 case TRM_APPLICATION:
4727 {
4728 nameNode nn = n->name;
4729 if (nn != (nameNode) 0)
4730 {
4731 if (nn->isOpId)
4732 {
4733 s = message ("%s (%q) ",
4734 ltoken_getRawString (nn->content.opid),
4735 termNodeList_unparse (n->args));
4736 /* must we handle n->given ? skip for now */
4737 }
4738 else
4739 {
4740 s = message ("%q ", printTermNode2 (nn->content.opform, n->args, n->given));
4741 }
4742 }
4743 else
4744 {
4745 llfatalbug
4746 (message ("termNode_unparse: expect non-empty nameNode: TRM_APPLICATION: %q",
4747 nameNode_unparse (nn)));
4748 }
4749 break;
4750 }
4751 case TRM_UNCHANGEDALL:
4752 s = cstring_makeLiteral ("unchanged (all)");
4753 break;
4754 case TRM_UNCHANGEDOTHERS:
4755 s = message ("unchanged (%q)", storeRefNodeList_unparse (n->unchanged));
4756 break;
4757 case TRM_SIZEOF:
4758 s = message ("sizeof (%q)", lclTypeSpecNode_unparse (n->sizeofField));
4759 break;
4760 case TRM_QUANTIFIER:
4761 {
4762 quantifiedTermNode x = n->quantified;
4763 s = message ("%q%s%q%s",
4764 quantifierNodeList_unparse (x->quantifiers),
4765 ltoken_getRawString (x->open),
4766 termNode_unparse (x->body),
4767 ltoken_getRawString (x->close));
4768 break;
4769 }
4770 }
4771 }
4772 return (message ("%q%q%q", front, s, back));
4773}
4774
4775static void modifyNode_free (/*@null@*/ /*@only@*/ modifyNode m)
4776{
4777 if (m != (modifyNode) 0)
4778 {
4779
4780 if (m->hasStoreRefList)
4781 {
4782 storeRefNodeList_free (m->list);
4783 /*@-branchstate@*/
4784 }
4785 /*@=branchstate@*/
4786
4787 ltoken_free (m->tok);
4788 sfree (m);
4789 }
4790}
4791
4792/*@only@*/ cstring
4793modifyNode_unparse (/*@null@*/ modifyNode m)
4794{
4795 if (m != (modifyNode) 0)
4796 {
4797 if (m->hasStoreRefList)
4798 {
4799 return (message (" modifies %q; \n", storeRefNodeList_unparse (m->list)));
4800 }
4801 else
4802 {
4803 if (m->modifiesNothing)
4804 {
4805 return (cstring_makeLiteral ("modifies nothing; \n"));
4806 }
4807 else
4808 {
4809 return (cstring_makeLiteral ("modifies anything; \n"));
4810 }
4811 }
4812 }
4813 return cstring_undefined;
4814}
4815
4816/*@only@*/ cstring
4817programNode_unparse (programNode p)
4818{
4819 if (p != (programNode) 0)
4820 {
4821 cstring s = cstring_undefined;
4822 int count;
4823
4824 switch (p->kind)
4825 {
4826 case ACT_SELF:
4827 {
4828 cstring back = cstring_undefined;
4829
4830 for (count = p->wrapped; count > 0; count--)
4831 {
4832 s = cstring_appendChar (s, '(');
4833 back = cstring_appendChar (back, ')');
4834 }
4835 s = message ("%q%q%q", s, stmtNode_unparse (p->content.self), back);
4836 break;
4837 }
4838 case ACT_ITER:
4839 s = message ("*(%q)", programNodeList_unparse (p->content.args));
4840 break;
4841 case ACT_ALTERNATE:
4842 s = message ("|(%q)", programNodeList_unparse (p->content.args));
4843 break;
4844 case ACT_SEQUENCE:
4845 s = programNodeList_unparse (p->content.args);
4846 break;
4847 }
4848
4849 return s;
4850 }
4851 return cstring_undefined;
4852}
4853
4854/*@only@*/ cstring
4855stmtNode_unparse (stmtNode x)
4856{
4857 cstring s = cstring_undefined;
4858
4859 if (x != (stmtNode) 0)
4860 {
4861 if (ltoken_isValid (x->lhs))
4862 {
4863 s = cstring_concat (ltoken_getRawString (x->lhs),
4864 cstring_makeLiteralTemp (" = "));
4865 }
4866
4867 s = message ("%q%s (%q)", s,
4868 ltoken_getRawString (x->operator),
4869 termNodeList_unparse (x->args));
4870 }
4871
4872 return s;
4873}
4874
4875/*@only@*/ lslOp
4876 makelslOpNode (/*@only@*/ /*@null@*/ nameNode name,
4877 /*@dependent@*/ sigNode s)
4878{
4879 lslOp x = (lslOp) dmalloc (sizeof (*x));
4880
4881 x->name = name;
4882 x->signature = s;
4883
4884 /* enter operator info into symtab */
4885 /* if not, they may need to be renamed in LCL imports */
4886
4887 if (g_lslParsingTraits)
4888 {
4889 if (name != NULL)
4890 {
4891 symtable_enterOp (g_symtab, nameNode_copySafe (name), sigNode_copy (s));
4892 }
4893 }
4894 else
4895 {
4896 /* nameNode_free (name); */ /* YIKES! */
4897 }
4898
4899 return x;
4900}
4901
4902/*@only@*/ cstring
4903lslOp_unparse (lslOp x)
4904{
4905 char *s = mstring_createEmpty ();
4906
4907 if (x != (lslOp) 0)
4908 {
4909 s = mstring_concatFree (s, cstring_toCharsSafe (nameNode_unparse (x->name)));
4910
4911 if (x->signature != (sigNode) 0)
4912 {
4913 s = mstring_concatFree (s, cstring_toCharsSafe (sigNode_unparse (x->signature)));
4914 }
4915 }
4916
4917 return cstring_fromCharsO (s);
4918}
4919
4920static bool
4921sameOpFormNode (/*@null@*/ opFormNode n1, /*@null@*/ opFormNode n2)
4922{
4923 if (n1 == n2)
4924 return TRUE;
4925
4926 if (n1 == 0)
4927 return FALSE;
4928
4929 if (n2 == 0)
4930 return FALSE;
4931
4932 if (n1->kind == n2->kind)
4933 {
4934 switch (n1->kind)
4935 {
4936 case OPF_IF:
4937 return TRUE;
4938 case OPF_ANYOP:
4939 case OPF_MANYOP:
4940 case OPF_ANYOPM:
4941 return (ltoken_similar (n1->content.anyop, n2->content.anyop));
4942 case OPF_MANYOPM:
4943 {
4944 /* want to treat eq and = the same */
4945 return ltoken_similar (n1->content.anyop, n2->content.anyop);
4946 }
4947 case OPF_MIDDLE:
4948 case OPF_MMIDDLE:
4949 case OPF_MIDDLEM:
4950 case OPF_MMIDDLEM:
4951 /* need to check the rawText of openSym and closeSym */
4952 if ((int) n1->content.middle == (int) n2->content.middle)
4953 {
4954 if (lsymbol_equal (ltoken_getRawText (n1->tok),
4955 ltoken_getRawText (n2->tok)) &&
4956 lsymbol_equal (ltoken_getRawText (n1->close),
4957 ltoken_getRawText (n2->close)))
4958 return TRUE;
4959 }
4960 return FALSE;
4961 case OPF_BMIDDLE:
4962 case OPF_BMMIDDLE:
4963 case OPF_BMIDDLEM:
4964 case OPF_BMMIDDLEM:
4965 return ((int) n1->content.middle == (int) n2->content.middle);
4966 case OPF_SELECT:
4967 case OPF_MAP:
4968 case OPF_MSELECT:
4969 case OPF_MMAP:
4970 return (ltoken_similar (n1->content.id, n2->content.id));
4971 }
4972 }
4973 return FALSE;
4974}
4975
4976bool
4977sameNameNode (/*@null@*/ nameNode n1, /*@null@*/ nameNode n2)
4978{
4979 if (n1 == n2)
4980 return TRUE;
4981 if (n1 != (nameNode) 0 && n2 != (nameNode) 0)
4982 {
4983 if (bool_equal (n1->isOpId, n2->isOpId))
4984 {
4985 if (n1->isOpId)
4986 return (ltoken_similar (n1->content.opid, n2->content.opid));
4987 else
4988 return sameOpFormNode (n1->content.opform,
4989 n2->content.opform);
4990 }
4991 }
4992 return FALSE;
4993}
4994
4995void CTypesNode_free (/*@only@*/ /*@null@*/ CTypesNode x)
4996{
4997 if (x != NULL)
4998 {
4999 ltokenList_free (x->ctypes);
5000 sfree (x);
5001 }
5002}
5003
5004/*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode x)
5005{
5006 if (x != NULL)
5007 {
5008 CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5009 newnode->intfield = x->intfield;
5010 newnode->ctypes = ltokenList_copy (x->ctypes);
5011 newnode->sort = x->sort;
5012
5013 return newnode;
5014 }
5015 else
5016 {
5017 return NULL;
5018 }
5019}
5020
5021/*@only@*/ CTypesNode
5022 makeCTypesNode (/*@only@*/ CTypesNode ctypes, ltoken ct)
5023{
5024 /*@only@*/ CTypesNode newnode;
5025 lsymbol sortname;
5026 bits sortbits;
5027
5028 if (ctypes == (CTypesNode) NULL)
5029 {
5030 newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5031 newnode->intfield = 0;
5032 newnode->ctypes = ltokenList_new ();
5033 newnode->sort = sort_makeNoSort ();
5034 }
5035 else
5036 {
5037 newnode = ctypes;
5038 }
5039
5040 if ((ltoken_getIntField (ct) & newnode->intfield) != 0)
5041 {
5042 lclerror (ct,
5043 message
5044 ("Duplicate type specifier ignored: %s",
5045 cstring_fromChars
5046 (lsymbol_toChars
5047 (lclctype_toSortDebug (ltoken_getIntField (ct))))));
5048
5049 /* evs --- don't know how to generator this error */
5050
5051 /* Use previous value, to keep things consistent */
5052 ltoken_free (ct);
5053 return newnode;
5054 }
5055
5056 sortbits = newnode->intfield | ltoken_getIntField (ct);
5057 sortname = lclctype_toSort (sortbits);
5058
5059 if (sortname == lsymbol_fromChars ("error"))
5060 {
5061 lclerror (ct, cstring_makeLiteral ("Invalid combination of type specifiers"));
5062 }
5063 else
5064 {
5065 newnode->intfield = sortbits;
5066 }
5067
5068 ltokenList_addh (newnode->ctypes, ct);
5069
5070 /*
5071 ** Sorts are assigned after CTypesNode is created during parsing,
5072 ** see bison grammar.
5073 */
5074
5075 return newnode;
5076}
5077
5078/*@only@*/ CTypesNode
5079makeTypeSpecifier (ltoken typedefname)
5080{
5081 CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5082 typeInfo ti = symtable_typeInfo (g_symtab, ltoken_getText (typedefname));
5083
5084 newnode->intfield = 0;
5085 newnode->ctypes = ltokenList_singleton (ltoken_copy (typedefname));
5086
5087 /* if we see "bool" include bool.h header file */
5088
5089 if (ltoken_getText (typedefname) == lsymbol_bool)
5090 {
5091 lhIncludeBool ();
5092 }
5093
5094 if (typeInfo_exists (ti))
5095 {
28bf4b0b 5096 /* must we be concern about whether this type is exported by module?
5097 No. Because all typedef's are exported. No hiding supported. */
5098 /* Later, may want to keep types around too */
5099 /* 3/2/93, use underlying sort */
616915dd 5100 newnode->sort = sort_getUnderlying (ti->basedOn);
5101 }
5102 else
5103 {
5104 lclerror (typedefname, message ("Unrecognized type: %s",
5105 ltoken_getRawString (typedefname)));
5106 /* evs --- Don't know how to get this message */
28bf4b0b 5107
616915dd 5108 newnode->sort = sort_makeNoSort ();
5109 }
5110
5111 ltoken_free (typedefname);
5112 return newnode;
5113}
5114
5115bool sigNode_equal (sigNode n1, sigNode n2)
5116{
5117 /* n1 and n2 are never 0 */
5118
5119 return ((n1 == n2) ||
5120 (n1->key == n2->key &&
5121 ltoken_similar (n1->range, n2->range) &&
5122 ltokenList_equal (n1->domain, n2->domain)));
5123}
5124
5125sort
5126typeExpr2ptrSort (sort base, /*@null@*/ typeExpr t)
5127{
5128 if (t != (typeExpr) 0)
5129 {
5130 switch (t->kind)
5131 {
5132 case TEXPR_BASE:
5133 return base;
5134 case TEXPR_PTR:
5135 return typeExpr2ptrSort (sort_makePtr (ltoken_undefined, base),
5136 t->content.pointer);
5137 case TEXPR_ARRAY:
5138 return typeExpr2ptrSort (sort_makeArr (ltoken_undefined, base),
5139 t->content.array.elementtype);
5140 case TEXPR_FCN:
5141 /* map all hof types to some sort of SRT_HOF */
5142 return sort_makeHOFSort (base);
5143 }
5144 }
5145 return base;
5146}
5147
5148static sort
5149typeExpr2returnSort (sort base, /*@null@*/ typeExpr t)
5150{
5151 if (t != (typeExpr) 0)
5152 {
5153 switch (t->kind)
5154 {
5155 case TEXPR_BASE:
5156 return base;
5157 case TEXPR_PTR:
5158 return typeExpr2returnSort (sort_makePtr (ltoken_undefined, base),
5159 t->content.pointer);
5160 case TEXPR_ARRAY:
5161 return typeExpr2returnSort (sort_makeArr (ltoken_undefined, base),
5162 t->content.array.elementtype);
5163 case TEXPR_FCN:
5164 return typeExpr2returnSort (base, t->content.function.returntype);
5165 }
5166 }
5167 return base;
5168}
5169
5170sort
5171lclTypeSpecNode2sort (lclTypeSpecNode type)
5172{
5173 if (type != (lclTypeSpecNode) 0)
5174 {
5175 switch (type->kind)
5176 {
5177 case LTS_TYPE:
5178 llassert (type->content.type != NULL);
5179 return sort_makePtrN (type->content.type->sort, type->pointers);
5180 case LTS_STRUCTUNION:
5181 llassert (type->content.structorunion != NULL);
5182 return sort_makePtrN (type->content.structorunion->sort,
5183 type->pointers);
5184 case LTS_ENUM:
5185 llassert (type->content.enumspec != NULL);
5186 return sort_makePtrN (type->content.enumspec->sort,
5187 type->pointers);
5188 case LTS_CONJ:
5189 return (lclTypeSpecNode2sort (type->content.conj->a));
5190 }
5191 }
5192 return (sort_makeNoSort ());
5193}
5194
5195lsymbol
5196checkAndEnterTag (tagKind k, ltoken opttagid)
5197{
5198 /* should be tagKind, instead of int */
5199 tagInfo t;
5200 sort sort = sort_makeNoSort ();
5201
5202 if (!ltoken_isUndefined (opttagid))
5203 {
5204 switch (k)
5205 {
5206 case TAG_FWDSTRUCT:
5207 case TAG_STRUCT:
5208 sort = sort_makeStr (opttagid);
5209 break;
5210 case TAG_FWDUNION:
5211 case TAG_UNION:
5212 sort = sort_makeUnion (opttagid);
5213 break;
5214 case TAG_ENUM:
5215 sort = sort_makeEnum (opttagid);
5216 break;
5217 }
5218
5219 /* see if it is already in symbol table */
5220 t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid));
5221
5222 if (tagInfo_exists (t))
5223 {
5224 if (t->kind == TAG_FWDUNION || t->kind == TAG_FWDSTRUCT)
5225 {
5226 /* this is fine, for mutually recursive types */
5227 }
5228 else
5229 { /* this is not good, complain later */
5230 cstring s;
5231
5232 switch (k)
5233 {
5234 case TAG_ENUM:
5235 s = cstring_makeLiteral ("Enum");
5236 break;
5237 case TAG_STRUCT:
5238 case TAG_FWDSTRUCT:
5239 s = cstring_makeLiteral ("Struct");
5240 break;
5241 case TAG_UNION:
5242 case TAG_FWDUNION:
5243 s = cstring_makeLiteral ("Union");
5244 break;
5245 }
5246
5247 t->sort = sort;
5248 t->kind = k;
5249 lclerror (opttagid,
5250 message ("Tag redefined: %q %s", s,
5251 ltoken_getRawString (opttagid)));
5252
5253 }
5254
5255 ltoken_free (opttagid);
5256 }
5257 else
5258 {
5259 tagInfo newnode = (tagInfo) dmalloc (sizeof (*newnode));
5260
5261 newnode->sort = sort;
5262 newnode->kind = k;
5263 newnode->id = opttagid;
5264 newnode->imported = FALSE;
5265 newnode->content.decls = stDeclNodeList_new ();
5266
5267 (void) symtable_enterTag (g_symtab, newnode);
5268 }
5269 }
5270
5271 return sort_getLsymbol (sort);
5272}
5273
5274static sort
5275extractReturnSort (lclTypeSpecNode t, declaratorNode d)
5276{
5277 sort sort;
5278 sort = lclTypeSpecNode2sort (t);
5279 sort = typeExpr2returnSort (sort, d->type);
5280 return sort;
5281}
5282
5283void
5284signNode_free (/*@only@*/ signNode sn)
5285{
5286 sortList_free (sn->domain);
5287 ltoken_free (sn->tok);
5288 sfree (sn);
5289}
5290
5291/*@only@*/ cstring
5292signNode_unparse (signNode sn)
5293{
5294 cstring s = cstring_undefined;
5295
5296 if (sn != (signNode) 0)
5297 {
5298 s = message (": %q -> %s", sortList_unparse (sn->domain),
5299 sort_unparseName (sn->range));
5300 }
5301 return s;
5302}
5303
5304static /*@only@*/ pairNodeList
5305 globalList_toPairNodeList (globalList g)
5306{
5307 /* expect list to be globals, drop private ones */
5308 pairNodeList result = pairNodeList_new ();
5309 pairNode p;
5310 declaratorNode vdnode;
5311 lclTypeSpecNode type;
5312 sort sort;
5313 lsymbol sym;
5314 initDeclNodeList decls;
5315
5316 varDeclarationNodeList_elements (g, x)
5317 {
5318 if (x->isSpecial)
5319 {
5320 ;
5321 }
5322 else
5323 {
5324 if (x->isGlobal && !x->isPrivate)
5325 {
5326 type = x->type;
5327 decls = x->decls;
5328
5329 initDeclNodeList_elements (decls, init)
5330 {
5331 p = (pairNode) dmalloc (sizeof (*p));
5332
5333 vdnode = init->declarator;
5334 sym = ltoken_getText (vdnode->id);
5335 /* 2/21/93, not sure if it should be extractReturnSort,
5336 or some call to typeExpr2ptrSort */
5337 sort = extractReturnSort (type, vdnode);
5338 p->sort = sort_makeGlobal (sort);
5339 /* if (!sort_isArrayKind (sort)) p->sort = sort_makeObj (sort);
5340 else p->sort = sort; */
5341 /* p->name = sym; */
5342 p->tok = ltoken_copy (vdnode->id);
5343 pairNodeList_addh (result, p);
5344 } end_initDeclNodeList_elements;
5345 }
5346 }
5347 } end_varDeclarationNodeList_elements;
5348 return result;
5349}
5350
5351void
5352enteringFcnScope (lclTypeSpecNode t, declaratorNode d, globalList g)
5353{
5354 scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
5355 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5356 sort returnSort;
5357 ltoken result = ltoken_copy (ltoken_id);
5358 pairNodeList paramPairs, globals;
5359 fctInfo fi = (fctInfo) dmalloc (sizeof (*fi));
5360 signNode sign = (signNode) dmalloc (sizeof (*sign));
5361 sortList domain = sortList_new ();
5362 unsigned int key;
5363
5364 paramPairs = extractParams (d->type);
5365 returnSort = extractReturnSort (t, d);
5366 globals = globalList_toPairNodeList (g);
5367
5368 sign->tok = ltoken_undefined;
5369 sign->range = returnSort;
5370
5371 key = MASH (0, sort_getLsymbol (returnSort));
5372
5373 pairNodeList_elements (paramPairs, p)
5374 {
5375 sortList_addh (domain, p->sort);
5376 key = MASH (key, sort_getLsymbol (p->sort));
5377 } end_pairNodeList_elements;
5378
5379 sign->domain = domain;
5380 sign->key = key;
5381
5382 /* push fcn onto symbol table stack first */
5383 fi->id = ltoken_copy (d->id);
5384 fi->export = TRUE;
5385 fi->signature = sign;
5386 fi->globals = globals;
5387
5388 (void) symtable_enterFct (g_symtab, fi);
5389
5390 /* push new fcn scope */
5391 si->kind = SPE_FCN;
5392 symtable_enterScope (g_symtab, si);
5393
5394 /* add "result" with return type to current scope */
5395 ltoken_setText (result, lsymbol_fromChars ("result"));
5396
5397 vi->id = result;
5398 vi->sort = sort_makeFormal (returnSort); /* make appropriate values */
5399 vi->kind = VRK_PARAM;
5400 vi->export = TRUE;
5401
5402 (void) symtable_enterVar (g_symtab, vi);
5403
5404 /*
5405 ** evs - 4 Mar 1995
5406 ** pust globals first (they are in outer scope)
5407 */
5408
5409 /* push onto symbol table the global variables declared in this function,
5410 together with their respective sorts */
5411
5412 pairNodeList_elements (globals, gl)
5413 {
5414 ltoken_free (vi->id);
5415 vi->id = ltoken_copy (gl->tok);
5416 vi->kind = VRK_GLOBAL;
5417 vi->sort = gl->sort;
5418 (void) symtable_enterVar (g_symtab, vi);
5419 } end_pairNodeList_elements;
5420
5421 /*
5422 ** could enter a new scope; instead, warn when variable shadows global
5423 ** that is used
5424 */
5425
5426 /*
5427 ** push onto symbol table the formal parameters of this function,
5428 ** together with their respective sorts
5429 */
5430
5431 pairNodeList_elements (paramPairs, pair)
5432 {
5433 ltoken_free (vi->id);
5434 vi->id = ltoken_copy (pair->tok);
5435 vi->sort = pair->sort;
5436 vi->kind = VRK_PARAM;
5437 (void) symtable_enterVar (g_symtab, vi);
5438 } end_pairNodeList_elements;
5439
5440 pairNodeList_free (paramPairs);
5441 varInfo_free (vi);
5442}
5443
5444void
5445enteringClaimScope (paramNodeList params, globalList g)
5446{
5447 scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
5448 pairNodeList globals;
5449 lclTypeSpecNode paramtype;
5450 typeExpr paramdecl;
5451 sort sort;
5452
5453 globals = globalList_toPairNodeList (g);
5454 /* push new claim scope */
5455 si->kind = SPE_CLAIM;
5456
5457 symtable_enterScope (g_symtab, si);
5458
5459 /* push onto symbol table the formal parameters of this function,
5460 together with their respective sorts */
5461
5462 paramNodeList_elements (params, param)
5463 {
5464 paramdecl = param->paramdecl;
5465 paramtype = param->type;
5466 if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0)
5467 {
5468 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5469
5470 sort = lclTypeSpecNode2sort (paramtype);
5471 sort = sort_makeFormal (sort);
5472 vi->sort = typeExpr2ptrSort (sort, paramdecl);
5473 vi->id = ltoken_copy (extractDeclarator (paramdecl));
5474 vi->kind = VRK_PARAM;
5475 vi->export = TRUE;
5476
5477 (void) symtable_enterVar (g_symtab, vi);
5478 varInfo_free (vi);
5479 }
5480 } end_paramNodeList_elements;
5481
5482 /* push onto symbol table the global variables declared in this function,
5483 together with their respective sorts */
5484
5485 pairNodeList_elements (globals, g2)
5486 {
5487 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5488
5489 vi->id = ltoken_copy (g2->tok);
5490 vi->kind = VRK_GLOBAL;
5491 vi->sort = g2->sort;
5492 vi->export = TRUE;
5493
5494 /* should catch duplicates in formals */
5495 (void) symtable_enterVar (g_symtab, vi);
5496 varInfo_free (vi);
5497 } end_pairNodeList_elements;
5498
5499 pairNodeList_free (globals);
5500 /* should not free it here! ltoken_free (claimId); @*/
5501}
5502
5503static /*@only@*/ pairNodeList
5504 extractParams (/*@null@*/ typeExpr te)
5505{
5506 /* extract the parameters from a function header declarator's typeExpr */
5507 sort sort;
5508 typeExpr paramdecl;
5509 paramNodeList params;
5510 lclTypeSpecNode paramtype;
5511 pairNodeList head = pairNodeList_new ();
5512 pairNode pair;
5513
5514 if (te != (typeExpr) 0)
5515 {
5516 params = typeExpr_toParamNodeList (te);
5517 if (paramNodeList_isDefined (params))
5518 {
5519 paramNodeList_elements (params, param)
5520 {
5521 paramdecl = param->paramdecl;
5522 paramtype = param->type;
5523 if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0)
5524 {
5525 pair = (pairNode) dmalloc (sizeof (*pair));
5526 sort = lclTypeSpecNode2sort (paramtype);
5527 /* 2/17/93, was sort_makeVal (sort) */
5528 sort = sort_makeFormal (sort);
5529 pair->sort = typeExpr2ptrSort (sort, paramdecl);
5530 /* pair->name = ltoken_getText (extractDeclarator (paramdecl)); */
5531 pair->tok = ltoken_copy (extractDeclarator (paramdecl));
5532 pairNodeList_addh (head, pair);
5533 }
5534 } end_paramNodeList_elements;
5535 }
5536 }
5537 return head;
5538}
5539
5540sort
5541sigNode_rangeSort (sigNode sig)
5542{
5543 if (sig == (sigNode) 0)
5544 {
5545 return sort_makeNoSort ();
5546 }
5547 else
5548 {
5549 return sort_fromLsymbol (ltoken_getText (sig->range));
5550 }
5551}
5552
5553/*@only@*/ sortList
5554 sigNode_domain (sigNode sig)
5555{
5556 sortList domain = sortList_new ();
5557
5558 if (sig == (sigNode) 0)
5559 {
5560 ;
5561 }
5562 else
5563 {
5564 ltokenList dom = sig->domain;
5565
5566 ltokenList_elements (dom, tok)
5567 {
5568 sortList_addh (domain, sort_fromLsymbol (ltoken_getText (tok)));
5569 } end_ltokenList_elements;
5570 }
5571
5572 return domain;
5573}
5574
5575opFormUnion
5576opFormUnion_createAnyOp (/*@temp@*/ ltoken t)
5577{
5578 opFormUnion u;
5579
5580 /* do not distinguish between .anyop and .id */
5581 u.anyop = t;
5582 return u;
5583}
5584
5585opFormUnion
5586opFormUnion_createMiddle (int middle)
5587{
5588 opFormUnion u;
5589
5590 u.middle = middle;
5591 return u;
5592}
5593
5594paramNode
5595markYieldParamNode (paramNode p)
5596{
5597 p->kind = PYIELD;
5598
5599 llassert (p->type != NULL);
5600 p->type->quals = qualList_add (p->type->quals, qual_createYield ());
5601
5602 return (p);
5603}
5604
5605/*@only@*/ lclTypeSpecNode
5606 lclTypeSpecNode_copySafe (lclTypeSpecNode n)
5607{
5608 lclTypeSpecNode ret = lclTypeSpecNode_copy (n);
5609
5610 llassert (ret != NULL);
5611 return ret;
5612}
5613
5614/*@null@*/ /*@only@*/ lclTypeSpecNode
5615 lclTypeSpecNode_copy (/*@null@*/ lclTypeSpecNode n)
5616{
5617 if (n != NULL)
5618 {
5619 switch (n->kind)
5620 {
5621 case LTS_CONJ:
5622 return (makeLclTypeSpecNodeConj (lclTypeSpecNode_copy (n->content.conj->a),
5623 lclTypeSpecNode_copy (n->content.conj->b)));
5624 case LTS_TYPE:
5625 return (makeLclTypeSpecNodeType (CTypesNode_copy (n->content.type)));
5626 case LTS_STRUCTUNION:
5627 return (makeLclTypeSpecNodeSU (strOrUnionNode_copy (n->content.structorunion)));
5628 case LTS_ENUM:
5629 return (makeLclTypeSpecNodeEnum (enumSpecNode_copy (n->content.enumspec)));
5630 }
5631 }
5632
5633 return NULL;
5634}
5635
5636void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode n)
5637{
5638 if (n != NULL)
5639 {
5640 switch (n->kind)
5641 {
5642 case LTS_CONJ:
5643 lclTypeSpecNode_free (n->content.conj->a);
5644 lclTypeSpecNode_free (n->content.conj->b);
5645 break;
5646 case LTS_TYPE:
5647 CTypesNode_free (n->content.type);
5648 break;
5649 case LTS_STRUCTUNION:
5650 strOrUnionNode_free (n->content.structorunion);
5651 break;
5652 case LTS_ENUM:
5653 enumSpecNode_free (n->content.enumspec);
5654 break;
5655 }
5656
5657 qualList_free (n->quals);
5658 sfree (n);
5659 }
5660}
5661
5662static /*@null@*/ opFormNode opFormNode_copy (/*@null@*/ opFormNode op)
5663{
5664 if (op != NULL)
5665 {
5666 opFormNode ret = (opFormNode) dmalloc (sizeof (*ret));
5667
5668 ret->tok = ltoken_copy (op->tok);
5669 ret->kind = op->kind;
5670 ret->content = op->content;
5671 ret->key = op->key;
5672 ret->close = ltoken_copy (op->close);
5673
5674 return ret;
5675 }
5676 else
5677 {
5678 return NULL;
5679 }
5680}
5681
5682void opFormNode_free (/*@null@*/ opFormNode op)
5683{
28bf4b0b 5684 if (op != NULL)
5685 {
5686 ltoken_free (op->tok);
5687 ltoken_free (op->close);
5688 sfree (op);
5689 }
616915dd 5690}
5691
5692void nameNode_free (nameNode n)
5693{
5694
5695 if (n != NULL)
5696 {
5697 if (!n->isOpId)
5698 {
5699 opFormNode_free (n->content.opform);
5700 }
5701
5702 sfree (n);
5703 }
5704}
5705
5706bool
5707lslOp_equal (lslOp x, lslOp y)
5708{
5709 return ((x == y) ||
5710 ((x != 0) && (y != 0) &&
5711 sameNameNode (x->name, y->name) &&
5712 sigNode_equal (x->signature, y->signature)));
5713}
5714
5715void lslOp_free (lslOp x)
5716{
5717 nameNode_free (x->name);
5718 sfree (x);
5719}
5720
5721void sigNode_free (sigNode x)
5722{
5723 if (x != NULL)
5724 {
5725 ltokenList_free (x->domain);
5726 ltoken_free (x->tok);
5727 ltoken_free (x->range);
5728 sfree (x);
5729 }
5730}
5731
5732void declaratorNode_free (/*@null@*/ /*@only@*/ declaratorNode x)
5733{
5734 if (x != NULL)
5735 {
5736 typeExpr_free (x->type);
5737 ltoken_free (x->id);
5738 sfree (x);
5739 }
5740}
5741
5742void abstBodyNode_free (/*@null@*/ /*@only@*/ abstBodyNode n)
5743{
5744 if (n != NULL)
5745 {
5746 lclPredicateNode_free (n->typeinv);
5747 fcnNodeList_free (n->fcns);
5748 ltoken_free (n->tok);
5749 sfree (n);
5750 }
5751}
5752
5753void fcnNode_free (/*@null@*/ /*@only@*/ fcnNode f)
5754{
5755 if (f != NULL)
5756 {
5757 lclTypeSpecNode_free (f->typespec);
5758 declaratorNode_free (f->declarator);
5759 globalList_free (f->globals);
5760 varDeclarationNodeList_free (f->inits);
5761 letDeclNodeList_free (f->lets);
5762 lclPredicateNode_free (f->checks);
5763 lclPredicateNode_free (f->require);
5764 lclPredicateNode_free (f->claim);
5765 lclPredicateNode_free (f->ensures);
5766 modifyNode_free (f->modify);
5767 ltoken_free (f->name);
5768 sfree (f);
5769 }
5770}
5771
5772void declaratorInvNode_free (/*@null@*/ /*@only@*/ declaratorInvNode x)
5773{
5774 if (x != NULL)
5775 {
5776 declaratorNode_free (x->declarator);
5777 abstBodyNode_free (x->body);
5778 sfree (x);
5779 }
5780}
5781
5782/*@only@*/ lslOp lslOp_copy (lslOp x)
5783{
5784 return (makelslOpNode (nameNode_copy (x->name), x->signature));
5785}
5786
5787sigNode sigNode_copy (sigNode s)
5788{
5789 llassert (s != NULL);
5790 return (makesigNode (ltoken_copy (s->tok),
5791 ltokenList_copy (s->domain),
5792 ltoken_copy (s->range)));
5793}
5794
5795/*@null@*/ nameNode nameNode_copy (/*@null@*/ nameNode n)
5796{
5797 if (n == NULL) return NULL;
5798 return nameNode_copySafe (n);
5799}
5800
5801nameNode nameNode_copySafe (nameNode n)
5802{
5803 if (n->isOpId)
5804 {
5805 return (makeNameNodeId (ltoken_copy (n->content.opid)));
5806 }
5807 else
5808 {
5809 /* error should be detected by lclint: forgot to copy opform! */
5810 return (makeNameNodeForm (opFormNode_copy (n->content.opform)));
5811 }
5812}
5813
5814bool initDeclNode_isRedeclaration (initDeclNode d)
5815{
5816 return (d->declarator->isRedecl);
5817}
5818
5819void termNode_free (/*@only@*/ /*@null@*/ termNode t)
5820{
28bf4b0b 5821 if (t != NULL)
5822 {
5823 sortSet_free (t->possibleSorts);
5824 lslOpSet_free (t->possibleOps);
5825 nameNode_free (t->name);
5826 termNodeList_free (t->args);
5827 sfree (t);
5828 }
616915dd 5829}
5830
5831/*@only@*/ termNode termNode_copySafe (termNode t)
5832{
5833 termNode ret = termNode_copy (t);
5834
5835 llassert (ret != NULL);
5836 return ret;
5837}
5838
5839/*@null@*/ /*@only@*/ termNode termNode_copy (/*@null@*/ termNode t)
5840{
5841 if (t != NULL)
5842 {
5843 termNode ret = (termNode) dmalloc (sizeof (*ret));
5844
5845 ret->wrapped = t->wrapped;
5846 ret->kind = t->kind;
5847 ret->sort = t->sort;
5848 ret->given = t->given;
5849 ret->possibleSorts = sortSet_copy (t->possibleSorts);
5850 ret->error_reported = t->error_reported;
5851 ret->possibleOps = lslOpSet_copy (t->possibleOps);
5852 ret->name = nameNode_copy (t->name);
5853 ret->args = termNodeList_copy (t->args);
5854
5855 if (t->kind == TRM_LITERAL
5856 || t->kind == TRM_SIZEOF
5857 || t->kind == TRM_VAR
5858 || t->kind == TRM_CONST
5859 || t->kind == TRM_ZEROARY)
5860 {
5861 ret->literal = ltoken_copy (t->literal);
5862 }
5863
5864 if (t->kind == TRM_UNCHANGEDOTHERS)
5865 {
5866 ret->unchanged = storeRefNodeList_copy (t->unchanged);
5867 }
5868
5869 if (t->kind == TRM_QUANTIFIER)
5870 {
5871 ret->quantified = quantifiedTermNode_copy (t->quantified);
5872 }
5873
5874 if (t->kind == TRM_SIZEOF)
5875 {
5876 ret->sizeofField = lclTypeSpecNode_copySafe (t->sizeofField);
5877 }
5878
5879 return ret;
5880 }
5881 else
5882 {
5883
5884 return NULL;
5885 }
5886}
5887
5888void importNode_free (/*@only@*/ /*@null@*/ importNode x)
5889{
28bf4b0b 5890 if (x != NULL)
5891 {
5892 ltoken_free (x->val);
5893 sfree (x);
5894 }
616915dd 5895}
5896
5897void initDeclNode_free (/*@only@*/ /*@null@*/ initDeclNode x)
5898{
5899 if (x != NULL)
5900 {
5901 declaratorNode_free (x->declarator);
5902 termNode_free (x->value);
5903 sfree (x);
5904 }
5905}
5906
5907void letDeclNode_free (/*@only@*/ /*@null@*/ letDeclNode x)
5908{
5909 if (x != NULL)
5910 {
5911 lclTypeSpecNode_free (x->sortspec);
5912 termNode_free (x->term);
5913 ltoken_free (x->varid);
5914 sfree (x);
5915 }
5916}
5917
5918void pairNode_free (/*@only@*/ /*@null@*/ pairNode x)
5919{
28bf4b0b 5920 if (x != NULL)
5921 {
5922 ltoken_free (x->tok);
5923 sfree (x);
5924 }
616915dd 5925}
5926
5927/*@null@*/ paramNode paramNode_copy (/*@null@*/ paramNode p)
5928{
5929 if (p != NULL)
5930 {
5931 paramNode ret = (paramNode) dmalloc (sizeof (*ret));
5932
5933 ret->type = lclTypeSpecNode_copy (p->type);
5934 ret->paramdecl = typeExpr_copy (p->paramdecl);
5935 ret->kind = p->kind;
5936 return ret;
5937 }
5938
5939 return NULL;
5940}
5941
5942void paramNode_free (/*@only@*/ /*@null@*/ paramNode x)
5943{
5944 if (x != NULL)
5945 {
5946 lclTypeSpecNode_free (x->type);
5947 typeExpr_free (x->paramdecl);
5948 sfree (x);
5949 }
5950}
5951
5952void programNode_free (/*@only@*/ /*@null@*/ programNode x)
5953{
5954 if (x != NULL)
5955 {
5956 switch (x->kind)
5957 {
5958 case ACT_SELF: stmtNode_free (x->content.self); break;
5959 case ACT_ITER:
5960 case ACT_ALTERNATE:
5961 case ACT_SEQUENCE: programNodeList_free (x->content.args); break;
5962 BADDEFAULT;
5963 }
5964 sfree (x);
5965 }
5966}
5967
5968quantifierNode quantifierNode_copy (quantifierNode x)
5969{
5970 quantifierNode ret = (quantifierNode) dmalloc (sizeof (*ret));
5971
5972 ret->quant = ltoken_copy (x->quant);
5973 ret->vars = varNodeList_copy (x->vars);
5974 ret->isForall = x->isForall;
5975
5976 return ret;
5977}
5978
5979void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode x)
5980{
5981 if (x != NULL)
5982 {
5983 varNodeList_free (x->vars);
5984 ltoken_free (x->quant);
5985 sfree (x);
5986 }
5987}
5988
5989void replaceNode_free (/*@only@*/ /*@null@*/ replaceNode x)
5990{
5991 if (x != NULL)
5992 {
5993 if (x->isCType)
5994 {
5995 ;
5996 }
5997 else
5998 {
5999 nameNode_free (x->content.renamesortname.name);
6000 sigNode_free (x->content.renamesortname.signature);
6001 }
6002
6003 typeNameNode_free (x->typename);
6004 ltoken_free (x->tok);
6005 sfree (x);
6006 }
6007}
6008
6009storeRefNode storeRefNode_copy (storeRefNode x)
6010{
6011 storeRefNode ret = (storeRefNode) dmalloc (sizeof (*ret));
6012
6013 ret->kind = x->kind;
6014
6015 switch (x->kind)
6016 {
6017 case SRN_TERM:
6018 ret->content.term = termNode_copySafe (x->content.term);
6019 break;
6020 case SRN_OBJ: case SRN_TYPE:
6021 ret->content.type = lclTypeSpecNode_copy (x->content.type);
6022 break;
6023 case SRN_SPECIAL:
6024 ret->content.ref = sRef_copy (x->content.ref);
6025 break;
6026 }
6027
6028 return ret;
6029}
6030
6031void storeRefNode_free (/*@only@*/ /*@null@*/ storeRefNode x)
6032{
6033 if (x != NULL)
6034 {
6035 if (storeRefNode_isTerm (x))
6036 {
6037 termNode_free (x->content.term);
6038 }
6039 else if (storeRefNode_isType (x) || storeRefNode_isObj (x))
6040 {
6041 lclTypeSpecNode_free (x->content.type);
6042 }
6043 else
6044 {
6045 /* nothing to free */
6046 }
6047
6048 sfree (x);
6049 }
6050}
6051
6052stDeclNode stDeclNode_copy (stDeclNode x)
6053{
6054 stDeclNode ret = (stDeclNode) dmalloc (sizeof (*ret));
6055
6056 ret->lcltypespec = lclTypeSpecNode_copySafe (x->lcltypespec);
6057 ret->declarators = declaratorNodeList_copy (x->declarators);
6058
6059 return ret;
6060}
6061
6062void stDeclNode_free (/*@only@*/ /*@null@*/ stDeclNode x)
6063{
6064 if (x != NULL)
6065 {
6066 lclTypeSpecNode_free (x->lcltypespec);
6067 declaratorNodeList_free (x->declarators);
6068 sfree (x);
6069 }
6070}
6071
6072void traitRefNode_free (/*@only@*/ /*@null@*/ traitRefNode x)
6073{
6074 if (x != NULL)
6075 {
6076 ltokenList_free (x->traitid);
6077 renamingNode_free (x->rename);
6078 sfree (x);
6079 }
6080}
6081
6082void typeNameNode_free (/*@only@*/ /*@null@*/ typeNameNode n)
6083{
6084 if (n != NULL)
6085 {
6086 typeNamePack_free (n->typename);
6087 opFormNode_free (n->opform);
6088 sfree (n);
6089 }
6090}
6091
6092void varDeclarationNode_free (/*@only@*/ /*@null@*/ varDeclarationNode x)
6093{
6094 if (x != NULL)
6095 {
6096 if (x->isSpecial)
6097 {
6098 ;
6099 }
6100 else
6101 {
6102 lclTypeSpecNode_free (x->type);
6103 initDeclNodeList_free (x->decls);
6104 sfree (x);
6105 }
6106 }
6107}
6108
6109varNode varNode_copy (varNode x)
6110{
6111 varNode ret = (varNode) dmalloc (sizeof (*ret));
6112
6113 ret->varid = ltoken_copy (x->varid);
6114 ret->isObj = x->isObj;
6115 ret->type = lclTypeSpecNode_copySafe (x->type);
6116 ret->sort = x->sort;
6117
6118 return ret;
6119}
6120
6121void varNode_free (/*@only@*/ /*@null@*/ varNode x)
6122{
6123 if (x != NULL)
6124 {
6125 lclTypeSpecNode_free (x->type);
6126 ltoken_free (x->varid);
6127 sfree (x);
6128 }
6129}
6130
6131void stmtNode_free (/*@only@*/ /*@null@*/ stmtNode x)
6132{
6133 if (x != NULL)
6134 {
6135 ltoken_free (x->lhs);
6136 termNodeList_free (x->args);
6137 ltoken_free (x->operator);
6138 sfree (x);
6139 }
6140}
6141
6142void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode x)
6143{
6144 if (x != NULL)
6145 {
6146 if (x->is_replace)
6147 {
6148 replaceNodeList_free (x->content.replace);
6149 }
6150 else
6151 {
6152 nameAndReplaceNode_free (x->content.name);
6153 }
6154
6155 sfree (x);
6156 }
6157}
6158
6159void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode x)
6160{
6161 if (x != NULL)
6162 {
6163 typeNameNodeList_free (x->namelist);
6164 replaceNodeList_free (x->replacelist);
6165 sfree (x);
6166 }
6167}
6168
6169void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack x)
6170{
6171 if (x != NULL)
6172 {
6173 lclTypeSpecNode_free (x->type);
6174 abstDeclaratorNode_free (x->abst);
6175 sfree (x);
6176 }
6177}
6178
6179cstring interfaceNode_unparse (interfaceNode x)
6180{
6181 if (x != NULL)
6182 {
6183 switch (x->kind)
6184 {
6185 case INF_IMPORTS:
6186 return (message ("[imports] %q", importNodeList_unparse (x->content.imports)));
6187 case INF_USES:
6188 return (message ("[uses] %q", traitRefNodeList_unparse (x->content.uses)));
6189 case INF_EXPORT:
6190 return (message ("[export] %q", exportNode_unparse (x->content.export)));
6191 case INF_PRIVATE:
6192 return (message ("[private] %q", privateNode_unparse (x->content.private)));
6193 }
6194
6195 BADBRANCH;
6196 }
6197 else
6198 {
6199 return (cstring_makeLiteral ("<interface node undefined>"));
6200 }
8250fa4a 6201
6202 BADBRANCHRET (cstring_undefined);
616915dd 6203}
6204
6205void interfaceNode_free (/*@null@*/ /*@only@*/ interfaceNode x)
6206{
6207 if (x != NULL)
6208 {
6209
6210 switch (x->kind)
6211 {
6212 case INF_IMPORTS: importNodeList_free (x->content.imports); break;
6213 case INF_USES: traitRefNodeList_free (x->content.uses); break;
6214 case INF_EXPORT: exportNode_free (x->content.export); break;
6215 case INF_PRIVATE: privateNode_free (x->content.private); break;
6216 }
6217 sfree (x);
6218 }
6219}
6220
6221void exportNode_free (/*@null@*/ /*@only@*/ exportNode x)
6222{
6223 if (x != NULL)
6224 {
6225 switch (x->kind)
6226 {
6227 case XPK_CONST: constDeclarationNode_free (x->content.constdeclaration); break;
6228 case XPK_VAR: varDeclarationNode_free (x->content.vardeclaration); break;
6229 case XPK_TYPE: typeNode_free (x->content.type); break;
6230 case XPK_FCN: fcnNode_free (x->content.fcn); break;
6231 case XPK_CLAIM: claimNode_free (x->content.claim); break;
6232 case XPK_ITER: iterNode_free (x->content.iter); break;
6233 }
6234
6235 sfree (x);
6236 }
6237}
6238
6239void privateNode_free (/*@null@*/ /*@only@*/ privateNode x)
6240{
6241 if (x != NULL)
6242 {
6243 switch (x->kind)
6244 {
6245 case PRIV_CONST:
6246 constDeclarationNode_free (x->content.constdeclaration); break;
6247 case PRIV_VAR:
6248 varDeclarationNode_free (x->content.vardeclaration); break;
6249 case PRIV_TYPE:
6250 typeNode_free (x->content.type); break;
6251 case PRIV_FUNCTION:
6252 fcnNode_free (x->content.fcn); break;
6253 }
6254
6255 sfree (x);
6256 }
6257}
6258
6259void constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode x)
6260{
6261 if (x != NULL)
6262 {
6263 lclTypeSpecNode_free (x->type);
6264 initDeclNodeList_free (x->decls);
6265 sfree (x);
6266 }
6267}
6268
6269void typeNode_free (/*@only@*/ /*@null@*/ typeNode t)
6270{
6271 if (t != NULL)
6272 {
6273 switch (t->kind)
6274 {
6275 case TK_ABSTRACT: abstractNode_free (t->content.abstract); break;
6276 case TK_EXPOSED: exposedNode_free (t->content.exposed); break;
6277 case TK_UNION: taggedUnionNode_free (t->content.taggedunion); break;
6278 }
6279
6280 sfree (t);
6281 }
6282}
6283
6284void claimNode_free (/*@only@*/ /*@null@*/ claimNode x)
6285{
6286 if (x != NULL)
6287 {
6288 paramNodeList_free (x->params);
6289 globalList_free (x->globals);
6290 letDeclNodeList_free (x->lets);
6291 lclPredicateNode_free (x->require);
6292 programNode_free (x->body);
6293 lclPredicateNode_free (x->ensures);
6294 ltoken_free (x->name);
6295 sfree (x);
6296 }
6297}
6298
6299void iterNode_free (/*@only@*/ /*@null@*/ iterNode x)
6300{
6301 if (x != NULL)
6302 {
6303 paramNodeList_free (x->params);
6304 ltoken_free (x->name);
6305 sfree (x);
6306 }
6307}
6308
6309void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode x)
6310{
6311 if (x != NULL)
6312 {
6313 abstBodyNode_free (x->body);
6314 ltoken_free (x->tok);
6315 ltoken_free (x->name);
6316 sfree (x);
6317 }
6318}
6319
6320void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode x)
6321{
6322 if (x != NULL)
6323 {
6324 lclTypeSpecNode_free (x->type);
6325 declaratorInvNodeList_free (x->decls);
6326 ltoken_free (x->tok);
6327 sfree (x);
6328 }
6329}
6330
6331void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode x)
6332{
6333 if (x != NULL)
6334 {
6335 stDeclNodeList_free (x->structdecls);
6336 declaratorNode_free (x->declarator);
6337 sfree (x);
6338 }
6339}
6340
6341/*@only@*/ /*@null@*/ strOrUnionNode
6342 strOrUnionNode_copy (/*@null@*/ strOrUnionNode n)
6343{
6344 if (n != NULL)
6345 {
6346 strOrUnionNode ret = (strOrUnionNode) dmalloc (sizeof (*ret));
6347
6348 ret->kind = n->kind;
6349 ret->tok = ltoken_copy (n->tok);
6350 ret->opttagid = ltoken_copy (n->opttagid);
6351 ret->sort = n->sort;
6352 ret->structdecls = stDeclNodeList_copy (n->structdecls);
6353
6354 return ret;
6355 }
6356 else
6357 {
6358 return NULL;
6359 }
6360}
6361
6362void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode n)
6363{
6364 if (n != NULL)
6365 {
6366 stDeclNodeList_free (n->structdecls);
6367 ltoken_free (n->tok);
6368 ltoken_free (n->opttagid);
6369 sfree (n);
6370 }
6371}
6372
6373void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode x)
6374{
6375 if (x != NULL)
6376 {
6377 ltokenList_free (x->enums);
6378 ltoken_free (x->tok);
6379 ltoken_free (x->opttagid);
6380 sfree (x);
6381 }
6382}
6383
6384/*@only@*/ /*@null@*/ enumSpecNode enumSpecNode_copy (/*@null@*/ enumSpecNode x)
6385{
6386 if (x != NULL)
6387 {
6388 enumSpecNode ret = (enumSpecNode) dmalloc (sizeof (*ret));
6389
6390 ret->tok = ltoken_copy (x->tok);
6391 ret->opttagid = ltoken_copy (x->opttagid);
6392 ret->enums = ltokenList_copy (x->enums);
6393 ret->sort = x->sort;
6394
6395 return ret;
6396 }
6397 else
6398 {
6399 return NULL;
6400 }
6401}
6402
6403void lsymbol_setbool (lsymbol s)
6404{
6405 lsymbol_bool = s;
6406}
6407
6408lsymbol lsymbol_getbool ()
6409{
6410 return lsymbol_bool;
6411}
6412
6413lsymbol lsymbol_getBool ()
6414{
6415 return lsymbol_Bool;
6416}
6417
6418lsymbol lsymbol_getFALSE ()
6419{
6420 return lsymbol_FALSE;
6421}
6422
6423lsymbol lsymbol_getTRUE ()
6424{
6425 return lsymbol_TRUE;
6426}
6427
6428
git-cvsimport mirror of splint
This page took 1.228613 seconds and 5 git commands to generate.