]> andersk Git - splint.git/blame - src/abstract.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Committing after merging Evan's changes.
[splint.git] / src / abstract.c
CommitLineData
616915dd 1/*
11db3170 2** Splint - annotation-assisted static program checker
c59f5181 3** Copyright (C) 1994-2003 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**
155af98d 20** For information on splint: info@splint.org
21** To report a bug: splint-bug@splint.org
11db3170 22** For more information: http://www.splint.org
616915dd 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
1b8ae690 37# include "splintMacros.nf"
616915dd 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 */
2a6e9c30 189 ti->basedOn = g_sortFloat;
616915dd 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;
2a6e9c30 239 ti->basedOn = g_sortBool;
1b8ae690 240 ti->export = FALSE; /* this wasn't set (detected by Splint) */
616915dd 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;
2a6e9c30 247 vi->sort = g_sortBool;
616915dd 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 /*
1b8ae690 490 ** bug detected by enum checking
616915dd 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{
abd7f895 1081 size_t len = cstring_length (s);
616915dd 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));
e5081f8c 1368 unsigned long int key;
616915dd 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;
e5081f8c 1386 return (s);
616915dd 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
e5081f8c 1416static unsigned long opFormNode2key (opFormNode op, opFormKind k)
616915dd 1417{
e5081f8c 1418 unsigned long int key;
616915dd 1419
1420 switch (k)
1421 {
1422 case OPF_IF:
1423 /* OPF_IF is the first enum, so it's 0 */
1424
1425 /*@-type@*/
1426 key = MASH (k, k + 1);
1427 /*@=type@*/
1428
1429 break;
1430 case OPF_ANYOP:
1431 case OPF_MANYOP:
1432 case OPF_ANYOPM:
1433 case OPF_MANYOPM:
1434 { /* treat eq and = the same */
1435 lsymbol sym = ltoken_getText (op->content.anyop);
1436
1437 if (sym == equalSymbol)
1438 {
1439 key = MASH (k, eqSymbol);
1440 }
1441 else
1442 {
1443 key = MASH (k, ltoken_getText (op->content.anyop));
1444 }
1445 break;
1446 }
1447 case OPF_MIDDLE:
1448 case OPF_MMIDDLE:
1449 case OPF_MIDDLEM:
1450 case OPF_MMIDDLEM:
1451 case OPF_BMIDDLE:
1452 case OPF_BMMIDDLE:
1453 case OPF_BMIDDLEM:
1454 case OPF_BMMIDDLEM:
1455 key = MASH (k, op->content.middle);
1456 key = MASH (key, ltoken_getRawText (op->tok));
1457 break;
1458 case OPF_SELECT:
1459 case OPF_MAP:
1460 case OPF_MSELECT:
1461 case OPF_MMAP:
1462 key = MASH (k, ltoken_getRawText (op->content.id));
1463 break;
1464 default:
1465 key = 0;
1466 }
1467
1468 return key;
1469}
1470
1471/*@only@*/ opFormNode
1472makeOpFormNode (ltoken t, opFormKind k, opFormUnion u,
1473 ltoken close)
1474{
1475 opFormNode n = (opFormNode) dmalloc (sizeof (*n));
e5081f8c 1476 unsigned long int key = 0;
616915dd 1477
1478 /*
1479 ** Assign a hash key here to speed up lookup of operators.
1480 */
1481
1482 n->tok = t;
1483 n->close = close;
1484 n->kind = k;
616915dd 1485
1486 switch (k)
1487 {
1488 case OPF_IF:
1489 n->content.middle = 0;
1490 /* OPF_IF is the first enum, so it's 0 */
1491 key = MASH /*@+enumint@*/ (k, k + 1) /*@=enumint@*/;
1492 break;
1493 case OPF_ANYOP:
1494 case OPF_MANYOP:
1495 case OPF_ANYOPM:
1496 case OPF_MANYOPM:
1497 { /* treat eq and = the same */
1498 lsymbol sym = ltoken_getText (u.anyop);
1499
1500 if (sym == equalSymbol)
1501 {
1502 key = MASH (k, eqSymbol);
1503 }
1504 else
1505 {
1506 key = MASH (k, ltoken_getText (u.anyop));
1507 }
1508
1509 n->content = u;
1510 break;
1511 }
1512 case OPF_MIDDLE:
1513 case OPF_MMIDDLE:
1514 case OPF_MIDDLEM:
1515 case OPF_MMIDDLEM:
1516 case OPF_BMIDDLE:
1517 case OPF_BMMIDDLE:
1518 case OPF_BMIDDLEM:
1519 case OPF_BMMIDDLEM:
1520 n->content = u;
1521 key = MASH (k, u.middle);
1522 key = MASH (key, ltoken_getRawText (t));
1523 break;
1524 case OPF_SELECT:
1525 case OPF_MAP:
1526 case OPF_MSELECT:
1527 case OPF_MMAP:
1528 key = MASH (k, ltoken_getRawText (u.id));
1529 n->content = u;
1530 break;
1531 default:
1532 {
1533 llbug (message ("makeOpFormNode: unknown opFormKind: %d", (int) k));
1534 }
1535 }
1536 n->key = key;
e5081f8c 1537 return (n);
616915dd 1538}
1539
1540static cstring printMiddle (int j)
1541{
1542 int i;
1543 char *s = mstring_createEmpty ();
1544
1545 for (i = j; i >= 1; i--)
1546 {
1547 s = mstring_concatFree1 (s, "__");
1548
1549 if (i != 1)
1550 {
1551 s = mstring_concatFree1 (s, ", ");
1552 }
1553 }
1554
1555 return cstring_fromCharsO (s);
1556}
1557
1558/*@only@*/ cstring
1559opFormNode_unparse (/*@null@*/ opFormNode n)
1560{
1561 if (n != (opFormNode) 0)
1562 {
1563 switch (n->kind)
1564 {
1565 case OPF_IF:
1566 return (cstring_makeLiteral ("if __ then __ else __ "));
1567 case OPF_ANYOP:
1568 return (cstring_copy (ltoken_getRawString (n->content.anyop)));
1569 case OPF_MANYOP:
1570 return (message ("__ %s", ltoken_getRawString (n->content.anyop)));
1571 case OPF_ANYOPM:
1572 return (message ("%s __ ", ltoken_getRawString (n->content.anyop)));
1573 case OPF_MANYOPM:
1574 return (message ("__ %s __ ", ltoken_getRawString (n->content.anyop)));
1575 case OPF_MIDDLE:
1576 return (message ("%s %q %s",
1577 ltoken_getRawString (n->tok),
1578 printMiddle (n->content.middle),
1579 ltoken_getRawString (n->close)));
1580 case OPF_MMIDDLE:
1581 return (message ("__ %s %q %s",
1582 ltoken_getRawString (n->tok),
1583 printMiddle (n->content.middle),
1584 ltoken_getRawString (n->close)));
1585 case OPF_MIDDLEM:
1586 return (message ("%s %q %s __",
1587 ltoken_getRawString (n->tok),
1588 printMiddle (n->content.middle),
1589 ltoken_getRawString (n->close)));
1590 case OPF_MMIDDLEM:
1591 return (message ("__ %s%q %s __",
1592 ltoken_getRawString (n->tok),
1593 printMiddle (n->content.middle),
1594 ltoken_getRawString (n->close)));
1595 case OPF_BMIDDLE:
1596 return (message ("[%q]", printMiddle (n->content.middle)));
1597 case OPF_BMMIDDLE:
1598 return (message ("__ [%q]", printMiddle (n->content.middle)));
1599 case OPF_BMIDDLEM:
1600 return (message ("[%q] __", printMiddle (n->content.middle)));
1601 case OPF_BMMIDDLEM:
1602 return (message ("__ [%q] __", printMiddle (n->content.middle)));
1603 case OPF_SELECT:
1604 return (message (" \\select %s", ltoken_getRawString (n->content.id)));
1605 case OPF_MAP:
1606 return (message (" \\field_arrow%s", ltoken_getRawString (n->content.id)));
1607 case OPF_MSELECT:
1608 return (message ("__ \\select %s", ltoken_getRawString (n->content.id)));
1609 case OPF_MMAP:
1610 return (message ("__ \\field_arrow %s", ltoken_getRawString (n->content.id)));
1611 default:
1612 llfatalbug (message ("opFormNodeUnparse: unknown kind: %d",
1613 (int) n->kind));
1614 }
1615 }
1616 return cstring_undefined;
1617}
1618
1619/*@only@*/ typeNameNode
1620makeTypeNameNode (bool isObj, lclTypeSpecNode t, abstDeclaratorNode n)
1621{
1622 typeNameNode tn = (typeNameNode) dmalloc (sizeof (*tn));
1623 typeNamePack p = (typeNamePack) dmalloc (sizeof (*p));
1624
1625 tn->isTypeName = TRUE;
1626 p->isObj = isObj;
1627 p->type = t;
1628 p->abst = n;
1629 tn->opform = (opFormNode) 0;
1630 tn->typename = p;
1631 return (tn);
1632}
1633
1634/*@only@*/ typeNameNode
1635makeTypeNameNodeOp (opFormNode n)
1636{
1637 typeNameNode t = (typeNameNode) dmalloc (sizeof (*t));
1638 t->typename = (typeNamePack) 0;
1639 t->opform = n;
1640 t->isTypeName = FALSE;
1641 return (t);
1642}
1643
1644/*@only@*/ cstring
1645typeNameNode_unparse (/*@null@*/ typeNameNode n)
1646{
1647 if (n != (typeNameNode) 0)
1648 {
1649 if (n->isTypeName)
1650 {
1651 cstring st = cstring_undefined;
1652 typeNamePack p = n->typename;
1653
1654 llassert (p != NULL);
1655
1656 if (p->isObj)
1657 st = cstring_makeLiteral ("obj ");
1658
1659 return (message ("%q%q%q", st, lclTypeSpecNode_unparse (p->type),
1660 abstDeclaratorNode_unparse (p->abst)));
1661
1662 }
1663 else
1664 return (opFormNode_unparse (n->opform));
1665 }
1666 return cstring_undefined;
1667}
1668
1669/*@only@*/ lclTypeSpecNode
1670makeLclTypeSpecNodeConj (/*@null@*/ lclTypeSpecNode a, /*@null@*/ lclTypeSpecNode b)
1671{
1672 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1673
1674 n->kind = LTS_CONJ;
f9264521 1675 n->pointers = pointers_undefined;
616915dd 1676 n->quals = qualList_new ();
1677 n->content.conj = (lclconj) dmalloc (sizeof (*n->content.conj));
1678 n->content.conj->a = a;
1679 n->content.conj->b = b;
1680
1681 return (n);
1682}
1683
1684/*@only@*/ lclTypeSpecNode
1685makeLclTypeSpecNodeType (/*@null@*/ CTypesNode x)
1686{
1687 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1688
1689 n->kind = LTS_TYPE;
f9264521 1690 n->pointers = pointers_undefined;
616915dd 1691 n->content.type = x;
1692 n->quals = qualList_new ();
1693 return (n);
1694}
1695
1696/*@only@*/ lclTypeSpecNode
1697makeLclTypeSpecNodeSU (/*@null@*/ strOrUnionNode x)
1698{
1699 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1700
1701 n->kind = LTS_STRUCTUNION;
f9264521 1702 n->pointers = pointers_undefined;
616915dd 1703 n->content.structorunion = x;
1704 n->quals = qualList_new ();
1705 return (n);
1706}
1707
1708/*@only@*/ lclTypeSpecNode
1709makeLclTypeSpecNodeEnum (/*@null@*/ enumSpecNode x)
1710{
1711 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1712
1713 n->quals = qualList_new ();
1714 n->kind = LTS_ENUM;
f9264521 1715 n->pointers = pointers_undefined;
616915dd 1716 n->content.enumspec = x;
1717 return (n);
1718}
1719
1720lclTypeSpecNode
1721lclTypeSpecNode_addQual (lclTypeSpecNode n, qual q)
1722{
1723 llassert (lclTypeSpecNode_isDefined (n));
1724 n->quals = qualList_add (n->quals, q);
1725 return n;
1726}
1727
1728/*@only@*/ cstring
1729lclTypeSpecNode_unparse (/*@null@*/ lclTypeSpecNode n)
1730{
1731 if (n != (lclTypeSpecNode) 0)
1732 {
1733 switch (n->kind)
1734 {
1735 case LTS_TYPE:
1736 llassert (n->content.type != NULL);
1737 return (printLeaves (n->content.type->ctypes));
1738 case LTS_STRUCTUNION:
1739 return (strOrUnionNode_unparse (n->content.structorunion));
1740 case LTS_ENUM:
1741 return (enumSpecNode_unparse (n->content.enumspec));
1742 case LTS_CONJ:
1743 return (lclTypeSpecNode_unparse (n->content.conj->a));
1744 default:
1745 llfatalbug (message ("lclTypeSpecNode_unparse: unknown lclTypeSpec kind: %d",
1746 (int) n->kind));
1747 }
1748 }
1749 return cstring_undefined;
1750}
1751
1752/*@only@*/ enumSpecNode
1753makeEnumSpecNode (ltoken t, ltoken optTagId,
1754 /*@owned@*/ ltokenList enums)
1755{
1756 enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n));
1757 tagInfo ti;
1758 smemberInfo *top = smemberInfo_undefined;
1759
1760 n->tok = t;
1761 n->opttagid = ltoken_copy (optTagId);
1762 n->enums = enums;
1763
1764 /* generate sort for this LCL type */
1765 n->sort = sort_makeEnum (optTagId);
1766
1767 if (!ltoken_isUndefined (optTagId))
1768 {
1769 /* First, check to see if tag is already defined */
1770 ti = symtable_tagInfo (g_symtab, ltoken_getText (optTagId));
1771
1772 if (tagInfo_exists (ti))
1773 {
1774 if (ti->kind == TAG_ENUM)
1775 {
1776 /* 23 Sep 1995 --- had been noting here...is this right? */
1777
1778 ti->content.enums = enums;
1779 ti->sort = n->sort;
1780 ti->imported = context_inImport ();
1781 }
1782 else
1783 {
1784 lclerror (optTagId,
1785 message ("Tag %s previously defined as %q, redefined as enum",
1786 ltoken_getRawString (optTagId),
1787 tagKind_unparse (ti->kind)));
1788
1789 /* evs --- shouldn't they be in different name spaces? */
1790 }
1791
1792 ltoken_free (optTagId);
1793 }
1794 else
1795 {
1796 ti = (tagInfo) dmalloc (sizeof (*ti));
1797
1798 ti->kind = TAG_ENUM;
1799 ti->id = optTagId;
1800 ti->content.enums = enums;
1801 ti->sort = n->sort;
1802 ti->imported = context_inImport ();
1803 /* First, store tag info in symbol table */
1804 (void) symtable_enterTag (g_symtab, ti);
1805 }
1806 }
1807
1808 /* check that enumeration constants are unique */
1809
1810 ltokenList_reset (enums);
1811
1812 while (!ltokenList_isFinished (enums))
1813 {
1814 ltoken c = ltokenList_current (enums);
1815 smemberInfo *ei = (smemberInfo *) dmalloc (sizeof (*ei));
1816
1817 ei->name = ltoken_getText (c);
1818 ei->next = top;
1819 ei->sort = n->sort;
1820 top = ei;
1821
1822 if (!varInfo_exists (symtable_varInfo (g_symtab, ltoken_getText (c))))
1823 { /* put info into symbol table */
1824 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
1825
1826 vi->id = ltoken_copy (c);
1827 vi->kind = VRK_ENUM;
1828 vi->sort = n->sort;
1829 vi->export = TRUE;
1830
1831 (void) symtable_enterVar (g_symtab, vi);
1832 varInfo_free (vi);
1833 }
1834 else
1835 {
1836 lclerror (c, message ("Enumerated value redeclared: %s",
1837 ltoken_getRawString (c)));
1838 ltokenList_removeCurrent (enums);
1839 }
1840 ltokenList_advance (enums);
1841 /*@-branchstate@*/
1842 }
1843 /*@=branchstate@*/
1844
1845 (void) sort_updateEnum (n->sort, top);
1846 return (n);
1847}
1848
1849/*@only@*/ enumSpecNode
1850makeEnumSpecNode2 (ltoken t, ltoken tagid)
1851{
1852 /* a reference, not a definition */
1853 enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n));
1854 tagInfo ti = symtable_tagInfo (g_symtab, ltoken_getText (tagid));
1855
1856 n->tok = t;
1857 n->opttagid = tagid;
1858 n->enums = ltokenList_new ();
1859
1860 if (tagInfo_exists (ti))
1861 {
1862 if (ti->kind == TAG_ENUM)
1863 {
1864 n->sort = ti->sort;
1865 }
1866 else
1867 {
1868 n->sort = sort_makeNoSort ();
1869 lclerror (tagid, message ("Tag %s defined as %q, used as enum",
1870 ltoken_getRawString (tagid),
1871 tagKind_unparse (ti->kind)));
1872 }
1873 }
1874 else
1875 {
1876 n->sort = sort_makeNoSort ();
1877 lclerror (t, message ("Undefined type: enum %s",
1878 ltoken_getRawString (tagid)));
1879 }
1880
1881 return (n);
1882}
1883
1884/*@only@*/ cstring
1885enumSpecNode_unparse (/*@null@*/ enumSpecNode n)
1886{
1887 if (n != (enumSpecNode) 0)
1888 {
1889 cstring s = cstring_makeLiteral ("enum ");
1890
1891 if (!ltoken_isUndefined (n->opttagid))
1892 {
1893 s = message ("%q%s ", s, ltoken_getRawString (n->opttagid));
1894 }
1895
1896 s = message ("%q{%q}", s, printLeaves2 (n->enums));
1897 return s;
1898 }
1899 return cstring_undefined;
1900}
1901
1902/*@only@*/ strOrUnionNode
1903makestrOrUnionNode (ltoken str, suKind k, ltoken opttagid,
1904 /*@only@*/ stDeclNodeList x)
1905{
1906 strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n));
1907 lsymbolSet set = lsymbolSet_new ();
1908 declaratorNodeList declarators;
1909 sort fieldsort, tsort1, tsort2;
1910 smemberInfo *mi, *top = smemberInfo_undefined;
1911 bool doTag = FALSE;
1912 bool isStruct = (k == SU_STRUCT);
1913 tagInfo t;
1914
1915
1916 n->kind = k;
1917 n->tok = str;
1918 n->opttagid = ltoken_copy (opttagid);
1919 n->structdecls = x;
1920 n->sort = isStruct ? sort_makeStr (opttagid) : sort_makeUnion (opttagid);
1921
1922 if (!ltoken_isUndefined (opttagid))
1923 {
1924 /* First, check to see if tag is already defined */
1925 t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid));
1926
1927 if (tagInfo_exists (t))
1928 {
1929 if ((t->kind == TAG_FWDUNION && k == SU_UNION) ||
1930 (t->kind == TAG_FWDSTRUCT && k == SU_STRUCT))
1931 {
1932 /* to allow self-recursive types and forward tag declarations */
1933 t->content.decls = stDeclNodeList_copy (x); /* update tag info */
1934 t->sort = n->sort;
1935 }
1936 else
1937 {
1938 lclerror (opttagid,
1939 message ("Tag %s previously defined as %q, used as %q",
1940 ltoken_getRawString (opttagid),
1941 tagKind_unparse (t->kind),
1942 cstring_makeLiteral (isStruct ? "struct" : "union")));
1943 }
1944 }
1945 else
1946 {
1947 doTag = TRUE;
1948 }
1949 }
1950 else
1951 {
1952 doTag = TRUE;
1953 }
1954
1955 if (doTag && !ltoken_isUndefined (opttagid))
1956 {
1957 t = (tagInfo) dmalloc (sizeof (*t));
1958
1959 /* can either override prev defn or use prev defn */
1960 /* override it so as to detect more errors */
1961
1962 t->kind = (k == SU_STRUCT) ? TAG_STRUCT : TAG_UNION;
1963 t->id = opttagid;
1964 t->content.decls = stDeclNodeList_copy (x);
1965 t->sort = n->sort;
1966 t->imported = FALSE;
1967
1968 /* Next, update tag info in symbol table */
1969 (void) symtable_enterTagForce (g_symtab, t);
1970 }
1971
1972 /* check no duplicate field names */
1973
1974 stDeclNodeList_elements (x, i)
1975 {
1976 fieldsort = lclTypeSpecNode2sort (i->lcltypespec);
1977
1978 /* need the locations, not values */
1979 /* fieldsort = sort_makeObj (fieldsort); */
1980 /* 2/19/93, was
1981 fieldsort = sort_makeGlobal (fieldsort); */
1982
1983 declarators = i->declarators;
1984
1985 declaratorNodeList_elements (declarators, decl)
1986 {
1987 lsymbol fieldname;
1988 mi = (smemberInfo *) dmalloc (sizeof (*mi));
1989 /* need to make dynamic copies */
1990 fieldname = ltoken_getText (decl->id);
1991
1992 /* 2/19/93, added */
1993 tsort1 = typeExpr2ptrSort (fieldsort, decl->type);
1994 tsort2 = sort_makeGlobal (tsort1);
1995
1996 mi->name = fieldname;
1997 mi->sort = tsort2; /* fieldsort; */
1998 mi->next = top;
1999 top = mi;
2000
2001 if (lsymbolSet_member (set, fieldname))
2002 {
2003 lclerror (decl->id,
2004 message ("Field name reused: %s",
2005 ltoken_getRawString (decl->id)));
2006 }
2007 else
2008 {
2009 (void) lsymbolSet_insert (set, fieldname);
2010 }
2011 /*@-branchstate@*/
2012 } end_declaratorNodeList_elements;
2013 /*@=branchstate@*/
2014 } end_stDeclNodeList_elements;
2015
2016 if (k == SU_STRUCT)
2017 {
2018 (void) sort_updateStr (n->sort, top);
2019 }
2020 else
2021 {
2022 (void) sort_updateUnion (n->sort, top);
2023 }
2024
2025 /* We shall keep the info with both tags and types if any
2026 of them are present. */
2027
2028 lsymbolSet_free (set);
2029
2030 return (n);
2031}
2032
2033/*@only@*/ strOrUnionNode
2034makeForwardstrOrUnionNode (ltoken str, suKind k,
2035 ltoken tagid)
2036{
2037 strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n));
2038 sort sort = sort_makeNoSort ();
2039 tagInfo t;
2040
2041 /* a reference, not a definition */
2042
2043 n->kind = k;
2044 n->tok = str;
2045 n->opttagid = tagid;
2046 n->structdecls = stDeclNodeList_new ();
2047
2048 /* get sort for this LCL type */
2049 t = symtable_tagInfo (g_symtab, ltoken_getText (tagid));
2050
2051 if (tagInfo_exists (t))
2052 {
2053 sort = t->sort;
2054
2055 if (!(((t->kind == TAG_STRUCT || t->kind == TAG_FWDSTRUCT) && k == SU_STRUCT)
2056 || ((t->kind == TAG_UNION || t->kind == TAG_FWDUNION) && k == SU_UNION)))
2057 {
2058 lclerror (tagid,
2059 message ("Tag %s previously defined as %q, used as %q",
2060 ltoken_getRawString (tagid),
2061 tagKind_unparse (t->kind),
2062 cstring_makeLiteral ((k == SU_STRUCT) ? "struct" : "union")));
2063 }
2064 }
2065 else
2066 {
2067 /*
2068 ** changed from error: 31 Mar 1994
2069 **
2070 ** lclerror (str, message ("Undefined type: %s %s", s, ltoken_getRawString (tagid));
2071 **
2072 */
2073
2074 /* forward struct's and union's are ok... */
2075
2076 if (k == SU_STRUCT)
2077 {
2078 (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy (tagid));
2079 lhForwardStruct (tagid);
2080 sort = sort_makeStr (tagid);
2081 }
2082 else
2083 {
2084 (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy (tagid));
2085 lhForwardUnion (tagid);
2086 sort = sort_makeUnion (tagid);
2087 }
2088 }
2089
2090 n->sort = sort;
2091 return (n);
2092}
2093
2094/*@only@*/ cstring
2095strOrUnionNode_unparse (/*@null@*/ strOrUnionNode n)
2096{
2097 if (n != (strOrUnionNode) 0)
2098 {
2099 cstring s;
2100 switch (n->kind)
2101 {
2102 case SU_STRUCT:
2103 s = cstring_makeLiteral ("struct ");
2104 break;
2105 case SU_UNION:
2106 s = cstring_makeLiteral ("union ");
2107 break;
2108 BADDEFAULT
2109 }
2110
2111 if (!ltoken_isUndefined (n->opttagid))
2112 {
2113 s = message ("%q%s ", s, ltoken_getRawString (n->opttagid));
2114 }
2115 s = message ("%q{%q}", s, stDeclNodeList_unparse (n->structdecls));
2116 return s;
2117 }
2118 return cstring_undefined;
2119}
2120
2121/*@only@*/ stDeclNode
2122makestDeclNode (lclTypeSpecNode s,
2123 declaratorNodeList x)
2124{
2125 stDeclNode n = (stDeclNode) dmalloc (sizeof (*n));
2126
2127 n->lcltypespec = s;
2128 n->declarators = x;
2129 return n;
2130}
2131
2132/*@only@*/ typeExpr
2133makeFunctionNode (typeExpr x, paramNodeList p)
2134{
2135 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2136
2137 y->wrapped = 0;
2138 y->kind = TEXPR_FCN;
2139 y->content.function.returntype = x;
2140 y->content.function.args = p;
2141 y->sort = sort_makeNoSort ();
2142
2143 return (y);
2144}
2145
2146static /*@observer@*/ ltoken
2147 extractDeclarator (/*@null@*/ typeExpr t)
2148{
2149 if (t != (typeExpr) 0)
2150 {
2151 switch (t->kind)
2152 {
2153 case TEXPR_BASE:
2154 return t->content.base;
2155 case TEXPR_PTR:
2156 return (extractDeclarator (t->content.pointer));
2157 case TEXPR_ARRAY:
2158 return (extractDeclarator (t->content.array.elementtype));
2159 case TEXPR_FCN:
2160 return (extractDeclarator (t->content.function.returntype));
2161 }
2162 }
2163
2164 return ltoken_undefined;
2165}
2166
2167/*@only@*/ typeExpr
2168makeTypeExpr (ltoken t)
2169{
2170 typeExpr x = (typeExpr) dmalloc (sizeof (*x));
2171
2172
2173 x->wrapped = 0;
2174 x->kind = TEXPR_BASE;
2175 x->content.base = t;
2176 x->sort = sort_makeNoSort ();
2177
2178 return (x);
2179}
2180
2181
2182/*@only@*/ declaratorNode
2183makeDeclaratorNode (typeExpr t)
2184{
2185 declaratorNode x = (declaratorNode) dmalloc (sizeof (*x));
2186
2187 x->id = ltoken_copy (extractDeclarator (t));
2188 x->type = t;
2189 x->isRedecl = FALSE;
2190
2191 return (x);
2192}
2193
2194static /*@only@*/ declaratorNode
2195makeUnknownDeclaratorNode (/*@only@*/ ltoken t)
2196{
2197 declaratorNode x = (declaratorNode) dmalloc (sizeof (*x));
2198
2199 x->id = t;
2200 x->type = (typeExpr) 0;
2201 x->isRedecl = FALSE;
2202
2203 return (x);
2204}
2205
2206static /*@only@*/ cstring
2207printTypeExpr2 (/*@null@*/ typeExpr x)
2208{
2209 paramNodeList params;
2210
2211 if (x != (typeExpr) 0)
2212 {
2213 cstring s; /* print out types in reverse order */
2214
2215 switch (x->kind)
2216 {
2217 case TEXPR_BASE:
2218 return (message ("%s ", ltoken_getRawString (x->content.base)));
2219 case TEXPR_PTR:
2220 return (message ("%qptr to ", printTypeExpr2 (x->content.pointer)));
2221 case TEXPR_ARRAY:
2222 return (message ("array[%q] of %q",
2223 termNode_unparse (x->content.array.size),
2224 printTypeExpr2 (x->content.array.elementtype)));
2225 case TEXPR_FCN:
2226 s = printTypeExpr2 (x->content.function.returntype);
2227 params = x->content.function.args;
2228 if (!paramNodeList_empty (params))
2229 {
2230 s = message ("%qfcn with args: (%q)", s,
2231 paramNodeList_unparse (x->content.function.args));
2232 }
2233 else
2234 s = message ("%qfcn with no args", s);
2235 return s;
2236 default:
2237 llfatalbug (message ("printTypeExpr2: unknown typeExprKind: %d", (int) x->kind));
2238 }
2239 }
2240 return cstring_undefined;
2241}
2242
2243/*@only@*/ cstring
2244declaratorNode_unparse (declaratorNode x)
2245{
2246 return (typeExpr_unparse (x->type));
2247}
2248
2249/*@only@*/ declaratorNode
2250 declaratorNode_copy (declaratorNode x)
2251{
2252 declaratorNode ret = (declaratorNode) dmalloc (sizeof (*ret));
2253
2254 ret->type = typeExpr_copy (x->type);
2255 ret->id = ltoken_copy (x->id);
2256 ret->isRedecl = x->isRedecl;
2257
2258 return (ret);
2259}
2260
2261static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr x)
2262{
2263 if (x == NULL)
2264 {
2265 return NULL;
2266 }
2267 else
2268 {
2269 typeExpr ret = (typeExpr) dmalloc (sizeof (*ret));
2270
2271 ret->wrapped = x->wrapped;
2272 ret->kind = x->kind;
2273
2274 switch (ret->kind)
2275 {
2276 case TEXPR_BASE:
2277 ret->content.base = ltoken_copy (x->content.base);
2278 break;
2279 case TEXPR_PTR:
2280 ret->content.pointer = typeExpr_copy (x->content.pointer);
2281 break;
2282 case TEXPR_ARRAY:
2283 ret->content.array.elementtype = typeExpr_copy (x->content.array.elementtype);
2284 ret->content.array.size = termNode_copy (x->content.array.size);
2285 break;
2286 case TEXPR_FCN:
2287 ret->content.function.returntype = typeExpr_copy (x->content.function.returntype);
2288 ret->content.function.args = paramNodeList_copy (x->content.function.args);
2289 break;
2290 }
2291
2292 ret->sort = x->sort;
2293 return ret;
2294 }
2295}
2296
2297static /*@only@*/ cstring
2298 typeExpr_unparseCode (/*@null@*/ typeExpr x)
2299{
2300 /* print out types in order of appearance in source */
2301 cstring s = cstring_undefined;
2302
2303 if (x != (typeExpr) 0)
2304 {
2305 switch (x->kind)
2306 {
2307 case TEXPR_BASE:
2308 return (cstring_copy (ltoken_getRawString (x->content.base)));
2309 case TEXPR_PTR:
2310 return (typeExpr_unparseCode (x->content.pointer));
2311 case TEXPR_ARRAY:
2312 return (typeExpr_unparseCode (x->content.array.elementtype));
2313 case TEXPR_FCN:
2314 return (typeExpr_unparseCode (x->content.function.returntype));
2315 }
2316 }
2317 return s;
2318}
2319
2320void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr x)
2321{
2322 if (x != (typeExpr) 0)
2323 {
2324 switch (x->kind)
2325 {
2326 case TEXPR_BASE:
2327 break;
2328 case TEXPR_PTR:
2329 typeExpr_free (x->content.pointer);
2330 break;
2331 case TEXPR_ARRAY:
2332 typeExpr_free (x->content.array.elementtype);
2333 termNode_free (x->content.array.size);
2334 break;
2335 case TEXPR_FCN:
2336 typeExpr_free (x->content.function.returntype);
2337 paramNodeList_free (x->content.function.args);
2338 break;
2339 /*@-branchstate@*/
2340 }
2341 /*@=branchstate@*/
2342
2343 sfree (x);
2344 }
2345}
2346
2347
2348/*@only@*/ cstring
2349declaratorNode_unparseCode (declaratorNode x)
2350{
2351 return (typeExpr_unparseCode (x->type));
2352}
2353
2354/*@only@*/ cstring
2355typeExpr_unparse (/*@null@*/ typeExpr x)
2356{
2357 cstring s = cstring_undefined; /* print out types in order of appearance in source */
2358 paramNodeList params;
2359 int i;
2360
2361 if (x != (typeExpr) 0)
2362 {
2363 cstring front = cstring_undefined;
2364 cstring back = cstring_undefined;
2365
2366 llassert (x->wrapped < 100);
2367
2368 for (i = x->wrapped; i >= 1; i--)
2369 {
2370 front = cstring_appendChar (front, '(');
2371 back = cstring_appendChar (back, ')');
2372 }
2373
2374 switch (x->kind)
2375 {
2376 case TEXPR_BASE:
2377 s = message ("%q%s", s, ltoken_getRawString (x->content.base));
2378 break;
2379 case TEXPR_PTR:
2380 s = message ("%q*%q", s, typeExpr_unparse (x->content.pointer));
2381 break;
2382 case TEXPR_ARRAY:
2383 s = message ("%q%q[%q]", s,
2384 typeExpr_unparse (x->content.array.elementtype),
2385 termNode_unparse (x->content.array.size));
2386 break;
2387 case TEXPR_FCN:
2388 s = message ("%q%q (", s,
2389 typeExpr_unparse (x->content.function.returntype));
2390 params = x->content.function.args;
2391
2392 if (!paramNodeList_empty (params))
2393 {
2394 s = message ("%q%q", s,
2395 paramNodeList_unparse (x->content.function.args));
2396 }
2397
2398 s = message ("%q)", s);
2399 break;
2400 }
2401 s = message ("%q%q%q", front, s, back);
2402 }
2403 else
2404 {
2405 s = cstring_makeLiteral ("?");
2406 }
2407
2408 return s;
2409}
2410
2411/*@only@*/ cstring
2412typeExpr_unparseNoBase (/*@null@*/ typeExpr x)
2413{
2414 cstring s = cstring_undefined; /* print out types in order of appearance in source */
2415 paramNodeList params;
2416 int i;
2417
2418 if (x != (typeExpr) 0)
2419 {
2420 cstring front = cstring_undefined;
2421 cstring back = cstring_undefined;
2422
2423 llassert (x->wrapped < 100);
2424
2425 for (i = x->wrapped; i >= 1; i--)
2426 {
2427 front = cstring_appendChar (front, '(');
2428 back = cstring_appendChar (back, ')');
2429 }
2430
2431 switch (x->kind)
2432 {
2433 case TEXPR_BASE:
2434 s = message ("%q /* %s */", s, ltoken_getRawString (x->content.base));
2435 break;
2436 case TEXPR_PTR:
2437 s = message ("%q*%q", s, typeExpr_unparseNoBase (x->content.pointer));
2438 break;
2439 case TEXPR_ARRAY:
2440 s = message ("%q%q[%q]", s,
2441 typeExpr_unparseNoBase (x->content.array.elementtype),
2442 termNode_unparse (x->content.array.size));
2443 break;
2444 case TEXPR_FCN:
2445 s = message ("%q%q (", s,
2446 typeExpr_unparseNoBase (x->content.function.returntype));
2447 params = x->content.function.args;
2448
2449 if (!paramNodeList_empty (params))
2450 {
2451 s = message ("%q%q", s,
2452 paramNodeList_unparse (x->content.function.args));
2453 }
2454
2455 s = message ("%q)", s);
2456 break;
2457 }
2458 s = message ("%q%q%q", front, s, back);
2459 }
2460 else
2461 {
2462 s = cstring_makeLiteral ("?");
2463 }
2464
2465 return s;
2466}
2467
2468cstring
2469typeExpr_name (/*@null@*/ typeExpr x)
2470{
2471 if (x != (typeExpr) 0)
2472 {
2473 switch (x->kind)
2474 {
2475 case TEXPR_BASE:
2476 return (cstring_copy (ltoken_getRawString (x->content.base)));
2477 case TEXPR_PTR:
2478 return (typeExpr_name (x->content.pointer));
2479 case TEXPR_ARRAY:
2480 return (typeExpr_name (x->content.array.elementtype));
2481 case TEXPR_FCN:
2482 return (typeExpr_name (x->content.function.returntype));
2483 }
2484 }
2485
2486 /* evs --- 14 Mar 1995
2487 ** not a bug: its okay to have empty parameter names
2488 ** llbug ("typeExpr_name: null");
2489 */
2490
2491 return cstring_undefined;
2492}
2493
2494/*@only@*/ typeExpr
2495 makePointerNode (ltoken star, /*@only@*/ /*@returned@*/ typeExpr x)
2496{
2497 if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0)))
2498 {
2499 x->content.function.returntype = makePointerNode (star, x->content.function.returntype);
2500 return x;
2501 }
2502 else
2503 {
2504 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2505
2506 y->wrapped = 0;
2507 y->kind = TEXPR_PTR;
2508 y->content.pointer = x;
2509 y->sort = sort_makeNoSort ();
2510 ltoken_free (star);
2511
2512 return y;
2513 }
2514}
2515
2516typeExpr makeArrayNode (/*@returned@*/ typeExpr x,
2517 /*@only@*/ arrayQualNode a)
2518{
2519 if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0)))
2520 {
2521 /*
2522 ** Spurious errors reported here, because of referencing
2523 ** in makeArrayNode.
2524 */
2525
2526 /*@i3@*/ x->content.function.returntype = makeArrayNode (x, a);
2527 /*@i1@*/ return x;
2528 }
2529 else
2530 {
2531 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2532 y->wrapped = 0;
2533 y->kind = TEXPR_ARRAY;
2534
2535 if (a == (arrayQualNode) 0)
2536 {
2537 y->content.array.size = (termNode) 0;
2538 }
2539 else
2540 {
2541 y->content.array.size = a->term;
2542 ltoken_free (a->tok);
2543 sfree (a);
2544 }
2545
2546 y->content.array.elementtype = x;
2547 y->sort = sort_makeNoSort ();
2548
2549 return (y);
2550 }
2551}
2552
2553/*@only@*/ constDeclarationNode
2554makeConstDeclarationNode (lclTypeSpecNode t, initDeclNodeList decls)
2555{
2556 constDeclarationNode n = (constDeclarationNode) dmalloc (sizeof (*n));
2557 sort s, s2, initValueSort;
2558 ltoken varid, errtok;
2559 termNode initValue;
2560
2561 s = lclTypeSpecNode2sort (t);
2562
2563 initDeclNodeList_elements (decls, init)
2564 {
2565 declaratorNode vdnode = init->declarator;
2566 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
2567
2568 varid = ltoken_copy (vdnode->id);
2569 s2 = typeExpr2ptrSort (s, vdnode->type);
2570 initValue = init->value;
2571
2572 if (termNode_isDefined (initValue) && !initValue->error_reported)
2573 {
2574 initValueSort = initValue->sort;
2575
2576 /* should keep the arguments in order */
2577 if (!sort_member_modulo_cstring (s2, initValue)
2578 && !initValue->error_reported)
2579 {
2580 errtok = termNode_errorToken (initValue);
2581
2582 lclerror
2583 (errtok,
2584 message ("Constant %s declared type %q, initialized to %q: %q",
2585 ltoken_unparse (varid),
2586 sort_unparse (s2),
2587 sort_unparse (initValueSort),
2588 termNode_unparse (initValue)));
2589 }
2590 }
2591
2592 vi->id = varid;
2593 vi->kind = VRK_CONST;
2594 vi->sort = s2;
2595 vi->export = TRUE;
2596
2597 (void) symtable_enterVar (g_symtab, vi);
2598 varInfo_free (vi);
2599
2600 } end_initDeclNodeList_elements;
2601
2602 n->type = t;
2603 n->decls = decls;
2604
2605 return n;
2606}
2607
2608varDeclarationNode makeInternalStateNode (void)
2609{
2610 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2611
2612 n->isSpecial = TRUE;
2613 n->sref = sRef_makeInternalState ();
2614
2615 /*@-compdef@*/ return n; /*@=compdef@*/
2616}
2617
2618varDeclarationNode makeFileSystemNode (void)
2619{
2620 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2621
2622 n->isSpecial = TRUE;
2623 n->sref = sRef_makeSystemState ();
2624
2625 /*@-compdef@*/ return n; /*@=compdef@*/
2626}
2627
2628/*@only@*/ varDeclarationNode
2629makeVarDeclarationNode (lclTypeSpecNode t, initDeclNodeList x,
2630 bool isGlobal, bool isPrivate)
2631{
2632 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2633 sort s, s2, initValueSort;
2634 ltoken varid, errtok;
2635 termNode initValue;
2636 declaratorNode vdnode;
2637
2638 n->isSpecial = FALSE;
2639 n->qualifier = QLF_NONE;
2640 n->isGlobal = isGlobal;
2641 n->isPrivate = isPrivate;
2642 n->decls = x;
2643
2644 s = lclTypeSpecNode2sort (t);
2645
2646 /* t is an lclTypeSpec, its sort may not be assigned yet */
2647
2648 initDeclNodeList_elements (x, init)
2649 {
2650 vdnode = init->declarator;
2651 varid = vdnode->id;
2652 s2 = typeExpr2ptrSort (s, vdnode->type);
2653 initValue = init->value;
2654
2655 if (termNode_isDefined (initValue) && !initValue->error_reported)
2656 {
2657 initValueSort = initValue->sort;
2658 /* should keep the arguments in order */
2659 if (!sort_member_modulo_cstring (s2, initValue)
2660 && !initValue->error_reported)
2661 {
2662 errtok = termNode_errorToken (initValue);
2663
2664 lclerror (errtok,
2665 message ("Variable %s declared type %q, initialized to %q",
2666 ltoken_unparse (varid),
2667 sort_unparse (s2),
2668 sort_unparse (initValueSort)));
2669 }
2670 }
2671
2672 /*
2673 ** If global, check that it has been declared already, don't push
2674 ** onto symbol table yet (wrong scope, done in enteringFcnScope
2675 */
2676
2677 if (isGlobal)
2678 {
2679 varInfo vi = symtable_varInfo (g_symtab, ltoken_getText (varid));
2680
2681 if (!varInfo_exists (vi))
2682 {
2683 lclerror (varid,
2684 message ("Undeclared global variable: %s",
2685 ltoken_getRawString (varid)));
2686 }
2687 else
2688 {
2689 if (vi->kind == VRK_CONST)
2690 {
2691 lclerror (varid,
2692 message ("Constant used in global list: %s",
2693 ltoken_getRawString (varid)));
2694 }
2695 }
2696 }
2697 else
2698 {
2699 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
2700
2701 vi->id = ltoken_copy (varid);
2702 if (isPrivate)
2703 {
2704 vi->kind = VRK_PRIVATE;
2705 /* check that initValue is not empty */
2706 if (initValue == (termNode) 0)
2707 {
2708 lclerror (varid,
2709 message ("Private variable must have initialization: %s",
2710 ltoken_getRawString (varid)));
2711 }
2712 }
2713 else
2714 {
2715 vi->kind = VRK_VAR;
2716 }
2717
2718 vi->sort = sort_makeGlobal (s2);
2719 vi->export = TRUE;
2720
2721 vdnode->isRedecl = symtable_enterVar (g_symtab, vi);
2722 varInfo_free (vi);
2723 }
2724 } end_initDeclNodeList_elements;
2725
2726 n->type = t;
2727
2728 return n;
2729}
2730
2731/*@only@*/ initDeclNode
2732makeInitDeclNode (declaratorNode d, termNode x)
2733{
2734 initDeclNode n = (initDeclNode) dmalloc (sizeof (*n));
2735
2736 n->declarator = d;
2737 n->value = x;
2738 return n;
2739}
2740
2741/*@only@*/ abstractNode
2742makeAbstractNode (ltoken t, ltoken name,
2743 bool isMutable, bool isRefCounted, abstBodyNode a)
2744{
2745 abstractNode n = (abstractNode) dmalloc (sizeof (*n));
2746 sort handle;
2747 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
2748
2749 n->tok = t;
2750 n->isMutable = isMutable;
2751 n->name = name;
2752 n->body = a;
2753 n->isRefCounted = isRefCounted;
2754
2755 if (isMutable)
2756 handle = sort_makeMutable (name, ltoken_getText (name));
2757 else
2758 handle = sort_makeImmutable (name, ltoken_getText (name));
2759 n->sort = handle;
2760
2761 ti->id = ltoken_createType (ltoken_getCode (ltoken_typename), SID_TYPE,
2762 ltoken_getText (name));
2763 ti->modifiable = isMutable;
2764 ti->abstract = TRUE;
2765 ti->basedOn = handle;
2766 ti->export = TRUE;
2767
2768 symtable_enterType (g_symtab, ti);
2769
2770
2771 return n;
2772}
2773
2774/*@only@*/ cstring
2775abstractNode_unparse (abstractNode n)
2776{
2777 if (n != (abstractNode) 0)
2778 {
2779 cstring s;
2780
2781 if (n->isMutable)
2782 s = cstring_makeLiteral ("mutable");
2783 else
2784 s = cstring_makeLiteral ("immutable");
2785
2786 return (message ("%q type %s%q;", s, ltoken_getRawString (n->name),
2787 abstBodyNode_unparse (n->body)));
2788 }
2789 return cstring_undefined;
2790}
2791
2792void
2793setExposedType (lclTypeSpecNode s)
2794{
2795 exposedType = s;
2796}
2797
2798/*@only@*/ exposedNode
2799makeExposedNode (ltoken t, lclTypeSpecNode s,
2800 declaratorInvNodeList d)
2801{
2802 exposedNode n = (exposedNode) dmalloc (sizeof (*n));
2803
2804 n->tok = t;
2805 n->type = s;
2806 n->decls = d;
2807
2808 return n;
2809}
2810
2811/*@only@*/ cstring
2812exposedNode_unparse (exposedNode n)
2813{
2814 if (n != (exposedNode) 0)
2815 {
2816 return (message ("typedef %q %q;",
2817 lclTypeSpecNode_unparse (n->type),
2818 declaratorInvNodeList_unparse (n->decls)));
2819 }
2820 return cstring_undefined;
2821}
2822
2823/*@only@*/ declaratorInvNode
2824makeDeclaratorInvNode (declaratorNode d, abstBodyNode b)
2825{
2826 declaratorInvNode n = (declaratorInvNode) dmalloc (sizeof (*n));
2827 n->declarator = d;
2828 n->body = b;
2829
2830 return (n);
2831}
2832
2833/*@only@*/ cstring
2834declaratorInvNode_unparse (declaratorInvNode d)
2835{
2836 return (message ("%q%q", declaratorNode_unparse (d->declarator),
2837 abstBodyNode_unparseExposed (d->body)));
2838}
2839
2840/*@only@*/ cstring
2841abstBodyNode_unparse (abstBodyNode n)
2842{
2843 if (n != (abstBodyNode) 0)
2844 {
2845 return (lclPredicateNode_unparse (n->typeinv));
2846 }
2847 return cstring_undefined;
2848}
2849
2850/*@only@*/ cstring
2851abstBodyNode_unparseExposed (abstBodyNode n)
2852{
2853 if (n != (abstBodyNode) 0)
2854 {
2855 return (message ("%q", lclPredicateNode_unparse (n->typeinv)));
2856 }
2857 return cstring_undefined;
2858}
2859
2860/*@only@*/ cstring
2861taggedUnionNode_unparse (taggedUnionNode n)
2862{
2863 if (n != (taggedUnionNode) 0)
2864 {
2865 return (message ("tagged union {%q}%q;\n",
2866 stDeclNodeList_unparse (n->structdecls),
2867 declaratorNode_unparse (n->declarator)));
2868 }
2869 return cstring_undefined;
2870}
2871
2872static /*@observer@*/ paramNodeList
2873 typeExpr_toParamNodeList (/*@null@*/ typeExpr te)
2874{
2875 if (te != (typeExpr) 0)
2876 {
2877 switch (te->kind)
2878 {
2879 case TEXPR_FCN:
2880 return te->content.function.args;
2881 case TEXPR_PTR:
2882 return typeExpr_toParamNodeList (te->content.pointer);
2883 case TEXPR_ARRAY:
2884 /* return typeExpr_toParamNodeList (te->content.array.elementtype); */
2885 case TEXPR_BASE:
2886 return paramNodeList_undefined;
2887 }
2888 }
2889 return paramNodeList_undefined;
2890}
2891
2892/*@only@*/ fcnNode
2893 fcnNode_fromDeclarator (/*@only@*/ /*@null@*/ lclTypeSpecNode t,
2894 /*@only@*/ declaratorNode d)
2895{
dfd82dce 2896 return (makeFcnNode (qual_createUnknown (), t, d,
2897 varDeclarationNodeList_new (),
2898 varDeclarationNodeList_new (),
2899 letDeclNodeList_new (),
616915dd 2900 (lclPredicateNode) 0,
2901 (lclPredicateNode) 0,
2902 (modifyNode) 0,
2903 (lclPredicateNode) 0,
2904 (lclPredicateNode) 0));
2905}
2906
2907/*@only@*/ iterNode
2908makeIterNode (ltoken id, paramNodeList p)
2909{
2910 iterNode x = (iterNode) dmalloc (sizeof (*x));
2911 bool hasYield = FALSE;
2912
2913 x->name = id;
2914 x->params = p;
2915
2916 /* check there is at least one yield param */
2917
2918 paramNodeList_elements (p, pe)
2919 {
2920 if (paramNode_isYield (pe))
2921 {
2922 hasYield = TRUE;
2923 break;
2924 }
2925 } end_paramNodeList_elements
2926
2927 if (!hasYield)
2928 {
2929 lclerror (id, message ("Iterator has no yield parameters: %s",
2930 ltoken_getRawString (id)));
2931 }
2932
2933 return (x);
2934}
2935
2936/*@only@*/ fcnNode
2937makeFcnNode (qual specQual,
2938 /*@null@*/ lclTypeSpecNode t,
2939 declaratorNode d,
2940 /*@null@*/ globalList g,
2941 /*@null@*/ varDeclarationNodeList privateinits,
2942 /*@null@*/ letDeclNodeList lets,
2943 /*@null@*/ lclPredicateNode checks,
2944 /*@null@*/ lclPredicateNode requires,
2945 /*@null@*/ modifyNode m,
2946 /*@null@*/ lclPredicateNode ensures,
2947 /*@null@*/ lclPredicateNode claims)
2948{
2949 fcnNode x = (fcnNode) dmalloc (sizeof (*x));
28bf4b0b 2950
616915dd 2951 if (d->type != (typeExpr)0 && (d->type)->kind != TEXPR_FCN)
2952 {
2953 lclerror (d->id, cstring_makeLiteral
2954 ("Attempt to specify function without parameter list"));
2955 d->type = makeFunctionNode (d->type, paramNodeList_new ());
2956 }
28bf4b0b 2957
616915dd 2958 x->special = specQual;
2959 x->typespec = t;
2960 x->declarator = d;
2961 x->globals = g;
2962 x->inits = privateinits;
2963 x->lets = lets;
2964 x->checks = checks;
2965 x->require = requires;
2966 x->modify = m;
2967 x->ensures = ensures;
2968 x->claim = claims;
2969
2970 /* extract info to fill in x->name =; x->signature =; */
2971 x->name = ltoken_copy (d->id);
2972
2973 return (x);
2974}
2975
2976/*@only@*/ claimNode
2977makeClaimNode (ltoken id, paramNodeList p,
2978 globalList g, letDeclNodeList lets, lclPredicateNode requires,
2979 programNode b, lclPredicateNode ensures)
2980{
2981 claimNode x = (claimNode) dmalloc (sizeof (*x));
2982
2983
2984 x->name = id;
2985 x->params = p;
2986 x->globals = g;
2987 x->lets = lets;
2988 x->require = requires;
2989 x->body = b;
2990 x->ensures = ensures;
2991 return (x);
2992}
2993
2994/*@only@*/ lclPredicateNode
2995makeIntraClaimNode (ltoken t, lclPredicateNode n)
2996{
2997 ltoken_free (n->tok);
2998 n->tok = t;
2999 n->kind = LPD_INTRACLAIM;
3000 return (n);
3001}
3002
3003/*@only@*/ lclPredicateNode
3004makeRequiresNode (ltoken t, lclPredicateNode n)
3005{
3006 ltoken_free (n->tok);
3007 n->tok = t;
3008 n->kind = LPD_REQUIRES;
3009 return (n);
3010}
3011
3012/*@only@*/ lclPredicateNode
3013makeChecksNode (ltoken t, lclPredicateNode n)
3014{
3015 ltoken_free (n->tok);
3016 n->tok = t;
3017 n->kind = LPD_CHECKS;
3018 return (n);
3019}
3020
3021/*@only@*/ lclPredicateNode
3022makeEnsuresNode (ltoken t, lclPredicateNode n)
3023{
3024 ltoken_free (n->tok);
3025 n->tok = t;
3026 n->kind = LPD_ENSURES;
3027 return (n);
3028}
3029
3030/*@only@*/ lclPredicateNode
3031makeLclPredicateNode (ltoken t, termNode n,
3032 lclPredicateKind k)
3033{
3034 lclPredicateNode x = (lclPredicateNode) dmalloc (sizeof (*x));
3035
3036 x->tok = t;
3037 x->predicate = n;
3038 x->kind = k;
3039 return (x);
3040}
3041
3042/*@only@*/ quantifierNode
3043makeQuantifierNode (varNodeList v, ltoken quant)
3044{
3045 quantifierNode x = (quantifierNode) dmalloc (sizeof (*x));
3046
3047 x->quant = quant;
3048 x->vars = v;
3049 x->isForall = cstring_equalLit (ltoken_unparse (quant), "\forall");
3050
3051 return (x);
3052}
3053
3054/*@only@*/ arrayQualNode
3055makeArrayQualNode (ltoken t, termNode term)
3056{
3057 arrayQualNode x = (arrayQualNode) dmalloc (sizeof (*x));
3058
3059 x->tok = t;
3060 x->term = term;
3061 return (x);
3062}
3063
3064/*@only@*/ varNode
3065makeVarNode (/*@only@*/ ltoken varid, bool isObj, lclTypeSpecNode t)
3066{
3067 varNode x = (varNode) dmalloc (sizeof (*x));
3068 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
3069 sort sort;
3070
3071 vi->id = ltoken_copy (varid);
3072 sort = lclTypeSpecNode2sort (t);
3073
3074 /* 9/3/93, The following is needed because we want value sorts to be
3075 the default, object sort is generated only if there is "obj" qualifier.
3076 There are 2 cases: (1) for immutable types (including C primitive types),
3077 we need to generate the object sort if qualifier is present; (2) for
3078 array, struct and union types, they are already in their object sorts.
3079 */
3080
3081 sort = sort_makeVal (sort); /* both cases are now value sorts */
3082
3083 if (isObj)
3084 {
3085 sort = sort_makeObj (sort);
3086 }
3087
3088
3089 vi->sort = sort;
3090 vi->kind = VRK_QUANT;
3091 vi->export = TRUE;
3092
3093 (void) symtable_enterVar (g_symtab, vi);
3094 varInfo_free (vi);
3095
3096 x->varid = varid;
3097 x->isObj = isObj;
3098 x->type = t;
3099 x->sort = sort_makeNoSort ();
3100
3101 return (x);
3102}
3103
3104/*@only@*/ abstBodyNode
3105makeAbstBodyNode (ltoken t, fcnNodeList f)
3106{
3107 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3108
3109 x->tok = t;
3110 x->typeinv = (lclPredicateNode)0;
3111 x->fcns = f;
3112 return (x);
3113}
3114
3115/*@only@*/ abstBodyNode
3116makeExposedBodyNode (ltoken t, lclPredicateNode inv)
3117{
3118 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3119
3120 x->tok = t;
3121 x->typeinv = inv;
3122 x->fcns = fcnNodeList_undefined;
3123 return (x);
3124}
3125
3126/*@only@*/ abstBodyNode
3127makeAbstBodyNode2 (ltoken t, ltokenList ops)
3128{
3129 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3130
3131 x->tok = t;
3132 x->typeinv = (lclPredicateNode) 0;
3133
3134 x->fcns = fcnNodeList_new ();
3135
3136 ltokenList_elements (ops, op)
3137 {
3138 x->fcns = fcnNodeList_add
3139 (x->fcns,
3140 fcnNode_fromDeclarator (lclTypeSpecNode_undefined,
3141 makeUnknownDeclaratorNode (ltoken_copy (op))));
3142 } end_ltokenList_elements;
3143
3144 ltokenList_free (ops);
3145
3146 return (x);
3147}
3148
3149/*@only@*/ stmtNode
3150 makeStmtNode (ltoken varId, ltoken fcnId, /*@only@*/ termNodeList v)
3151{
3152 stmtNode n = (stmtNode) dmalloc (sizeof (*n));
3153
3154 n->lhs = varId;
3155 n->operator = fcnId;
3156 n->args = v;
3157 return (n);
3158}
3159
3160/* printDeclarators -> declaratorNodeList_unparse */
3161
3162static cstring abstDeclaratorNode_unparse (abstDeclaratorNode x)
3163{
3164 return (typeExpr_unparse ((typeExpr) x));
3165}
3166
3167/*@only@*/ paramNode
3168makeParamNode (lclTypeSpecNode t, typeExpr d)
3169{
3170 paramNode x = (paramNode) dmalloc (sizeof (*x));
3171
3172 paramNode_checkQualifiers (t, d);
3173
3174 x->type = t;
3175 x->paramdecl = d;
3176 x->kind = PNORMAL; /*< forgot this! >*/
3177
3178 return (x);
3179}
3180
3181/*@only@*/ paramNode
3182paramNode_elipsis (void)
3183{
3184 paramNode x = (paramNode) dmalloc (sizeof (*x));
3185
3186 x->type = (lclTypeSpecNode) 0;
3187 x->paramdecl = (typeExpr) 0;
3188 x->kind = PELIPSIS;
3189
3190 return (x);
3191}
3192
3193static /*@observer@*/ ltoken typeExpr_getTok (typeExpr d)
3194{
3195 while (d != (typeExpr)0)
3196 {
3197 if (d->kind == TEXPR_BASE)
3198 {
3199 return (d->content.base);
3200 }
3201 else
3202 {
3203 if (d->kind == TEXPR_PTR)
3204 {
3205 d = d->content.pointer;
3206 }
3207 else if (d->kind == TEXPR_ARRAY)
3208 {
3209 d = d->content.array.elementtype;
3210 }
3211 else if (d->kind == TEXPR_FCN)
3212 {
3213 d = d->content.function.returntype;
3214 }
3215 else
3216 {
3217 BADBRANCH;
3218 }
3219 }
3220 }
3221
3222 llfatalerror (cstring_makeLiteral ("typeExpr_getTok: unreachable code"));
3223 BADEXIT;
3224}
3225
3226void
3227paramNode_checkQualifiers (lclTypeSpecNode t, typeExpr d)
3228{
3229 bool isPointer = FALSE;
3230 bool isUser = FALSE;
3231 bool hasAlloc = FALSE;
3232 bool hasAlias = FALSE;
3233
3234 llassert (lclTypeSpecNode_isDefined (t));
3235
f9264521 3236 if (pointers_isUndefined (t->pointers)
616915dd 3237 && (d != (typeExpr)0 && d->kind != TEXPR_PTR) && d->kind != TEXPR_ARRAY)
3238 {
3239 if (t->kind == LTS_TYPE)
3240 {
3241 sortNode sn;
3242
3243 llassert (t->content.type != NULL);
3244
3245 sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort));
3246
28bf4b0b 3247 if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY
3248 || sn->kind == SRT_HOF || sn->kind == SRT_NONE)
616915dd 3249 {
3250 isPointer = TRUE;
3251 }
3252 }
3253 }
3254 else
3255 {
3256 isPointer = TRUE;
3257 }
3258
3259 if (d != (typeExpr)0 && d->kind != TEXPR_BASE)
3260 {
3261 if (t->kind == LTS_TYPE)
3262 {
3263 sortNode sn;
3264
3265 llassert (t->content.type != NULL);
3266 sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort));
3267
28bf4b0b 3268 if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY
3269 || sn->kind == SRT_HOF || sn->kind == SRT_NONE)
616915dd 3270 {
3271 isUser = TRUE;
3272 }
3273 }
3274 }
3275 else
3276 {
3277 isPointer = TRUE;
3278 }
3279
3280 if (d != (typeExpr)NULL)
3281 {
3282 qualList_elements (t->quals, q)
3283 {
3284 if (qual_isAllocQual (q))
3285 {
3286 if (hasAlloc)
3287 {
3288 ltoken tok = typeExpr_getTok (d);
3289 lclerror (tok, message ("Parameter declared with multiple allocation "
3290 "qualifiers: %q", typeExpr_unparse (d)));
3291 }
3292 hasAlloc = TRUE;
3293
3294 if (!isPointer)
3295 {
3296 ltoken tok = typeExpr_getTok (d);
3297 lclerror (tok, message ("Non-pointer declared as %s parameter: %q",
3298 qual_unparse (q),
3299 typeExpr_unparse (d)));
3300 }
3301 }
3302 if (qual_isAliasQual (q))
3303 {
3304 if (hasAlias)
3305 {
3306 ltoken tok = typeExpr_getTok (d);
3307 lclerror (tok, message ("Parameter declared with multiple alias qualifiers: %q",
3308 typeExpr_unparse (d)));
3309 }
3310 hasAlias = TRUE;
3311
3312 if (!(isPointer || isUser))
3313 {
3314 ltoken tok = typeExpr_getTok (d);
3315 lclerror (tok, message ("Unsharable type declared as %s parameter: %q",
3316 qual_unparse (q),
3317 typeExpr_unparse (d)));
3318 }
3319 }
3320 } end_qualList_elements;
3321 }
3322}
3323
3324/*@only@*/ cstring
3325paramNode_unparse (paramNode x)
3326{
3327 if (x != (paramNode) 0)
3328 {
3329 if (x->kind == PELIPSIS)
3330 {
3331 return (cstring_makeLiteral ("..."));
3332 }
3333
3334 if (x->paramdecl != (typeExpr) 0)
3335 { /* handle (void) */
3336 return (message ("%q %q", lclTypeSpecNode_unparse (x->type),
3337 typeExpr_unparse (x->paramdecl)));
3338 }
3339 else
3340 {
3341 return (lclTypeSpecNode_unparse (x->type));
3342 }
3343 }
3344 return cstring_undefined;
3345}
3346
3347static cstring
3348lclTypeSpecNode_unparseAltComments (/*@null@*/ lclTypeSpecNode typespec) /*@*/
3349{
3350 if (typespec != (lclTypeSpecNode) 0)
3351 {
3352 cstring s = qualList_toCComments (typespec->quals);
3353
3354 switch (typespec->kind)
3355 {
3356 case LTS_TYPE:
3357 {
3358 llassert (typespec->content.type != NULL);
3359
3360 return (cstring_concatFree
3361 (s, printLeaves (typespec->content.type->ctypes)));
3362 }
3363 case LTS_ENUM:
3364 {
3365 bool first = TRUE;
3366 enumSpecNode n = typespec->content.enumspec;
3367
3368 s = cstring_concatFree (s, cstring_makeLiteral ("enum"));
3369 llassert (n != NULL);
3370
3371 if (!ltoken_isUndefined (n->opttagid))
3372 {
3373 s = message ("%q %s", s, ltoken_unparse (n->opttagid));
3374 }
3375 s = message ("%q {", s);
3376
3377 ltokenList_elements (n->enums, e)
3378 {
3379 if (first)
3380 {
3381 first = FALSE;
3382 s = message ("%q%s", s, ltoken_getRawString (e));
3383 }
3384 else
3385 s = message ("%q, %s", s, ltoken_getRawString (e));
3386 } end_ltokenList_elements;
3387
3388 return (message ("%q}", s));
3389 }
3390 case LTS_STRUCTUNION:
3391 {
3392 strOrUnionNode n = typespec->content.structorunion;
3393 stDeclNodeList decls;
3394
3395 llassert (n != NULL);
3396
3397 switch (n->kind)
3398 {
3399 case SU_STRUCT:
3400 s = cstring_concatFree (s, cstring_makeLiteral ("struct "));
3401 /*@switchbreak@*/ break;
3402 case SU_UNION:
3403 s = cstring_concatFree (s, cstring_makeLiteral ("union "));
3404 /*@switchbreak@*/ break;
3405 }
3406
3407 if (!ltoken_isUndefined (n->opttagid))
3408 {
3409 if (stDeclNodeList_size (n->structdecls) == 0)
3410 {
3411 return (message ("%q%s", s, ltoken_unparse (n->opttagid)));
3412 }
3413
d5047b91 3414 s = message ("%q%s {\n\t", s, ltoken_unparse (n->opttagid));
616915dd 3415 }
3416 else
3417 {
d5047b91 3418 s = message ("%q{\n\t", s);
616915dd 3419 }
3420
3421 decls = n->structdecls;
3422
3423 stDeclNodeList_elements (decls, f)
3424 {
d5047b91 3425 s = message ("%q%q %q;\n\t", s,
616915dd 3426 lclTypeSpecNode_unparseAltComments (f->lcltypespec),
3427 declaratorNodeList_unparse (f->declarators));
3428 } end_stDeclNodeList_elements;
3429
d5047b91 3430 return (message ("%q }", s));
616915dd 3431 }
3432 case LTS_CONJ:
3433 {
3434 cstring_free (s);
3435
3436 return
3437 (message
3438 ("%q, %q",
3439 lclTypeSpecNode_unparseAltComments (typespec->content.conj->a),
3440 lclTypeSpecNode_unparseAltComments (typespec->content.conj->b)));
3441 }
3442 BADDEFAULT;
3443 }
3444 }
3445 else
3446 {
3447 llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec");
3448
3449 return cstring_undefined;
3450 }
3451
3452 BADEXIT;
3453}
3454
3455cstring lclTypeSpecNode_unparseComments (/*@null@*/ lclTypeSpecNode typespec)
3456{
3457 if (typespec != (lclTypeSpecNode) 0)
3458 {
3459 cstring s = qualList_toCComments (typespec->quals);
3460
3461 switch (typespec->kind)
3462 {
3463 case LTS_TYPE:
3464 {
3465 llassert (typespec->content.type != NULL);
3466
3467 return (cstring_concatFree
3468 (s, printLeaves (typespec->content.type->ctypes)));
3469 }
3470 case LTS_ENUM:
3471 {
3472 bool first = TRUE;
3473 enumSpecNode n = typespec->content.enumspec;
3474
3475 s = cstring_concatFree (s, cstring_makeLiteral ("enum"));
3476 llassert (n != NULL);
3477
3478 if (!ltoken_isUndefined (n->opttagid))
3479 {
3480 s = message ("%q %s", s, ltoken_unparse (n->opttagid));
3481 }
3482 s = message ("%q {", s);
3483
3484 ltokenList_elements (n->enums, e)
3485 {
3486 if (first)
3487 {
3488 first = FALSE;
3489 s = message ("%q%s", s, ltoken_getRawString (e));
3490 }
3491 else
3492 s = message ("%q, %s", s, ltoken_getRawString (e));
3493 } end_ltokenList_elements;
3494
3495 return (message ("%q}", s));
3496 }
3497 case LTS_STRUCTUNION:
3498 {
3499 strOrUnionNode n = typespec->content.structorunion;
3500 stDeclNodeList decls;
3501
3502 llassert (n != NULL);
3503
3504 switch (n->kind)
3505 {
3506 case SU_STRUCT:
3507 s = cstring_concatFree (s, cstring_makeLiteral ("struct "));
3508 /*@switchbreak@*/ break;
3509 case SU_UNION:
3510 s = cstring_concatFree (s, cstring_makeLiteral ("union "));
3511 /*@switchbreak@*/ break;
3512 }
3513
3514 if (!ltoken_isUndefined (n->opttagid))
3515 {
3516 if (stDeclNodeList_size (n->structdecls) == 0)
3517 {
3518 return (message ("%q%s", s, ltoken_unparse (n->opttagid)));
3519 }
3520
d5047b91 3521 s = message ("%q%s {\n\t", s, ltoken_unparse (n->opttagid));
616915dd 3522 }
3523 else
3524 {
d5047b91 3525 s = message ("%q{\n\t", s);
616915dd 3526 }
3527
3528 decls = n->structdecls;
3529
3530 stDeclNodeList_elements (decls, f)
3531 {
d5047b91 3532 s = message ("%q%q %q;\n\t", s,
616915dd 3533 lclTypeSpecNode_unparseComments (f->lcltypespec),
3534 declaratorNodeList_unparse (f->declarators));
3535 } end_stDeclNodeList_elements;
3536
d5047b91 3537 return (message ("%q }", s));
616915dd 3538 }
3539 case LTS_CONJ:
3540 {
3541 cstring_free (s);
3542
3543 return
3544 (message
3545 ("%q /*@alt %q@*/",
3546 lclTypeSpecNode_unparseComments (typespec->content.conj->a),
3547 lclTypeSpecNode_unparseAltComments (typespec->content.conj->b)));
3548 }
3549 BADDEFAULT;
3550 }
3551 }
3552 else
3553 {
3554 llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec");
3555
3556 return cstring_undefined;
3557 }
3558
3559 BADEXIT;
3560}
3561
3562/*@only@*/ cstring
3563paramNode_unparseComments (paramNode x)
3564{
3565 if (x != (paramNode) 0)
3566 {
3567 if (x->kind == PELIPSIS)
3568 {
3569 return (cstring_makeLiteral ("..."));
3570 }
3571
3572 if (x->paramdecl != (typeExpr) 0)
3573 { /* handle (void) */
3574 return (message ("%q %q",
3575 lclTypeSpecNode_unparseComments (x->type),
3576 typeExpr_unparseNoBase (x->paramdecl)));
3577 }
3578 else
3579 {
3580 return (lclTypeSpecNode_unparseComments (x->type));
3581 }
3582 }
3583 return cstring_undefined;
3584}
3585
3586/*@only@*/ termNode
3587makeIfTermNode (ltoken ift, termNode ifn, ltoken thent,
3588 termNode thenn, ltoken elset,
3589 termNode elsen)
3590{
3591 termNode t = (termNode) dmalloc (sizeof (*t));
3592 opFormNode opform = makeOpFormNode (ift, OPF_IF, opFormUnion_createMiddle (0),
3593 ltoken_undefined);
3594 nameNode nn = makeNameNodeForm (opform);
3595 termNodeList args = termNodeList_new ();
3596
3597 t->error_reported = FALSE;
3598 t->wrapped = 0;
3599 termNodeList_addh (args, ifn);
3600 termNodeList_addh (args, thenn);
3601 termNodeList_addh (args, elsen);
3602 t->name = nn;
3603 t->args = args;
3604 t->kind = TRM_APPLICATION;
3605 t->sort = sort_makeNoSort ();
3606 t->given = t->sort;
3607 t->possibleSorts = sortSet_new ();
3608 t->possibleOps = lslOpSet_new ();
3609
3610 ltoken_free (thent);
3611 ltoken_free (elset);
3612
3613 return (t);
3614}
3615
3616static /*@observer@*/ ltoken
3617 nameNode2anyOp (nameNode n)
3618{
3619 if (n != (nameNode) 0)
3620 {
3621 opFormNode opnode = n->content.opform;
3622 opFormKind kind;
3623
3624 llassert (opnode != NULL);
3625
3626 kind = opnode->kind;
3627
3628 if (kind == OPF_MANYOPM || kind == OPF_ANYOP ||
3629 kind == OPF_MANYOP || kind == OPF_ANYOPM)
3630 {
3631 opFormUnion u;
3632
3633 u = opnode->content;
3634 return u.anyop;
3635 }
3636 }
3637 return ltoken_undefined;
3638}
3639
3640/*@only@*/ termNode
3641makeInfixTermNode (termNode x, ltoken op, termNode y)
3642{
3643 termNode t = (termNode) dmalloc (sizeof (*t));
3644 opFormNode opform;
3645 nameNode nn;
3646 termNodeList args = termNodeList_new ();
3647
3648 checkAssociativity (x, op);
3649
3650 opform = makeOpFormNode (op, OPF_MANYOPM,
3651 opFormUnion_createAnyOp (op),
3652 ltoken_undefined);
3653
3654 nn = makeNameNodeForm (opform);
3655
3656 t->error_reported = FALSE;
3657 t->wrapped = 0;
3658 termNodeList_addh (args, x);
3659 termNodeList_addh (args, y);
3660 t->name = nn;
3661 t->args = args;
3662 t->kind = TRM_APPLICATION;
3663 t->sort = sort_makeNoSort ();
3664 t->given = t->sort;
28bf4b0b 3665 t->possibleSorts = sortSet_new (); /* sort_equal */
616915dd 3666 t->possibleOps = lslOpSet_new ();
3667 return (t);
3668}
3669
3670/*@only@*/ quantifiedTermNode
3671 quantifiedTermNode_copy (quantifiedTermNode q)
3672{
3673 quantifiedTermNode ret = (quantifiedTermNode) dmalloc (sizeof (*ret));
3674
3675 ret->quantifiers = quantifierNodeList_copy (q->quantifiers);
3676 ret->open = ltoken_copy (q->open);
3677 ret->close = ltoken_copy (q->close);
3678 ret->body = termNode_copySafe (q->body);
3679
3680 return (ret);
3681}
3682
3683/*@only@*/ termNode
3684makeQuantifiedTermNode (quantifierNodeList qn, ltoken open,
3685 termNode t, ltoken close)
3686{
3687 sort sort;
3688 termNode n = (termNode) dmalloc (sizeof (*n));
3689 quantifiedTermNode q = (quantifiedTermNode) dmalloc (sizeof (*q));
3690
1b8ae690 3691 n->name = NULL; /*> missing this --- detected by splint <*/
616915dd 3692 n->error_reported = FALSE;
3693 n->wrapped = 0;
3694 n->error_reported = FALSE;
3695 n->kind = TRM_QUANTIFIER;
3696 n->possibleSorts = sortSet_new ();
3697 n->possibleOps = lslOpSet_new ();
3698 n->kind = TRM_UNCHANGEDALL;
3699 n->args = termNodeList_new (); /*< forgot this >*/
3700
3701 termNodeList_free (t->args);
3702 t->args = termNodeList_new ();
3703
2a6e9c30 3704 sort = g_sortBool;
616915dd 3705 n->sort = sort;
3706 (void) sortSet_insert (n->possibleSorts, sort);
3707
3708 q->quantifiers = qn;
3709 q->open = open;
3710 q->close = close;
3711 q->body = t;
3712
3713 n->quantified = q;
3714 return (n);
3715}
3716
3717/*@only@*/ termNode
3718makePostfixTermNode (/*@returned@*/ /*@only@*/ termNode secondary, ltokenList postfixops)
3719{
3720 termNode top = secondary;
3721
3722 ltokenList_elements (postfixops, op)
3723 {
3724 top = makePostfixTermNode2 (top, ltoken_copy (op));
3725 /*@i@*/ } end_ltokenList_elements;
3726
3727 ltokenList_free (postfixops);
3728
3729 return (top); /* dep as only? */
3730}
3731
3732/*
3733** secondary is returned in the args list
3734*/
3735
3736/*@only@*/ termNode
3737makePostfixTermNode2 (/*@returned@*/ /*@only@*/ termNode secondary,
3738 /*@only@*/ ltoken postfixop)
3739{
3740 termNode t = (termNode) dmalloc (sizeof (*t));
3741
3742 opFormNode opform = makeOpFormNode (postfixop,
3743 OPF_MANYOP, opFormUnion_createAnyOp (postfixop),
3744 ltoken_undefined);
3745 nameNode nn = makeNameNodeForm (opform);
3746 termNodeList args = termNodeList_new ();
3747
3748 t->error_reported = FALSE;
3749 t->wrapped = 0;
3750 termNodeList_addh (args, secondary);
3751 t->name = nn;
3752 t->args = args;
3753 t->kind = TRM_APPLICATION;
3754 t->sort = sort_makeNoSort ();
3755 t->given = t->sort;
3756 t->possibleSorts = sortSet_new ();
3757 t->possibleOps = lslOpSet_new ();
3758 return t;
3759}
3760
3761/*@only@*/ termNode
3762makePrefixTermNode (ltoken op, termNode arg)
3763{
3764 termNode t = (termNode) dmalloc (sizeof (*t));
3765 termNodeList args = termNodeList_new ();
3766 opFormNode opform = makeOpFormNode (op, OPF_ANYOPM, opFormUnion_createAnyOp (op),
3767 ltoken_undefined);
3768 nameNode nn = makeNameNodeForm (opform);
3769
3770 t->error_reported = FALSE;
3771 t->wrapped = 0;
3772 t->name = nn;
3773 termNodeList_addh (args, arg);
3774 t->args = args;
3775 t->kind = TRM_APPLICATION;
3776 t->sort = sort_makeNoSort ();
3777 t->given = t->sort;
3778 t->possibleSorts = sortSet_new ();
3779 t->possibleOps = lslOpSet_new ();
3780 return t;
3781}
3782
3783/*@only@*/ termNode
3784makeOpCallTermNode (ltoken op, ltoken open,
3785 termNodeList args, ltoken close)
3786{
3787 /* like prefixTerm, but with opId LPAR termNodeList RPAR */
3788 termNode t = (termNode) dmalloc (sizeof (*t));
3789 nameNode nn = makeNameNodeId (op);
3790
3791 t->error_reported = FALSE;
3792 t->wrapped = 0;
3793 t->name = nn;
3794 t->args = args;
3795 t->kind = TRM_APPLICATION;
3796 t->sort = sort_makeNoSort ();
3797 t->given = t->sort;
3798 t->possibleSorts = sortSet_new ();
3799 t->possibleOps = lslOpSet_new ();
3800
3801 ltoken_free (open);
3802 ltoken_free (close);
3803
3804 return t;
3805}
3806
3807/*@exposed@*/ termNode
3808CollapseInfixTermNode (/*@returned@*/ termNode secondary, termNodeList infix)
3809{
3810 termNode left = secondary;
3811
3812 termNodeList_elements (infix, node)
3813 {
3814 termNodeList_addl (node->args, termNode_copySafe (left));
3815 left = node;
3816 /* computePossibleSorts (left); */
3817 } end_termNodeList_elements;
3818
3819 return (left);
3820}
3821
3822static void
3823checkAssociativity (termNode x, ltoken op)
3824{
3825 ltoken lastOpToken;
3826
3827 if (x->wrapped == 0 && /* no parentheses */
3828 x->kind == TRM_APPLICATION && x->name != (nameNode) 0 &&
3829 (!x->name->isOpId))
3830 {
3831 lastOpToken = nameNode2anyOp (x->name);
3832
3833 if ((ltoken_getCode (lastOpToken) == logicalOp &&
3834 ltoken_getCode (op) == logicalOp) ||
3835 ((ltoken_getCode (lastOpToken) == simpleOp ||
3836 ltoken_getCode (lastOpToken) == LLT_MULOP) &&
3837 (ltoken_getCode (op) == simpleOp ||
3838 ltoken_getCode (op) == LLT_MULOP)))
3839 if (ltoken_getText (lastOpToken) != ltoken_getText (op))
3840 {
3841 lclerror (op,
3842 message
3843 ("Parentheses needed to specify associativity of %s and %s",
3844 cstring_fromChars (lsymbol_toChars (ltoken_getText (lastOpToken))),
3845 cstring_fromChars (lsymbol_toChars (ltoken_getText (op)))));
3846 }
3847 }
3848}
3849
3850termNodeList
3851pushInfixOpPartNode (/*@returned@*/ termNodeList x, ltoken op,
3852 /*@only@*/ termNode secondary)
3853{
3854 termNode lastLeftTerm;
3855 termNodeList args = termNodeList_new ();
3856 termNode t = (termNode) dmalloc (sizeof (*t));
3857 opFormNode opform;
3858 nameNode nn;
3859
3860 termNodeList_addh (args, secondary);
3861
3862 if (!termNodeList_empty (x))
3863 {
3864 termNodeList_reset (x);
3865 lastLeftTerm = termNodeList_current (x);
3866 checkAssociativity (lastLeftTerm, op);
3867 }
3868
3869 opform = makeOpFormNode (op, OPF_MANYOPM,
3870 opFormUnion_createAnyOp (op), ltoken_undefined);
3871
3872 nn = makeNameNodeForm (opform);
3873
3874 t->error_reported = FALSE;
3875 t->wrapped = 0;
3876 t->name = nn;
3877 t->kind = TRM_APPLICATION;
3878 t->args = args;
3879 t->sort = sort_makeNoSort ();
3880 t->given = t->sort;
3881 t->possibleSorts = sortSet_new ();
3882 t->possibleOps = lslOpSet_new ();
3883 termNodeList_addh (x, t);
3884 /* don't compute sort yet, do it in CollapseInfixTermNode */
3885 return (x);
3886}
3887
3888termNode
3889updateMatchedNode (/*@only@*/ termNode left, /*@returned@*/ termNode t,
3890 /*@only@*/ termNode right)
3891{
3892 opFormNode op;
3893
3894 if ((t == (termNode) 0) || (t->name == NULL) || t->name->isOpId)
3895 {
3896 llbugexitlit ("updateMatchedNode: expect opForm in nameNode");
3897 }
3898
3899 op = t->name->content.opform;
3900 llassert (op != NULL);
3901
3902 if (left == (termNode) 0)
3903 {
3904 if (right == (termNode) 0)
3905 {
3906 /* op->kind is not changed */
3907 termNode_free (right);
3908 }
3909 else
3910 {
3911 op->kind = OPF_MIDDLEM;
3912 op->key = opFormNode2key (op, OPF_MIDDLEM);
3913 termNodeList_addh (t->args, right);
3914 }
3915 }
3916 else
3917 {
3918 termNodeList_addl (t->args, left);
3919 if (right == (termNode) 0)
3920 {
3921 op->kind = OPF_MMIDDLE;
3922 op->key = opFormNode2key (op, OPF_MMIDDLE);
3923 }
3924 else
3925 {
3926 op->kind = OPF_MMIDDLEM;
3927 op->key = opFormNode2key (op, OPF_MMIDDLEM);
3928 termNodeList_addh (t->args, right);
3929 }
3930 }
3931 return t;
3932}
3933
3934/*@only@*/ termNode
3935 updateSqBracketedNode (/*@only@*/ termNode left,
3936 /*@only@*/ /*@returned@*/ termNode t,
3937 /*@only@*/ termNode right)
3938{
3939 opFormNode op;
3940
3941 if ((t == (termNode) 0) || (t->name == NULL) || (t->name->isOpId))
3942 {
3943 llbugexitlit ("updateSqBracketededNode: expect opForm in nameNode");
3944 }
3945
3946 op = t->name->content.opform;
3947 llassert (op != NULL);
3948
3949 if (left == (termNode) 0)
3950 {
3951 if (right == (termNode) 0)
3952 {
3953 /* op->kind is not changed */
3954 }
3955 else
3956 {
3957 op->kind = OPF_BMIDDLEM;
3958 op->key = opFormNode2key (op, OPF_BMIDDLEM);
3959 termNodeList_addh (t->args, right);
3960 }
3961 }
3962 else
3963 {
3964 termNodeList_addl (t->args, left);
3965
3966 if (right == (termNode) 0)
3967 {
3968 op->kind = OPF_BMMIDDLE;
3969 op->key = opFormNode2key (op, OPF_BMMIDDLE);
3970 }
3971 else
3972 {
3973 op->kind = OPF_BMMIDDLEM;
3974 op->key = opFormNode2key (op, OPF_BMMIDDLEM);
3975 termNodeList_addh (t->args, right);
3976 }
3977 }
3978 return t;
3979}
3980
3981/*@only@*/ termNode
3982makeSqBracketedNode (ltoken lbracket,
3983 termNodeList args, ltoken rbracket)
3984{
3985 termNode t = (termNode) dmalloc (sizeof (*t));
3986 int size;
3987 opFormNode opform;
3988 nameNode nn;
3989
3990 t->error_reported = FALSE;
3991 t->wrapped = 0;
3992
3993 size = termNodeList_size (args);
3994 opform = makeOpFormNode (lbracket, OPF_BMIDDLE, opFormUnion_createMiddle (size),
3995 rbracket);
3996 nn = makeNameNodeForm (opform);
3997 t->name = nn;
3998 t->kind = TRM_APPLICATION;
3999 t->args = args;
4000 t->sort = sort_makeNoSort ();
4001 t->given = t->sort;
4002 t->possibleSorts = sortSet_new ();
4003 t->possibleOps = lslOpSet_new ();
4004 /* do sort checking later, not here, incomplete parse */
4005 return (t);
4006}
4007
4008/*@only@*/ termNode
4009makeMatchedNode (ltoken open, termNodeList args, ltoken close)
4010{
4011 /* matched : open args close */
4012 termNode t = (termNode) dmalloc (sizeof (*t));
4013 int size;
4014 opFormNode opform;
4015 nameNode nn;
4016
4017 t->error_reported = FALSE;
4018 t->wrapped = 0;
4019
4020 size = termNodeList_size (args);
4021 opform = makeOpFormNode (open, OPF_MIDDLE, opFormUnion_createMiddle (size), close);
4022 nn = makeNameNodeForm (opform);
4023 t->name = nn;
4024 t->kind = TRM_APPLICATION;
4025 t->args = args;
4026 t->sort = sort_makeNoSort ();
4027 t->given = t->sort;
4028 t->possibleSorts = sortSet_new ();
4029 t->possibleOps = lslOpSet_new ();
4030 /* do sort checking later, not here, incomplete parse */
4031 return (t);
4032}
4033
4034/*@only@*/ termNode
4035makeSimpleTermNode (ltoken varid)
4036{
4037 sort theSort = sort_makeNoSort ();
4038 lsymbol sym;
4039 opInfo oi;
4040 varInfo vi;
4041 termNode n = (termNode) dmalloc (sizeof (*n));
4042
4043 n->error_reported = FALSE;
4044 n->wrapped = 0;
4045 n->name = (nameNode) 0;
4046 n->given = theSort;
4047 n->args = termNodeList_new ();
4048 n->possibleSorts = sortSet_new ();
4049 n->possibleOps = lslOpSet_new ();
4050
4051 sym = ltoken_getText (varid);
4052
4053 /* lookup current scope */
4054 vi = symtable_varInfoInScope (g_symtab, sym);
4055
4056 if (varInfo_exists (vi))
4057 {
4058 theSort = vi->sort;
4059 n->kind = TRM_VAR;
4060 n->sort = theSort;
4061 n->literal = varid;
4062 (void) sortSet_insert (n->possibleSorts, theSort);
4063 }
4064 else
4065 { /* need to handle LCL constants */
4066 vi = symtable_varInfo (g_symtab, sym);
4067
4068 if (varInfo_exists (vi) && vi->kind == VRK_CONST)
4069 {
4070 theSort = vi->sort;
4071 n->kind = TRM_CONST;
4072 n->sort = theSort;
4073 n->literal = varid;
4074 (void) sortSet_insert (n->possibleSorts, theSort);
4075 }
4076 else
4077 { /* and LSL operators (true, false, new, nil, etc) */
4078 nameNode nn = makeNameNodeId (ltoken_copy (varid));
4079 oi = symtable_opInfo (g_symtab, nn);
4080
4081 if (opInfo_exists (oi) && (oi->name->isOpId) &&
4082 !sigNodeSet_isEmpty (oi->signatures))
4083 {
4084 sigNodeSet_elements (oi->signatures, x)
4085 {
4086 if (ltokenList_empty (x->domain))
4087 /* yes, it really is empty, not not empty */
4088 {
4089 lslOp op = (lslOp) dmalloc (sizeof (*op));
4090
4091 op->name = nameNode_copy (nn);
4092 op->signature = x;
4093 (void) sortSet_insert (n->possibleSorts, sigNode_rangeSort (x));
4094 (void) lslOpSet_insert (n->possibleOps, op);
4095 }
4096 } end_sigNodeSet_elements;
4097 }
4098
4099 nameNode_free (nn);
4100
4101 if (sortSet_size (n->possibleSorts) == 0)
4102 {
4103 lclerror
4104 (varid,
4105 message ("Unrecognized identifier (constant, variable or operator): %s",
4106 ltoken_getRawString (varid)));
4107
4108 }
4109
4110 n->sort = sort_makeNoSort ();
4111 n->literal = varid;
4112 n->kind = TRM_ZEROARY;
4113 }
4114 }
4115
4116 return (n);
4117}
4118
4119/*@only@*/ termNode
4120makeSelectTermNode (termNode pri, ltoken select, /*@dependent@*/ ltoken id)
4121{
4122 termNode t = (termNode) dmalloc (sizeof (*t));
4123 opFormNode opform = makeOpFormNode (select,
4124 OPF_MSELECT, opFormUnion_createAnyOp (id),
4125 ltoken_undefined);
4126 nameNode nn = makeNameNodeForm (opform);
4127 termNodeList args = termNodeList_new ();
4128
4129 t->error_reported = FALSE;
4130 t->wrapped = 0;
4131 t->name = nn;
4132 t->kind = TRM_APPLICATION;
4133 termNodeList_addh (args, pri);
4134 t->args = args;
4135 t->kind = TRM_APPLICATION;
4136 t->sort = sort_makeNoSort ();
4137 t->given = t->sort;
4138 t->possibleSorts = sortSet_new ();
4139 t->possibleOps = lslOpSet_new ();
4140
4141 return t;
4142}
4143
4144/*@only@*/ termNode
4145makeMapTermNode (termNode pri, ltoken map, /*@dependent@*/ ltoken id)
4146{
4147 termNode t = (termNode) dmalloc (sizeof (*t));
4148 opFormNode opform = makeOpFormNode (map, OPF_MMAP, opFormUnion_createAnyOp (id),
4149 ltoken_undefined);
4150 nameNode nn = makeNameNodeForm (opform);
4151 termNodeList args = termNodeList_new ();
4152
4153 t->error_reported = FALSE;
4154 t->wrapped = 0;
4155 t->kind = TRM_APPLICATION;
4156 t->name = nn;
4157 termNodeList_addh (args, pri);
4158 t->args = args;
4159 t->kind = TRM_APPLICATION;
4160 t->sort = sort_makeNoSort ();
4161 t->given = t->sort;
4162 t->possibleSorts = sortSet_new ();
4163 t->possibleOps = lslOpSet_new ();
4164 return t;
4165}
4166
4167/*@only@*/ termNode
4168makeLiteralTermNode (ltoken tok, sort s)
4169{
4170 nameNode nn = makeNameNodeId (ltoken_copy (tok));
4171 opInfo oi = symtable_opInfo (g_symtab, nn);
4172 lslOp op = (lslOp) dmalloc (sizeof (*op));
4173 termNode n = (termNode) dmalloc (sizeof (*n));
4174 sigNode sign;
4175 ltoken range;
4176
4177 n->name = nn;
4178 n->error_reported = FALSE;
4179 n->wrapped = 0;
4180 n->kind = TRM_LITERAL;
4181 n->literal = tok;
4182 n->given = sort_makeNoSort ();
4183 n->sort = n->given;
4184 n->args = termNodeList_new ();
4185 n->possibleSorts = sortSet_new ();
4186 n->possibleOps = lslOpSet_new ();
4187
4188 /* look up signatures for this operator too */
4189
4190 range = ltoken_create (simpleId, sort_getLsymbol (s));
dfd82dce 4191 sign = makesigNode (ltoken_undefined, ltokenList_new (),
616915dd 4192 ltoken_copy (range));
4193
4194 if (opInfo_exists (oi) && (oi->name->isOpId)
4195 && (sigNodeSet_size (oi->signatures) > 0))
4196 {
4197 sigNodeSet_elements (oi->signatures, x)
4198 {
4199 if (ltokenList_empty (x->domain))
4200 {
4201 lslOp opn = (lslOp) dmalloc (sizeof (*opn));
4202 sort sort;
4203
4204 opn->name = nameNode_copy (nn);
4205 opn->signature = x;
4206 sort = sigNode_rangeSort (x);
4207 (void) sortSet_insert (n->possibleSorts, sort);
4208 (void) lslOpSet_insert (n->possibleOps, opn);
4209 }
4210 } end_sigNodeSet_elements;
4211 }
4212
4213 /* insert into literal term */
4214 (void) sortSet_insert (n->possibleSorts, s);
4215
4216 op->name = nameNode_copy (nn);
4217 op->signature = sign;
4218 (void) lslOpSet_insert (n->possibleOps, op);
4219
4220 /* enter the literal as an operator into the operator table */
4221 /* 8/9/93. C's char constant 'c' syntax conflicts
4222 with LSL's lslinit.lsi table. Throw out, because it's not
4223 needed anyway. */
4224 /* symtable_enterOp (g_symtab, nn, sign); */
4225
2a6e9c30 4226 if (s == g_sortInt)
616915dd 4227 {
4228 sigNode osign;
4229 lslOp opn = (lslOp) dmalloc (sizeof (*opn));
4230
4231 /* if it is a C int, we should overload it as double too because
4232 C allows you to say "x > 2". */
4233
2a6e9c30 4234 (void) sortSet_insert (n->possibleSorts, g_sortDouble);
616915dd 4235
4236 ltoken_setText (range, lsymbol_fromChars ("double"));
4237 osign = makesigNode (ltoken_undefined, ltokenList_new (), range);
4238 opn->name = nameNode_copy (nn);
4239 opn->signature = osign;
4240 (void) lslOpSet_insert (n->possibleOps, opn);
4241
4242 symtable_enterOp (g_symtab, nameNode_copySafe (nn), sigNode_copy (osign));
4243 }
4244 else
4245 {
4246 ltoken_free (range);
4247 }
4248
4249 /* future: could overload cstrings to be both char_Vec as well as
4250 char_ObjPtr */
4251
4252 /*@-mustfree@*/
4253 return n;
4254} /*@=mustfree@*/
4255
4256/*@only@*/ termNode
4257makeUnchangedTermNode1 (ltoken op, /*@unused@*/ ltoken all)
4258{
4259 termNode t = (termNode) dmalloc (sizeof (*t));
4260
4261 t->error_reported = FALSE;
4262 t->wrapped = 0;
4263 t->kind = TRM_UNCHANGEDALL;
2a6e9c30 4264 t->sort = g_sortBool;
616915dd 4265 t->literal = op;
4266 t->given = sort_makeNoSort ();
4267 t->name = NULL; /*< missing this >*/
4268 t->args = termNodeList_new ();
4269 t->possibleSorts = sortSet_new ();
4270 t->possibleOps = lslOpSet_new ();
4271 (void) sortSet_insert (t->possibleSorts, t->sort);
4272
4273 ltoken_free (all);
4274
4275 return t;
4276}
4277
4278/*@only@*/ termNode
4279makeUnchangedTermNode2 (ltoken op, storeRefNodeList x)
4280{
4281 termNode t = (termNode) dmalloc (sizeof (*t));
4282 ltoken errtok;
4283 sort sort;
4284
4285 t->name = NULL; /*< missing this >*/
4286 t->error_reported = FALSE;
4287 t->wrapped = 0;
4288 t->kind = TRM_UNCHANGEDOTHERS;
2a6e9c30 4289 t->sort = g_sortBool;
616915dd 4290 t->literal = op;
4291 t->unchanged = x;
4292 t->given = sort_makeNoSort ();
4293 t->possibleSorts = sortSet_new ();
4294 t->possibleOps = lslOpSet_new ();
4295 t->args = termNodeList_new ();
4296
4297 (void) sortSet_insert (t->possibleSorts, t->sort);
4298 /* check storeRefNode's are mutable, uses sort of term */
4299
4300 storeRefNodeList_elements (x, sto)
4301 {
4302 if (storeRefNode_isTerm (sto))
4303 {
4304 sort = sto->content.term->sort;
4305 if (!sort_mutable (sort))
4306 {
4307 errtok = termNode_errorToken (sto->content.term);
4308 lclerror (errtok,
4309 message ("Term denoting immutable object used in unchanged list: %q",
4310 termNode_unparse (sto->content.term)));
4311 }
4312 }
4313 else
4314 {
4315 if (storeRefNode_isType (sto))
4316 {
4317 lclTypeSpecNode type = sto->content.type;
4318 sort = lclTypeSpecNode2sort (type);
4319 if (!sort_mutable (sort))
4320 {
4321 errtok = lclTypeSpecNode_errorToken (type);
4322 lclerror (errtok, message ("Immutable type used in unchanged list: %q",
4323 sort_unparse (sort)));
4324 }
4325 }
4326 }
4327 } end_storeRefNodeList_elements;
4328
4329 return t;
4330}
4331
4332/*@only@*/ termNode
4333 makeSizeofTermNode (ltoken op, lclTypeSpecNode type)
4334{
4335 termNode t = (termNode) dmalloc (sizeof (*t));
4336
4337 t->name = NULL; /*< missing this >*/
4338 t->error_reported = FALSE;
4339 t->wrapped = 0;
4340 t->kind = TRM_SIZEOF;
2a6e9c30 4341 t->sort = g_sortInt;
616915dd 4342 t->literal = op;
4343 t->sizeofField = type;
4344 t->given = sort_makeNoSort ();
4345 t->possibleSorts = sortSet_new ();
4346 t->possibleOps = lslOpSet_new ();
4347 t->args = termNodeList_new ();
4348
4349 (void) sortSet_insert (t->possibleSorts, t->sort);
4350 /* nothing to check */
4351 return (t);
4352}
4353
4354/*@only@*/ cstring
4355claimNode_unparse (claimNode c)
4356{
4357 if (c != (claimNode) 0)
4358 {
4359 cstring s = message ("claims (%q)%q{\n%q",
4360 paramNodeList_unparse (c->params),
4361 varDeclarationNodeList_unparse (c->globals),
4362 lclPredicateNode_unparse (c->require));
4363
4364 if (c->body != NULL)
4365 {
4366 s = message ("%qbody {%q}\n", s, programNode_unparse (c->body));
4367 }
4368 s = message ("%q%q}\n", s, lclPredicateNode_unparse (c->ensures));
4369 return s;
4370 }
4371 return cstring_undefined;
4372}
4373
4374static void
4375WrongArity (ltoken tok, int expect, int size)
4376{
4377 lclerror (tok, message ("Expecting %d arguments but given %d", expect, size));
4378}
4379
4380static cstring
4381printTermNode2 (/*@null@*/ opFormNode op, termNodeList args, sort sort)
4382{
4383 if (op != (opFormNode) 0)
4384 {
4385 cstring s = cstring_undefined;
4386 cstring sortText;
4387 cstring sortSpace;
4388
4389 if (sort != sort_makeNoSort ())
4390 {
4391 sortText = message (": %s", cstring_fromChars (lsymbol_toChars (sort_getLsymbol (sort))));
4392 sortSpace = cstring_makeLiteral (" ");
4393 }
4394 else
4395 {
4396 sortText = cstring_undefined;
4397 sortSpace = cstring_undefined;
4398 }
4399
4400 switch (op->kind)
4401 {
4402 case OPF_IF:
4403 {
4404 int size = termNodeList_size (args);
4405
4406 if (size == 3)
4407 {
4408 s = message ("if %q then %q else %q\n",
4409 termNode_unparse (termNodeList_getN (args, 0)),
4410 termNode_unparse (termNodeList_getN (args, 1)),
4411 termNode_unparse (termNodeList_getN (args, 2)));
4412 }
4413 else
4414 {
4415 WrongArity (op->tok, 3, size);
4416 s = cstring_makeLiteral ("if __ then __ else __");
4417 }
4418 s = message ("%q%s", s, sortText);
4419 break;
4420 }
4421 case OPF_ANYOP:
4422 { /* ymtan ? */
4423 s = message ("%s %s",
4424 ltoken_getRawString (op->content.anyop),
4425 sortText);
4426 break;
4427 }
4428 case OPF_MANYOP:
4429 {
4430 int size = termNodeList_size (args);
4431
4432 if (size == 1)
4433 {
4434 s = message ("%q ", termNode_unparse (termNodeList_head (args)));
4435 }
4436 else
4437 {
4438 WrongArity (op->content.anyop, 1, size);
4439 s = cstring_makeLiteral ("__ ");
4440 }
4441 s = message ("%q%s%s", s, ltoken_getRawString (op->content.anyop),
4442 sortText);
4443 break;
4444 }
4445 case OPF_ANYOPM:
4446 {
4447 int size = termNodeList_size (args);
4448
4449 s = message ("%s ", ltoken_getRawString (op->content.anyop));
4450
4451 if (size == 1)
4452 {
4453 s = message ("%q%q", s, termNode_unparse (termNodeList_head (args)));
4454 }
4455 else
4456 {
4457 WrongArity (op->content.anyop, 1, size);
4458 s = message ("%q__", s);
4459 }
4460 s = message ("%q%s", s, sortText);
4461 break;
4462 }
4463 case OPF_MANYOPM:
4464 {
4465 int size = termNodeList_size (args);
4466
4467 if (size == 2)
4468 {
4469 s = message ("%q %s %q",
4470 termNode_unparse (termNodeList_getN (args, 0)),
4471 ltoken_getRawString (op->content.anyop),
4472 termNode_unparse (termNodeList_getN (args, 1)));
4473 }
4474 else
4475 {
4476 WrongArity (op->content.anyop, 2, size);
4477 s = message ("__ %s __", ltoken_getRawString (op->content.anyop));
4478 }
4479 s = message ("%q%s", s, sortText);
4480 break;
4481 }
4482 case OPF_MIDDLE:
4483 {
4484 int size = termNodeList_size (args);
4485 int expect = op->content.middle;
4486
4487 /* ymtan ? use { or openSym token ? */
4488
4489 if (size == expect)
4490 {
4491 s = message ("{%q}", termNodeList_unparse (args));
4492 }
4493 else
4494 {
4495 WrongArity (op->tok, expect, size);
4496 s = cstring_makeLiteral ("{ * }");
4497 }
4498
4499 s = message ("%q%s", s, sortText);
11db3170 4500 break;
616915dd 4501 }
4502 case OPF_MMIDDLE:
4503 {
4504 int size = termNodeList_size (args);
4505 int expect = op->content.middle + 1;
4506
4507 if (size == expect)
4508 {
4509 s = message ("%q{%q}",
4510 termNode_unparse (termNodeList_head (args)),
4511 termNodeList_unparseTail (args));
4512 }
4513 else
4514 {
4515 WrongArity (op->tok, expect, size);
4516 s = cstring_makeLiteral ("__ { * }");
4517 }
4518
4519 s = message ("%q%s", s, sortText);
4520 break;
4521 }
4522 case OPF_MIDDLEM:
4523 {
4524 int size = termNodeList_size (args);
4525 int expect = op->content.middle + 1;
4526
4527 if (size == expect)
4528 {
4529 termNodeList_finish (args);
4530
4531 s = message ("{%q}%s%s%q",
4532 termNodeList_unparseToCurrent (args),
4533 sortText, sortSpace,
4534 termNode_unparse (termNodeList_current (args)));
4535 }
4536 else
4537 {
4538 WrongArity (op->tok, expect, size);
4539
4540 s = message ("{ * }%s __", sortText);
4541
4542 /* used to put in extra space! evs 94-01-05 */
4543 }
4544 break;
4545 }
4546 case OPF_MMIDDLEM:
4547 {
4548 int size = termNodeList_size (args);
4549 int expect = op->content.middle + 2;
4550
4551 if (size == expect)
4552 {
4553 termNodeList_finish (args);
4554
4555 s = message ("%q {%q} %s%s%q",
4556 termNode_unparse (termNodeList_head (args)),
4557 termNodeList_unparseSecondToCurrent (args),
4558 sortText, sortSpace,
4559 termNode_unparse (termNodeList_current (args)));
4560 }
4561 else
4562 {
4563 WrongArity (op->tok, expect, size);
4564 s = message ("__ { * } %s __", sortText);
4565
4566 /* also had extra space? */
4567 }
4568 break;
4569 }
4570 case OPF_BMIDDLE:
4571 {
4572 int size = termNodeList_size (args);
4573 int expect = op->content.middle;
4574
4575 if (size == expect)
4576 {
4577 s = message ("[%q]", termNodeList_unparse (args));
4578 }
4579 else
4580 {
4581 WrongArity (op->tok, expect, size);
4582 s = cstring_makeLiteral ("[ * ]");
4583 }
4584 s = message ("%q%s", s, sortText);
4585 break;
4586 }
4587 case OPF_BMMIDDLE:
4588 {
4589 int size = termNodeList_size (args);
4590 int expect = op->content.middle + 1;
4591
4592 if (size == expect)
4593 {
4594 s = message ("%q[%q]",
4595 termNode_unparse (termNodeList_head (args)),
4596 termNodeList_unparseTail (args));
4597 }
4598 else
4599 {
4600 WrongArity (op->tok, expect, size);
4601 s = cstring_makeLiteral ("__ [ * ]");
4602 }
4603
4604 s = message ("%q%s", s, sortText);
4605 break;
4606 }
4607 case OPF_BMMIDDLEM:
4608 {
4609 int size = termNodeList_size (args);
4610 int expect = op->content.middle + 1;
4611
4612 if (size == expect)
4613 {
4614 s = message ("%q[%q] __",
4615 termNode_unparse (termNodeList_head (args)),
4616 termNodeList_unparseTail (args));
4617 }
4618 else
4619 {
4620 WrongArity (op->tok, expect, size);
4621 s = cstring_makeLiteral ("__ [ * ] __");
4622 }
4623 s = message ("%q%s", s, sortText);
4624 break;
4625 }
4626 case OPF_BMIDDLEM:
4627 {
4628 int size = termNodeList_size (args);
4629 int expect = op->content.middle + 1;
4630
4631 if (size == expect)
4632 {
4633 termNodeList_finish (args);
4634
4635 s = message ("[%q]%s%s%q",
4636 termNodeList_unparseToCurrent (args),
4637 sortText, sortSpace,
4638 termNode_unparse (termNodeList_current (args)));
4639 }
4640 else
4641 {
4642 WrongArity (op->tok, expect, size);
4643 s = cstring_makeLiteral ("[ * ] __");
4644 }
4645
4646 break;
4647 }
4648 case OPF_SELECT:
4649 { /* ymtan constant, check args ? */
4650 s = cstring_prependChar ('.', ltoken_getRawString (op->content.id));
4651 break;
4652 }
4653 case OPF_MAP:
4654 s = cstring_concat (cstring_makeLiteralTemp ("->"),
4655 ltoken_getRawString (op->content.id));
4656 break;
4657 case OPF_MSELECT:
4658 {
4659 int size = termNodeList_size (args);
4660
4661 if (size == 1)
4662 {
4663 s = message ("%q.%s", termNode_unparse (termNodeList_head (args)),
4664 ltoken_getRawString (op->content.id));
4665 }
4666 else
4667 {
4668 WrongArity (op->content.id, 1, size);
4669 s = cstring_concat (cstring_makeLiteralTemp ("__."),
4670 ltoken_getRawString (op->content.id));
4671 }
4672 break;
4673 }
4674 case OPF_MMAP:
4675 {
4676 int size = termNodeList_size (args);
4677
4678 if (size == 1)
4679 {
4680 s = message ("%q->%s", termNode_unparse (termNodeList_head (args)),
4681 ltoken_getRawString (op->content.id));
4682 }
4683 else
4684 {
4685 WrongArity (op->content.id, 1, size);
4686 s = cstring_concat (cstring_makeLiteralTemp ("__->"),
4687 ltoken_getRawString (op->content.id));
4688 }
4689 break;
4690 }
4691 }
4692
4693 cstring_free (sortSpace);
4694 cstring_free (sortText);
4695 return s;
4696 }
4697 return cstring_undefined;
4698}
4699
4700/*@only@*/ cstring
4701termNode_unparse (/*@null@*/ termNode n)
4702{
4703 cstring s = cstring_undefined;
4704 cstring back = cstring_undefined;
4705 cstring front = cstring_undefined;
4706 int count;
4707
4708 if (n != (termNode) 0)
4709 {
4710 for (count = n->wrapped; count > 0; count--)
4711 {
4712 front = cstring_appendChar (front, '(');
4713 back = cstring_appendChar (back, ')');
4714 }
4715
4716 switch (n->kind)
4717 {
4718 case TRM_LITERAL:
4719 case TRM_CONST:
4720 case TRM_VAR:
4721 case TRM_ZEROARY:
4722 s = cstring_copy (ltoken_getRawString (n->literal));
4723 break;
4724 case TRM_APPLICATION:
4725 {
4726 nameNode nn = n->name;
4727 if (nn != (nameNode) 0)
4728 {
4729 if (nn->isOpId)
4730 {
4731 s = message ("%s (%q) ",
4732 ltoken_getRawString (nn->content.opid),
4733 termNodeList_unparse (n->args));
4734 /* must we handle n->given ? skip for now */
4735 }
4736 else
4737 {
4738 s = message ("%q ", printTermNode2 (nn->content.opform, n->args, n->given));
4739 }
4740 }
4741 else
4742 {
4743 llfatalbug
4744 (message ("termNode_unparse: expect non-empty nameNode: TRM_APPLICATION: %q",
4745 nameNode_unparse (nn)));
4746 }
4747 break;
4748 }
4749 case TRM_UNCHANGEDALL:
4750 s = cstring_makeLiteral ("unchanged (all)");
4751 break;
4752 case TRM_UNCHANGEDOTHERS:
4753 s = message ("unchanged (%q)", storeRefNodeList_unparse (n->unchanged));
4754 break;
4755 case TRM_SIZEOF:
4756 s = message ("sizeof (%q)", lclTypeSpecNode_unparse (n->sizeofField));
4757 break;
4758 case TRM_QUANTIFIER:
4759 {
4760 quantifiedTermNode x = n->quantified;
4761 s = message ("%q%s%q%s",
4762 quantifierNodeList_unparse (x->quantifiers),
4763 ltoken_getRawString (x->open),
4764 termNode_unparse (x->body),
4765 ltoken_getRawString (x->close));
4766 break;
4767 }
4768 }
4769 }
4770 return (message ("%q%q%q", front, s, back));
4771}
4772
4773static void modifyNode_free (/*@null@*/ /*@only@*/ modifyNode m)
4774{
4775 if (m != (modifyNode) 0)
4776 {
4777
4778 if (m->hasStoreRefList)
4779 {
4780 storeRefNodeList_free (m->list);
4781 /*@-branchstate@*/
4782 }
4783 /*@=branchstate@*/
4784
4785 ltoken_free (m->tok);
4786 sfree (m);
4787 }
4788}
4789
4790/*@only@*/ cstring
4791modifyNode_unparse (/*@null@*/ modifyNode m)
4792{
4793 if (m != (modifyNode) 0)
4794 {
4795 if (m->hasStoreRefList)
4796 {
4797 return (message (" modifies %q; \n", storeRefNodeList_unparse (m->list)));
4798 }
4799 else
4800 {
4801 if (m->modifiesNothing)
4802 {
4803 return (cstring_makeLiteral ("modifies nothing; \n"));
4804 }
4805 else
4806 {
4807 return (cstring_makeLiteral ("modifies anything; \n"));
4808 }
4809 }
4810 }
4811 return cstring_undefined;
4812}
4813
4814/*@only@*/ cstring
4815programNode_unparse (programNode p)
4816{
4817 if (p != (programNode) 0)
4818 {
4819 cstring s = cstring_undefined;
4820 int count;
4821
4822 switch (p->kind)
4823 {
4824 case ACT_SELF:
4825 {
4826 cstring back = cstring_undefined;
4827
4828 for (count = p->wrapped; count > 0; count--)
4829 {
4830 s = cstring_appendChar (s, '(');
4831 back = cstring_appendChar (back, ')');
4832 }
4833 s = message ("%q%q%q", s, stmtNode_unparse (p->content.self), back);
4834 break;
4835 }
4836 case ACT_ITER:
4837 s = message ("*(%q)", programNodeList_unparse (p->content.args));
4838 break;
4839 case ACT_ALTERNATE:
4840 s = message ("|(%q)", programNodeList_unparse (p->content.args));
4841 break;
4842 case ACT_SEQUENCE:
4843 s = programNodeList_unparse (p->content.args);
4844 break;
4845 }
4846
4847 return s;
4848 }
4849 return cstring_undefined;
4850}
4851
4852/*@only@*/ cstring
4853stmtNode_unparse (stmtNode x)
4854{
4855 cstring s = cstring_undefined;
4856
4857 if (x != (stmtNode) 0)
4858 {
4859 if (ltoken_isValid (x->lhs))
4860 {
4861 s = cstring_concat (ltoken_getRawString (x->lhs),
4862 cstring_makeLiteralTemp (" = "));
4863 }
4864
4865 s = message ("%q%s (%q)", s,
4866 ltoken_getRawString (x->operator),
4867 termNodeList_unparse (x->args));
4868 }
4869
4870 return s;
4871}
4872
4873/*@only@*/ lslOp
4874 makelslOpNode (/*@only@*/ /*@null@*/ nameNode name,
4875 /*@dependent@*/ sigNode s)
4876{
4877 lslOp x = (lslOp) dmalloc (sizeof (*x));
4878
4879 x->name = name;
4880 x->signature = s;
4881
4882 /* enter operator info into symtab */
4883 /* if not, they may need to be renamed in LCL imports */
4884
4885 if (g_lslParsingTraits)
4886 {
4887 if (name != NULL)
4888 {
4889 symtable_enterOp (g_symtab, nameNode_copySafe (name), sigNode_copy (s));
4890 }
4891 }
4892 else
4893 {
4894 /* nameNode_free (name); */ /* YIKES! */
4895 }
4896
4897 return x;
4898}
4899
4900/*@only@*/ cstring
4901lslOp_unparse (lslOp x)
4902{
4903 char *s = mstring_createEmpty ();
4904
4905 if (x != (lslOp) 0)
4906 {
4907 s = mstring_concatFree (s, cstring_toCharsSafe (nameNode_unparse (x->name)));
4908
4909 if (x->signature != (sigNode) 0)
4910 {
4911 s = mstring_concatFree (s, cstring_toCharsSafe (sigNode_unparse (x->signature)));
4912 }
4913 }
4914
4915 return cstring_fromCharsO (s);
4916}
4917
4918static bool
4919sameOpFormNode (/*@null@*/ opFormNode n1, /*@null@*/ opFormNode n2)
4920{
4921 if (n1 == n2)
4922 return TRUE;
4923
4924 if (n1 == 0)
4925 return FALSE;
4926
4927 if (n2 == 0)
4928 return FALSE;
4929
4930 if (n1->kind == n2->kind)
4931 {
4932 switch (n1->kind)
4933 {
4934 case OPF_IF:
4935 return TRUE;
4936 case OPF_ANYOP:
4937 case OPF_MANYOP:
4938 case OPF_ANYOPM:
4939 return (ltoken_similar (n1->content.anyop, n2->content.anyop));
4940 case OPF_MANYOPM:
4941 {
4942 /* want to treat eq and = the same */
4943 return ltoken_similar (n1->content.anyop, n2->content.anyop);
4944 }
4945 case OPF_MIDDLE:
4946 case OPF_MMIDDLE:
4947 case OPF_MIDDLEM:
4948 case OPF_MMIDDLEM:
4949 /* need to check the rawText of openSym and closeSym */
4950 if ((int) n1->content.middle == (int) n2->content.middle)
4951 {
4952 if (lsymbol_equal (ltoken_getRawText (n1->tok),
4953 ltoken_getRawText (n2->tok)) &&
4954 lsymbol_equal (ltoken_getRawText (n1->close),
4955 ltoken_getRawText (n2->close)))
4956 return TRUE;
4957 }
4958 return FALSE;
4959 case OPF_BMIDDLE:
4960 case OPF_BMMIDDLE:
4961 case OPF_BMIDDLEM:
4962 case OPF_BMMIDDLEM:
4963 return ((int) n1->content.middle == (int) n2->content.middle);
4964 case OPF_SELECT:
4965 case OPF_MAP:
4966 case OPF_MSELECT:
4967 case OPF_MMAP:
4968 return (ltoken_similar (n1->content.id, n2->content.id));
4969 }
4970 }
4971 return FALSE;
4972}
4973
4974bool
4975sameNameNode (/*@null@*/ nameNode n1, /*@null@*/ nameNode n2)
4976{
4977 if (n1 == n2)
4978 return TRUE;
4979 if (n1 != (nameNode) 0 && n2 != (nameNode) 0)
4980 {
4981 if (bool_equal (n1->isOpId, n2->isOpId))
4982 {
4983 if (n1->isOpId)
4984 return (ltoken_similar (n1->content.opid, n2->content.opid));
4985 else
4986 return sameOpFormNode (n1->content.opform,
4987 n2->content.opform);
4988 }
4989 }
4990 return FALSE;
4991}
4992
4993void CTypesNode_free (/*@only@*/ /*@null@*/ CTypesNode x)
4994{
4995 if (x != NULL)
4996 {
4997 ltokenList_free (x->ctypes);
4998 sfree (x);
4999 }
5000}
5001
5002/*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode x)
5003{
5004 if (x != NULL)
5005 {
5006 CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5007 newnode->intfield = x->intfield;
5008 newnode->ctypes = ltokenList_copy (x->ctypes);
5009 newnode->sort = x->sort;
5010
5011 return newnode;
5012 }
5013 else
5014 {
5015 return NULL;
5016 }
5017}
5018
5019/*@only@*/ CTypesNode
5020 makeCTypesNode (/*@only@*/ CTypesNode ctypes, ltoken ct)
5021{
5022 /*@only@*/ CTypesNode newnode;
5023 lsymbol sortname;
5024 bits sortbits;
5025
5026 if (ctypes == (CTypesNode) NULL)
5027 {
5028 newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5029 newnode->intfield = 0;
5030 newnode->ctypes = ltokenList_new ();
5031 newnode->sort = sort_makeNoSort ();
5032 }
5033 else
5034 {
5035 newnode = ctypes;
5036 }
5037
5038 if ((ltoken_getIntField (ct) & newnode->intfield) != 0)
5039 {
5040 lclerror (ct,
5041 message
5042 ("Duplicate type specifier ignored: %s",
5043 cstring_fromChars
5044 (lsymbol_toChars
5045 (lclctype_toSortDebug (ltoken_getIntField (ct))))));
5046
5047 /* evs --- don't know how to generator this error */
5048
5049 /* Use previous value, to keep things consistent */
5050 ltoken_free (ct);
5051 return newnode;
5052 }
5053
5054 sortbits = newnode->intfield | ltoken_getIntField (ct);
5055 sortname = lclctype_toSort (sortbits);
5056
5057 if (sortname == lsymbol_fromChars ("error"))
5058 {
5059 lclerror (ct, cstring_makeLiteral ("Invalid combination of type specifiers"));
5060 }
5061 else
5062 {
5063 newnode->intfield = sortbits;
5064 }
5065
5066 ltokenList_addh (newnode->ctypes, ct);
5067
5068 /*
5069 ** Sorts are assigned after CTypesNode is created during parsing,
5070 ** see bison grammar.
5071 */
5072
5073 return newnode;
5074}
5075
5076/*@only@*/ CTypesNode
5077makeTypeSpecifier (ltoken typedefname)
5078{
5079 CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5080 typeInfo ti = symtable_typeInfo (g_symtab, ltoken_getText (typedefname));
5081
5082 newnode->intfield = 0;
5083 newnode->ctypes = ltokenList_singleton (ltoken_copy (typedefname));
5084
5085 /* if we see "bool" include bool.h header file */
5086
5087 if (ltoken_getText (typedefname) == lsymbol_bool)
5088 {
5089 lhIncludeBool ();
5090 }
5091
5092 if (typeInfo_exists (ti))
5093 {
28bf4b0b 5094 /* must we be concern about whether this type is exported by module?
5095 No. Because all typedef's are exported. No hiding supported. */
5096 /* Later, may want to keep types around too */
5097 /* 3/2/93, use underlying sort */
616915dd 5098 newnode->sort = sort_getUnderlying (ti->basedOn);
5099 }
5100 else
5101 {
5102 lclerror (typedefname, message ("Unrecognized type: %s",
5103 ltoken_getRawString (typedefname)));
5104 /* evs --- Don't know how to get this message */
28bf4b0b 5105
616915dd 5106 newnode->sort = sort_makeNoSort ();
5107 }
5108
5109 ltoken_free (typedefname);
5110 return newnode;
5111}
5112
5113bool sigNode_equal (sigNode n1, sigNode n2)
5114{
5115 /* n1 and n2 are never 0 */
5116
5117 return ((n1 == n2) ||
5118 (n1->key == n2->key &&
5119 ltoken_similar (n1->range, n2->range) &&
5120 ltokenList_equal (n1->domain, n2->domain)));
5121}
5122
5123sort
5124typeExpr2ptrSort (sort base, /*@null@*/ typeExpr t)
5125{
5126 if (t != (typeExpr) 0)
5127 {
5128 switch (t->kind)
5129 {
5130 case TEXPR_BASE:
5131 return base;
5132 case TEXPR_PTR:
5133 return typeExpr2ptrSort (sort_makePtr (ltoken_undefined, base),
5134 t->content.pointer);
5135 case TEXPR_ARRAY:
5136 return typeExpr2ptrSort (sort_makeArr (ltoken_undefined, base),
5137 t->content.array.elementtype);
5138 case TEXPR_FCN:
5139 /* map all hof types to some sort of SRT_HOF */
5140 return sort_makeHOFSort (base);
5141 }
5142 }
5143 return base;
5144}
5145
5146static sort
5147typeExpr2returnSort (sort base, /*@null@*/ typeExpr t)
5148{
5149 if (t != (typeExpr) 0)
5150 {
5151 switch (t->kind)
5152 {
5153 case TEXPR_BASE:
5154 return base;
5155 case TEXPR_PTR:
5156 return typeExpr2returnSort (sort_makePtr (ltoken_undefined, base),
5157 t->content.pointer);
5158 case TEXPR_ARRAY:
5159 return typeExpr2returnSort (sort_makeArr (ltoken_undefined, base),
5160 t->content.array.elementtype);
5161 case TEXPR_FCN:
5162 return typeExpr2returnSort (base, t->content.function.returntype);
5163 }
5164 }
5165 return base;
5166}
5167
5168sort
5169lclTypeSpecNode2sort (lclTypeSpecNode type)
5170{
5171 if (type != (lclTypeSpecNode) 0)
5172 {
5173 switch (type->kind)
5174 {
5175 case LTS_TYPE:
5176 llassert (type->content.type != NULL);
5177 return sort_makePtrN (type->content.type->sort, type->pointers);
5178 case LTS_STRUCTUNION:
5179 llassert (type->content.structorunion != NULL);
f9264521 5180 return sort_makePtrN (type->content.structorunion->sort, type->pointers);
616915dd 5181 case LTS_ENUM:
5182 llassert (type->content.enumspec != NULL);
f9264521 5183 return sort_makePtrN (type->content.enumspec->sort, type->pointers);
616915dd 5184 case LTS_CONJ:
5185 return (lclTypeSpecNode2sort (type->content.conj->a));
5186 }
5187 }
5188 return (sort_makeNoSort ());
5189}
5190
5191lsymbol
5192checkAndEnterTag (tagKind k, ltoken opttagid)
5193{
5194 /* should be tagKind, instead of int */
5195 tagInfo t;
5196 sort sort = sort_makeNoSort ();
5197
5198 if (!ltoken_isUndefined (opttagid))
5199 {
5200 switch (k)
5201 {
5202 case TAG_FWDSTRUCT:
5203 case TAG_STRUCT:
5204 sort = sort_makeStr (opttagid);
5205 break;
5206 case TAG_FWDUNION:
5207 case TAG_UNION:
5208 sort = sort_makeUnion (opttagid);
5209 break;
5210 case TAG_ENUM:
5211 sort = sort_makeEnum (opttagid);
5212 break;
5213 }
5214
5215 /* see if it is already in symbol table */
5216 t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid));
5217
5218 if (tagInfo_exists (t))
5219 {
5220 if (t->kind == TAG_FWDUNION || t->kind == TAG_FWDSTRUCT)
5221 {
5222 /* this is fine, for mutually recursive types */
5223 }
5224 else
5225 { /* this is not good, complain later */
5226 cstring s;
5227
5228 switch (k)
5229 {
5230 case TAG_ENUM:
5231 s = cstring_makeLiteral ("Enum");
5232 break;
5233 case TAG_STRUCT:
5234 case TAG_FWDSTRUCT:
5235 s = cstring_makeLiteral ("Struct");
5236 break;
5237 case TAG_UNION:
5238 case TAG_FWDUNION:
5239 s = cstring_makeLiteral ("Union");
5240 break;
5241 }
5242
5243 t->sort = sort;
5244 t->kind = k;
5245 lclerror (opttagid,
5246 message ("Tag redefined: %q %s", s,
5247 ltoken_getRawString (opttagid)));
5248
5249 }
5250
5251 ltoken_free (opttagid);
5252 }
5253 else
5254 {
5255 tagInfo newnode = (tagInfo) dmalloc (sizeof (*newnode));
5256
5257 newnode->sort = sort;
5258 newnode->kind = k;
5259 newnode->id = opttagid;
5260 newnode->imported = FALSE;
5261 newnode->content.decls = stDeclNodeList_new ();
5262
5263 (void) symtable_enterTag (g_symtab, newnode);
5264 }
5265 }
5266
5267 return sort_getLsymbol (sort);
5268}
5269
5270static sort
5271extractReturnSort (lclTypeSpecNode t, declaratorNode d)
5272{
5273 sort sort;
5274 sort = lclTypeSpecNode2sort (t);
5275 sort = typeExpr2returnSort (sort, d->type);
5276 return sort;
5277}
5278
5279void
5280signNode_free (/*@only@*/ signNode sn)
5281{
5282 sortList_free (sn->domain);
5283 ltoken_free (sn->tok);
5284 sfree (sn);
5285}
5286
5287/*@only@*/ cstring
5288signNode_unparse (signNode sn)
5289{
5290 cstring s = cstring_undefined;
5291
5292 if (sn != (signNode) 0)
5293 {
5294 s = message (": %q -> %s", sortList_unparse (sn->domain),
5295 sort_unparseName (sn->range));
5296 }
5297 return s;
5298}
5299
5300static /*@only@*/ pairNodeList
5301 globalList_toPairNodeList (globalList g)
5302{
5303 /* expect list to be globals, drop private ones */
5304 pairNodeList result = pairNodeList_new ();
5305 pairNode p;
5306 declaratorNode vdnode;
5307 lclTypeSpecNode type;
5308 sort sort;
5309 lsymbol sym;
5310 initDeclNodeList decls;
5311
5312 varDeclarationNodeList_elements (g, x)
5313 {
5314 if (x->isSpecial)
5315 {
5316 ;
5317 }
5318 else
5319 {
5320 if (x->isGlobal && !x->isPrivate)
5321 {
5322 type = x->type;
5323 decls = x->decls;
5324
5325 initDeclNodeList_elements (decls, init)
5326 {
5327 p = (pairNode) dmalloc (sizeof (*p));
5328
5329 vdnode = init->declarator;
5330 sym = ltoken_getText (vdnode->id);
5331 /* 2/21/93, not sure if it should be extractReturnSort,
5332 or some call to typeExpr2ptrSort */
5333 sort = extractReturnSort (type, vdnode);
5334 p->sort = sort_makeGlobal (sort);
5335 /* if (!sort_isArrayKind (sort)) p->sort = sort_makeObj (sort);
5336 else p->sort = sort; */
5337 /* p->name = sym; */
5338 p->tok = ltoken_copy (vdnode->id);
5339 pairNodeList_addh (result, p);
5340 } end_initDeclNodeList_elements;
5341 }
5342 }
5343 } end_varDeclarationNodeList_elements;
5344 return result;
5345}
5346
5347void
5348enteringFcnScope (lclTypeSpecNode t, declaratorNode d, globalList g)
5349{
5350 scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
5351 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5352 sort returnSort;
5353 ltoken result = ltoken_copy (ltoken_id);
5354 pairNodeList paramPairs, globals;
5355 fctInfo fi = (fctInfo) dmalloc (sizeof (*fi));
5356 signNode sign = (signNode) dmalloc (sizeof (*sign));
5357 sortList domain = sortList_new ();
e5081f8c 5358 unsigned long int key;
616915dd 5359
5360 paramPairs = extractParams (d->type);
5361 returnSort = extractReturnSort (t, d);
5362 globals = globalList_toPairNodeList (g);
5363
5364 sign->tok = ltoken_undefined;
5365 sign->range = returnSort;
5366
5367 key = MASH (0, sort_getLsymbol (returnSort));
5368
5369 pairNodeList_elements (paramPairs, p)
5370 {
5371 sortList_addh (domain, p->sort);
5372 key = MASH (key, sort_getLsymbol (p->sort));
5373 } end_pairNodeList_elements;
5374
5375 sign->domain = domain;
5376 sign->key = key;
5377
5378 /* push fcn onto symbol table stack first */
5379 fi->id = ltoken_copy (d->id);
5380 fi->export = TRUE;
5381 fi->signature = sign;
5382 fi->globals = globals;
5383
5384 (void) symtable_enterFct (g_symtab, fi);
5385
5386 /* push new fcn scope */
5387 si->kind = SPE_FCN;
5388 symtable_enterScope (g_symtab, si);
5389
5390 /* add "result" with return type to current scope */
5391 ltoken_setText (result, lsymbol_fromChars ("result"));
5392
5393 vi->id = result;
5394 vi->sort = sort_makeFormal (returnSort); /* make appropriate values */
5395 vi->kind = VRK_PARAM;
5396 vi->export = TRUE;
5397
5398 (void) symtable_enterVar (g_symtab, vi);
5399
5400 /*
5401 ** evs - 4 Mar 1995
5402 ** pust globals first (they are in outer scope)
5403 */
5404
5405 /* push onto symbol table the global variables declared in this function,
5406 together with their respective sorts */
5407
5408 pairNodeList_elements (globals, gl)
5409 {
5410 ltoken_free (vi->id);
5411 vi->id = ltoken_copy (gl->tok);
5412 vi->kind = VRK_GLOBAL;
5413 vi->sort = gl->sort;
5414 (void) symtable_enterVar (g_symtab, vi);
5415 } end_pairNodeList_elements;
5416
5417 /*
5418 ** could enter a new scope; instead, warn when variable shadows global
5419 ** that is used
5420 */
5421
5422 /*
5423 ** push onto symbol table the formal parameters of this function,
5424 ** together with their respective sorts
5425 */
5426
5427 pairNodeList_elements (paramPairs, pair)
5428 {
5429 ltoken_free (vi->id);
5430 vi->id = ltoken_copy (pair->tok);
5431 vi->sort = pair->sort;
5432 vi->kind = VRK_PARAM;
5433 (void) symtable_enterVar (g_symtab, vi);
5434 } end_pairNodeList_elements;
5435
5436 pairNodeList_free (paramPairs);
5437 varInfo_free (vi);
5438}
5439
5440void
5441enteringClaimScope (paramNodeList params, globalList g)
5442{
5443 scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
5444 pairNodeList globals;
5445 lclTypeSpecNode paramtype;
5446 typeExpr paramdecl;
5447 sort sort;
5448
5449 globals = globalList_toPairNodeList (g);
5450 /* push new claim scope */
5451 si->kind = SPE_CLAIM;
5452
5453 symtable_enterScope (g_symtab, si);
5454
5455 /* push onto symbol table the formal parameters of this function,
5456 together with their respective sorts */
5457
5458 paramNodeList_elements (params, param)
5459 {
5460 paramdecl = param->paramdecl;
5461 paramtype = param->type;
5462 if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0)
5463 {
5464 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5465
5466 sort = lclTypeSpecNode2sort (paramtype);
5467 sort = sort_makeFormal (sort);
5468 vi->sort = typeExpr2ptrSort (sort, paramdecl);
5469 vi->id = ltoken_copy (extractDeclarator (paramdecl));
5470 vi->kind = VRK_PARAM;
5471 vi->export = TRUE;
5472
5473 (void) symtable_enterVar (g_symtab, vi);
5474 varInfo_free (vi);
5475 }
5476 } end_paramNodeList_elements;
5477
5478 /* push onto symbol table the global variables declared in this function,
5479 together with their respective sorts */
5480
5481 pairNodeList_elements (globals, g2)
5482 {
5483 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5484
5485 vi->id = ltoken_copy (g2->tok);
5486 vi->kind = VRK_GLOBAL;
5487 vi->sort = g2->sort;
5488 vi->export = TRUE;
5489
5490 /* should catch duplicates in formals */
5491 (void) symtable_enterVar (g_symtab, vi);
5492 varInfo_free (vi);
5493 } end_pairNodeList_elements;
5494
5495 pairNodeList_free (globals);
5496 /* should not free it here! ltoken_free (claimId); @*/
5497}
5498
5499static /*@only@*/ pairNodeList
5500 extractParams (/*@null@*/ typeExpr te)
5501{
5502 /* extract the parameters from a function header declarator's typeExpr */
5503 sort sort;
5504 typeExpr paramdecl;
5505 paramNodeList params;
5506 lclTypeSpecNode paramtype;
5507 pairNodeList head = pairNodeList_new ();
5508 pairNode pair;
5509
5510 if (te != (typeExpr) 0)
5511 {
5512 params = typeExpr_toParamNodeList (te);
5513 if (paramNodeList_isDefined (params))
5514 {
5515 paramNodeList_elements (params, param)
5516 {
5517 paramdecl = param->paramdecl;
5518 paramtype = param->type;
5519 if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0)
5520 {
5521 pair = (pairNode) dmalloc (sizeof (*pair));
5522 sort = lclTypeSpecNode2sort (paramtype);
5523 /* 2/17/93, was sort_makeVal (sort) */
5524 sort = sort_makeFormal (sort);
5525 pair->sort = typeExpr2ptrSort (sort, paramdecl);
5526 /* pair->name = ltoken_getText (extractDeclarator (paramdecl)); */
5527 pair->tok = ltoken_copy (extractDeclarator (paramdecl));
5528 pairNodeList_addh (head, pair);
5529 }
5530 } end_paramNodeList_elements;
5531 }
5532 }
5533 return head;
5534}
5535
5536sort
5537sigNode_rangeSort (sigNode sig)
5538{
5539 if (sig == (sigNode) 0)
5540 {
5541 return sort_makeNoSort ();
5542 }
5543 else
5544 {
5545 return sort_fromLsymbol (ltoken_getText (sig->range));
5546 }
5547}
5548
5549/*@only@*/ sortList
5550 sigNode_domain (sigNode sig)
5551{
5552 sortList domain = sortList_new ();
5553
5554 if (sig == (sigNode) 0)
5555 {
5556 ;
5557 }
5558 else
5559 {
5560 ltokenList dom = sig->domain;
5561
5562 ltokenList_elements (dom, tok)
5563 {
5564 sortList_addh (domain, sort_fromLsymbol (ltoken_getText (tok)));
5565 } end_ltokenList_elements;
5566 }
5567
5568 return domain;
5569}
5570
5571opFormUnion
5572opFormUnion_createAnyOp (/*@temp@*/ ltoken t)
5573{
5574 opFormUnion u;
5575
5576 /* do not distinguish between .anyop and .id */
5577 u.anyop = t;
5578 return u;
5579}
5580
5581opFormUnion
5582opFormUnion_createMiddle (int middle)
5583{
5584 opFormUnion u;
5585
5586 u.middle = middle;
5587 return u;
5588}
5589
5590paramNode
5591markYieldParamNode (paramNode p)
5592{
5593 p->kind = PYIELD;
5594
5595 llassert (p->type != NULL);
5596 p->type->quals = qualList_add (p->type->quals, qual_createYield ());
5597
5598 return (p);
5599}
5600
5601/*@only@*/ lclTypeSpecNode
5602 lclTypeSpecNode_copySafe (lclTypeSpecNode n)
5603{
5604 lclTypeSpecNode ret = lclTypeSpecNode_copy (n);
5605
5606 llassert (ret != NULL);
5607 return ret;
5608}
5609
5610/*@null@*/ /*@only@*/ lclTypeSpecNode
5611 lclTypeSpecNode_copy (/*@null@*/ lclTypeSpecNode n)
5612{
5613 if (n != NULL)
5614 {
5615 switch (n->kind)
5616 {
5617 case LTS_CONJ:
5618 return (makeLclTypeSpecNodeConj (lclTypeSpecNode_copy (n->content.conj->a),
5619 lclTypeSpecNode_copy (n->content.conj->b)));
5620 case LTS_TYPE:
5621 return (makeLclTypeSpecNodeType (CTypesNode_copy (n->content.type)));
5622 case LTS_STRUCTUNION:
5623 return (makeLclTypeSpecNodeSU (strOrUnionNode_copy (n->content.structorunion)));
5624 case LTS_ENUM:
5625 return (makeLclTypeSpecNodeEnum (enumSpecNode_copy (n->content.enumspec)));
5626 }
5627 }
5628
5629 return NULL;
5630}
5631
5632void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode n)
5633{
5634 if (n != NULL)
5635 {
5636 switch (n->kind)
5637 {
5638 case LTS_CONJ:
5639 lclTypeSpecNode_free (n->content.conj->a);
5640 lclTypeSpecNode_free (n->content.conj->b);
5641 break;
5642 case LTS_TYPE:
5643 CTypesNode_free (n->content.type);
5644 break;
5645 case LTS_STRUCTUNION:
5646 strOrUnionNode_free (n->content.structorunion);
5647 break;
5648 case LTS_ENUM:
5649 enumSpecNode_free (n->content.enumspec);
5650 break;
5651 }
5652
5653 qualList_free (n->quals);
5654 sfree (n);
5655 }
5656}
5657
5658static /*@null@*/ opFormNode opFormNode_copy (/*@null@*/ opFormNode op)
5659{
5660 if (op != NULL)
5661 {
5662 opFormNode ret = (opFormNode) dmalloc (sizeof (*ret));
5663
5664 ret->tok = ltoken_copy (op->tok);
5665 ret->kind = op->kind;
5666 ret->content = op->content;
5667 ret->key = op->key;
5668 ret->close = ltoken_copy (op->close);
5669
5670 return ret;
5671 }
5672 else
5673 {
5674 return NULL;
5675 }
5676}
5677
5678void opFormNode_free (/*@null@*/ opFormNode op)
5679{
28bf4b0b 5680 if (op != NULL)
5681 {
5682 ltoken_free (op->tok);
5683 ltoken_free (op->close);
5684 sfree (op);
5685 }
616915dd 5686}
5687
5688void nameNode_free (nameNode n)
5689{
5690
5691 if (n != NULL)
5692 {
5693 if (!n->isOpId)
5694 {
5695 opFormNode_free (n->content.opform);
5696 }
5697
5698 sfree (n);
5699 }
5700}
5701
5702bool
5703lslOp_equal (lslOp x, lslOp y)
5704{
5705 return ((x == y) ||
5706 ((x != 0) && (y != 0) &&
5707 sameNameNode (x->name, y->name) &&
5708 sigNode_equal (x->signature, y->signature)));
5709}
5710
5711void lslOp_free (lslOp x)
5712{
5713 nameNode_free (x->name);
5714 sfree (x);
5715}
5716
5717void sigNode_free (sigNode x)
5718{
5719 if (x != NULL)
5720 {
5721 ltokenList_free (x->domain);
5722 ltoken_free (x->tok);
5723 ltoken_free (x->range);
5724 sfree (x);
5725 }
5726}
5727
5728void declaratorNode_free (/*@null@*/ /*@only@*/ declaratorNode x)
5729{
5730 if (x != NULL)
5731 {
5732 typeExpr_free (x->type);
5733 ltoken_free (x->id);
5734 sfree (x);
5735 }
5736}
5737
5738void abstBodyNode_free (/*@null@*/ /*@only@*/ abstBodyNode n)
5739{
5740 if (n != NULL)
5741 {
5742 lclPredicateNode_free (n->typeinv);
5743 fcnNodeList_free (n->fcns);
5744 ltoken_free (n->tok);
5745 sfree (n);
5746 }
5747}
5748
5749void fcnNode_free (/*@null@*/ /*@only@*/ fcnNode f)
5750{
5751 if (f != NULL)
5752 {
5753 lclTypeSpecNode_free (f->typespec);
5754 declaratorNode_free (f->declarator);
5755 globalList_free (f->globals);
5756 varDeclarationNodeList_free (f->inits);
5757 letDeclNodeList_free (f->lets);
5758 lclPredicateNode_free (f->checks);
5759 lclPredicateNode_free (f->require);
5760 lclPredicateNode_free (f->claim);
5761 lclPredicateNode_free (f->ensures);
5762 modifyNode_free (f->modify);
5763 ltoken_free (f->name);
5764 sfree (f);
5765 }
5766}
5767
5768void declaratorInvNode_free (/*@null@*/ /*@only@*/ declaratorInvNode x)
5769{
5770 if (x != NULL)
5771 {
5772 declaratorNode_free (x->declarator);
5773 abstBodyNode_free (x->body);
5774 sfree (x);
5775 }
5776}
5777
5778/*@only@*/ lslOp lslOp_copy (lslOp x)
5779{
5780 return (makelslOpNode (nameNode_copy (x->name), x->signature));
5781}
5782
5783sigNode sigNode_copy (sigNode s)
5784{
5785 llassert (s != NULL);
5786 return (makesigNode (ltoken_copy (s->tok),
5787 ltokenList_copy (s->domain),
5788 ltoken_copy (s->range)));
5789}
5790
5791/*@null@*/ nameNode nameNode_copy (/*@null@*/ nameNode n)
5792{
5793 if (n == NULL) return NULL;
5794 return nameNode_copySafe (n);
5795}
5796
5797nameNode nameNode_copySafe (nameNode n)
5798{
5799 if (n->isOpId)
5800 {
5801 return (makeNameNodeId (ltoken_copy (n->content.opid)));
5802 }
5803 else
5804 {
1b8ae690 5805 /* error should be detected by splint: forgot to copy opform! */
616915dd 5806 return (makeNameNodeForm (opFormNode_copy (n->content.opform)));
5807 }
5808}
5809
5810bool initDeclNode_isRedeclaration (initDeclNode d)
5811{
5812 return (d->declarator->isRedecl);
5813}
5814
5815void termNode_free (/*@only@*/ /*@null@*/ termNode t)
5816{
28bf4b0b 5817 if (t != NULL)
5818 {
5819 sortSet_free (t->possibleSorts);
5820 lslOpSet_free (t->possibleOps);
5821 nameNode_free (t->name);
5822 termNodeList_free (t->args);
5823 sfree (t);
5824 }
616915dd 5825}
5826
5827/*@only@*/ termNode termNode_copySafe (termNode t)
5828{
5829 termNode ret = termNode_copy (t);
5830
5831 llassert (ret != NULL);
5832 return ret;
5833}
5834
5835/*@null@*/ /*@only@*/ termNode termNode_copy (/*@null@*/ termNode t)
5836{
5837 if (t != NULL)
5838 {
5839 termNode ret = (termNode) dmalloc (sizeof (*ret));
5840
5841 ret->wrapped = t->wrapped;
5842 ret->kind = t->kind;
5843 ret->sort = t->sort;
5844 ret->given = t->given;
5845 ret->possibleSorts = sortSet_copy (t->possibleSorts);
5846 ret->error_reported = t->error_reported;
5847 ret->possibleOps = lslOpSet_copy (t->possibleOps);
5848 ret->name = nameNode_copy (t->name);
5849 ret->args = termNodeList_copy (t->args);
5850
5851 if (t->kind == TRM_LITERAL
5852 || t->kind == TRM_SIZEOF
5853 || t->kind == TRM_VAR
5854 || t->kind == TRM_CONST
5855 || t->kind == TRM_ZEROARY)
5856 {
5857 ret->literal = ltoken_copy (t->literal);
5858 }
5859
5860 if (t->kind == TRM_UNCHANGEDOTHERS)
5861 {
5862 ret->unchanged = storeRefNodeList_copy (t->unchanged);
5863 }
5864
5865 if (t->kind == TRM_QUANTIFIER)
5866 {
5867 ret->quantified = quantifiedTermNode_copy (t->quantified);
5868 }
5869
5870 if (t->kind == TRM_SIZEOF)
5871 {
5872 ret->sizeofField = lclTypeSpecNode_copySafe (t->sizeofField);
5873 }
5874
5875 return ret;
5876 }
5877 else
5878 {
5879
5880 return NULL;
5881 }
5882}
5883
5884void importNode_free (/*@only@*/ /*@null@*/ importNode x)
5885{
28bf4b0b 5886 if (x != NULL)
5887 {
5888 ltoken_free (x->val);
5889 sfree (x);
5890 }
616915dd 5891}
5892
5893void initDeclNode_free (/*@only@*/ /*@null@*/ initDeclNode x)
5894{
5895 if (x != NULL)
5896 {
5897 declaratorNode_free (x->declarator);
5898 termNode_free (x->value);
5899 sfree (x);
5900 }
5901}
5902
5903void letDeclNode_free (/*@only@*/ /*@null@*/ letDeclNode x)
5904{
5905 if (x != NULL)
5906 {
5907 lclTypeSpecNode_free (x->sortspec);
5908 termNode_free (x->term);
5909 ltoken_free (x->varid);
5910 sfree (x);
5911 }
5912}
5913
5914void pairNode_free (/*@only@*/ /*@null@*/ pairNode x)
5915{
28bf4b0b 5916 if (x != NULL)
5917 {
5918 ltoken_free (x->tok);
5919 sfree (x);
5920 }
616915dd 5921}
5922
5923/*@null@*/ paramNode paramNode_copy (/*@null@*/ paramNode p)
5924{
5925 if (p != NULL)
5926 {
5927 paramNode ret = (paramNode) dmalloc (sizeof (*ret));
5928
5929 ret->type = lclTypeSpecNode_copy (p->type);
5930 ret->paramdecl = typeExpr_copy (p->paramdecl);
5931 ret->kind = p->kind;
5932 return ret;
5933 }
5934
5935 return NULL;
5936}
5937
5938void paramNode_free (/*@only@*/ /*@null@*/ paramNode x)
5939{
5940 if (x != NULL)
5941 {
5942 lclTypeSpecNode_free (x->type);
5943 typeExpr_free (x->paramdecl);
5944 sfree (x);
5945 }
5946}
5947
5948void programNode_free (/*@only@*/ /*@null@*/ programNode x)
5949{
5950 if (x != NULL)
5951 {
5952 switch (x->kind)
5953 {
5954 case ACT_SELF: stmtNode_free (x->content.self); break;
5955 case ACT_ITER:
5956 case ACT_ALTERNATE:
5957 case ACT_SEQUENCE: programNodeList_free (x->content.args); break;
5958 BADDEFAULT;
5959 }
5960 sfree (x);
5961 }
5962}
5963
5964quantifierNode quantifierNode_copy (quantifierNode x)
5965{
5966 quantifierNode ret = (quantifierNode) dmalloc (sizeof (*ret));
5967
5968 ret->quant = ltoken_copy (x->quant);
5969 ret->vars = varNodeList_copy (x->vars);
5970 ret->isForall = x->isForall;
5971
5972 return ret;
5973}
5974
5975void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode x)
5976{
5977 if (x != NULL)
5978 {
5979 varNodeList_free (x->vars);
5980 ltoken_free (x->quant);
5981 sfree (x);
5982 }
5983}
5984
5985void replaceNode_free (/*@only@*/ /*@null@*/ replaceNode x)
5986{
5987 if (x != NULL)
5988 {
5989 if (x->isCType)
5990 {
5991 ;
5992 }
5993 else
5994 {
5995 nameNode_free (x->content.renamesortname.name);
5996 sigNode_free (x->content.renamesortname.signature);
5997 }
5998
5999 typeNameNode_free (x->typename);
6000 ltoken_free (x->tok);
6001 sfree (x);
6002 }
6003}
6004
6005storeRefNode storeRefNode_copy (storeRefNode x)
6006{
6007 storeRefNode ret = (storeRefNode) dmalloc (sizeof (*ret));
6008
6009 ret->kind = x->kind;
6010
6011 switch (x->kind)
6012 {
6013 case SRN_TERM:
6014 ret->content.term = termNode_copySafe (x->content.term);
6015 break;
6016 case SRN_OBJ: case SRN_TYPE:
6017 ret->content.type = lclTypeSpecNode_copy (x->content.type);
6018 break;
6019 case SRN_SPECIAL:
6020 ret->content.ref = sRef_copy (x->content.ref);
6021 break;
6022 }
6023
6024 return ret;
6025}
6026
6027void storeRefNode_free (/*@only@*/ /*@null@*/ storeRefNode x)
6028{
6029 if (x != NULL)
6030 {
6031 if (storeRefNode_isTerm (x))
6032 {
6033 termNode_free (x->content.term);
6034 }
6035 else if (storeRefNode_isType (x) || storeRefNode_isObj (x))
6036 {
6037 lclTypeSpecNode_free (x->content.type);
6038 }
6039 else
6040 {
6041 /* nothing to free */
6042 }
6043
6044 sfree (x);
6045 }
6046}
6047
6048stDeclNode stDeclNode_copy (stDeclNode x)
6049{
6050 stDeclNode ret = (stDeclNode) dmalloc (sizeof (*ret));
6051
6052 ret->lcltypespec = lclTypeSpecNode_copySafe (x->lcltypespec);
6053 ret->declarators = declaratorNodeList_copy (x->declarators);
6054
6055 return ret;
6056}
6057
6058void stDeclNode_free (/*@only@*/ /*@null@*/ stDeclNode x)
6059{
6060 if (x != NULL)
6061 {
6062 lclTypeSpecNode_free (x->lcltypespec);
6063 declaratorNodeList_free (x->declarators);
6064 sfree (x);
6065 }
6066}
6067
6068void traitRefNode_free (/*@only@*/ /*@null@*/ traitRefNode x)
6069{
6070 if (x != NULL)
6071 {
6072 ltokenList_free (x->traitid);
6073 renamingNode_free (x->rename);
6074 sfree (x);
6075 }
6076}
6077
6078void typeNameNode_free (/*@only@*/ /*@null@*/ typeNameNode n)
6079{
6080 if (n != NULL)
6081 {
6082 typeNamePack_free (n->typename);
6083 opFormNode_free (n->opform);
6084 sfree (n);
6085 }
6086}
6087
6088void varDeclarationNode_free (/*@only@*/ /*@null@*/ varDeclarationNode x)
6089{
6090 if (x != NULL)
6091 {
6092 if (x->isSpecial)
6093 {
6094 ;
6095 }
6096 else
6097 {
6098 lclTypeSpecNode_free (x->type);
6099 initDeclNodeList_free (x->decls);
6100 sfree (x);
6101 }
6102 }
6103}
6104
6105varNode varNode_copy (varNode x)
6106{
6107 varNode ret = (varNode) dmalloc (sizeof (*ret));
6108
6109 ret->varid = ltoken_copy (x->varid);
6110 ret->isObj = x->isObj;
6111 ret->type = lclTypeSpecNode_copySafe (x->type);
6112 ret->sort = x->sort;
6113
6114 return ret;
6115}
6116
6117void varNode_free (/*@only@*/ /*@null@*/ varNode x)
6118{
6119 if (x != NULL)
6120 {
6121 lclTypeSpecNode_free (x->type);
6122 ltoken_free (x->varid);
6123 sfree (x);
6124 }
6125}
6126
6127void stmtNode_free (/*@only@*/ /*@null@*/ stmtNode x)
6128{
6129 if (x != NULL)
6130 {
6131 ltoken_free (x->lhs);
6132 termNodeList_free (x->args);
6133 ltoken_free (x->operator);
6134 sfree (x);
6135 }
6136}
6137
6138void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode x)
6139{
6140 if (x != NULL)
6141 {
6142 if (x->is_replace)
6143 {
6144 replaceNodeList_free (x->content.replace);
6145 }
6146 else
6147 {
6148 nameAndReplaceNode_free (x->content.name);
6149 }
6150
6151 sfree (x);
6152 }
6153}
6154
6155void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode x)
6156{
6157 if (x != NULL)
6158 {
6159 typeNameNodeList_free (x->namelist);
6160 replaceNodeList_free (x->replacelist);
6161 sfree (x);
6162 }
6163}
6164
6165void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack x)
6166{
6167 if (x != NULL)
6168 {
6169 lclTypeSpecNode_free (x->type);
6170 abstDeclaratorNode_free (x->abst);
6171 sfree (x);
6172 }
6173}
6174
6175cstring interfaceNode_unparse (interfaceNode x)
6176{
6177 if (x != NULL)
6178 {
6179 switch (x->kind)
6180 {
6181 case INF_IMPORTS:
6182 return (message ("[imports] %q", importNodeList_unparse (x->content.imports)));
6183 case INF_USES:
6184 return (message ("[uses] %q", traitRefNodeList_unparse (x->content.uses)));
6185 case INF_EXPORT:
6186 return (message ("[export] %q", exportNode_unparse (x->content.export)));
6187 case INF_PRIVATE:
6188 return (message ("[private] %q", privateNode_unparse (x->content.private)));
6189 }
6190
6191 BADBRANCH;
6192 }
6193 else
6194 {
6195 return (cstring_makeLiteral ("<interface node undefined>"));
6196 }
8250fa4a 6197
6198 BADBRANCHRET (cstring_undefined);
616915dd 6199}
6200
6201void interfaceNode_free (/*@null@*/ /*@only@*/ interfaceNode x)
6202{
6203 if (x != NULL)
6204 {
6205
6206 switch (x->kind)
6207 {
6208 case INF_IMPORTS: importNodeList_free (x->content.imports); break;
6209 case INF_USES: traitRefNodeList_free (x->content.uses); break;
6210 case INF_EXPORT: exportNode_free (x->content.export); break;
6211 case INF_PRIVATE: privateNode_free (x->content.private); break;
6212 }
6213 sfree (x);
6214 }
6215}
6216
6217void exportNode_free (/*@null@*/ /*@only@*/ exportNode x)
6218{
6219 if (x != NULL)
6220 {
6221 switch (x->kind)
6222 {
6223 case XPK_CONST: constDeclarationNode_free (x->content.constdeclaration); break;
6224 case XPK_VAR: varDeclarationNode_free (x->content.vardeclaration); break;
6225 case XPK_TYPE: typeNode_free (x->content.type); break;
6226 case XPK_FCN: fcnNode_free (x->content.fcn); break;
6227 case XPK_CLAIM: claimNode_free (x->content.claim); break;
6228 case XPK_ITER: iterNode_free (x->content.iter); break;
6229 }
6230
6231 sfree (x);
6232 }
6233}
6234
6235void privateNode_free (/*@null@*/ /*@only@*/ privateNode x)
6236{
6237 if (x != NULL)
6238 {
6239 switch (x->kind)
6240 {
6241 case PRIV_CONST:
6242 constDeclarationNode_free (x->content.constdeclaration); break;
6243 case PRIV_VAR:
6244 varDeclarationNode_free (x->content.vardeclaration); break;
6245 case PRIV_TYPE:
6246 typeNode_free (x->content.type); break;
6247 case PRIV_FUNCTION:
6248 fcnNode_free (x->content.fcn); break;
6249 }
6250
6251 sfree (x);
6252 }
6253}
6254
6255void constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode x)
6256{
6257 if (x != NULL)
6258 {
6259 lclTypeSpecNode_free (x->type);
6260 initDeclNodeList_free (x->decls);
6261 sfree (x);
6262 }
6263}
6264
6265void typeNode_free (/*@only@*/ /*@null@*/ typeNode t)
6266{
6267 if (t != NULL)
6268 {
6269 switch (t->kind)
6270 {
6271 case TK_ABSTRACT: abstractNode_free (t->content.abstract); break;
6272 case TK_EXPOSED: exposedNode_free (t->content.exposed); break;
6273 case TK_UNION: taggedUnionNode_free (t->content.taggedunion); break;
6274 }
6275
6276 sfree (t);
6277 }
6278}
6279
6280void claimNode_free (/*@only@*/ /*@null@*/ claimNode x)
6281{
6282 if (x != NULL)
6283 {
6284 paramNodeList_free (x->params);
6285 globalList_free (x->globals);
6286 letDeclNodeList_free (x->lets);
6287 lclPredicateNode_free (x->require);
6288 programNode_free (x->body);
6289 lclPredicateNode_free (x->ensures);
6290 ltoken_free (x->name);
6291 sfree (x);
6292 }
6293}
6294
6295void iterNode_free (/*@only@*/ /*@null@*/ iterNode x)
6296{
6297 if (x != NULL)
6298 {
6299 paramNodeList_free (x->params);
6300 ltoken_free (x->name);
6301 sfree (x);
6302 }
6303}
6304
6305void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode x)
6306{
6307 if (x != NULL)
6308 {
6309 abstBodyNode_free (x->body);
6310 ltoken_free (x->tok);
6311 ltoken_free (x->name);
6312 sfree (x);
6313 }
6314}
6315
6316void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode x)
6317{
6318 if (x != NULL)
6319 {
6320 lclTypeSpecNode_free (x->type);
6321 declaratorInvNodeList_free (x->decls);
6322 ltoken_free (x->tok);
6323 sfree (x);
6324 }
6325}
6326
6327void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode x)
6328{
6329 if (x != NULL)
6330 {
6331 stDeclNodeList_free (x->structdecls);
6332 declaratorNode_free (x->declarator);
6333 sfree (x);
6334 }
6335}
6336
6337/*@only@*/ /*@null@*/ strOrUnionNode
6338 strOrUnionNode_copy (/*@null@*/ strOrUnionNode n)
6339{
6340 if (n != NULL)
6341 {
6342 strOrUnionNode ret = (strOrUnionNode) dmalloc (sizeof (*ret));
6343
6344 ret->kind = n->kind;
6345 ret->tok = ltoken_copy (n->tok);
6346 ret->opttagid = ltoken_copy (n->opttagid);
6347 ret->sort = n->sort;
6348 ret->structdecls = stDeclNodeList_copy (n->structdecls);
6349
6350 return ret;
6351 }
6352 else
6353 {
6354 return NULL;
6355 }
6356}
6357
6358void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode n)
6359{
6360 if (n != NULL)
6361 {
6362 stDeclNodeList_free (n->structdecls);
6363 ltoken_free (n->tok);
6364 ltoken_free (n->opttagid);
6365 sfree (n);
6366 }
6367}
6368
6369void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode x)
6370{
6371 if (x != NULL)
6372 {
6373 ltokenList_free (x->enums);
6374 ltoken_free (x->tok);
6375 ltoken_free (x->opttagid);
6376 sfree (x);
6377 }
6378}
6379
6380/*@only@*/ /*@null@*/ enumSpecNode enumSpecNode_copy (/*@null@*/ enumSpecNode x)
6381{
6382 if (x != NULL)
6383 {
6384 enumSpecNode ret = (enumSpecNode) dmalloc (sizeof (*ret));
6385
6386 ret->tok = ltoken_copy (x->tok);
6387 ret->opttagid = ltoken_copy (x->opttagid);
6388 ret->enums = ltokenList_copy (x->enums);
6389 ret->sort = x->sort;
6390
6391 return ret;
6392 }
6393 else
6394 {
6395 return NULL;
6396 }
6397}
6398
6399void lsymbol_setbool (lsymbol s)
6400{
6401 lsymbol_bool = s;
6402}
6403
6404lsymbol lsymbol_getbool ()
6405{
6406 return lsymbol_bool;
6407}
6408
6409lsymbol lsymbol_getBool ()
6410{
6411 return lsymbol_Bool;
6412}
6413
6414lsymbol lsymbol_getFALSE ()
6415{
6416 return lsymbol_FALSE;
6417}
6418
6419lsymbol lsymbol_getTRUE ()
6420{
6421 return lsymbol_TRUE;
6422}
6423
6424
git-cvsimport mirror of splint
This page took 0.951384 seconds and 5 git commands to generate.