src/abstract.c

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