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