2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
27 ** Module for building abstract syntax trees for LCL.
29 ** This module is too close to the surface syntax of LCL.
34 ** Massachusetts Institute of Technology
37 # include "splintMacros.nf"
39 # include "lslparse.h"
40 # include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
45 static lsymbol lsymbol_Bool;
46 static lsymbol lsymbol_bool;
47 static lsymbol lsymbol_TRUE;
48 static lsymbol lsymbol_FALSE;
50 static void lclPredicateNode_free (/*@only@*/ /*@null@*/ lclPredicateNode p_x) ;
51 static void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode p_x) ;
52 static void CTypesNode_free (/*@null@*/ /*@only@*/ CTypesNode p_x);
53 static /*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode p_x) /*@*/ ;
55 constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode p_x);
56 static void claimNode_free (/*@only@*/ /*@null@*/ claimNode p_x);
57 static void iterNode_free (/*@only@*/ /*@null@*/ iterNode p_x);
58 static void abstBodyNode_free (/*@only@*/ /*@null@*/ abstBodyNode p_n);
59 static void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode p_x);
60 static void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode p_x);
61 static void typeNode_free (/*@only@*/ /*@null@*/ typeNode p_t);
62 static /*@null@*/ strOrUnionNode
63 strOrUnionNode_copy (/*@null@*/ strOrUnionNode p_n) /*@*/ ;
64 static void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode p_n)
65 /*@modifies *p_n @*/ ;
67 static void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode p_x);
68 static /*@only@*/ /*@null@*/ enumSpecNode
69 enumSpecNode_copy (/*@null@*/ enumSpecNode p_x) /*@*/ ;
70 static /*@only@*/ lclTypeSpecNode
71 lclTypeSpecNode_copySafe (lclTypeSpecNode p_n) /*@*/ ;
72 static void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode p_n);
73 static void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack p_x);
74 static void opFormNode_free (/*@only@*/ /*@null@*/ opFormNode p_op);
75 static quantifiedTermNode quantifiedTermNode_copy (quantifiedTermNode p_q) /*@*/ ;
76 static void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode p_x);
77 static void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode p_x);
78 static void exportNode_free (/*@null@*/ /*@only@*/ exportNode p_x);
79 static void privateNode_free (/*@only@*/ /*@null@*/ privateNode p_x);
80 static /*@null@*/ termNode termNode_copy (/*@null@*/ termNode p_t) /*@*/ ;
82 stmtNode_free (/*@only@*/ /*@null@*/ stmtNode p_x) /*@modifies *p_x@*/ ;
83 static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr p_x) /*@*/ ;
85 static lsymbol ConditionalSymbol;
86 static lsymbol equalSymbol;
87 static lsymbol eqSymbol;
88 static lclTypeSpecNode exposedType;
90 static /*@only@*/ cstring abstDeclaratorNode_unparse (abstDeclaratorNode p_x);
91 static pairNodeList extractParams (/*@null@*/ typeExpr p_te);
92 static sort extractReturnSort (lclTypeSpecNode p_t, declaratorNode p_d);
93 static void checkAssociativity (termNode p_x, ltoken p_op);
94 static void LCLBootstrap (void);
95 static cstring printMiddle (int p_j);
96 static void paramNode_checkQualifiers (lclTypeSpecNode p_t, typeExpr p_d);
99 resetImports (cstring current)
101 lsymbolSet_free (g_currentImports);
103 g_currentImports = lsymbolSet_new (); /* equal_symbol; */
104 (void) lsymbolSet_insert (g_currentImports,
105 lsymbol_fromString (current));
111 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
116 ltokenList domain = ltokenList_new ();
119 equalSymbol = lsymbol_fromChars ("=");
120 eqSymbol = lsymbol_fromChars ("\\eq");
123 ** not: cstring_toCharsSafe (context_getBoolName ())
124 ** we use the hard wired "bool" name.
127 lsymbol_bool = lsymbol_fromChars ("bool");
128 lsymbol_Bool = lsymbol_fromChars ("Bool");
130 lsymbol_TRUE = lsymbol_fromChars ("TRUE");
131 lsymbol_FALSE = lsymbol_fromChars ("FALSE");
133 ConditionalSymbol = lsymbol_fromChars ("if__then__else__");
135 /* generate operators for
136 ** __ \not, __ \implies __ , __ \and __, __ \or __
139 range = ltoken_create (simpleId, lsymbol_bool);
140 dom = ltoken_create (simpleId, lsymbol_bool);
142 ltokenList_addh (domain, ltoken_copy (dom));
144 domain2 = ltokenList_copy (domain); /* moved this here (before release) */
146 sign = makesigNode (ltoken_undefined, domain, ltoken_copy (range));
148 opform = makeOpFormNode (ltoken_undefined, OPF_ANYOPM,
149 opFormUnion_createAnyOp (ltoken_not),
151 nn = makeNameNodeForm (opform);
152 symtable_enterOp (g_symtab, nn, sign);
154 ltokenList_addh (domain2, dom);
156 sign = makesigNode (ltoken_undefined, domain2, range);
158 opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM,
159 opFormUnion_createAnyOp (ltoken_and),
162 nn = makeNameNodeForm (opform);
163 symtable_enterOp (g_symtab, nn, sigNode_copy (sign));
165 opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM,
166 opFormUnion_createAnyOp (ltoken_or),
169 nn = makeNameNodeForm (opform);
170 symtable_enterOp (g_symtab, nn, sigNode_copy (sign));
172 opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM,
173 opFormUnion_createAnyOp (ltoken_implies),
175 nn = makeNameNodeForm (opform);
176 symtable_enterOp (g_symtab, nn, sign);
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 */
184 ti->id = ltoken_createType (LLT_TYPEDEF_NAME, SID_TYPE, lsymbol_fromChars ("float"));
186 ti->modifiable = FALSE;
187 ti->abstract = FALSE;
188 ti->export = FALSE; /* this is implicit, not exported */
189 ti->basedOn = sort_float;
190 symtable_enterType (g_symtab, ti);
194 declareForwardType (declaratorNode declare)
196 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
200 typedefname = ltoken_getText (declare->id);
201 ti->id = ltoken_copy (declare->id);
203 ltoken_setCode (ti->id, LLT_TYPEDEF_NAME);
204 ltoken_setIdType (ti->id, SID_TYPE);
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);
213 symtable_enterType (g_symtab, ti);
216 void LCLBuiltins (void)
218 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
219 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
221 /* immutable type bool;
223 constant bool FALSE = false;
224 constant bool TRUE = true; */
226 /* the following defines the builtin LSL sorts and operators */
229 /* now LCL builtin proper */
230 /* do "immutable type bool;" */
232 ti->id = ltoken_copy (ltoken_bool);
234 ltoken_setCode (ti->id, LLT_TYPEDEF_NAME);
235 ltoken_setIdType (ti->id, SID_TYPE);
237 ti->modifiable = FALSE;
239 ti->basedOn = sort_bool;
240 ti->export = FALSE; /* this wasn't set (detected by Splint) */
241 symtable_enterType (g_symtab, ti);
243 /* do "constant bool FALSE = false;" */
244 vi->id = ltoken_createType (simpleId, SID_VAR, lsymbol_fromChars ("FALSE"));
246 vi->kind = VRK_CONST;
247 vi->sort = sort_bool;
250 (void) symtable_enterVar (g_symtab, vi);
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);
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.
277 s = sort_makeImmutable (ltoken_undefined, lsymbol_bool);
278 range = ltoken_create (simpleId, lsymbol_bool);
279 sign = makesigNode (ltoken_undefined, ltokenList_new (), range);
281 nn1 = (nameNode) dmalloc (sizeof (*nn1));
284 nn1->content.opid = ltoken_create (simpleId, lsymbol_fromChars ("true"));
286 symtable_enterOp (g_symtab, nn1, sign);
288 nn2 = (nameNode) dmalloc (sizeof (*nn2));
290 nn2->content.opid = ltoken_create (simpleId, lsymbol_fromChars ("false"));
292 symtable_enterOp (g_symtab, nn2, sigNode_copy (sign));
296 consInterfaceNode (/*@only@*/ interfaceNode n, /*@returned@*/ interfaceNodeList ns)
298 /* n is never empty, but ns may be empty */
299 interfaceNodeList_addl (ns, n);
303 /*@only@*/ interfaceNode
304 makeInterfaceNodeImports (/*@only@*/ importNodeList x)
306 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
307 lsymbol importSymbol;
309 i->kind = INF_IMPORTS;
310 i->content.imports = x; /* an importNodeList */
312 importNodeList_elements (x, imp)
314 importSymbol = ltoken_getRawText (imp->val);
316 if (lsymbolSet_member (g_currentImports, importSymbol))
319 message ("Circular imports: %s",
320 cstring_fromChars (lsymbol_toChars (importSymbol))));
324 processImport (importSymbol, imp->val, imp->kind);
326 } end_importNodeList_elements;
328 lhOutLine (cstring_undefined);
332 /*@only@*/ interfaceNode
333 makeInterfaceNodeUses (/*@only@*/ traitRefNodeList x)
335 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
339 /* read in LSL traits */
344 /*@only@*/ interfaceNode
345 interfaceNode_makeConst (/*@only@*/ constDeclarationNode x)
347 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
348 exportNode e = (exportNode) dmalloc (sizeof (*e));
351 e->content.constdeclaration = x;
352 i->kind = INF_EXPORT;
353 i->content.export = e;
358 /*@only@*/ interfaceNode
359 interfaceNode_makeVar (/*@only@*/ varDeclarationNode x)
361 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
362 exportNode e = (exportNode) dmalloc (sizeof (*e));
365 e->content.vardeclaration = x;
366 i->kind = INF_EXPORT;
367 i->content.export = e;
369 if (context_msgLh ())
371 lhOutLine (lhVarDecl (x->type, x->decls, x->qualifier));
377 /*@only@*/ interfaceNode
378 interfaceNode_makeType (/*@only@*/ typeNode x)
380 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
381 exportNode e = (exportNode) dmalloc (sizeof (*e));
384 i->kind = INF_EXPORT;
385 i->content.export = e;
387 if (context_msgLh ())
390 lhOutLine (lhType (x));
396 /*@only@*/ interfaceNode
397 interfaceNode_makeFcn (/*@only@*/ fcnNode x)
399 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
400 exportNode e = (exportNode) dmalloc (sizeof (*e));
404 i->kind = INF_EXPORT;
405 i->content.export = e;
407 if (context_msgLh ())
409 llassert (x->typespec != NULL);
410 llassert (x->declarator != NULL);
412 lhOutLine (lhFunction (x->typespec, x->declarator));
418 /*@only@*/ interfaceNode
419 interfaceNode_makeClaim (/*@only@*/ claimNode x)
421 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
422 exportNode e = (exportNode) dmalloc (sizeof (*e));
425 e->content.claim = x;
426 i->kind = INF_EXPORT;
427 i->content.export = e;
431 /*@only@*/ interfaceNode
432 interfaceNode_makeIter (/*@only@*/ iterNode x)
434 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
435 exportNode e = (exportNode) dmalloc (sizeof (*e));
439 i->kind = INF_EXPORT;
440 i->content.export = e;
444 /*@only@*/ interfaceNode
445 interfaceNode_makePrivConst (/*@only@*/ constDeclarationNode x)
447 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
448 privateNode e = (privateNode) dmalloc (sizeof (*e));
450 e->kind = PRIV_CONST;
451 e->content.constdeclaration = x;
452 i->kind = INF_PRIVATE;
453 i->content.private = e;
457 /*@only@*/ interfaceNode
458 interfaceNode_makePrivVar (/*@only@*/ varDeclarationNode x)
460 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
461 privateNode e = (privateNode) dmalloc (sizeof (*e));
464 e->content.vardeclaration = x;
465 i->kind = INF_PRIVATE;
466 i->content.private = e;
470 /*@only@*/ interfaceNode
471 interfaceNode_makePrivType (/*@only@*/ typeNode x)
473 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
474 privateNode e = (privateNode) dmalloc (sizeof (*e));
478 i->kind = INF_PRIVATE;
479 i->content.private = e;
483 /*@only@*/ interfaceNode
484 interfaceNode_makePrivFcn (/*@only@*/ fcnNode x)
486 interfaceNode i = (interfaceNode) dmalloc (sizeof (*i));
487 privateNode e = (privateNode) dmalloc (sizeof (*e));
490 ** bug detected by enum checking
491 ** e->kind = XPK_FCN;
494 e->kind = PRIV_FUNCTION;
496 i->kind = INF_PRIVATE;
497 i->content.private = e;
502 exportNode_unparse (exportNode n)
504 if (n != (exportNode) 0)
511 constDeclarationNode_unparse (n->content.constdeclaration)));
515 varDeclarationNode_unparse (n->content.vardeclaration)));
517 return (message ("%q\n", typeNode_unparse (n->content.type)));
519 return (fcnNode_unparse (n->content.fcn));
521 return (claimNode_unparse (n->content.claim));
523 return (iterNode_unparse (n->content.iter));
525 llfatalbug (message ("exportNode_unparse: unknown kind: %d", (int) n->kind));
528 return cstring_undefined;
532 privateNode_unparse (privateNode n)
534 if (n != (privateNode) 0)
539 return (constDeclarationNode_unparse (n->content.constdeclaration));
541 return (varDeclarationNode_unparse (n->content.vardeclaration));
543 return (typeNode_unparse (n->content.type));
545 return (fcnNode_unparse (n->content.fcn));
547 llfatalbug (message ("privateNode_unparse: unknown kind: %d",
551 return cstring_undefined;
554 void lclPredicateNode_free (/*@null@*/ /*@only@*/ lclPredicateNode x)
558 termNode_free (x->predicate);
559 ltoken_free (x->tok);
564 static /*@only@*/ cstring
565 lclPredicateNode_unparse (/*@null@*/ lclPredicateNode p) /*@*/
567 if (p != (lclPredicateNode) 0)
569 cstring st = cstring_undefined;
574 st = cstring_makeLiteral (" requires ");
577 st = cstring_makeLiteral (" checks ");
580 st = cstring_makeLiteral (" ensures ");
583 st = cstring_makeLiteral (" claims ");
586 st = cstring_makeLiteral ("constraint ");
589 st = cstring_makeLiteral ("initially ");
594 llfatalbug (message ("lclPredicateNode_unparse: unknown kind: %d",
597 return (message ("%q%q;\n", st, termNode_unparse (p->predicate)));
599 return cstring_undefined;
603 ltoken_similar (ltoken t1, ltoken t2)
605 lsymbol sym1 = ltoken_getText (t1);
606 lsymbol sym2 = ltoken_getText (t2);
613 if ((sym1 == eqSymbol && sym2 == equalSymbol) ||
614 (sym2 == eqSymbol && sym1 == equalSymbol))
619 if ((sym1 == lsymbol_bool && sym2 == lsymbol_Bool) ||
620 (sym2 == lsymbol_bool && sym1 == lsymbol_Bool))
629 iterNode_unparse (/*@null@*/ iterNode i)
631 if (i != (iterNode) 0)
633 return (message ("iter %s %q", ltoken_unparse (i->name),
634 paramNodeList_unparse (i->params)));
636 return cstring_undefined;
641 fcnNode_unparse (/*@null@*/ fcnNode f)
643 if (f != (fcnNode) 0)
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)));
656 return cstring_undefined;
660 varDeclarationNode_unparse (/*@null@*/ varDeclarationNode x)
662 if (x != (varDeclarationNode) 0)
668 return (sRef_unparse (x->sref));
672 switch (x->qualifier)
675 st = cstring_undefined;
678 st = cstring_makeLiteral ("const ");
681 st = cstring_makeLiteral ("volatile ");
686 st = message ("%q%q %q", st, lclTypeSpecNode_unparse (x->type),
687 initDeclNodeList_unparse (x->decls));
692 return cstring_undefined;
696 typeNode_unparse (/*@null@*/ typeNode t)
698 if (t != (typeNode) 0)
703 return (abstractNode_unparse (t->content.abstract));
705 return (exposedNode_unparse (t->content.exposed));
707 return (taggedUnionNode_unparse (t->content.taggedunion));
709 llfatalbug (message ("typeNode_unparse: unknown kind: %d", (int)t->kind));
712 return cstring_undefined;
716 constDeclarationNode_unparse (/*@null@*/ constDeclarationNode x)
718 if (x != (constDeclarationNode) 0)
720 return (message ("constant %q %q", lclTypeSpecNode_unparse (x->type),
721 initDeclNodeList_unparse (x->decls)));
724 return cstring_undefined;
727 /*@only@*/ storeRefNode
728 makeStoreRefNodeTerm (/*@only@*/ termNode t)
730 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
737 /*@only@*/ storeRefNode
738 makeStoreRefNodeType (/*@only@*/ lclTypeSpecNode t, bool isObj)
740 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
742 x->kind = isObj ? SRN_OBJ : SRN_TYPE;
748 makeStoreRefNodeInternal (void)
750 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
752 x->kind = SRN_SPECIAL;
753 x->content.ref = sRef_makeInternalState ();
758 makeStoreRefNodeSystem (void)
760 storeRefNode x = (storeRefNode) dmalloc (sizeof (*x));
762 x->kind = SRN_SPECIAL;
763 x->content.ref = sRef_makeSystemState ();
767 /*@only@*/ modifyNode
768 makeModifyNodeSpecial (/*@only@*/ ltoken t, bool modifiesNothing)
770 modifyNode x = (modifyNode) dmalloc (sizeof (*x));
773 x->modifiesNothing = modifiesNothing;
774 x->hasStoreRefList = FALSE;
778 /*@only@*/ modifyNode
779 makeModifyNodeRef (/*@only@*/ ltoken t, /*@only@*/ storeRefNodeList y)
781 modifyNode x = (modifyNode) dmalloc (sizeof (*x));
785 x->hasStoreRefList = TRUE;
786 x->modifiesNothing = FALSE;
788 /* check that all storeRef's are modifiable */
790 storeRefNodeList_elements (y, sr)
792 if (storeRefNode_isTerm (sr))
794 sort = sr->content.term->sort;
796 if (!sort_mutable (sort) && sort_isValidSort (sort))
798 ltoken errtok = termNode_errorToken (sr->content.term);
800 message ("Term denoting immutable object used in modifies list: %q",
801 termNode_unparse (sr->content.term)));
806 if (!storeRefNode_isSpecial (sr))
808 sort = lclTypeSpecNode2sort (sr->content.type);
810 if (storeRefNode_isObj (sr))
812 sort = sort_makeObj (sort);
815 if (!sort_mutable (sort))
817 ltoken errtok = lclTypeSpecNode_errorToken (sr->content.type);
819 message ("Immutable type used in modifies list: %q",
820 sort_unparse (sort)));
824 } end_storeRefNodeList_elements;
828 /*@observer@*/ ltoken
829 termNode_errorToken (/*@null@*/ termNode n)
831 if (n != (termNode) 0)
836 case TRM_UNCHANGEDALL:
837 case TRM_UNCHANGEDOTHERS:
841 case TRM_ZEROARY: /* also the default kind, when no in symbol table */
844 return n->quantified->open;
845 case TRM_APPLICATION:
850 return n->name->content.opid;
854 llassert (n->name->content.opform != NULL);
855 return n->name->content.opform->tok;
860 return ltoken_undefined;
864 return ltoken_undefined;
867 /*@observer@*/ ltoken
868 nameNode_errorToken (/*@null@*/ nameNode nn)
870 if (nn != (nameNode) 0)
874 return nn->content.opid;
878 if (nn->content.opform != NULL)
880 return nn->content.opform->tok;
885 return ltoken_undefined;
888 /*@observer@*/ ltoken
889 lclTypeSpecNode_errorToken (/*@null@*/ lclTypeSpecNode t)
891 if (t != (lclTypeSpecNode) 0)
897 llassert (t->content.type != NULL);
899 if (ltokenList_empty (t->content.type->ctypes))
902 return (ltokenList_head (t->content.type->ctypes));
904 case LTS_STRUCTUNION:
905 llassert (t->content.structorunion != NULL);
906 return t->content.structorunion->tok;
908 llassert (t->content.enumspec != NULL);
909 return t->content.enumspec->tok;
911 return (lclTypeSpecNode_errorToken (t->content.conj->a));
915 return ltoken_undefined;
919 sort_member_modulo_cstring (sort s, /*@null@*/ termNode t)
922 if (t != (termNode) 0)
924 if (t->kind == TRM_LITERAL)
925 { /* allow multiple types */
928 sortSet_elements (t->possibleSorts, el)
930 if (sort_compatible_modulo_cstring (s, el))
934 } end_sortSet_elements;
936 sn = sort_lookup (s);
938 if (sn->kind == SRT_PTR)
940 char *lit = lsymbol_toChars (ltoken_getText (t->literal));
946 if (sscanf (lit, "%ld", &val) == 1)
948 if (val == 0) return TRUE;
957 return sort_compatible_modulo_cstring (s, t->sort);
963 /*@only@*/ letDeclNode
964 makeLetDeclNode (ltoken varid, /*@only@*/ /*@null@*/ lclTypeSpecNode t,
965 /*@only@*/ termNode term)
967 letDeclNode x = (letDeclNode) dmalloc (sizeof (*x));
968 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
972 if (t != (lclTypeSpecNode) 0)
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)
981 errtok = termNode_errorToken (term);
983 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
984 /* sprintf (ERRMSG, "expect `%s' type but given term has `%s' type",
985 sort_unparse (s), sort_unparse (termsort)); */
988 message ("Let declaration expects type %q", sort_unparse (s)));
989 /* evs --- don't know how to generated this message or what it means? */
996 /* assign variable its type and sort, store in symbol table */
997 vi->id = ltoken_copy (varid);
1002 (void) symtable_enterVar (g_symtab, vi);
1008 x->sort = sort_makeNoSort ();
1013 /*@only@*/ programNode
1014 makeProgramNodeAction (/*@only@*/ programNodeList x, actionKind k)
1016 programNode n = (programNode) dmalloc (sizeof (*n));
1019 n->content.args = x;
1023 /*@only@*/ programNode
1024 makeProgramNode (/*@only@*/ stmtNode x)
1026 programNode n = (programNode) dmalloc (sizeof (*n));
1030 n->content.self = x;
1035 makeAbstractTypeNode (/*@only@*/ abstractNode x)
1037 typeNode n = (typeNode) dmalloc (sizeof (*n));
1039 n->kind = TK_ABSTRACT;
1040 n->content.abstract = x;
1046 makeExposedTypeNode (/*@only@*/ exposedNode x)
1048 typeNode n = (typeNode) dmalloc (sizeof (*n));
1050 n->kind = TK_EXPOSED;
1051 n->content.exposed = x;
1056 ** evs added 8 Sept 1993
1059 /*@only@*/ importNode
1060 importNode_makePlain (/*@only@*/ ltoken t)
1062 importNode imp = (importNode) dmalloc (sizeof (*imp));
1064 imp->kind = IMPPLAIN;
1069 /*@only@*/ importNode
1070 importNode_makeBracketed (/*@only@*/ ltoken t)
1072 importNode imp = (importNode) dmalloc (sizeof (*imp));
1074 imp->kind = IMPBRACKET;
1079 static cstring extractQuote (/*@only@*/ cstring s)
1081 size_t len = cstring_length (s);
1082 char *sc = cstring_toCharsSafe (s);
1086 *(sc + len - 1) = '\0';
1087 t = cstring_fromChars (mstring_copy (sc + 1));
1092 /*@only@*/ importNode
1093 importNode_makeQuoted (/*@only@*/ ltoken t)
1095 importNode imp = (importNode) dmalloc (sizeof (*imp));
1096 cstring q = extractQuote (cstring_copy (ltoken_getRawString (t)));
1098 imp->kind = IMPQUOTE;
1100 ltoken_setRawText (t, lsymbol_fromString (q));
1109 ** check that is it '<' and '>'
1110 ** should probably be in a different file?
1113 static void cylerror (/*@only@*/ char *s)
1120 checkBrackets (ltoken lb, ltoken rb)
1122 /* no attempt at error recovery...not really necessary */
1125 tname = ltoken_getRawString (lb);
1127 if (!cstring_equalLit (tname, "<"))
1129 cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname)));
1132 tname = ltoken_getRawString (rb);
1134 if (!cstring_equalLit (tname, ">"))
1136 cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname)));
1140 /*@only@*/ traitRefNode
1141 makeTraitRefNode (/*@only@*/ ltokenList fl, /*@only@*/ renamingNode r)
1143 traitRefNode n = (traitRefNode) dmalloc (sizeof (*n));
1151 ** printLeaves: no commas
1154 static /*@only@*/ cstring
1155 printLeaves (ltokenList f)
1157 bool firstone = TRUE;
1158 cstring s = cstring_undefined;
1160 ltokenList_elements (f, i)
1164 s = cstring_copy (ltoken_unparse (i));
1169 s = message ("%q %s", s, ltoken_unparse (i));
1171 } end_ltokenList_elements;
1178 printLeaves2 (ltokenList f)
1180 return (ltokenList_unparse (f));
1184 printRawLeaves2 (ltokenList f)
1187 cstring s = cstring_undefined;
1189 ltokenList_elements (f, i)
1193 s = message ("%s", ltoken_getRawString (i));
1197 s = message ("%q, %s", s, ltoken_getRawString (i));
1198 } end_ltokenList_elements;
1203 /*@only@*/ renamingNode
1204 makeRenamingNode (/*@only@*/ typeNameNodeList n, /*@only@*/ replaceNodeList r)
1206 renamingNode ren = (renamingNode) dmalloc (sizeof (*ren));
1208 if (typeNameNodeList_empty (n))
1210 ren->is_replace = TRUE;
1211 ren->content.replace = r;
1212 typeNameNodeList_free (n);
1216 nameAndReplaceNode nr = (nameAndReplaceNode) dmalloc (sizeof (*nr));
1217 nr->replacelist = r;
1219 ren->is_replace = FALSE;
1220 ren->content.name = nr;
1227 renamingNode_unparse (/*@null@*/ renamingNode x)
1229 if (x != (renamingNode) 0)
1233 return (replaceNodeList_unparse (x->content.replace));
1237 return (message ("%q%q", typeNameNodeList_unparse (x->content.name->namelist),
1238 replaceNodeList_unparse (x->content.name->replacelist)));
1241 return cstring_undefined;
1244 /*@only@*/ replaceNode
1245 makeReplaceNameNode (ltoken t, typeNameNode tn, nameNode nn)
1247 replaceNode r = (replaceNode) dmalloc (sizeof (*r));
1252 r->content.renamesortname.name = nn;
1253 r->content.renamesortname.signature = (sigNode) NULL;
1258 /*@only@*/ replaceNode
1259 makeReplaceNode (ltoken t, typeNameNode tn,
1260 bool is_ctype, ltoken ct,
1261 nameNode nn, sigNode sn)
1263 replaceNode r = (replaceNode) dmalloc (sizeof (*r));
1266 r->isCType = is_ctype;
1271 r->content.ctype = ct;
1277 r->content.renamesortname.name = nn;
1278 r->content.renamesortname.signature = sn;
1286 replaceNode_unparse (/*@null@*/ replaceNode x)
1288 if (x != (replaceNode) 0)
1292 st = message ("%q for ", typeNameNode_unparse (x->typename));
1296 st = message ("%q%s", st, ltoken_getRawString (x->content.ctype));
1300 st = message ("%q%q%q", st, nameNode_unparse (x->content.renamesortname.name),
1301 sigNode_unparse (x->content.renamesortname.signature));
1305 return cstring_undefined;
1309 makeNameNodeForm (/*@only@*/ /*@null@*/ opFormNode opform)
1311 nameNode nn = (nameNode) dmalloc (sizeof (*nn));
1314 nn->content.opform = opform;
1320 makeNameNodeId (/*@only@*/ ltoken opid)
1322 nameNode nn = (nameNode) dmalloc (sizeof (*nn));
1325 ** current LSL -syms output bug produces "if_then_else_" rather
1326 ** than 6 separate tokens
1329 if (ltoken_getText (opid) == ConditionalSymbol)
1331 opFormNode opform = makeOpFormNode (ltoken_undefined, OPF_IF,
1332 opFormUnion_createMiddle (0),
1335 nn->content.opform = opform;
1341 nn->content.opid = opid;
1348 nameNode_unparse (/*@null@*/ nameNode n)
1350 if (n != (nameNode) 0)
1354 return (cstring_copy (ltoken_getRawString (n->content.opid))); /*!!!*/
1358 return (opFormNode_unparse (n->content.opform));
1361 return cstring_undefined;
1365 makesigNode (ltoken t, /*@only@*/ ltokenList domain, ltoken range)
1367 sigNode s = (sigNode) dmalloc (sizeof (*s));
1371 ** Assign a hash key here to speed up lookup of operators.
1377 key = MASH (0, ltoken_getText (range));
1379 ltokenList_elements (domain, id)
1381 lsymbol sym = ltoken_getText (id);
1382 key = MASH (key, sym);
1383 } end_ltokenList_elements;
1389 cstring sigNode_unparse (/*@null@*/ sigNode n)
1391 if (n != (sigNode) 0)
1393 return (message (":%q -> %s", printLeaves2 (n->domain),
1394 ltoken_unparse (n->range)));
1397 return cstring_undefined;
1400 void sigNode_markOwned (sigNode n)
1402 sfreeEventually (n);
1406 sigNode_unparseText (/*@null@*/ sigNode n)
1408 if (n != (sigNode) 0)
1410 return (message ("%q -> %s", printLeaves2 (n->domain),
1411 ltoken_unparse (n->range)));
1413 return cstring_undefined;
1417 opFormNode2key (opFormNode op, opFormKind k)
1424 /* OPF_IF is the first enum, so it's 0 */
1427 key = MASH (k, k + 1);
1435 { /* treat eq and = the same */
1436 lsymbol sym = ltoken_getText (op->content.anyop);
1438 if (sym == equalSymbol)
1440 key = MASH (k, eqSymbol);
1444 key = MASH (k, ltoken_getText (op->content.anyop));
1456 key = MASH (k, op->content.middle);
1457 key = MASH (key, ltoken_getRawText (op->tok));
1463 key = MASH (k, ltoken_getRawText (op->content.id));
1472 /*@only@*/ opFormNode
1473 makeOpFormNode (ltoken t, opFormKind k, opFormUnion u,
1476 opFormNode n = (opFormNode) dmalloc (sizeof (*n));
1477 unsigned int key = 0;
1480 ** Assign a hash key here to speed up lookup of operators.
1491 n->content.middle = 0;
1492 /* OPF_IF is the first enum, so it's 0 */
1493 key = MASH /*@+enumint@*/ (k, k + 1) /*@=enumint@*/;
1499 { /* treat eq and = the same */
1500 lsymbol sym = ltoken_getText (u.anyop);
1502 if (sym == equalSymbol)
1504 key = MASH (k, eqSymbol);
1508 key = MASH (k, ltoken_getText (u.anyop));
1523 key = MASH (k, u.middle);
1524 key = MASH (key, ltoken_getRawText (t));
1530 key = MASH (k, ltoken_getRawText (u.id));
1535 llbug (message ("makeOpFormNode: unknown opFormKind: %d", (int) k));
1542 static cstring printMiddle (int j)
1545 char *s = mstring_createEmpty ();
1547 for (i = j; i >= 1; i--)
1549 s = mstring_concatFree1 (s, "__");
1553 s = mstring_concatFree1 (s, ", ");
1557 return cstring_fromCharsO (s);
1561 opFormNode_unparse (/*@null@*/ opFormNode n)
1563 if (n != (opFormNode) 0)
1568 return (cstring_makeLiteral ("if __ then __ else __ "));
1570 return (cstring_copy (ltoken_getRawString (n->content.anyop)));
1572 return (message ("__ %s", ltoken_getRawString (n->content.anyop)));
1574 return (message ("%s __ ", ltoken_getRawString (n->content.anyop)));
1576 return (message ("__ %s __ ", ltoken_getRawString (n->content.anyop)));
1578 return (message ("%s %q %s",
1579 ltoken_getRawString (n->tok),
1580 printMiddle (n->content.middle),
1581 ltoken_getRawString (n->close)));
1583 return (message ("__ %s %q %s",
1584 ltoken_getRawString (n->tok),
1585 printMiddle (n->content.middle),
1586 ltoken_getRawString (n->close)));
1588 return (message ("%s %q %s __",
1589 ltoken_getRawString (n->tok),
1590 printMiddle (n->content.middle),
1591 ltoken_getRawString (n->close)));
1593 return (message ("__ %s%q %s __",
1594 ltoken_getRawString (n->tok),
1595 printMiddle (n->content.middle),
1596 ltoken_getRawString (n->close)));
1598 return (message ("[%q]", printMiddle (n->content.middle)));
1600 return (message ("__ [%q]", printMiddle (n->content.middle)));
1602 return (message ("[%q] __", printMiddle (n->content.middle)));
1604 return (message ("__ [%q] __", printMiddle (n->content.middle)));
1606 return (message (" \\select %s", ltoken_getRawString (n->content.id)));
1608 return (message (" \\field_arrow%s", ltoken_getRawString (n->content.id)));
1610 return (message ("__ \\select %s", ltoken_getRawString (n->content.id)));
1612 return (message ("__ \\field_arrow %s", ltoken_getRawString (n->content.id)));
1614 llfatalbug (message ("opFormNodeUnparse: unknown kind: %d",
1618 return cstring_undefined;
1621 /*@only@*/ typeNameNode
1622 makeTypeNameNode (bool isObj, lclTypeSpecNode t, abstDeclaratorNode n)
1624 typeNameNode tn = (typeNameNode) dmalloc (sizeof (*tn));
1625 typeNamePack p = (typeNamePack) dmalloc (sizeof (*p));
1627 tn->isTypeName = TRUE;
1631 tn->opform = (opFormNode) 0;
1636 /*@only@*/ typeNameNode
1637 makeTypeNameNodeOp (opFormNode n)
1639 typeNameNode t = (typeNameNode) dmalloc (sizeof (*t));
1640 t->typename = (typeNamePack) 0;
1642 t->isTypeName = FALSE;
1647 typeNameNode_unparse (/*@null@*/ typeNameNode n)
1649 if (n != (typeNameNode) 0)
1653 cstring st = cstring_undefined;
1654 typeNamePack p = n->typename;
1656 llassert (p != NULL);
1659 st = cstring_makeLiteral ("obj ");
1661 return (message ("%q%q%q", st, lclTypeSpecNode_unparse (p->type),
1662 abstDeclaratorNode_unparse (p->abst)));
1666 return (opFormNode_unparse (n->opform));
1668 return cstring_undefined;
1671 /*@only@*/ lclTypeSpecNode
1672 makeLclTypeSpecNodeConj (/*@null@*/ lclTypeSpecNode a, /*@null@*/ lclTypeSpecNode b)
1674 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1677 n->pointers = pointers_undefined;
1678 n->quals = qualList_new ();
1679 n->content.conj = (lclconj) dmalloc (sizeof (*n->content.conj));
1680 n->content.conj->a = a;
1681 n->content.conj->b = b;
1686 /*@only@*/ lclTypeSpecNode
1687 makeLclTypeSpecNodeType (/*@null@*/ CTypesNode x)
1689 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1692 n->pointers = pointers_undefined;
1693 n->content.type = x;
1694 n->quals = qualList_new ();
1698 /*@only@*/ lclTypeSpecNode
1699 makeLclTypeSpecNodeSU (/*@null@*/ strOrUnionNode x)
1701 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1703 n->kind = LTS_STRUCTUNION;
1704 n->pointers = pointers_undefined;
1705 n->content.structorunion = x;
1706 n->quals = qualList_new ();
1710 /*@only@*/ lclTypeSpecNode
1711 makeLclTypeSpecNodeEnum (/*@null@*/ enumSpecNode x)
1713 lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n));
1715 n->quals = qualList_new ();
1717 n->pointers = pointers_undefined;
1718 n->content.enumspec = x;
1723 lclTypeSpecNode_addQual (lclTypeSpecNode n, qual q)
1725 llassert (lclTypeSpecNode_isDefined (n));
1726 n->quals = qualList_add (n->quals, q);
1731 lclTypeSpecNode_unparse (/*@null@*/ lclTypeSpecNode n)
1733 if (n != (lclTypeSpecNode) 0)
1738 llassert (n->content.type != NULL);
1739 return (printLeaves (n->content.type->ctypes));
1740 case LTS_STRUCTUNION:
1741 return (strOrUnionNode_unparse (n->content.structorunion));
1743 return (enumSpecNode_unparse (n->content.enumspec));
1745 return (lclTypeSpecNode_unparse (n->content.conj->a));
1747 llfatalbug (message ("lclTypeSpecNode_unparse: unknown lclTypeSpec kind: %d",
1751 return cstring_undefined;
1754 /*@only@*/ enumSpecNode
1755 makeEnumSpecNode (ltoken t, ltoken optTagId,
1756 /*@owned@*/ ltokenList enums)
1758 enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n));
1760 smemberInfo *top = smemberInfo_undefined;
1763 n->opttagid = ltoken_copy (optTagId);
1766 /* generate sort for this LCL type */
1767 n->sort = sort_makeEnum (optTagId);
1769 if (!ltoken_isUndefined (optTagId))
1771 /* First, check to see if tag is already defined */
1772 ti = symtable_tagInfo (g_symtab, ltoken_getText (optTagId));
1774 if (tagInfo_exists (ti))
1776 if (ti->kind == TAG_ENUM)
1778 /* 23 Sep 1995 --- had been noting here...is this right? */
1780 ti->content.enums = enums;
1782 ti->imported = context_inImport ();
1787 message ("Tag %s previously defined as %q, redefined as enum",
1788 ltoken_getRawString (optTagId),
1789 tagKind_unparse (ti->kind)));
1791 /* evs --- shouldn't they be in different name spaces? */
1794 ltoken_free (optTagId);
1798 ti = (tagInfo) dmalloc (sizeof (*ti));
1800 ti->kind = TAG_ENUM;
1802 ti->content.enums = enums;
1804 ti->imported = context_inImport ();
1805 /* First, store tag info in symbol table */
1806 (void) symtable_enterTag (g_symtab, ti);
1810 /* check that enumeration constants are unique */
1812 ltokenList_reset (enums);
1814 while (!ltokenList_isFinished (enums))
1816 ltoken c = ltokenList_current (enums);
1817 smemberInfo *ei = (smemberInfo *) dmalloc (sizeof (*ei));
1819 ei->name = ltoken_getText (c);
1824 if (!varInfo_exists (symtable_varInfo (g_symtab, ltoken_getText (c))))
1825 { /* put info into symbol table */
1826 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
1828 vi->id = ltoken_copy (c);
1829 vi->kind = VRK_ENUM;
1833 (void) symtable_enterVar (g_symtab, vi);
1838 lclerror (c, message ("Enumerated value redeclared: %s",
1839 ltoken_getRawString (c)));
1840 ltokenList_removeCurrent (enums);
1842 ltokenList_advance (enums);
1847 (void) sort_updateEnum (n->sort, top);
1851 /*@only@*/ enumSpecNode
1852 makeEnumSpecNode2 (ltoken t, ltoken tagid)
1854 /* a reference, not a definition */
1855 enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n));
1856 tagInfo ti = symtable_tagInfo (g_symtab, ltoken_getText (tagid));
1859 n->opttagid = tagid;
1860 n->enums = ltokenList_new ();
1862 if (tagInfo_exists (ti))
1864 if (ti->kind == TAG_ENUM)
1870 n->sort = sort_makeNoSort ();
1871 lclerror (tagid, message ("Tag %s defined as %q, used as enum",
1872 ltoken_getRawString (tagid),
1873 tagKind_unparse (ti->kind)));
1878 n->sort = sort_makeNoSort ();
1879 lclerror (t, message ("Undefined type: enum %s",
1880 ltoken_getRawString (tagid)));
1887 enumSpecNode_unparse (/*@null@*/ enumSpecNode n)
1889 if (n != (enumSpecNode) 0)
1891 cstring s = cstring_makeLiteral ("enum ");
1893 if (!ltoken_isUndefined (n->opttagid))
1895 s = message ("%q%s ", s, ltoken_getRawString (n->opttagid));
1898 s = message ("%q{%q}", s, printLeaves2 (n->enums));
1901 return cstring_undefined;
1904 /*@only@*/ strOrUnionNode
1905 makestrOrUnionNode (ltoken str, suKind k, ltoken opttagid,
1906 /*@only@*/ stDeclNodeList x)
1908 strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n));
1909 lsymbolSet set = lsymbolSet_new ();
1910 declaratorNodeList declarators;
1911 sort fieldsort, tsort1, tsort2;
1912 smemberInfo *mi, *top = smemberInfo_undefined;
1914 bool isStruct = (k == SU_STRUCT);
1920 n->opttagid = ltoken_copy (opttagid);
1922 n->sort = isStruct ? sort_makeStr (opttagid) : sort_makeUnion (opttagid);
1924 if (!ltoken_isUndefined (opttagid))
1926 /* First, check to see if tag is already defined */
1927 t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid));
1929 if (tagInfo_exists (t))
1931 if ((t->kind == TAG_FWDUNION && k == SU_UNION) ||
1932 (t->kind == TAG_FWDSTRUCT && k == SU_STRUCT))
1934 /* to allow self-recursive types and forward tag declarations */
1935 t->content.decls = stDeclNodeList_copy (x); /* update tag info */
1941 message ("Tag %s previously defined as %q, used as %q",
1942 ltoken_getRawString (opttagid),
1943 tagKind_unparse (t->kind),
1944 cstring_makeLiteral (isStruct ? "struct" : "union")));
1957 if (doTag && !ltoken_isUndefined (opttagid))
1959 t = (tagInfo) dmalloc (sizeof (*t));
1961 /* can either override prev defn or use prev defn */
1962 /* override it so as to detect more errors */
1964 t->kind = (k == SU_STRUCT) ? TAG_STRUCT : TAG_UNION;
1966 t->content.decls = stDeclNodeList_copy (x);
1968 t->imported = FALSE;
1970 /* Next, update tag info in symbol table */
1971 (void) symtable_enterTagForce (g_symtab, t);
1974 /* check no duplicate field names */
1976 stDeclNodeList_elements (x, i)
1978 fieldsort = lclTypeSpecNode2sort (i->lcltypespec);
1980 /* need the locations, not values */
1981 /* fieldsort = sort_makeObj (fieldsort); */
1983 fieldsort = sort_makeGlobal (fieldsort); */
1985 declarators = i->declarators;
1987 declaratorNodeList_elements (declarators, decl)
1990 mi = (smemberInfo *) dmalloc (sizeof (*mi));
1991 /* need to make dynamic copies */
1992 fieldname = ltoken_getText (decl->id);
1994 /* 2/19/93, added */
1995 tsort1 = typeExpr2ptrSort (fieldsort, decl->type);
1996 tsort2 = sort_makeGlobal (tsort1);
1998 mi->name = fieldname;
1999 mi->sort = tsort2; /* fieldsort; */
2003 if (lsymbolSet_member (set, fieldname))
2006 message ("Field name reused: %s",
2007 ltoken_getRawString (decl->id)));
2011 (void) lsymbolSet_insert (set, fieldname);
2014 } end_declaratorNodeList_elements;
2016 } end_stDeclNodeList_elements;
2020 (void) sort_updateStr (n->sort, top);
2024 (void) sort_updateUnion (n->sort, top);
2027 /* We shall keep the info with both tags and types if any
2028 of them are present. */
2030 lsymbolSet_free (set);
2035 /*@only@*/ strOrUnionNode
2036 makeForwardstrOrUnionNode (ltoken str, suKind k,
2039 strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n));
2040 sort sort = sort_makeNoSort ();
2043 /* a reference, not a definition */
2047 n->opttagid = tagid;
2048 n->structdecls = stDeclNodeList_new ();
2050 /* get sort for this LCL type */
2051 t = symtable_tagInfo (g_symtab, ltoken_getText (tagid));
2053 if (tagInfo_exists (t))
2057 if (!(((t->kind == TAG_STRUCT || t->kind == TAG_FWDSTRUCT) && k == SU_STRUCT)
2058 || ((t->kind == TAG_UNION || t->kind == TAG_FWDUNION) && k == SU_UNION)))
2061 message ("Tag %s previously defined as %q, used as %q",
2062 ltoken_getRawString (tagid),
2063 tagKind_unparse (t->kind),
2064 cstring_makeLiteral ((k == SU_STRUCT) ? "struct" : "union")));
2070 ** changed from error: 31 Mar 1994
2072 ** lclerror (str, message ("Undefined type: %s %s", s, ltoken_getRawString (tagid));
2076 /* forward struct's and union's are ok... */
2080 (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy (tagid));
2081 lhForwardStruct (tagid);
2082 sort = sort_makeStr (tagid);
2086 (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy (tagid));
2087 lhForwardUnion (tagid);
2088 sort = sort_makeUnion (tagid);
2097 strOrUnionNode_unparse (/*@null@*/ strOrUnionNode n)
2099 if (n != (strOrUnionNode) 0)
2105 s = cstring_makeLiteral ("struct ");
2108 s = cstring_makeLiteral ("union ");
2113 if (!ltoken_isUndefined (n->opttagid))
2115 s = message ("%q%s ", s, ltoken_getRawString (n->opttagid));
2117 s = message ("%q{%q}", s, stDeclNodeList_unparse (n->structdecls));
2120 return cstring_undefined;
2123 /*@only@*/ stDeclNode
2124 makestDeclNode (lclTypeSpecNode s,
2125 declaratorNodeList x)
2127 stDeclNode n = (stDeclNode) dmalloc (sizeof (*n));
2135 makeFunctionNode (typeExpr x, paramNodeList p)
2137 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2140 y->kind = TEXPR_FCN;
2141 y->content.function.returntype = x;
2142 y->content.function.args = p;
2143 y->sort = sort_makeNoSort ();
2148 static /*@observer@*/ ltoken
2149 extractDeclarator (/*@null@*/ typeExpr t)
2151 if (t != (typeExpr) 0)
2156 return t->content.base;
2158 return (extractDeclarator (t->content.pointer));
2160 return (extractDeclarator (t->content.array.elementtype));
2162 return (extractDeclarator (t->content.function.returntype));
2166 return ltoken_undefined;
2170 makeTypeExpr (ltoken t)
2172 typeExpr x = (typeExpr) dmalloc (sizeof (*x));
2176 x->kind = TEXPR_BASE;
2177 x->content.base = t;
2178 x->sort = sort_makeNoSort ();
2184 /*@only@*/ declaratorNode
2185 makeDeclaratorNode (typeExpr t)
2187 declaratorNode x = (declaratorNode) dmalloc (sizeof (*x));
2189 x->id = ltoken_copy (extractDeclarator (t));
2191 x->isRedecl = FALSE;
2196 static /*@only@*/ declaratorNode
2197 makeUnknownDeclaratorNode (/*@only@*/ ltoken t)
2199 declaratorNode x = (declaratorNode) dmalloc (sizeof (*x));
2202 x->type = (typeExpr) 0;
2203 x->isRedecl = FALSE;
2208 static /*@only@*/ cstring
2209 printTypeExpr2 (/*@null@*/ typeExpr x)
2211 paramNodeList params;
2213 if (x != (typeExpr) 0)
2215 cstring s; /* print out types in reverse order */
2220 return (message ("%s ", ltoken_getRawString (x->content.base)));
2222 return (message ("%qptr to ", printTypeExpr2 (x->content.pointer)));
2224 return (message ("array[%q] of %q",
2225 termNode_unparse (x->content.array.size),
2226 printTypeExpr2 (x->content.array.elementtype)));
2228 s = printTypeExpr2 (x->content.function.returntype);
2229 params = x->content.function.args;
2230 if (!paramNodeList_empty (params))
2232 s = message ("%qfcn with args: (%q)", s,
2233 paramNodeList_unparse (x->content.function.args));
2236 s = message ("%qfcn with no args", s);
2239 llfatalbug (message ("printTypeExpr2: unknown typeExprKind: %d", (int) x->kind));
2242 return cstring_undefined;
2246 declaratorNode_unparse (declaratorNode x)
2248 return (typeExpr_unparse (x->type));
2251 /*@only@*/ declaratorNode
2252 declaratorNode_copy (declaratorNode x)
2254 declaratorNode ret = (declaratorNode) dmalloc (sizeof (*ret));
2256 ret->type = typeExpr_copy (x->type);
2257 ret->id = ltoken_copy (x->id);
2258 ret->isRedecl = x->isRedecl;
2263 static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr x)
2271 typeExpr ret = (typeExpr) dmalloc (sizeof (*ret));
2273 ret->wrapped = x->wrapped;
2274 ret->kind = x->kind;
2279 ret->content.base = ltoken_copy (x->content.base);
2282 ret->content.pointer = typeExpr_copy (x->content.pointer);
2285 ret->content.array.elementtype = typeExpr_copy (x->content.array.elementtype);
2286 ret->content.array.size = termNode_copy (x->content.array.size);
2289 ret->content.function.returntype = typeExpr_copy (x->content.function.returntype);
2290 ret->content.function.args = paramNodeList_copy (x->content.function.args);
2294 ret->sort = x->sort;
2299 static /*@only@*/ cstring
2300 typeExpr_unparseCode (/*@null@*/ typeExpr x)
2302 /* print out types in order of appearance in source */
2303 cstring s = cstring_undefined;
2305 if (x != (typeExpr) 0)
2310 return (cstring_copy (ltoken_getRawString (x->content.base)));
2312 return (typeExpr_unparseCode (x->content.pointer));
2314 return (typeExpr_unparseCode (x->content.array.elementtype));
2316 return (typeExpr_unparseCode (x->content.function.returntype));
2322 void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr x)
2324 if (x != (typeExpr) 0)
2331 typeExpr_free (x->content.pointer);
2334 typeExpr_free (x->content.array.elementtype);
2335 termNode_free (x->content.array.size);
2338 typeExpr_free (x->content.function.returntype);
2339 paramNodeList_free (x->content.function.args);
2351 declaratorNode_unparseCode (declaratorNode x)
2353 return (typeExpr_unparseCode (x->type));
2357 typeExpr_unparse (/*@null@*/ typeExpr x)
2359 cstring s = cstring_undefined; /* print out types in order of appearance in source */
2360 paramNodeList params;
2363 if (x != (typeExpr) 0)
2365 cstring front = cstring_undefined;
2366 cstring back = cstring_undefined;
2368 llassert (x->wrapped < 100);
2370 for (i = x->wrapped; i >= 1; i--)
2372 front = cstring_appendChar (front, '(');
2373 back = cstring_appendChar (back, ')');
2379 s = message ("%q%s", s, ltoken_getRawString (x->content.base));
2382 s = message ("%q*%q", s, typeExpr_unparse (x->content.pointer));
2385 s = message ("%q%q[%q]", s,
2386 typeExpr_unparse (x->content.array.elementtype),
2387 termNode_unparse (x->content.array.size));
2390 s = message ("%q%q (", s,
2391 typeExpr_unparse (x->content.function.returntype));
2392 params = x->content.function.args;
2394 if (!paramNodeList_empty (params))
2396 s = message ("%q%q", s,
2397 paramNodeList_unparse (x->content.function.args));
2400 s = message ("%q)", s);
2403 s = message ("%q%q%q", front, s, back);
2407 s = cstring_makeLiteral ("?");
2414 typeExpr_unparseNoBase (/*@null@*/ typeExpr x)
2416 cstring s = cstring_undefined; /* print out types in order of appearance in source */
2417 paramNodeList params;
2420 if (x != (typeExpr) 0)
2422 cstring front = cstring_undefined;
2423 cstring back = cstring_undefined;
2425 llassert (x->wrapped < 100);
2427 for (i = x->wrapped; i >= 1; i--)
2429 front = cstring_appendChar (front, '(');
2430 back = cstring_appendChar (back, ')');
2436 s = message ("%q /* %s */", s, ltoken_getRawString (x->content.base));
2439 s = message ("%q*%q", s, typeExpr_unparseNoBase (x->content.pointer));
2442 s = message ("%q%q[%q]", s,
2443 typeExpr_unparseNoBase (x->content.array.elementtype),
2444 termNode_unparse (x->content.array.size));
2447 s = message ("%q%q (", s,
2448 typeExpr_unparseNoBase (x->content.function.returntype));
2449 params = x->content.function.args;
2451 if (!paramNodeList_empty (params))
2453 s = message ("%q%q", s,
2454 paramNodeList_unparse (x->content.function.args));
2457 s = message ("%q)", s);
2460 s = message ("%q%q%q", front, s, back);
2464 s = cstring_makeLiteral ("?");
2471 typeExpr_name (/*@null@*/ typeExpr x)
2473 if (x != (typeExpr) 0)
2478 return (cstring_copy (ltoken_getRawString (x->content.base)));
2480 return (typeExpr_name (x->content.pointer));
2482 return (typeExpr_name (x->content.array.elementtype));
2484 return (typeExpr_name (x->content.function.returntype));
2488 /* evs --- 14 Mar 1995
2489 ** not a bug: its okay to have empty parameter names
2490 ** llbug ("typeExpr_name: null");
2493 return cstring_undefined;
2497 makePointerNode (ltoken star, /*@only@*/ /*@returned@*/ typeExpr x)
2499 if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0)))
2501 x->content.function.returntype = makePointerNode (star, x->content.function.returntype);
2506 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2509 y->kind = TEXPR_PTR;
2510 y->content.pointer = x;
2511 y->sort = sort_makeNoSort ();
2518 typeExpr makeArrayNode (/*@returned@*/ typeExpr x,
2519 /*@only@*/ arrayQualNode a)
2521 if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0)))
2524 ** Spurious errors reported here, because of referencing
2525 ** in makeArrayNode.
2528 /*@i3@*/ x->content.function.returntype = makeArrayNode (x, a);
2533 typeExpr y = (typeExpr) dmalloc (sizeof (*y));
2535 y->kind = TEXPR_ARRAY;
2537 if (a == (arrayQualNode) 0)
2539 y->content.array.size = (termNode) 0;
2543 y->content.array.size = a->term;
2544 ltoken_free (a->tok);
2548 y->content.array.elementtype = x;
2549 y->sort = sort_makeNoSort ();
2555 /*@only@*/ constDeclarationNode
2556 makeConstDeclarationNode (lclTypeSpecNode t, initDeclNodeList decls)
2558 constDeclarationNode n = (constDeclarationNode) dmalloc (sizeof (*n));
2559 sort s, s2, initValueSort;
2560 ltoken varid, errtok;
2563 s = lclTypeSpecNode2sort (t);
2565 initDeclNodeList_elements (decls, init)
2567 declaratorNode vdnode = init->declarator;
2568 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
2570 varid = ltoken_copy (vdnode->id);
2571 s2 = typeExpr2ptrSort (s, vdnode->type);
2572 initValue = init->value;
2574 if (termNode_isDefined (initValue) && !initValue->error_reported)
2576 initValueSort = initValue->sort;
2578 /* should keep the arguments in order */
2579 if (!sort_member_modulo_cstring (s2, initValue)
2580 && !initValue->error_reported)
2582 errtok = termNode_errorToken (initValue);
2586 message ("Constant %s declared type %q, initialized to %q: %q",
2587 ltoken_unparse (varid),
2589 sort_unparse (initValueSort),
2590 termNode_unparse (initValue)));
2595 vi->kind = VRK_CONST;
2599 (void) symtable_enterVar (g_symtab, vi);
2602 } end_initDeclNodeList_elements;
2610 varDeclarationNode makeInternalStateNode (void)
2612 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2614 n->isSpecial = TRUE;
2615 n->sref = sRef_makeInternalState ();
2617 /*@-compdef@*/ return n; /*@=compdef@*/
2620 varDeclarationNode makeFileSystemNode (void)
2622 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2624 n->isSpecial = TRUE;
2625 n->sref = sRef_makeSystemState ();
2627 /*@-compdef@*/ return n; /*@=compdef@*/
2630 /*@only@*/ varDeclarationNode
2631 makeVarDeclarationNode (lclTypeSpecNode t, initDeclNodeList x,
2632 bool isGlobal, bool isPrivate)
2634 varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n));
2635 sort s, s2, initValueSort;
2636 ltoken varid, errtok;
2638 declaratorNode vdnode;
2640 n->isSpecial = FALSE;
2641 n->qualifier = QLF_NONE;
2642 n->isGlobal = isGlobal;
2643 n->isPrivate = isPrivate;
2646 s = lclTypeSpecNode2sort (t);
2648 /* t is an lclTypeSpec, its sort may not be assigned yet */
2650 initDeclNodeList_elements (x, init)
2652 vdnode = init->declarator;
2654 s2 = typeExpr2ptrSort (s, vdnode->type);
2655 initValue = init->value;
2657 if (termNode_isDefined (initValue) && !initValue->error_reported)
2659 initValueSort = initValue->sort;
2660 /* should keep the arguments in order */
2661 if (!sort_member_modulo_cstring (s2, initValue)
2662 && !initValue->error_reported)
2664 errtok = termNode_errorToken (initValue);
2667 message ("Variable %s declared type %q, initialized to %q",
2668 ltoken_unparse (varid),
2670 sort_unparse (initValueSort)));
2675 ** If global, check that it has been declared already, don't push
2676 ** onto symbol table yet (wrong scope, done in enteringFcnScope
2681 varInfo vi = symtable_varInfo (g_symtab, ltoken_getText (varid));
2683 if (!varInfo_exists (vi))
2686 message ("Undeclared global variable: %s",
2687 ltoken_getRawString (varid)));
2691 if (vi->kind == VRK_CONST)
2694 message ("Constant used in global list: %s",
2695 ltoken_getRawString (varid)));
2701 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
2703 vi->id = ltoken_copy (varid);
2706 vi->kind = VRK_PRIVATE;
2707 /* check that initValue is not empty */
2708 if (initValue == (termNode) 0)
2711 message ("Private variable must have initialization: %s",
2712 ltoken_getRawString (varid)));
2720 vi->sort = sort_makeGlobal (s2);
2723 vdnode->isRedecl = symtable_enterVar (g_symtab, vi);
2726 } end_initDeclNodeList_elements;
2733 /*@only@*/ initDeclNode
2734 makeInitDeclNode (declaratorNode d, termNode x)
2736 initDeclNode n = (initDeclNode) dmalloc (sizeof (*n));
2743 /*@only@*/ abstractNode
2744 makeAbstractNode (ltoken t, ltoken name,
2745 bool isMutable, bool isRefCounted, abstBodyNode a)
2747 abstractNode n = (abstractNode) dmalloc (sizeof (*n));
2749 typeInfo ti = (typeInfo) dmalloc (sizeof (*ti));
2752 n->isMutable = isMutable;
2755 n->isRefCounted = isRefCounted;
2758 handle = sort_makeMutable (name, ltoken_getText (name));
2760 handle = sort_makeImmutable (name, ltoken_getText (name));
2763 ti->id = ltoken_createType (ltoken_getCode (ltoken_typename), SID_TYPE,
2764 ltoken_getText (name));
2765 ti->modifiable = isMutable;
2766 ti->abstract = TRUE;
2767 ti->basedOn = handle;
2770 symtable_enterType (g_symtab, ti);
2777 abstractNode_unparse (abstractNode n)
2779 if (n != (abstractNode) 0)
2784 s = cstring_makeLiteral ("mutable");
2786 s = cstring_makeLiteral ("immutable");
2788 return (message ("%q type %s%q;", s, ltoken_getRawString (n->name),
2789 abstBodyNode_unparse (n->body)));
2791 return cstring_undefined;
2795 setExposedType (lclTypeSpecNode s)
2800 /*@only@*/ exposedNode
2801 makeExposedNode (ltoken t, lclTypeSpecNode s,
2802 declaratorInvNodeList d)
2804 exposedNode n = (exposedNode) dmalloc (sizeof (*n));
2814 exposedNode_unparse (exposedNode n)
2816 if (n != (exposedNode) 0)
2818 return (message ("typedef %q %q;",
2819 lclTypeSpecNode_unparse (n->type),
2820 declaratorInvNodeList_unparse (n->decls)));
2822 return cstring_undefined;
2825 /*@only@*/ declaratorInvNode
2826 makeDeclaratorInvNode (declaratorNode d, abstBodyNode b)
2828 declaratorInvNode n = (declaratorInvNode) dmalloc (sizeof (*n));
2836 declaratorInvNode_unparse (declaratorInvNode d)
2838 return (message ("%q%q", declaratorNode_unparse (d->declarator),
2839 abstBodyNode_unparseExposed (d->body)));
2843 abstBodyNode_unparse (abstBodyNode n)
2845 if (n != (abstBodyNode) 0)
2847 return (lclPredicateNode_unparse (n->typeinv));
2849 return cstring_undefined;
2853 abstBodyNode_unparseExposed (abstBodyNode n)
2855 if (n != (abstBodyNode) 0)
2857 return (message ("%q", lclPredicateNode_unparse (n->typeinv)));
2859 return cstring_undefined;
2863 taggedUnionNode_unparse (taggedUnionNode n)
2865 if (n != (taggedUnionNode) 0)
2867 return (message ("tagged union {%q}%q;\n",
2868 stDeclNodeList_unparse (n->structdecls),
2869 declaratorNode_unparse (n->declarator)));
2871 return cstring_undefined;
2874 static /*@observer@*/ paramNodeList
2875 typeExpr_toParamNodeList (/*@null@*/ typeExpr te)
2877 if (te != (typeExpr) 0)
2882 return te->content.function.args;
2884 return typeExpr_toParamNodeList (te->content.pointer);
2886 /* return typeExpr_toParamNodeList (te->content.array.elementtype); */
2888 return paramNodeList_undefined;
2891 return paramNodeList_undefined;
2895 fcnNode_fromDeclarator (/*@only@*/ /*@null@*/ lclTypeSpecNode t,
2896 /*@only@*/ declaratorNode d)
2898 return (makeFcnNode (qual_createUnknown (), t, d,
2899 varDeclarationNodeList_new (),
2900 varDeclarationNodeList_new (),
2901 letDeclNodeList_new (),
2902 (lclPredicateNode) 0,
2903 (lclPredicateNode) 0,
2905 (lclPredicateNode) 0,
2906 (lclPredicateNode) 0));
2910 makeIterNode (ltoken id, paramNodeList p)
2912 iterNode x = (iterNode) dmalloc (sizeof (*x));
2913 bool hasYield = FALSE;
2918 /* check there is at least one yield param */
2920 paramNodeList_elements (p, pe)
2922 if (paramNode_isYield (pe))
2927 } end_paramNodeList_elements
2931 lclerror (id, message ("Iterator has no yield parameters: %s",
2932 ltoken_getRawString (id)));
2939 makeFcnNode (qual specQual,
2940 /*@null@*/ lclTypeSpecNode t,
2942 /*@null@*/ globalList g,
2943 /*@null@*/ varDeclarationNodeList privateinits,
2944 /*@null@*/ letDeclNodeList lets,
2945 /*@null@*/ lclPredicateNode checks,
2946 /*@null@*/ lclPredicateNode requires,
2947 /*@null@*/ modifyNode m,
2948 /*@null@*/ lclPredicateNode ensures,
2949 /*@null@*/ lclPredicateNode claims)
2951 fcnNode x = (fcnNode) dmalloc (sizeof (*x));
2953 if (d->type != (typeExpr)0 && (d->type)->kind != TEXPR_FCN)
2955 lclerror (d->id, cstring_makeLiteral
2956 ("Attempt to specify function without parameter list"));
2957 d->type = makeFunctionNode (d->type, paramNodeList_new ());
2960 x->special = specQual;
2964 x->inits = privateinits;
2967 x->require = requires;
2969 x->ensures = ensures;
2972 /* extract info to fill in x->name =; x->signature =; */
2973 x->name = ltoken_copy (d->id);
2978 /*@only@*/ claimNode
2979 makeClaimNode (ltoken id, paramNodeList p,
2980 globalList g, letDeclNodeList lets, lclPredicateNode requires,
2981 programNode b, lclPredicateNode ensures)
2983 claimNode x = (claimNode) dmalloc (sizeof (*x));
2990 x->require = requires;
2992 x->ensures = ensures;
2996 /*@only@*/ lclPredicateNode
2997 makeIntraClaimNode (ltoken t, lclPredicateNode n)
2999 ltoken_free (n->tok);
3001 n->kind = LPD_INTRACLAIM;
3005 /*@only@*/ lclPredicateNode
3006 makeRequiresNode (ltoken t, lclPredicateNode n)
3008 ltoken_free (n->tok);
3010 n->kind = LPD_REQUIRES;
3014 /*@only@*/ lclPredicateNode
3015 makeChecksNode (ltoken t, lclPredicateNode n)
3017 ltoken_free (n->tok);
3019 n->kind = LPD_CHECKS;
3023 /*@only@*/ lclPredicateNode
3024 makeEnsuresNode (ltoken t, lclPredicateNode n)
3026 ltoken_free (n->tok);
3028 n->kind = LPD_ENSURES;
3032 /*@only@*/ lclPredicateNode
3033 makeLclPredicateNode (ltoken t, termNode n,
3036 lclPredicateNode x = (lclPredicateNode) dmalloc (sizeof (*x));
3044 /*@only@*/ quantifierNode
3045 makeQuantifierNode (varNodeList v, ltoken quant)
3047 quantifierNode x = (quantifierNode) dmalloc (sizeof (*x));
3051 x->isForall = cstring_equalLit (ltoken_unparse (quant), "\forall");
3056 /*@only@*/ arrayQualNode
3057 makeArrayQualNode (ltoken t, termNode term)
3059 arrayQualNode x = (arrayQualNode) dmalloc (sizeof (*x));
3067 makeVarNode (/*@only@*/ ltoken varid, bool isObj, lclTypeSpecNode t)
3069 varNode x = (varNode) dmalloc (sizeof (*x));
3070 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
3073 vi->id = ltoken_copy (varid);
3074 sort = lclTypeSpecNode2sort (t);
3076 /* 9/3/93, The following is needed because we want value sorts to be
3077 the default, object sort is generated only if there is "obj" qualifier.
3078 There are 2 cases: (1) for immutable types (including C primitive types),
3079 we need to generate the object sort if qualifier is present; (2) for
3080 array, struct and union types, they are already in their object sorts.
3083 sort = sort_makeVal (sort); /* both cases are now value sorts */
3087 sort = sort_makeObj (sort);
3092 vi->kind = VRK_QUANT;
3095 (void) symtable_enterVar (g_symtab, vi);
3101 x->sort = sort_makeNoSort ();
3106 /*@only@*/ abstBodyNode
3107 makeAbstBodyNode (ltoken t, fcnNodeList f)
3109 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3112 x->typeinv = (lclPredicateNode)0;
3117 /*@only@*/ abstBodyNode
3118 makeExposedBodyNode (ltoken t, lclPredicateNode inv)
3120 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3124 x->fcns = fcnNodeList_undefined;
3128 /*@only@*/ abstBodyNode
3129 makeAbstBodyNode2 (ltoken t, ltokenList ops)
3131 abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x));
3134 x->typeinv = (lclPredicateNode) 0;
3136 x->fcns = fcnNodeList_new ();
3138 ltokenList_elements (ops, op)
3140 x->fcns = fcnNodeList_add
3142 fcnNode_fromDeclarator (lclTypeSpecNode_undefined,
3143 makeUnknownDeclaratorNode (ltoken_copy (op))));
3144 } end_ltokenList_elements;
3146 ltokenList_free (ops);
3152 makeStmtNode (ltoken varId, ltoken fcnId, /*@only@*/ termNodeList v)
3154 stmtNode n = (stmtNode) dmalloc (sizeof (*n));
3157 n->operator = fcnId;
3162 /* printDeclarators -> declaratorNodeList_unparse */
3164 static cstring abstDeclaratorNode_unparse (abstDeclaratorNode x)
3166 return (typeExpr_unparse ((typeExpr) x));
3169 /*@only@*/ paramNode
3170 makeParamNode (lclTypeSpecNode t, typeExpr d)
3172 paramNode x = (paramNode) dmalloc (sizeof (*x));
3174 paramNode_checkQualifiers (t, d);
3178 x->kind = PNORMAL; /*< forgot this! >*/
3183 /*@only@*/ paramNode
3184 paramNode_elipsis (void)
3186 paramNode x = (paramNode) dmalloc (sizeof (*x));
3188 x->type = (lclTypeSpecNode) 0;
3189 x->paramdecl = (typeExpr) 0;
3195 static /*@observer@*/ ltoken typeExpr_getTok (typeExpr d)
3197 while (d != (typeExpr)0)
3199 if (d->kind == TEXPR_BASE)
3201 return (d->content.base);
3205 if (d->kind == TEXPR_PTR)
3207 d = d->content.pointer;
3209 else if (d->kind == TEXPR_ARRAY)
3211 d = d->content.array.elementtype;
3213 else if (d->kind == TEXPR_FCN)
3215 d = d->content.function.returntype;
3224 llfatalerror (cstring_makeLiteral ("typeExpr_getTok: unreachable code"));
3229 paramNode_checkQualifiers (lclTypeSpecNode t, typeExpr d)
3231 bool isPointer = FALSE;
3232 bool isUser = FALSE;
3233 bool hasAlloc = FALSE;
3234 bool hasAlias = FALSE;
3236 llassert (lclTypeSpecNode_isDefined (t));
3238 if (pointers_isUndefined (t->pointers)
3239 && (d != (typeExpr)0 && d->kind != TEXPR_PTR) && d->kind != TEXPR_ARRAY)
3241 if (t->kind == LTS_TYPE)
3245 llassert (t->content.type != NULL);
3247 sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort));
3249 if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY
3250 || sn->kind == SRT_HOF || sn->kind == SRT_NONE)
3261 if (d != (typeExpr)0 && d->kind != TEXPR_BASE)
3263 if (t->kind == LTS_TYPE)
3267 llassert (t->content.type != NULL);
3268 sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort));
3270 if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY
3271 || sn->kind == SRT_HOF || sn->kind == SRT_NONE)
3282 if (d != (typeExpr)NULL)
3284 qualList_elements (t->quals, q)
3286 if (qual_isAllocQual (q))
3290 ltoken tok = typeExpr_getTok (d);
3291 lclerror (tok, message ("Parameter declared with multiple allocation "
3292 "qualifiers: %q", typeExpr_unparse (d)));
3298 ltoken tok = typeExpr_getTok (d);
3299 lclerror (tok, message ("Non-pointer declared as %s parameter: %q",
3301 typeExpr_unparse (d)));
3304 if (qual_isAliasQual (q))
3308 ltoken tok = typeExpr_getTok (d);
3309 lclerror (tok, message ("Parameter declared with multiple alias qualifiers: %q",
3310 typeExpr_unparse (d)));
3314 if (!(isPointer || isUser))
3316 ltoken tok = typeExpr_getTok (d);
3317 lclerror (tok, message ("Unsharable type declared as %s parameter: %q",
3319 typeExpr_unparse (d)));
3322 } end_qualList_elements;
3327 paramNode_unparse (paramNode x)
3329 if (x != (paramNode) 0)
3331 if (x->kind == PELIPSIS)
3333 return (cstring_makeLiteral ("..."));
3336 if (x->paramdecl != (typeExpr) 0)
3337 { /* handle (void) */
3338 return (message ("%q %q", lclTypeSpecNode_unparse (x->type),
3339 typeExpr_unparse (x->paramdecl)));
3343 return (lclTypeSpecNode_unparse (x->type));
3346 return cstring_undefined;
3350 lclTypeSpecNode_unparseAltComments (/*@null@*/ lclTypeSpecNode typespec) /*@*/
3352 if (typespec != (lclTypeSpecNode) 0)
3354 cstring s = qualList_toCComments (typespec->quals);
3356 switch (typespec->kind)
3360 llassert (typespec->content.type != NULL);
3362 return (cstring_concatFree
3363 (s, printLeaves (typespec->content.type->ctypes)));
3368 enumSpecNode n = typespec->content.enumspec;
3370 s = cstring_concatFree (s, cstring_makeLiteral ("enum"));
3371 llassert (n != NULL);
3373 if (!ltoken_isUndefined (n->opttagid))
3375 s = message ("%q %s", s, ltoken_unparse (n->opttagid));
3377 s = message ("%q {", s);
3379 ltokenList_elements (n->enums, e)
3384 s = message ("%q%s", s, ltoken_getRawString (e));
3387 s = message ("%q, %s", s, ltoken_getRawString (e));
3388 } end_ltokenList_elements;
3390 return (message ("%q}", s));
3392 case LTS_STRUCTUNION:
3394 strOrUnionNode n = typespec->content.structorunion;
3395 stDeclNodeList decls;
3397 llassert (n != NULL);
3402 s = cstring_concatFree (s, cstring_makeLiteral ("struct "));
3403 /*@switchbreak@*/ break;
3405 s = cstring_concatFree (s, cstring_makeLiteral ("union "));
3406 /*@switchbreak@*/ break;
3409 if (!ltoken_isUndefined (n->opttagid))
3411 if (stDeclNodeList_size (n->structdecls) == 0)
3413 return (message ("%q%s", s, ltoken_unparse (n->opttagid)));
3416 s = message ("%q%s {\n\t", s, ltoken_unparse (n->opttagid));
3420 s = message ("%q{\n\t", s);
3423 decls = n->structdecls;
3425 stDeclNodeList_elements (decls, f)
3427 s = message ("%q%q %q;\n\t", s,
3428 lclTypeSpecNode_unparseAltComments (f->lcltypespec),
3429 declaratorNodeList_unparse (f->declarators));
3430 } end_stDeclNodeList_elements;
3432 return (message ("%q }", s));
3441 lclTypeSpecNode_unparseAltComments (typespec->content.conj->a),
3442 lclTypeSpecNode_unparseAltComments (typespec->content.conj->b)));
3449 llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec");
3451 return cstring_undefined;
3457 cstring lclTypeSpecNode_unparseComments (/*@null@*/ lclTypeSpecNode typespec)
3459 if (typespec != (lclTypeSpecNode) 0)
3461 cstring s = qualList_toCComments (typespec->quals);
3463 switch (typespec->kind)
3467 llassert (typespec->content.type != NULL);
3469 return (cstring_concatFree
3470 (s, printLeaves (typespec->content.type->ctypes)));
3475 enumSpecNode n = typespec->content.enumspec;
3477 s = cstring_concatFree (s, cstring_makeLiteral ("enum"));
3478 llassert (n != NULL);
3480 if (!ltoken_isUndefined (n->opttagid))
3482 s = message ("%q %s", s, ltoken_unparse (n->opttagid));
3484 s = message ("%q {", s);
3486 ltokenList_elements (n->enums, e)
3491 s = message ("%q%s", s, ltoken_getRawString (e));
3494 s = message ("%q, %s", s, ltoken_getRawString (e));
3495 } end_ltokenList_elements;
3497 return (message ("%q}", s));
3499 case LTS_STRUCTUNION:
3501 strOrUnionNode n = typespec->content.structorunion;
3502 stDeclNodeList decls;
3504 llassert (n != NULL);
3509 s = cstring_concatFree (s, cstring_makeLiteral ("struct "));
3510 /*@switchbreak@*/ break;
3512 s = cstring_concatFree (s, cstring_makeLiteral ("union "));
3513 /*@switchbreak@*/ break;
3516 if (!ltoken_isUndefined (n->opttagid))
3518 if (stDeclNodeList_size (n->structdecls) == 0)
3520 return (message ("%q%s", s, ltoken_unparse (n->opttagid)));
3523 s = message ("%q%s {\n\t", s, ltoken_unparse (n->opttagid));
3527 s = message ("%q{\n\t", s);
3530 decls = n->structdecls;
3532 stDeclNodeList_elements (decls, f)
3534 s = message ("%q%q %q;\n\t", s,
3535 lclTypeSpecNode_unparseComments (f->lcltypespec),
3536 declaratorNodeList_unparse (f->declarators));
3537 } end_stDeclNodeList_elements;
3539 return (message ("%q }", s));
3548 lclTypeSpecNode_unparseComments (typespec->content.conj->a),
3549 lclTypeSpecNode_unparseAltComments (typespec->content.conj->b)));
3556 llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec");
3558 return cstring_undefined;
3565 paramNode_unparseComments (paramNode x)
3567 if (x != (paramNode) 0)
3569 if (x->kind == PELIPSIS)
3571 return (cstring_makeLiteral ("..."));
3574 if (x->paramdecl != (typeExpr) 0)
3575 { /* handle (void) */
3576 return (message ("%q %q",
3577 lclTypeSpecNode_unparseComments (x->type),
3578 typeExpr_unparseNoBase (x->paramdecl)));
3582 return (lclTypeSpecNode_unparseComments (x->type));
3585 return cstring_undefined;
3589 makeIfTermNode (ltoken ift, termNode ifn, ltoken thent,
3590 termNode thenn, ltoken elset,
3593 termNode t = (termNode) dmalloc (sizeof (*t));
3594 opFormNode opform = makeOpFormNode (ift, OPF_IF, opFormUnion_createMiddle (0),
3596 nameNode nn = makeNameNodeForm (opform);
3597 termNodeList args = termNodeList_new ();
3599 t->error_reported = FALSE;
3601 termNodeList_addh (args, ifn);
3602 termNodeList_addh (args, thenn);
3603 termNodeList_addh (args, elsen);
3606 t->kind = TRM_APPLICATION;
3607 t->sort = sort_makeNoSort ();
3609 t->possibleSorts = sortSet_new ();
3610 t->possibleOps = lslOpSet_new ();
3612 ltoken_free (thent);
3613 ltoken_free (elset);
3618 static /*@observer@*/ ltoken
3619 nameNode2anyOp (nameNode n)
3621 if (n != (nameNode) 0)
3623 opFormNode opnode = n->content.opform;
3626 llassert (opnode != NULL);
3628 kind = opnode->kind;
3630 if (kind == OPF_MANYOPM || kind == OPF_ANYOP ||
3631 kind == OPF_MANYOP || kind == OPF_ANYOPM)
3635 u = opnode->content;
3639 return ltoken_undefined;
3643 makeInfixTermNode (termNode x, ltoken op, termNode y)
3645 termNode t = (termNode) dmalloc (sizeof (*t));
3648 termNodeList args = termNodeList_new ();
3650 checkAssociativity (x, op);
3652 opform = makeOpFormNode (op, OPF_MANYOPM,
3653 opFormUnion_createAnyOp (op),
3656 nn = makeNameNodeForm (opform);
3658 t->error_reported = FALSE;
3660 termNodeList_addh (args, x);
3661 termNodeList_addh (args, y);
3664 t->kind = TRM_APPLICATION;
3665 t->sort = sort_makeNoSort ();
3667 t->possibleSorts = sortSet_new (); /* sort_equal */
3668 t->possibleOps = lslOpSet_new ();
3672 /*@only@*/ quantifiedTermNode
3673 quantifiedTermNode_copy (quantifiedTermNode q)
3675 quantifiedTermNode ret = (quantifiedTermNode) dmalloc (sizeof (*ret));
3677 ret->quantifiers = quantifierNodeList_copy (q->quantifiers);
3678 ret->open = ltoken_copy (q->open);
3679 ret->close = ltoken_copy (q->close);
3680 ret->body = termNode_copySafe (q->body);
3686 makeQuantifiedTermNode (quantifierNodeList qn, ltoken open,
3687 termNode t, ltoken close)
3690 termNode n = (termNode) dmalloc (sizeof (*n));
3691 quantifiedTermNode q = (quantifiedTermNode) dmalloc (sizeof (*q));
3693 n->name = NULL; /*> missing this --- detected by splint <*/
3694 n->error_reported = FALSE;
3696 n->error_reported = FALSE;
3697 n->kind = TRM_QUANTIFIER;
3698 n->possibleSorts = sortSet_new ();
3699 n->possibleOps = lslOpSet_new ();
3700 n->kind = TRM_UNCHANGEDALL;
3701 n->args = termNodeList_new (); /*< forgot this >*/
3703 termNodeList_free (t->args);
3704 t->args = termNodeList_new ();
3708 (void) sortSet_insert (n->possibleSorts, sort);
3710 q->quantifiers = qn;
3720 makePostfixTermNode (/*@returned@*/ /*@only@*/ termNode secondary, ltokenList postfixops)
3722 termNode top = secondary;
3724 ltokenList_elements (postfixops, op)
3726 top = makePostfixTermNode2 (top, ltoken_copy (op));
3727 /*@i@*/ } end_ltokenList_elements;
3729 ltokenList_free (postfixops);
3731 return (top); /* dep as only? */
3735 ** secondary is returned in the args list
3739 makePostfixTermNode2 (/*@returned@*/ /*@only@*/ termNode secondary,
3740 /*@only@*/ ltoken postfixop)
3742 termNode t = (termNode) dmalloc (sizeof (*t));
3744 opFormNode opform = makeOpFormNode (postfixop,
3745 OPF_MANYOP, opFormUnion_createAnyOp (postfixop),
3747 nameNode nn = makeNameNodeForm (opform);
3748 termNodeList args = termNodeList_new ();
3750 t->error_reported = FALSE;
3752 termNodeList_addh (args, secondary);
3755 t->kind = TRM_APPLICATION;
3756 t->sort = sort_makeNoSort ();
3758 t->possibleSorts = sortSet_new ();
3759 t->possibleOps = lslOpSet_new ();
3764 makePrefixTermNode (ltoken op, termNode arg)
3766 termNode t = (termNode) dmalloc (sizeof (*t));
3767 termNodeList args = termNodeList_new ();
3768 opFormNode opform = makeOpFormNode (op, OPF_ANYOPM, opFormUnion_createAnyOp (op),
3770 nameNode nn = makeNameNodeForm (opform);
3772 t->error_reported = FALSE;
3775 termNodeList_addh (args, arg);
3777 t->kind = TRM_APPLICATION;
3778 t->sort = sort_makeNoSort ();
3780 t->possibleSorts = sortSet_new ();
3781 t->possibleOps = lslOpSet_new ();
3786 makeOpCallTermNode (ltoken op, ltoken open,
3787 termNodeList args, ltoken close)
3789 /* like prefixTerm, but with opId LPAR termNodeList RPAR */
3790 termNode t = (termNode) dmalloc (sizeof (*t));
3791 nameNode nn = makeNameNodeId (op);
3793 t->error_reported = FALSE;
3797 t->kind = TRM_APPLICATION;
3798 t->sort = sort_makeNoSort ();
3800 t->possibleSorts = sortSet_new ();
3801 t->possibleOps = lslOpSet_new ();
3804 ltoken_free (close);
3809 /*@exposed@*/ termNode
3810 CollapseInfixTermNode (/*@returned@*/ termNode secondary, termNodeList infix)
3812 termNode left = secondary;
3814 termNodeList_elements (infix, node)
3816 termNodeList_addl (node->args, termNode_copySafe (left));
3818 /* computePossibleSorts (left); */
3819 } end_termNodeList_elements;
3825 checkAssociativity (termNode x, ltoken op)
3829 if (x->wrapped == 0 && /* no parentheses */
3830 x->kind == TRM_APPLICATION && x->name != (nameNode) 0 &&
3833 lastOpToken = nameNode2anyOp (x->name);
3835 if ((ltoken_getCode (lastOpToken) == logicalOp &&
3836 ltoken_getCode (op) == logicalOp) ||
3837 ((ltoken_getCode (lastOpToken) == simpleOp ||
3838 ltoken_getCode (lastOpToken) == LLT_MULOP) &&
3839 (ltoken_getCode (op) == simpleOp ||
3840 ltoken_getCode (op) == LLT_MULOP)))
3841 if (ltoken_getText (lastOpToken) != ltoken_getText (op))
3845 ("Parentheses needed to specify associativity of %s and %s",
3846 cstring_fromChars (lsymbol_toChars (ltoken_getText (lastOpToken))),
3847 cstring_fromChars (lsymbol_toChars (ltoken_getText (op)))));
3853 pushInfixOpPartNode (/*@returned@*/ termNodeList x, ltoken op,
3854 /*@only@*/ termNode secondary)
3856 termNode lastLeftTerm;
3857 termNodeList args = termNodeList_new ();
3858 termNode t = (termNode) dmalloc (sizeof (*t));
3862 termNodeList_addh (args, secondary);
3864 if (!termNodeList_empty (x))
3866 termNodeList_reset (x);
3867 lastLeftTerm = termNodeList_current (x);
3868 checkAssociativity (lastLeftTerm, op);
3871 opform = makeOpFormNode (op, OPF_MANYOPM,
3872 opFormUnion_createAnyOp (op), ltoken_undefined);
3874 nn = makeNameNodeForm (opform);
3876 t->error_reported = FALSE;
3879 t->kind = TRM_APPLICATION;
3881 t->sort = sort_makeNoSort ();
3883 t->possibleSorts = sortSet_new ();
3884 t->possibleOps = lslOpSet_new ();
3885 termNodeList_addh (x, t);
3886 /* don't compute sort yet, do it in CollapseInfixTermNode */
3891 updateMatchedNode (/*@only@*/ termNode left, /*@returned@*/ termNode t,
3892 /*@only@*/ termNode right)
3896 if ((t == (termNode) 0) || (t->name == NULL) || t->name->isOpId)
3898 llbugexitlit ("updateMatchedNode: expect opForm in nameNode");
3901 op = t->name->content.opform;
3902 llassert (op != NULL);
3904 if (left == (termNode) 0)
3906 if (right == (termNode) 0)
3908 /* op->kind is not changed */
3909 termNode_free (right);
3913 op->kind = OPF_MIDDLEM;
3914 op->key = opFormNode2key (op, OPF_MIDDLEM);
3915 termNodeList_addh (t->args, right);
3920 termNodeList_addl (t->args, left);
3921 if (right == (termNode) 0)
3923 op->kind = OPF_MMIDDLE;
3924 op->key = opFormNode2key (op, OPF_MMIDDLE);
3928 op->kind = OPF_MMIDDLEM;
3929 op->key = opFormNode2key (op, OPF_MMIDDLEM);
3930 termNodeList_addh (t->args, right);
3937 updateSqBracketedNode (/*@only@*/ termNode left,
3938 /*@only@*/ /*@returned@*/ termNode t,
3939 /*@only@*/ termNode right)
3943 if ((t == (termNode) 0) || (t->name == NULL) || (t->name->isOpId))
3945 llbugexitlit ("updateSqBracketededNode: expect opForm in nameNode");
3948 op = t->name->content.opform;
3949 llassert (op != NULL);
3951 if (left == (termNode) 0)
3953 if (right == (termNode) 0)
3955 /* op->kind is not changed */
3959 op->kind = OPF_BMIDDLEM;
3960 op->key = opFormNode2key (op, OPF_BMIDDLEM);
3961 termNodeList_addh (t->args, right);
3966 termNodeList_addl (t->args, left);
3968 if (right == (termNode) 0)
3970 op->kind = OPF_BMMIDDLE;
3971 op->key = opFormNode2key (op, OPF_BMMIDDLE);
3975 op->kind = OPF_BMMIDDLEM;
3976 op->key = opFormNode2key (op, OPF_BMMIDDLEM);
3977 termNodeList_addh (t->args, right);
3984 makeSqBracketedNode (ltoken lbracket,
3985 termNodeList args, ltoken rbracket)
3987 termNode t = (termNode) dmalloc (sizeof (*t));
3992 t->error_reported = FALSE;
3995 size = termNodeList_size (args);
3996 opform = makeOpFormNode (lbracket, OPF_BMIDDLE, opFormUnion_createMiddle (size),
3998 nn = makeNameNodeForm (opform);
4000 t->kind = TRM_APPLICATION;
4002 t->sort = sort_makeNoSort ();
4004 t->possibleSorts = sortSet_new ();
4005 t->possibleOps = lslOpSet_new ();
4006 /* do sort checking later, not here, incomplete parse */
4011 makeMatchedNode (ltoken open, termNodeList args, ltoken close)
4013 /* matched : open args close */
4014 termNode t = (termNode) dmalloc (sizeof (*t));
4019 t->error_reported = FALSE;
4022 size = termNodeList_size (args);
4023 opform = makeOpFormNode (open, OPF_MIDDLE, opFormUnion_createMiddle (size), close);
4024 nn = makeNameNodeForm (opform);
4026 t->kind = TRM_APPLICATION;
4028 t->sort = sort_makeNoSort ();
4030 t->possibleSorts = sortSet_new ();
4031 t->possibleOps = lslOpSet_new ();
4032 /* do sort checking later, not here, incomplete parse */
4037 makeSimpleTermNode (ltoken varid)
4039 sort theSort = sort_makeNoSort ();
4043 termNode n = (termNode) dmalloc (sizeof (*n));
4045 n->error_reported = FALSE;
4047 n->name = (nameNode) 0;
4049 n->args = termNodeList_new ();
4050 n->possibleSorts = sortSet_new ();
4051 n->possibleOps = lslOpSet_new ();
4053 sym = ltoken_getText (varid);
4055 /* lookup current scope */
4056 vi = symtable_varInfoInScope (g_symtab, sym);
4058 if (varInfo_exists (vi))
4064 (void) sortSet_insert (n->possibleSorts, theSort);
4067 { /* need to handle LCL constants */
4068 vi = symtable_varInfo (g_symtab, sym);
4070 if (varInfo_exists (vi) && vi->kind == VRK_CONST)
4073 n->kind = TRM_CONST;
4076 (void) sortSet_insert (n->possibleSorts, theSort);
4079 { /* and LSL operators (true, false, new, nil, etc) */
4080 nameNode nn = makeNameNodeId (ltoken_copy (varid));
4081 oi = symtable_opInfo (g_symtab, nn);
4083 if (opInfo_exists (oi) && (oi->name->isOpId) &&
4084 !sigNodeSet_isEmpty (oi->signatures))
4086 sigNodeSet_elements (oi->signatures, x)
4088 if (ltokenList_empty (x->domain))
4089 /* yes, it really is empty, not not empty */
4091 lslOp op = (lslOp) dmalloc (sizeof (*op));
4093 op->name = nameNode_copy (nn);
4095 (void) sortSet_insert (n->possibleSorts, sigNode_rangeSort (x));
4096 (void) lslOpSet_insert (n->possibleOps, op);
4098 } end_sigNodeSet_elements;
4103 if (sortSet_size (n->possibleSorts) == 0)
4107 message ("Unrecognized identifier (constant, variable or operator): %s",
4108 ltoken_getRawString (varid)));
4112 n->sort = sort_makeNoSort ();
4114 n->kind = TRM_ZEROARY;
4122 makeSelectTermNode (termNode pri, ltoken select, /*@dependent@*/ ltoken id)
4124 termNode t = (termNode) dmalloc (sizeof (*t));
4125 opFormNode opform = makeOpFormNode (select,
4126 OPF_MSELECT, opFormUnion_createAnyOp (id),
4128 nameNode nn = makeNameNodeForm (opform);
4129 termNodeList args = termNodeList_new ();
4131 t->error_reported = FALSE;
4134 t->kind = TRM_APPLICATION;
4135 termNodeList_addh (args, pri);
4137 t->kind = TRM_APPLICATION;
4138 t->sort = sort_makeNoSort ();
4140 t->possibleSorts = sortSet_new ();
4141 t->possibleOps = lslOpSet_new ();
4147 makeMapTermNode (termNode pri, ltoken map, /*@dependent@*/ ltoken id)
4149 termNode t = (termNode) dmalloc (sizeof (*t));
4150 opFormNode opform = makeOpFormNode (map, OPF_MMAP, opFormUnion_createAnyOp (id),
4152 nameNode nn = makeNameNodeForm (opform);
4153 termNodeList args = termNodeList_new ();
4155 t->error_reported = FALSE;
4157 t->kind = TRM_APPLICATION;
4159 termNodeList_addh (args, pri);
4161 t->kind = TRM_APPLICATION;
4162 t->sort = sort_makeNoSort ();
4164 t->possibleSorts = sortSet_new ();
4165 t->possibleOps = lslOpSet_new ();
4170 makeLiteralTermNode (ltoken tok, sort s)
4172 nameNode nn = makeNameNodeId (ltoken_copy (tok));
4173 opInfo oi = symtable_opInfo (g_symtab, nn);
4174 lslOp op = (lslOp) dmalloc (sizeof (*op));
4175 termNode n = (termNode) dmalloc (sizeof (*n));
4180 n->error_reported = FALSE;
4182 n->kind = TRM_LITERAL;
4184 n->given = sort_makeNoSort ();
4186 n->args = termNodeList_new ();
4187 n->possibleSorts = sortSet_new ();
4188 n->possibleOps = lslOpSet_new ();
4190 /* look up signatures for this operator too */
4192 range = ltoken_create (simpleId, sort_getLsymbol (s));
4193 sign = makesigNode (ltoken_undefined, ltokenList_new (),
4194 ltoken_copy (range));
4196 if (opInfo_exists (oi) && (oi->name->isOpId)
4197 && (sigNodeSet_size (oi->signatures) > 0))
4199 sigNodeSet_elements (oi->signatures, x)
4201 if (ltokenList_empty (x->domain))
4203 lslOp opn = (lslOp) dmalloc (sizeof (*opn));
4206 opn->name = nameNode_copy (nn);
4208 sort = sigNode_rangeSort (x);
4209 (void) sortSet_insert (n->possibleSorts, sort);
4210 (void) lslOpSet_insert (n->possibleOps, opn);
4212 } end_sigNodeSet_elements;
4215 /* insert into literal term */
4216 (void) sortSet_insert (n->possibleSorts, s);
4218 op->name = nameNode_copy (nn);
4219 op->signature = sign;
4220 (void) lslOpSet_insert (n->possibleOps, op);
4222 /* enter the literal as an operator into the operator table */
4223 /* 8/9/93. C's char constant 'c' syntax conflicts
4224 with LSL's lslinit.lsi table. Throw out, because it's not
4226 /* symtable_enterOp (g_symtab, nn, sign); */
4231 lslOp opn = (lslOp) dmalloc (sizeof (*opn));
4233 /* if it is a C int, we should overload it as double too because
4234 C allows you to say "x > 2". */
4236 (void) sortSet_insert (n->possibleSorts, sort_double);
4238 ltoken_setText (range, lsymbol_fromChars ("double"));
4239 osign = makesigNode (ltoken_undefined, ltokenList_new (), range);
4240 opn->name = nameNode_copy (nn);
4241 opn->signature = osign;
4242 (void) lslOpSet_insert (n->possibleOps, opn);
4244 symtable_enterOp (g_symtab, nameNode_copySafe (nn), sigNode_copy (osign));
4248 ltoken_free (range);
4251 /* future: could overload cstrings to be both char_Vec as well as
4259 makeUnchangedTermNode1 (ltoken op, /*@unused@*/ ltoken all)
4261 termNode t = (termNode) dmalloc (sizeof (*t));
4263 t->error_reported = FALSE;
4265 t->kind = TRM_UNCHANGEDALL;
4266 t->sort = sort_bool;
4268 t->given = sort_makeNoSort ();
4269 t->name = NULL; /*< missing this >*/
4270 t->args = termNodeList_new ();
4271 t->possibleSorts = sortSet_new ();
4272 t->possibleOps = lslOpSet_new ();
4273 (void) sortSet_insert (t->possibleSorts, t->sort);
4281 makeUnchangedTermNode2 (ltoken op, storeRefNodeList x)
4283 termNode t = (termNode) dmalloc (sizeof (*t));
4287 t->name = NULL; /*< missing this >*/
4288 t->error_reported = FALSE;
4290 t->kind = TRM_UNCHANGEDOTHERS;
4291 t->sort = sort_bool;
4294 t->given = sort_makeNoSort ();
4295 t->possibleSorts = sortSet_new ();
4296 t->possibleOps = lslOpSet_new ();
4297 t->args = termNodeList_new ();
4299 (void) sortSet_insert (t->possibleSorts, t->sort);
4300 /* check storeRefNode's are mutable, uses sort of term */
4302 storeRefNodeList_elements (x, sto)
4304 if (storeRefNode_isTerm (sto))
4306 sort = sto->content.term->sort;
4307 if (!sort_mutable (sort))
4309 errtok = termNode_errorToken (sto->content.term);
4311 message ("Term denoting immutable object used in unchanged list: %q",
4312 termNode_unparse (sto->content.term)));
4317 if (storeRefNode_isType (sto))
4319 lclTypeSpecNode type = sto->content.type;
4320 sort = lclTypeSpecNode2sort (type);
4321 if (!sort_mutable (sort))
4323 errtok = lclTypeSpecNode_errorToken (type);
4324 lclerror (errtok, message ("Immutable type used in unchanged list: %q",
4325 sort_unparse (sort)));
4329 } end_storeRefNodeList_elements;
4335 makeSizeofTermNode (ltoken op, lclTypeSpecNode type)
4337 termNode t = (termNode) dmalloc (sizeof (*t));
4339 t->name = NULL; /*< missing this >*/
4340 t->error_reported = FALSE;
4342 t->kind = TRM_SIZEOF;
4345 t->sizeofField = type;
4346 t->given = sort_makeNoSort ();
4347 t->possibleSorts = sortSet_new ();
4348 t->possibleOps = lslOpSet_new ();
4349 t->args = termNodeList_new ();
4351 (void) sortSet_insert (t->possibleSorts, t->sort);
4352 /* nothing to check */
4357 claimNode_unparse (claimNode c)
4359 if (c != (claimNode) 0)
4361 cstring s = message ("claims (%q)%q{\n%q",
4362 paramNodeList_unparse (c->params),
4363 varDeclarationNodeList_unparse (c->globals),
4364 lclPredicateNode_unparse (c->require));
4366 if (c->body != NULL)
4368 s = message ("%qbody {%q}\n", s, programNode_unparse (c->body));
4370 s = message ("%q%q}\n", s, lclPredicateNode_unparse (c->ensures));
4373 return cstring_undefined;
4377 WrongArity (ltoken tok, int expect, int size)
4379 lclerror (tok, message ("Expecting %d arguments but given %d", expect, size));
4383 printTermNode2 (/*@null@*/ opFormNode op, termNodeList args, sort sort)
4385 if (op != (opFormNode) 0)
4387 cstring s = cstring_undefined;
4391 if (sort != sort_makeNoSort ())
4393 sortText = message (": %s", cstring_fromChars (lsymbol_toChars (sort_getLsymbol (sort))));
4394 sortSpace = cstring_makeLiteral (" ");
4398 sortText = cstring_undefined;
4399 sortSpace = cstring_undefined;
4406 int size = termNodeList_size (args);
4410 s = message ("if %q then %q else %q\n",
4411 termNode_unparse (termNodeList_getN (args, 0)),
4412 termNode_unparse (termNodeList_getN (args, 1)),
4413 termNode_unparse (termNodeList_getN (args, 2)));
4417 WrongArity (op->tok, 3, size);
4418 s = cstring_makeLiteral ("if __ then __ else __");
4420 s = message ("%q%s", s, sortText);
4425 s = message ("%s %s",
4426 ltoken_getRawString (op->content.anyop),
4432 int size = termNodeList_size (args);
4436 s = message ("%q ", termNode_unparse (termNodeList_head (args)));
4440 WrongArity (op->content.anyop, 1, size);
4441 s = cstring_makeLiteral ("__ ");
4443 s = message ("%q%s%s", s, ltoken_getRawString (op->content.anyop),
4449 int size = termNodeList_size (args);
4451 s = message ("%s ", ltoken_getRawString (op->content.anyop));
4455 s = message ("%q%q", s, termNode_unparse (termNodeList_head (args)));
4459 WrongArity (op->content.anyop, 1, size);
4460 s = message ("%q__", s);
4462 s = message ("%q%s", s, sortText);
4467 int size = termNodeList_size (args);
4471 s = message ("%q %s %q",
4472 termNode_unparse (termNodeList_getN (args, 0)),
4473 ltoken_getRawString (op->content.anyop),
4474 termNode_unparse (termNodeList_getN (args, 1)));
4478 WrongArity (op->content.anyop, 2, size);
4479 s = message ("__ %s __", ltoken_getRawString (op->content.anyop));
4481 s = message ("%q%s", s, sortText);
4486 int size = termNodeList_size (args);
4487 int expect = op->content.middle;
4489 /* ymtan ? use { or openSym token ? */
4493 s = message ("{%q}", termNodeList_unparse (args));
4497 WrongArity (op->tok, expect, size);
4498 s = cstring_makeLiteral ("{ * }");
4501 s = message ("%q%s", s, sortText);
4506 int size = termNodeList_size (args);
4507 int expect = op->content.middle + 1;
4511 s = message ("%q{%q}",
4512 termNode_unparse (termNodeList_head (args)),
4513 termNodeList_unparseTail (args));
4517 WrongArity (op->tok, expect, size);
4518 s = cstring_makeLiteral ("__ { * }");
4521 s = message ("%q%s", s, sortText);
4526 int size = termNodeList_size (args);
4527 int expect = op->content.middle + 1;
4531 termNodeList_finish (args);
4533 s = message ("{%q}%s%s%q",
4534 termNodeList_unparseToCurrent (args),
4535 sortText, sortSpace,
4536 termNode_unparse (termNodeList_current (args)));
4540 WrongArity (op->tok, expect, size);
4542 s = message ("{ * }%s __", sortText);
4544 /* used to put in extra space! evs 94-01-05 */
4550 int size = termNodeList_size (args);
4551 int expect = op->content.middle + 2;
4555 termNodeList_finish (args);
4557 s = message ("%q {%q} %s%s%q",
4558 termNode_unparse (termNodeList_head (args)),
4559 termNodeList_unparseSecondToCurrent (args),
4560 sortText, sortSpace,
4561 termNode_unparse (termNodeList_current (args)));
4565 WrongArity (op->tok, expect, size);
4566 s = message ("__ { * } %s __", sortText);
4568 /* also had extra space? */
4574 int size = termNodeList_size (args);
4575 int expect = op->content.middle;
4579 s = message ("[%q]", termNodeList_unparse (args));
4583 WrongArity (op->tok, expect, size);
4584 s = cstring_makeLiteral ("[ * ]");
4586 s = message ("%q%s", s, sortText);
4591 int size = termNodeList_size (args);
4592 int expect = op->content.middle + 1;
4596 s = message ("%q[%q]",
4597 termNode_unparse (termNodeList_head (args)),
4598 termNodeList_unparseTail (args));
4602 WrongArity (op->tok, expect, size);
4603 s = cstring_makeLiteral ("__ [ * ]");
4606 s = message ("%q%s", s, sortText);
4611 int size = termNodeList_size (args);
4612 int expect = op->content.middle + 1;
4616 s = message ("%q[%q] __",
4617 termNode_unparse (termNodeList_head (args)),
4618 termNodeList_unparseTail (args));
4622 WrongArity (op->tok, expect, size);
4623 s = cstring_makeLiteral ("__ [ * ] __");
4625 s = message ("%q%s", s, sortText);
4630 int size = termNodeList_size (args);
4631 int expect = op->content.middle + 1;
4635 termNodeList_finish (args);
4637 s = message ("[%q]%s%s%q",
4638 termNodeList_unparseToCurrent (args),
4639 sortText, sortSpace,
4640 termNode_unparse (termNodeList_current (args)));
4644 WrongArity (op->tok, expect, size);
4645 s = cstring_makeLiteral ("[ * ] __");
4651 { /* ymtan constant, check args ? */
4652 s = cstring_prependChar ('.', ltoken_getRawString (op->content.id));
4656 s = cstring_concat (cstring_makeLiteralTemp ("->"),
4657 ltoken_getRawString (op->content.id));
4661 int size = termNodeList_size (args);
4665 s = message ("%q.%s", termNode_unparse (termNodeList_head (args)),
4666 ltoken_getRawString (op->content.id));
4670 WrongArity (op->content.id, 1, size);
4671 s = cstring_concat (cstring_makeLiteralTemp ("__."),
4672 ltoken_getRawString (op->content.id));
4678 int size = termNodeList_size (args);
4682 s = message ("%q->%s", termNode_unparse (termNodeList_head (args)),
4683 ltoken_getRawString (op->content.id));
4687 WrongArity (op->content.id, 1, size);
4688 s = cstring_concat (cstring_makeLiteralTemp ("__->"),
4689 ltoken_getRawString (op->content.id));
4695 cstring_free (sortSpace);
4696 cstring_free (sortText);
4699 return cstring_undefined;
4703 termNode_unparse (/*@null@*/ termNode n)
4705 cstring s = cstring_undefined;
4706 cstring back = cstring_undefined;
4707 cstring front = cstring_undefined;
4710 if (n != (termNode) 0)
4712 for (count = n->wrapped; count > 0; count--)
4714 front = cstring_appendChar (front, '(');
4715 back = cstring_appendChar (back, ')');
4724 s = cstring_copy (ltoken_getRawString (n->literal));
4726 case TRM_APPLICATION:
4728 nameNode nn = n->name;
4729 if (nn != (nameNode) 0)
4733 s = message ("%s (%q) ",
4734 ltoken_getRawString (nn->content.opid),
4735 termNodeList_unparse (n->args));
4736 /* must we handle n->given ? skip for now */
4740 s = message ("%q ", printTermNode2 (nn->content.opform, n->args, n->given));
4746 (message ("termNode_unparse: expect non-empty nameNode: TRM_APPLICATION: %q",
4747 nameNode_unparse (nn)));
4751 case TRM_UNCHANGEDALL:
4752 s = cstring_makeLiteral ("unchanged (all)");
4754 case TRM_UNCHANGEDOTHERS:
4755 s = message ("unchanged (%q)", storeRefNodeList_unparse (n->unchanged));
4758 s = message ("sizeof (%q)", lclTypeSpecNode_unparse (n->sizeofField));
4760 case TRM_QUANTIFIER:
4762 quantifiedTermNode x = n->quantified;
4763 s = message ("%q%s%q%s",
4764 quantifierNodeList_unparse (x->quantifiers),
4765 ltoken_getRawString (x->open),
4766 termNode_unparse (x->body),
4767 ltoken_getRawString (x->close));
4772 return (message ("%q%q%q", front, s, back));
4775 static void modifyNode_free (/*@null@*/ /*@only@*/ modifyNode m)
4777 if (m != (modifyNode) 0)
4780 if (m->hasStoreRefList)
4782 storeRefNodeList_free (m->list);
4787 ltoken_free (m->tok);
4793 modifyNode_unparse (/*@null@*/ modifyNode m)
4795 if (m != (modifyNode) 0)
4797 if (m->hasStoreRefList)
4799 return (message (" modifies %q; \n", storeRefNodeList_unparse (m->list)));
4803 if (m->modifiesNothing)
4805 return (cstring_makeLiteral ("modifies nothing; \n"));
4809 return (cstring_makeLiteral ("modifies anything; \n"));
4813 return cstring_undefined;
4817 programNode_unparse (programNode p)
4819 if (p != (programNode) 0)
4821 cstring s = cstring_undefined;
4828 cstring back = cstring_undefined;
4830 for (count = p->wrapped; count > 0; count--)
4832 s = cstring_appendChar (s, '(');
4833 back = cstring_appendChar (back, ')');
4835 s = message ("%q%q%q", s, stmtNode_unparse (p->content.self), back);
4839 s = message ("*(%q)", programNodeList_unparse (p->content.args));
4842 s = message ("|(%q)", programNodeList_unparse (p->content.args));
4845 s = programNodeList_unparse (p->content.args);
4851 return cstring_undefined;
4855 stmtNode_unparse (stmtNode x)
4857 cstring s = cstring_undefined;
4859 if (x != (stmtNode) 0)
4861 if (ltoken_isValid (x->lhs))
4863 s = cstring_concat (ltoken_getRawString (x->lhs),
4864 cstring_makeLiteralTemp (" = "));
4867 s = message ("%q%s (%q)", s,
4868 ltoken_getRawString (x->operator),
4869 termNodeList_unparse (x->args));
4876 makelslOpNode (/*@only@*/ /*@null@*/ nameNode name,
4877 /*@dependent@*/ sigNode s)
4879 lslOp x = (lslOp) dmalloc (sizeof (*x));
4884 /* enter operator info into symtab */
4885 /* if not, they may need to be renamed in LCL imports */
4887 if (g_lslParsingTraits)
4891 symtable_enterOp (g_symtab, nameNode_copySafe (name), sigNode_copy (s));
4896 /* nameNode_free (name); */ /* YIKES! */
4903 lslOp_unparse (lslOp x)
4905 char *s = mstring_createEmpty ();
4909 s = mstring_concatFree (s, cstring_toCharsSafe (nameNode_unparse (x->name)));
4911 if (x->signature != (sigNode) 0)
4913 s = mstring_concatFree (s, cstring_toCharsSafe (sigNode_unparse (x->signature)));
4917 return cstring_fromCharsO (s);
4921 sameOpFormNode (/*@null@*/ opFormNode n1, /*@null@*/ opFormNode n2)
4932 if (n1->kind == n2->kind)
4941 return (ltoken_similar (n1->content.anyop, n2->content.anyop));
4944 /* want to treat eq and = the same */
4945 return ltoken_similar (n1->content.anyop, n2->content.anyop);
4951 /* need to check the rawText of openSym and closeSym */
4952 if ((int) n1->content.middle == (int) n2->content.middle)
4954 if (lsymbol_equal (ltoken_getRawText (n1->tok),
4955 ltoken_getRawText (n2->tok)) &&
4956 lsymbol_equal (ltoken_getRawText (n1->close),
4957 ltoken_getRawText (n2->close)))
4965 return ((int) n1->content.middle == (int) n2->content.middle);
4970 return (ltoken_similar (n1->content.id, n2->content.id));
4977 sameNameNode (/*@null@*/ nameNode n1, /*@null@*/ nameNode n2)
4981 if (n1 != (nameNode) 0 && n2 != (nameNode) 0)
4983 if (bool_equal (n1->isOpId, n2->isOpId))
4986 return (ltoken_similar (n1->content.opid, n2->content.opid));
4988 return sameOpFormNode (n1->content.opform,
4989 n2->content.opform);
4995 void CTypesNode_free (/*@only@*/ /*@null@*/ CTypesNode x)
4999 ltokenList_free (x->ctypes);
5004 /*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode x)
5008 CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5009 newnode->intfield = x->intfield;
5010 newnode->ctypes = ltokenList_copy (x->ctypes);
5011 newnode->sort = x->sort;
5021 /*@only@*/ CTypesNode
5022 makeCTypesNode (/*@only@*/ CTypesNode ctypes, ltoken ct)
5024 /*@only@*/ CTypesNode newnode;
5028 if (ctypes == (CTypesNode) NULL)
5030 newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5031 newnode->intfield = 0;
5032 newnode->ctypes = ltokenList_new ();
5033 newnode->sort = sort_makeNoSort ();
5040 if ((ltoken_getIntField (ct) & newnode->intfield) != 0)
5044 ("Duplicate type specifier ignored: %s",
5047 (lclctype_toSortDebug (ltoken_getIntField (ct))))));
5049 /* evs --- don't know how to generator this error */
5051 /* Use previous value, to keep things consistent */
5056 sortbits = newnode->intfield | ltoken_getIntField (ct);
5057 sortname = lclctype_toSort (sortbits);
5059 if (sortname == lsymbol_fromChars ("error"))
5061 lclerror (ct, cstring_makeLiteral ("Invalid combination of type specifiers"));
5065 newnode->intfield = sortbits;
5068 ltokenList_addh (newnode->ctypes, ct);
5071 ** Sorts are assigned after CTypesNode is created during parsing,
5072 ** see bison grammar.
5078 /*@only@*/ CTypesNode
5079 makeTypeSpecifier (ltoken typedefname)
5081 CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode));
5082 typeInfo ti = symtable_typeInfo (g_symtab, ltoken_getText (typedefname));
5084 newnode->intfield = 0;
5085 newnode->ctypes = ltokenList_singleton (ltoken_copy (typedefname));
5087 /* if we see "bool" include bool.h header file */
5089 if (ltoken_getText (typedefname) == lsymbol_bool)
5094 if (typeInfo_exists (ti))
5096 /* must we be concern about whether this type is exported by module?
5097 No. Because all typedef's are exported. No hiding supported. */
5098 /* Later, may want to keep types around too */
5099 /* 3/2/93, use underlying sort */
5100 newnode->sort = sort_getUnderlying (ti->basedOn);
5104 lclerror (typedefname, message ("Unrecognized type: %s",
5105 ltoken_getRawString (typedefname)));
5106 /* evs --- Don't know how to get this message */
5108 newnode->sort = sort_makeNoSort ();
5111 ltoken_free (typedefname);
5115 bool sigNode_equal (sigNode n1, sigNode n2)
5117 /* n1 and n2 are never 0 */
5119 return ((n1 == n2) ||
5120 (n1->key == n2->key &&
5121 ltoken_similar (n1->range, n2->range) &&
5122 ltokenList_equal (n1->domain, n2->domain)));
5126 typeExpr2ptrSort (sort base, /*@null@*/ typeExpr t)
5128 if (t != (typeExpr) 0)
5135 return typeExpr2ptrSort (sort_makePtr (ltoken_undefined, base),
5136 t->content.pointer);
5138 return typeExpr2ptrSort (sort_makeArr (ltoken_undefined, base),
5139 t->content.array.elementtype);
5141 /* map all hof types to some sort of SRT_HOF */
5142 return sort_makeHOFSort (base);
5149 typeExpr2returnSort (sort base, /*@null@*/ typeExpr t)
5151 if (t != (typeExpr) 0)
5158 return typeExpr2returnSort (sort_makePtr (ltoken_undefined, base),
5159 t->content.pointer);
5161 return typeExpr2returnSort (sort_makeArr (ltoken_undefined, base),
5162 t->content.array.elementtype);
5164 return typeExpr2returnSort (base, t->content.function.returntype);
5171 lclTypeSpecNode2sort (lclTypeSpecNode type)
5173 if (type != (lclTypeSpecNode) 0)
5178 llassert (type->content.type != NULL);
5179 return sort_makePtrN (type->content.type->sort, type->pointers);
5180 case LTS_STRUCTUNION:
5181 llassert (type->content.structorunion != NULL);
5182 return sort_makePtrN (type->content.structorunion->sort, type->pointers);
5184 llassert (type->content.enumspec != NULL);
5185 return sort_makePtrN (type->content.enumspec->sort, type->pointers);
5187 return (lclTypeSpecNode2sort (type->content.conj->a));
5190 return (sort_makeNoSort ());
5194 checkAndEnterTag (tagKind k, ltoken opttagid)
5196 /* should be tagKind, instead of int */
5198 sort sort = sort_makeNoSort ();
5200 if (!ltoken_isUndefined (opttagid))
5206 sort = sort_makeStr (opttagid);
5210 sort = sort_makeUnion (opttagid);
5213 sort = sort_makeEnum (opttagid);
5217 /* see if it is already in symbol table */
5218 t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid));
5220 if (tagInfo_exists (t))
5222 if (t->kind == TAG_FWDUNION || t->kind == TAG_FWDSTRUCT)
5224 /* this is fine, for mutually recursive types */
5227 { /* this is not good, complain later */
5233 s = cstring_makeLiteral ("Enum");
5237 s = cstring_makeLiteral ("Struct");
5241 s = cstring_makeLiteral ("Union");
5248 message ("Tag redefined: %q %s", s,
5249 ltoken_getRawString (opttagid)));
5253 ltoken_free (opttagid);
5257 tagInfo newnode = (tagInfo) dmalloc (sizeof (*newnode));
5259 newnode->sort = sort;
5261 newnode->id = opttagid;
5262 newnode->imported = FALSE;
5263 newnode->content.decls = stDeclNodeList_new ();
5265 (void) symtable_enterTag (g_symtab, newnode);
5269 return sort_getLsymbol (sort);
5273 extractReturnSort (lclTypeSpecNode t, declaratorNode d)
5276 sort = lclTypeSpecNode2sort (t);
5277 sort = typeExpr2returnSort (sort, d->type);
5282 signNode_free (/*@only@*/ signNode sn)
5284 sortList_free (sn->domain);
5285 ltoken_free (sn->tok);
5290 signNode_unparse (signNode sn)
5292 cstring s = cstring_undefined;
5294 if (sn != (signNode) 0)
5296 s = message (": %q -> %s", sortList_unparse (sn->domain),
5297 sort_unparseName (sn->range));
5302 static /*@only@*/ pairNodeList
5303 globalList_toPairNodeList (globalList g)
5305 /* expect list to be globals, drop private ones */
5306 pairNodeList result = pairNodeList_new ();
5308 declaratorNode vdnode;
5309 lclTypeSpecNode type;
5312 initDeclNodeList decls;
5314 varDeclarationNodeList_elements (g, x)
5322 if (x->isGlobal && !x->isPrivate)
5327 initDeclNodeList_elements (decls, init)
5329 p = (pairNode) dmalloc (sizeof (*p));
5331 vdnode = init->declarator;
5332 sym = ltoken_getText (vdnode->id);
5333 /* 2/21/93, not sure if it should be extractReturnSort,
5334 or some call to typeExpr2ptrSort */
5335 sort = extractReturnSort (type, vdnode);
5336 p->sort = sort_makeGlobal (sort);
5337 /* if (!sort_isArrayKind (sort)) p->sort = sort_makeObj (sort);
5338 else p->sort = sort; */
5339 /* p->name = sym; */
5340 p->tok = ltoken_copy (vdnode->id);
5341 pairNodeList_addh (result, p);
5342 } end_initDeclNodeList_elements;
5345 } end_varDeclarationNodeList_elements;
5350 enteringFcnScope (lclTypeSpecNode t, declaratorNode d, globalList g)
5352 scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
5353 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5355 ltoken result = ltoken_copy (ltoken_id);
5356 pairNodeList paramPairs, globals;
5357 fctInfo fi = (fctInfo) dmalloc (sizeof (*fi));
5358 signNode sign = (signNode) dmalloc (sizeof (*sign));
5359 sortList domain = sortList_new ();
5362 paramPairs = extractParams (d->type);
5363 returnSort = extractReturnSort (t, d);
5364 globals = globalList_toPairNodeList (g);
5366 sign->tok = ltoken_undefined;
5367 sign->range = returnSort;
5369 key = MASH (0, sort_getLsymbol (returnSort));
5371 pairNodeList_elements (paramPairs, p)
5373 sortList_addh (domain, p->sort);
5374 key = MASH (key, sort_getLsymbol (p->sort));
5375 } end_pairNodeList_elements;
5377 sign->domain = domain;
5380 /* push fcn onto symbol table stack first */
5381 fi->id = ltoken_copy (d->id);
5383 fi->signature = sign;
5384 fi->globals = globals;
5386 (void) symtable_enterFct (g_symtab, fi);
5388 /* push new fcn scope */
5390 symtable_enterScope (g_symtab, si);
5392 /* add "result" with return type to current scope */
5393 ltoken_setText (result, lsymbol_fromChars ("result"));
5396 vi->sort = sort_makeFormal (returnSort); /* make appropriate values */
5397 vi->kind = VRK_PARAM;
5400 (void) symtable_enterVar (g_symtab, vi);
5404 ** pust globals first (they are in outer scope)
5407 /* push onto symbol table the global variables declared in this function,
5408 together with their respective sorts */
5410 pairNodeList_elements (globals, gl)
5412 ltoken_free (vi->id);
5413 vi->id = ltoken_copy (gl->tok);
5414 vi->kind = VRK_GLOBAL;
5415 vi->sort = gl->sort;
5416 (void) symtable_enterVar (g_symtab, vi);
5417 } end_pairNodeList_elements;
5420 ** could enter a new scope; instead, warn when variable shadows global
5425 ** push onto symbol table the formal parameters of this function,
5426 ** together with their respective sorts
5429 pairNodeList_elements (paramPairs, pair)
5431 ltoken_free (vi->id);
5432 vi->id = ltoken_copy (pair->tok);
5433 vi->sort = pair->sort;
5434 vi->kind = VRK_PARAM;
5435 (void) symtable_enterVar (g_symtab, vi);
5436 } end_pairNodeList_elements;
5438 pairNodeList_free (paramPairs);
5443 enteringClaimScope (paramNodeList params, globalList g)
5445 scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
5446 pairNodeList globals;
5447 lclTypeSpecNode paramtype;
5451 globals = globalList_toPairNodeList (g);
5452 /* push new claim scope */
5453 si->kind = SPE_CLAIM;
5455 symtable_enterScope (g_symtab, si);
5457 /* push onto symbol table the formal parameters of this function,
5458 together with their respective sorts */
5460 paramNodeList_elements (params, param)
5462 paramdecl = param->paramdecl;
5463 paramtype = param->type;
5464 if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0)
5466 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5468 sort = lclTypeSpecNode2sort (paramtype);
5469 sort = sort_makeFormal (sort);
5470 vi->sort = typeExpr2ptrSort (sort, paramdecl);
5471 vi->id = ltoken_copy (extractDeclarator (paramdecl));
5472 vi->kind = VRK_PARAM;
5475 (void) symtable_enterVar (g_symtab, vi);
5478 } end_paramNodeList_elements;
5480 /* push onto symbol table the global variables declared in this function,
5481 together with their respective sorts */
5483 pairNodeList_elements (globals, g2)
5485 varInfo vi = (varInfo) dmalloc (sizeof (*vi));
5487 vi->id = ltoken_copy (g2->tok);
5488 vi->kind = VRK_GLOBAL;
5489 vi->sort = g2->sort;
5492 /* should catch duplicates in formals */
5493 (void) symtable_enterVar (g_symtab, vi);
5495 } end_pairNodeList_elements;
5497 pairNodeList_free (globals);
5498 /* should not free it here! ltoken_free (claimId); @*/
5501 static /*@only@*/ pairNodeList
5502 extractParams (/*@null@*/ typeExpr te)
5504 /* extract the parameters from a function header declarator's typeExpr */
5507 paramNodeList params;
5508 lclTypeSpecNode paramtype;
5509 pairNodeList head = pairNodeList_new ();
5512 if (te != (typeExpr) 0)
5514 params = typeExpr_toParamNodeList (te);
5515 if (paramNodeList_isDefined (params))
5517 paramNodeList_elements (params, param)
5519 paramdecl = param->paramdecl;
5520 paramtype = param->type;
5521 if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0)
5523 pair = (pairNode) dmalloc (sizeof (*pair));
5524 sort = lclTypeSpecNode2sort (paramtype);
5525 /* 2/17/93, was sort_makeVal (sort) */
5526 sort = sort_makeFormal (sort);
5527 pair->sort = typeExpr2ptrSort (sort, paramdecl);
5528 /* pair->name = ltoken_getText (extractDeclarator (paramdecl)); */
5529 pair->tok = ltoken_copy (extractDeclarator (paramdecl));
5530 pairNodeList_addh (head, pair);
5532 } end_paramNodeList_elements;
5539 sigNode_rangeSort (sigNode sig)
5541 if (sig == (sigNode) 0)
5543 return sort_makeNoSort ();
5547 return sort_fromLsymbol (ltoken_getText (sig->range));
5552 sigNode_domain (sigNode sig)
5554 sortList domain = sortList_new ();
5556 if (sig == (sigNode) 0)
5562 ltokenList dom = sig->domain;
5564 ltokenList_elements (dom, tok)
5566 sortList_addh (domain, sort_fromLsymbol (ltoken_getText (tok)));
5567 } end_ltokenList_elements;
5574 opFormUnion_createAnyOp (/*@temp@*/ ltoken t)
5578 /* do not distinguish between .anyop and .id */
5584 opFormUnion_createMiddle (int middle)
5593 markYieldParamNode (paramNode p)
5597 llassert (p->type != NULL);
5598 p->type->quals = qualList_add (p->type->quals, qual_createYield ());
5603 /*@only@*/ lclTypeSpecNode
5604 lclTypeSpecNode_copySafe (lclTypeSpecNode n)
5606 lclTypeSpecNode ret = lclTypeSpecNode_copy (n);
5608 llassert (ret != NULL);
5612 /*@null@*/ /*@only@*/ lclTypeSpecNode
5613 lclTypeSpecNode_copy (/*@null@*/ lclTypeSpecNode n)
5620 return (makeLclTypeSpecNodeConj (lclTypeSpecNode_copy (n->content.conj->a),
5621 lclTypeSpecNode_copy (n->content.conj->b)));
5623 return (makeLclTypeSpecNodeType (CTypesNode_copy (n->content.type)));
5624 case LTS_STRUCTUNION:
5625 return (makeLclTypeSpecNodeSU (strOrUnionNode_copy (n->content.structorunion)));
5627 return (makeLclTypeSpecNodeEnum (enumSpecNode_copy (n->content.enumspec)));
5634 void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode n)
5641 lclTypeSpecNode_free (n->content.conj->a);
5642 lclTypeSpecNode_free (n->content.conj->b);
5645 CTypesNode_free (n->content.type);
5647 case LTS_STRUCTUNION:
5648 strOrUnionNode_free (n->content.structorunion);
5651 enumSpecNode_free (n->content.enumspec);
5655 qualList_free (n->quals);
5660 static /*@null@*/ opFormNode opFormNode_copy (/*@null@*/ opFormNode op)
5664 opFormNode ret = (opFormNode) dmalloc (sizeof (*ret));
5666 ret->tok = ltoken_copy (op->tok);
5667 ret->kind = op->kind;
5668 ret->content = op->content;
5670 ret->close = ltoken_copy (op->close);
5680 void opFormNode_free (/*@null@*/ opFormNode op)
5684 ltoken_free (op->tok);
5685 ltoken_free (op->close);
5690 void nameNode_free (nameNode n)
5697 opFormNode_free (n->content.opform);
5705 lslOp_equal (lslOp x, lslOp y)
5708 ((x != 0) && (y != 0) &&
5709 sameNameNode (x->name, y->name) &&
5710 sigNode_equal (x->signature, y->signature)));
5713 void lslOp_free (lslOp x)
5715 nameNode_free (x->name);
5719 void sigNode_free (sigNode x)
5723 ltokenList_free (x->domain);
5724 ltoken_free (x->tok);
5725 ltoken_free (x->range);
5730 void declaratorNode_free (/*@null@*/ /*@only@*/ declaratorNode x)
5734 typeExpr_free (x->type);
5735 ltoken_free (x->id);
5740 void abstBodyNode_free (/*@null@*/ /*@only@*/ abstBodyNode n)
5744 lclPredicateNode_free (n->typeinv);
5745 fcnNodeList_free (n->fcns);
5746 ltoken_free (n->tok);
5751 void fcnNode_free (/*@null@*/ /*@only@*/ fcnNode f)
5755 lclTypeSpecNode_free (f->typespec);
5756 declaratorNode_free (f->declarator);
5757 globalList_free (f->globals);
5758 varDeclarationNodeList_free (f->inits);
5759 letDeclNodeList_free (f->lets);
5760 lclPredicateNode_free (f->checks);
5761 lclPredicateNode_free (f->require);
5762 lclPredicateNode_free (f->claim);
5763 lclPredicateNode_free (f->ensures);
5764 modifyNode_free (f->modify);
5765 ltoken_free (f->name);
5770 void declaratorInvNode_free (/*@null@*/ /*@only@*/ declaratorInvNode x)
5774 declaratorNode_free (x->declarator);
5775 abstBodyNode_free (x->body);
5780 /*@only@*/ lslOp lslOp_copy (lslOp x)
5782 return (makelslOpNode (nameNode_copy (x->name), x->signature));
5785 sigNode sigNode_copy (sigNode s)
5787 llassert (s != NULL);
5788 return (makesigNode (ltoken_copy (s->tok),
5789 ltokenList_copy (s->domain),
5790 ltoken_copy (s->range)));
5793 /*@null@*/ nameNode nameNode_copy (/*@null@*/ nameNode n)
5795 if (n == NULL) return NULL;
5796 return nameNode_copySafe (n);
5799 nameNode nameNode_copySafe (nameNode n)
5803 return (makeNameNodeId (ltoken_copy (n->content.opid)));
5807 /* error should be detected by splint: forgot to copy opform! */
5808 return (makeNameNodeForm (opFormNode_copy (n->content.opform)));
5812 bool initDeclNode_isRedeclaration (initDeclNode d)
5814 return (d->declarator->isRedecl);
5817 void termNode_free (/*@only@*/ /*@null@*/ termNode t)
5821 sortSet_free (t->possibleSorts);
5822 lslOpSet_free (t->possibleOps);
5823 nameNode_free (t->name);
5824 termNodeList_free (t->args);
5829 /*@only@*/ termNode termNode_copySafe (termNode t)
5831 termNode ret = termNode_copy (t);
5833 llassert (ret != NULL);
5837 /*@null@*/ /*@only@*/ termNode termNode_copy (/*@null@*/ termNode t)
5841 termNode ret = (termNode) dmalloc (sizeof (*ret));
5843 ret->wrapped = t->wrapped;
5844 ret->kind = t->kind;
5845 ret->sort = t->sort;
5846 ret->given = t->given;
5847 ret->possibleSorts = sortSet_copy (t->possibleSorts);
5848 ret->error_reported = t->error_reported;
5849 ret->possibleOps = lslOpSet_copy (t->possibleOps);
5850 ret->name = nameNode_copy (t->name);
5851 ret->args = termNodeList_copy (t->args);
5853 if (t->kind == TRM_LITERAL
5854 || t->kind == TRM_SIZEOF
5855 || t->kind == TRM_VAR
5856 || t->kind == TRM_CONST
5857 || t->kind == TRM_ZEROARY)
5859 ret->literal = ltoken_copy (t->literal);
5862 if (t->kind == TRM_UNCHANGEDOTHERS)
5864 ret->unchanged = storeRefNodeList_copy (t->unchanged);
5867 if (t->kind == TRM_QUANTIFIER)
5869 ret->quantified = quantifiedTermNode_copy (t->quantified);
5872 if (t->kind == TRM_SIZEOF)
5874 ret->sizeofField = lclTypeSpecNode_copySafe (t->sizeofField);
5886 void importNode_free (/*@only@*/ /*@null@*/ importNode x)
5890 ltoken_free (x->val);
5895 void initDeclNode_free (/*@only@*/ /*@null@*/ initDeclNode x)
5899 declaratorNode_free (x->declarator);
5900 termNode_free (x->value);
5905 void letDeclNode_free (/*@only@*/ /*@null@*/ letDeclNode x)
5909 lclTypeSpecNode_free (x->sortspec);
5910 termNode_free (x->term);
5911 ltoken_free (x->varid);
5916 void pairNode_free (/*@only@*/ /*@null@*/ pairNode x)
5920 ltoken_free (x->tok);
5925 /*@null@*/ paramNode paramNode_copy (/*@null@*/ paramNode p)
5929 paramNode ret = (paramNode) dmalloc (sizeof (*ret));
5931 ret->type = lclTypeSpecNode_copy (p->type);
5932 ret->paramdecl = typeExpr_copy (p->paramdecl);
5933 ret->kind = p->kind;
5940 void paramNode_free (/*@only@*/ /*@null@*/ paramNode x)
5944 lclTypeSpecNode_free (x->type);
5945 typeExpr_free (x->paramdecl);
5950 void programNode_free (/*@only@*/ /*@null@*/ programNode x)
5956 case ACT_SELF: stmtNode_free (x->content.self); break;
5959 case ACT_SEQUENCE: programNodeList_free (x->content.args); break;
5966 quantifierNode quantifierNode_copy (quantifierNode x)
5968 quantifierNode ret = (quantifierNode) dmalloc (sizeof (*ret));
5970 ret->quant = ltoken_copy (x->quant);
5971 ret->vars = varNodeList_copy (x->vars);
5972 ret->isForall = x->isForall;
5977 void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode x)
5981 varNodeList_free (x->vars);
5982 ltoken_free (x->quant);
5987 void replaceNode_free (/*@only@*/ /*@null@*/ replaceNode x)
5997 nameNode_free (x->content.renamesortname.name);
5998 sigNode_free (x->content.renamesortname.signature);
6001 typeNameNode_free (x->typename);
6002 ltoken_free (x->tok);
6007 storeRefNode storeRefNode_copy (storeRefNode x)
6009 storeRefNode ret = (storeRefNode) dmalloc (sizeof (*ret));
6011 ret->kind = x->kind;
6016 ret->content.term = termNode_copySafe (x->content.term);
6018 case SRN_OBJ: case SRN_TYPE:
6019 ret->content.type = lclTypeSpecNode_copy (x->content.type);
6022 ret->content.ref = sRef_copy (x->content.ref);
6029 void storeRefNode_free (/*@only@*/ /*@null@*/ storeRefNode x)
6033 if (storeRefNode_isTerm (x))
6035 termNode_free (x->content.term);
6037 else if (storeRefNode_isType (x) || storeRefNode_isObj (x))
6039 lclTypeSpecNode_free (x->content.type);
6043 /* nothing to free */
6050 stDeclNode stDeclNode_copy (stDeclNode x)
6052 stDeclNode ret = (stDeclNode) dmalloc (sizeof (*ret));
6054 ret->lcltypespec = lclTypeSpecNode_copySafe (x->lcltypespec);
6055 ret->declarators = declaratorNodeList_copy (x->declarators);
6060 void stDeclNode_free (/*@only@*/ /*@null@*/ stDeclNode x)
6064 lclTypeSpecNode_free (x->lcltypespec);
6065 declaratorNodeList_free (x->declarators);
6070 void traitRefNode_free (/*@only@*/ /*@null@*/ traitRefNode x)
6074 ltokenList_free (x->traitid);
6075 renamingNode_free (x->rename);
6080 void typeNameNode_free (/*@only@*/ /*@null@*/ typeNameNode n)
6084 typeNamePack_free (n->typename);
6085 opFormNode_free (n->opform);
6090 void varDeclarationNode_free (/*@only@*/ /*@null@*/ varDeclarationNode x)
6100 lclTypeSpecNode_free (x->type);
6101 initDeclNodeList_free (x->decls);
6107 varNode varNode_copy (varNode x)
6109 varNode ret = (varNode) dmalloc (sizeof (*ret));
6111 ret->varid = ltoken_copy (x->varid);
6112 ret->isObj = x->isObj;
6113 ret->type = lclTypeSpecNode_copySafe (x->type);
6114 ret->sort = x->sort;
6119 void varNode_free (/*@only@*/ /*@null@*/ varNode x)
6123 lclTypeSpecNode_free (x->type);
6124 ltoken_free (x->varid);
6129 void stmtNode_free (/*@only@*/ /*@null@*/ stmtNode x)
6133 ltoken_free (x->lhs);
6134 termNodeList_free (x->args);
6135 ltoken_free (x->operator);
6140 void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode x)
6146 replaceNodeList_free (x->content.replace);
6150 nameAndReplaceNode_free (x->content.name);
6157 void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode x)
6161 typeNameNodeList_free (x->namelist);
6162 replaceNodeList_free (x->replacelist);
6167 void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack x)
6171 lclTypeSpecNode_free (x->type);
6172 abstDeclaratorNode_free (x->abst);
6177 cstring interfaceNode_unparse (interfaceNode x)
6184 return (message ("[imports] %q", importNodeList_unparse (x->content.imports)));
6186 return (message ("[uses] %q", traitRefNodeList_unparse (x->content.uses)));
6188 return (message ("[export] %q", exportNode_unparse (x->content.export)));
6190 return (message ("[private] %q", privateNode_unparse (x->content.private)));
6197 return (cstring_makeLiteral ("<interface node undefined>"));
6200 BADBRANCHRET (cstring_undefined);
6203 void interfaceNode_free (/*@null@*/ /*@only@*/ interfaceNode x)
6210 case INF_IMPORTS: importNodeList_free (x->content.imports); break;
6211 case INF_USES: traitRefNodeList_free (x->content.uses); break;
6212 case INF_EXPORT: exportNode_free (x->content.export); break;
6213 case INF_PRIVATE: privateNode_free (x->content.private); break;
6219 void exportNode_free (/*@null@*/ /*@only@*/ exportNode x)
6225 case XPK_CONST: constDeclarationNode_free (x->content.constdeclaration); break;
6226 case XPK_VAR: varDeclarationNode_free (x->content.vardeclaration); break;
6227 case XPK_TYPE: typeNode_free (x->content.type); break;
6228 case XPK_FCN: fcnNode_free (x->content.fcn); break;
6229 case XPK_CLAIM: claimNode_free (x->content.claim); break;
6230 case XPK_ITER: iterNode_free (x->content.iter); break;
6237 void privateNode_free (/*@null@*/ /*@only@*/ privateNode x)
6244 constDeclarationNode_free (x->content.constdeclaration); break;
6246 varDeclarationNode_free (x->content.vardeclaration); break;
6248 typeNode_free (x->content.type); break;
6250 fcnNode_free (x->content.fcn); break;
6257 void constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode x)
6261 lclTypeSpecNode_free (x->type);
6262 initDeclNodeList_free (x->decls);
6267 void typeNode_free (/*@only@*/ /*@null@*/ typeNode t)
6273 case TK_ABSTRACT: abstractNode_free (t->content.abstract); break;
6274 case TK_EXPOSED: exposedNode_free (t->content.exposed); break;
6275 case TK_UNION: taggedUnionNode_free (t->content.taggedunion); break;
6282 void claimNode_free (/*@only@*/ /*@null@*/ claimNode x)
6286 paramNodeList_free (x->params);
6287 globalList_free (x->globals);
6288 letDeclNodeList_free (x->lets);
6289 lclPredicateNode_free (x->require);
6290 programNode_free (x->body);
6291 lclPredicateNode_free (x->ensures);
6292 ltoken_free (x->name);
6297 void iterNode_free (/*@only@*/ /*@null@*/ iterNode x)
6301 paramNodeList_free (x->params);
6302 ltoken_free (x->name);
6307 void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode x)
6311 abstBodyNode_free (x->body);
6312 ltoken_free (x->tok);
6313 ltoken_free (x->name);
6318 void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode x)
6322 lclTypeSpecNode_free (x->type);
6323 declaratorInvNodeList_free (x->decls);
6324 ltoken_free (x->tok);
6329 void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode x)
6333 stDeclNodeList_free (x->structdecls);
6334 declaratorNode_free (x->declarator);
6339 /*@only@*/ /*@null@*/ strOrUnionNode
6340 strOrUnionNode_copy (/*@null@*/ strOrUnionNode n)
6344 strOrUnionNode ret = (strOrUnionNode) dmalloc (sizeof (*ret));
6346 ret->kind = n->kind;
6347 ret->tok = ltoken_copy (n->tok);
6348 ret->opttagid = ltoken_copy (n->opttagid);
6349 ret->sort = n->sort;
6350 ret->structdecls = stDeclNodeList_copy (n->structdecls);
6360 void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode n)
6364 stDeclNodeList_free (n->structdecls);
6365 ltoken_free (n->tok);
6366 ltoken_free (n->opttagid);
6371 void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode x)
6375 ltokenList_free (x->enums);
6376 ltoken_free (x->tok);
6377 ltoken_free (x->opttagid);
6382 /*@only@*/ /*@null@*/ enumSpecNode enumSpecNode_copy (/*@null@*/ enumSpecNode x)
6386 enumSpecNode ret = (enumSpecNode) dmalloc (sizeof (*ret));
6388 ret->tok = ltoken_copy (x->tok);
6389 ret->opttagid = ltoken_copy (x->opttagid);
6390 ret->enums = ltokenList_copy (x->enums);
6391 ret->sort = x->sort;
6401 void lsymbol_setbool (lsymbol s)
6406 lsymbol lsymbol_getbool ()
6408 return lsymbol_bool;
6411 lsymbol lsymbol_getBool ()
6413 return lsymbol_Bool;
6416 lsymbol lsymbol_getFALSE ()
6418 return lsymbol_FALSE;
6421 lsymbol lsymbol_getTRUE ()
6423 return lsymbol_TRUE;