src/abstract.c

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