src/llgrammar.y

   1 /*;-*-C-*-;
   2 ** Copyright (c) Massachusetts Institute of Technology 1994-1998.
   3 **          All Rights Reserved.
   4 **          Unpublished rights reserved under the copyright laws of
   5 **          the United States.
   6 **
   7 ** THIS MATERIAL IS PROVIDED AS IS, WITH ABSOLUTELY NO WARRANTY EXPRESSED
   8 ** OR IMPLIED.  ANY USE IS AT YOUR OWN RISK.
   9 **
  10 ** This code is distributed freely and may be used freely under the
  11 ** following conditions:
  12 **
  13 **     1. This notice may not be removed or altered.
  14 **
  15 **     2. Works derived from this code are not distributed for
  16 **        commercial gain without explicit permission from MIT
  17 **        (for permission contact lclint-request@sds.lcs.mit.edu).
  18 */
  19 /*
  20 **       Copyright (c) Massachusetts Institute of Technology, 1993
  21 **          All Rights Reserved.  Unpublished rights reserved
  22 **          under the copyright laws of the United States.
  23 **++
  24 **  FACILITY:  LSLC
  25 **
  26 **  MODULE DESCRIPTION:
  27 **
  28 **      FILENAME: llgramar.y
  29 **
  30 **      PURPOSE:  bison grammar for LCL language.
  31 **
  32 **  AUTHORS:
  33 **      Yang Meng Tan, Massachusetts Institute of Technology
  34 */
  35
  36 %{
  37
  38 # include "lclintMacros.nf"
  39 # include "llbasic.h"
  40 # include "lclscan.h"
  41 # include "checking.h"
  42 # include "lslparse.h"
  43 # include "lh.h"
  44 # include "usymtab_interface.h"
  45
  46 /*@-noparams@*/
  47 static /*@unused@*/ void yyprint ();
  48 /*@=noparams@*/
  49
  50 /*@-redecl@*/
  51 void ylerror (char *) /*@modifies *g_msgstream@*/ ;
  52 /*@=redecl@*/
  53
  54 bool g_inTypeDef = FALSE;
  55
  56 /*@constant int YYDEBUG;@*/
  57 # define YYDEBUG 1
  58
  59 /*@notfunction@*/
  60 # define YYPRINT(file, type, value) yyprint (file, type, value)
  61
  62 /*
  63 ** This is necessary, or else when the bison-generated code #include's malloc.h,
  64 ** there will be a parse error.
  65 **
  66 ** Unfortunately, it means the error checking on malloc, etc. is lost for allocations
  67 ** in bison-generated files under Win32.
  68 */
  69
  70 # ifdef WIN32
  71 # undef malloc
  72 # undef calloc
  73 # undef realloc
  74 # endif
  75
  76 %}
  77
  78 /*@-readonlytrans@*/
  79
  80 %union
  81 {
  82   ltoken ltok;  /* a leaf is also an ltoken */
  83   qual typequal;
  84   unsigned int count;
  85   /*@only@*/ ltokenList ltokenList;
  86   /*@only@*/ abstDeclaratorNode abstDecl;
  87   /*@only@*/ declaratorNode declare;
  88   /*@only@*/ declaratorNodeList declarelist;
  89   /*@only@*/ typeExpr typeexpr;
  90   /*@only@*/ arrayQualNode array;
  91   /*@only@*/ quantifierNode quantifier;
  92   /*@only@*/ quantifierNodeList quantifiers;
  93   /*@only@*/ varNode var;
  94   /*@only@*/ varNodeList vars;
  95   /*@only@*/ storeRefNode storeref;
  96   /*@only@*/ storeRefNodeList storereflist;
  97   /*@only@*/ termNode term;
  98   /*@only@*/ termNodeList termlist;
  99   /*@only@*/ programNode program;
 100   /*@only@*/ stmtNode stmt;
 101   /*@only@*/ claimNode claim;
 102   /*@only@*/ typeNode type;
 103   /*@only@*/ iterNode iter;
 104   /*@only@*/ fcnNode fcn;
 105   /*@only@*/ fcnNodeList fcns;
 106   /*@only@*/ letDeclNode letdecl;
 107   /*@only@*/ letDeclNodeList letdecls;
 108   /*@only@*/ lclPredicateNode lclpredicate;
 109   /*@only@*/ modifyNode modify;
 110   /*@only@*/ paramNode param;
 111   /*@only@*/ paramNodeList paramlist;
 112   /*@only@*/ declaratorInvNodeList declaratorinvs;
 113   /*@only@*/ declaratorInvNode declaratorinv;
 114   /*@only@*/ abstBodyNode abstbody;
 115   /*@only@*/ abstractNode abstract;
 116   /*@only@*/ exposedNode exposed;
 117   /*    taggedUnionNode taggedunion; */
 118   /*@only@*/ globalList globals;
 119   /*@only@*/ constDeclarationNode constdeclaration;
 120   /*@only@*/ varDeclarationNode vardeclaration;
 121   /*@only@*/ varDeclarationNodeList vardeclarationlist;
 122   /*@only@*/ initDeclNodeList initdecls;
 123   /*@only@*/ initDeclNode initdecl;
 124   /*@only@*/ stDeclNodeList structdecls;
 125   /*@only@*/ stDeclNode structdecl;
 126   /*@only@*/ strOrUnionNode structorunion;
 127   /*@only@*/ enumSpecNode enumspec;
 128   /*@only@*/ lclTypeSpecNode lcltypespec;
 129   /*@only@*/ typeNameNode typname;
 130   /*@only@*/ opFormNode opform;
 131   /*@only@*/ sigNode signature;
 132   /*@only@*/ nameNode name;
 133   /*@only@*/ typeNameNodeList namelist;
 134   /*@only@*/ replaceNode replace;
 135   /*@only@*/ replaceNodeList replacelist;
 136   /*@only@*/ renamingNode renaming;
 137   /*@only@*/ traitRefNode traitref;
 138   /*@only@*/ traitRefNodeList traitreflist;
 139   /*@only@*/ importNode import;
 140   /*@only@*/ importNodeList importlist;
 141   /*@only@*/ interfaceNode iface;
 142   /*@only@*/ interfaceNodeList interfacelist;
 143   /*@only@*/ CTypesNode ctypes;
 144   /*@-redef@*/
 145 } /*@=redef@*/
 146
 147 /* Order of precedence is increasing going down the list */
 148
 149 %left     simpleOp
 150 %right    PREFIX_OP
 151 %left     POSTFIX_OP
 152 %left     LLT_MULOP
 153   /* as arithmetic binary operator, or as iteration construct in claims */
 154 %left     LLT_SEMI
 155 %left     LLT_VERTICALBAR
 156 %nonassoc ITERATION_OP /* two * cannot follow each other */
 157 %left     LLT_LPAR LLT_LBRACKET selectSym
 158   /* to allow mixing if-then-else with other kinds of terms */
 159 %left     LLT_IF_THEN_ELSE
 160 %left     logicalOp
 161
 162 /* Note: the grammar parses b = p /\ q as (b = p) /\ q, that is,
 163     = has higher precedence than logicalOp.
 164    Reminder: = > logicalOp >= if_then_else > == (present in LSL) */
 165
 166 /* Precedence of claim operators: ( > * > | >; (| and; left-assoc) */
 167
 168 /* These are not needed in the grammar,
 169    but needed in init files and lclscanline.c */
 170
 171 %token <ltok> eqSepSym          /* \eqsep */
 172 %token <ltok> equationSym     /* \equals or == */
 173 %token <ltok> commentSym        /* \comment */
 174 %token <ltok> LLT_WHITESPACE
 175 %token <ltok> LLT_EOL  /*@-varuse@*/  /* yacc declares yytranslate here */
 176 /* used to bypass parsing problems in C types */
 177 %token <ltok> LLT_TYPEDEF_NAME /*@=varuse@*/
 178
 179 /* LSL reserved extension symbols */
 180
 181 %token <ltok> quantifierSym     /* \forall */
 182 %token <ltok> logicalOp         /* \implies, \and, \not, \or */
 183 %token <ltok> selectSym         /* \select */
 184 %token <ltok> openSym           /* \( */
 185 %token <ltok> closeSym          /* \) */
 186 %token <ltok> sepSym            /* \, */
 187
 188 %token <ltok> simpleId          /* \: id-char +, Ordinary Identifier */
 189 %token <ltok> mapSym            /* \arrow, -> */
 190 %token <ltok> markerSym         /* \marker, __ */
 191 %token <ltok> preSym            /* \pre */
 192 %token <ltok> postSym           /* \post */
 193 %token <ltok> anySym            /* \any */
 194
 195 /* Generic LSL operators */
 196
 197 %token <ltok> simpleOp          /* opSym - reserved */
 198
 199 /* Reserved special symbols */
 200
 201 %token <ltok> LLT_COLON              /* : */
 202 %token <ltok> LLT_COMMA              /* , */
 203 %token <ltok> LLT_EQUALS             /* = */
 204 %token <ltok> LLT_LBRACE             /* { */
 205 %token <ltok> LLT_RBRACE             /* } */
 206 %token <ltok> LLT_LBRACKET           /* [ */
 207 %token <ltok> LLT_RBRACKET           /* ] */
 208 %token <ltok> LLT_LPAR               /* ( */
 209 %token <ltok> LLT_RPAR               /* ) */
 210 %token <ltok> LLT_QUOTE              /* ' */
 211 %token <ltok> LLT_SEMI               /*; */
 212 %token <ltok> LLT_VERTICALBAR        /* | */
 213
 214 /* C operator tokens and Combined C/LSL operator tokens */
 215
 216 %token <ltok> eqOp                /* \eq, \neq, ==, != */
 217 %token <ltok> LLT_MULOP               /* * */
 218
 219 /* LCL C literal tokens */
 220
 221 %token <ltok> LLT_CCHAR
 222 %token <ltok> LLT_CFLOAT
 223 %token <ltok> LLT_CINTEGER
 224 %token <ltok> LLT_LCSTRING
 225
 226 /* LCL reserved words */
 227
 228 %token <ltok> LLT_ALL
 229 %token <ltok> LLT_ANYTHING
 230 %token <ltok> LLT_BE
 231 %token <ltok> LLT_BODY
 232 %token <ltok> LLT_CLAIMS
 233 %token <ltok> LLT_CHECKS
 234 %token <ltok> LLT_CONSTANT
 235 %token <ltok> LLT_ELSE
 236 %token <ltok> LLT_ENSURES
 237 %token <ltok> LLT_FOR
 238 %token <ltok> LLT_FRESH
 239 %token <ltok> LLT_IF
 240 %token <ltok> LLT_IMMUTABLE
 241 %token <ltok> LLT_IMPORTS
 242 %token <ltok> LLT_CONSTRAINT /* was INVARIANT */
 243 %token <ltok> LLT_ISSUB
 244 %token <ltok> LLT_LET
 245 %token <ltok> LLT_MODIFIES
 246 %token <ltok> LLT_MUTABLE
 247 %token <ltok> LLT_NOTHING
 248 %token <ltok> LLT_INTERNAL
 249 %token <ltok> LLT_FILESYS
 250 %token <ltok> LLT_OBJ
 251 %token <ltok> LLT_OUT
 252 %token <ltok> LLT_SEF
 253 %token <ltok> LLT_ONLY LLT_PARTIAL LLT_OWNED LLT_DEPENDENT LLT_KEEP LLT_KEPT LLT_TEMP
 254 %token <ltok> LLT_SHARED LLT_UNIQUE LLT_UNUSED
 255 %token <ltok> LLT_EXITS LLT_MAYEXIT LLT_NEVEREXIT LLT_TRUEEXIT LLT_FALSEEXIT
 256 %token <ltok> LLT_UNDEF LLT_KILLED
 257 %token <ltok> LLT_CHECKMOD LLT_CHECKED LLT_UNCHECKED LLT_CHECKEDSTRICT
 258 %token <ltok> LLT_TRUENULL
 259 %token <ltok> LLT_FALSENULL
 260 %token <ltok> LLT_LNULL
 261 %token <ltok> LLT_LNOTNULL
 262 %token <ltok> LLT_RETURNED
 263 %token <ltok> LLT_OBSERVER
 264 %token <ltok> LLT_EXPOSED
 265 %token <ltok> LLT_REFCOUNTED
 266 %token <ltok> LLT_REFS
 267 %token <ltok> LLT_RELNULL
 268 %token <ltok> LLT_RELDEF
 269 %token <ltok> LLT_KILLREF
 270 %token <ltok> LLT_NULLTERMINATED
 271 %token <ltok> LLT_TEMPREF
 272 %token <ltok> LLT_NEWREF
 273 %token <ltok> LLT_PRIVATE
 274 %token <ltok> LLT_REQUIRES
 275 %token <ltok> LLT_RESULT
 276 %token <ltok> LLT_SIZEOF
 277 %token <ltok> LLT_SPEC
 278 %token <ltok> LLT_TAGGEDUNION  /* keep it for other parts of LCL checker */
 279 %token <ltok> LLT_THEN
 280 %token <ltok> LLT_TYPE
 281 %token <ltok> LLT_TYPEDEF
 282 %token <ltok> LLT_UNCHANGED
 283 %token <ltok> LLT_USES
 284
 285 /* LCL C keywords */
 286
 287 %token <ltok> LLT_CHAR
 288 %token <ltok> LLT_CONST
 289 %token <ltok> LLT_DOUBLE
 290 %token <ltok> LLT_ENUM
 291 %token <ltok> LLT_FLOAT
 292 %token <ltok> LLT_INT
 293 %token <ltok> LLT_ITER
 294 %token <ltok> LLT_YIELD
 295 %token <ltok> LLT_LONG
 296 %token <ltok> LLT_SHORT
 297 %token <ltok> LLT_SIGNED
 298 %token <ltok> LLT_UNKNOWN
 299 %token <ltok> LLT_STRUCT
 300 %token <ltok> LLT_TELIPSIS
 301 %token <ltok> LLT_UNION
 302 %token <ltok> LLT_UNSIGNED
 303 %token <ltok> LLT_VOID
 304 %token <ltok> LLT_VOLATILE
 305
 306 %token <ltok> LLT_PRINTFLIKE LLT_SCANFLIKE LLT_MESSAGELIKE
 307
 308 %type <interfacelist> interface externals optDeclarations declarations
 309 %type <iface> external declaration imports uses export private private2
 310 %type <type> type
 311 %type <fcn> fcn
 312 %type <fcns> fcns
 313 %type <claim> claim
 314 %type <iter> iter
 315 %type <vardeclaration> varDeclaration globalDecl privateInit
 316 %type <globals> globals
 317 %type <ltokenList> interfaceNameList traitIdList domain sortList
 318 %type <import> importName
 319 %type <importlist> importNameList
 320 %type <traitreflist> traitRefNodeList
 321 %type <traitref> traitRef
 322 %type <renaming> renaming
 323 %type <namelist> nameList
 324 %type <name> name
 325 %type <replacelist> replaceNodeList
 326 %type <replace> replace
 327 %type <opform> opForm
 328 %type <signature> signature
 329 %type <typname> typeName
 330 %type <count> middle placeList pointers
 331 %type <abstDecl> optAbstDeclarator
 332 %type <lcltypespec> lclTypeSpec lclType sortSpec
 333 %type <ltokenList> enumeratorList postfixOps
 334 %type <ctypes> CTypes typeSpecifier
 335 %type <structorunion> structOrUnionSpec
 336 %type <enumspec> enumSpec
 337 %type <declare> declarator
 338 %type <typeexpr> notype_decl after_type_decl abstDeclarator parameter_decl
 339 %type <declarelist> declaratorList
 340 %type <structdecls> structDecls
 341 %type <structdecl> structDecl
 342 %type <constdeclaration> constDeclaration
 343 %type <initdecls> initDecls
 344 %type <initdecl> initDecl
 345 %type <vardeclarationlist> privateInits
 346 %type <abstract> abstract
 347 %type <exposed> exposed
 348 %type <declaratorinvs> declaratorInvs
 349 %type <declaratorinv> declaratorInv
 350 %type <abstbody> abstBody optExposedBody
 351 %type <lclpredicate> optClaim optEnsure optRequire optChecks lclPredicate
 352 %type <lclpredicate> optTypeInv typeInv
 353 %type <modify> optModify
 354 %type <letdecls> optLetDecl beDeclList
 355 %type <letdecl> beDecl
 356 %type <term> term constLclExpr initializer value equalityTerm
 357 %type <term> simpleOpTerm prefixOpTerm secondary primary lclPrimary
 358 %type <term> bracketed sqBracketed matched term0 cLiteral
 359 %type <termlist> args infixOpPart valueList termList
 360 %type <program> optBody callExpr
 361 %type <stmt> stmt
 362 %type <storereflist> storeRefList
 363 %type <storeref> storeRef
 364 %type <var> quantified
 365 %type <vars> quantifiedList
 366 %type <quantifier> quantifier
 367 %type <quantifiers> quantifiers
 368 %type <array> arrayQual
 369 %type <paramlist> optParamList paramList realParamList iterParamList realIterParamList
 370 %type <param> param iterParam
 371 %type <ltok> open close anyOp separator simpleOp2 stateFcn
 372 %type <ltok> interfaceName
 373 %type <ltok> varId fcnId tagId claimId sortId traitId opId CType optTagId
 374 %type <ltok> simpleIdOrTypedefName
 375 %type <typequal> specialQualifier special
 376
 377 /*
 378 ** Conventions in calling static semantic routines:
 379 **   The inputs are in strict order (in AST) as well as in the position of
 380 **   the call to the static semantic routine.
 381 */
 382
 383 /*@=redef@*/
 384 /*@=readonlytrans@*/
 385
 386 %%
 387
 388 interface
 389  : externals { lhExternals ($1); } optDeclarations
 390    { interfaceNodeList_free ($1); interfaceNodeList_free ($3); }
 391
 392 externals
 393  : /* empty */        { $$ = interfaceNodeList_new (); }
 394  | externals external { $$ = interfaceNodeList_addh ($1, $2);}
 395
 396 external
 397  : imports
 398  | uses
 399
 400 optDeclarations
 401  : /* empty */              { $$ = interfaceNodeList_new (); }
 402  | export declarations      { $$ = consInterfaceNode ($1, $2);}
 403  | private declarations     { $$ = consInterfaceNode ($1, $2);}
 404
 405 declarations
 406  : /* empty */              { $$ = interfaceNodeList_new (); }
 407  | declarations declaration { $$ = interfaceNodeList_addh ($1, $2);}
 408
 409 declaration
 410  : export
 411  | private
 412  | uses
 413
 414 imports
 415  : LLT_IMPORTS importNameList LLT_SEMI
 416    { $$ = makeInterfaceNodeImports ($2);
 417      /* assume subspecs are already processed, symbol table info in external file */
 418    }
 419
 420 uses
 421  : LLT_USES traitRefNodeList LLT_SEMI
 422    { $$ = makeInterfaceNodeUses ($2); readlsignatures ($$);}
 423
 424 export
 425  : constDeclaration
 426    { declareConstant ($1); $$ = interfaceNode_makeConst ($1); }
 427  | varDeclaration
 428    { declareVar ($1); $$ = interfaceNode_makeVar ($1); }
 429  | type
 430    { declareType ($1); $$ = interfaceNode_makeType ($1); }
 431  | fcn
 432    { declareFcn ($1, typeId_invalid); $$ = interfaceNode_makeFcn ($1); }
 433  | claim
 434    { $$ = interfaceNode_makeClaim ($1); }
 435  | iter
 436    { declareIter ($1); $$ = interfaceNode_makeIter ($1); }
 437
 438 iter
 439  : LLT_ITER varId LLT_LPAR iterParamList LLT_RPAR LLT_SEMI
 440    { $$ = makeIterNode ($2, $4); }
 441
 442 iterParamList
 443  : /* empty */         { $$ = paramNodeList_new (); }
 444  | realIterParamList   { $$ = $1; }
 445
 446 realIterParamList
 447  : iterParam
 448    { $$ = paramNodeList_add (paramNodeList_new (),  $1); }
 449  | realIterParamList LLT_COMMA iterParam
 450    { $$ = paramNodeList_add ($1,$3); }
 451
 452 iterParam
 453  : LLT_YIELD param            { $$ = markYieldParamNode ($2); }
 454  | param                  { $$ = $1; }
 455
 456 private
 457  : LLT_SPEC { symtable_export (g_symtab, FALSE); } private2
 458    { $$ = $3; symtable_export (g_symtab, TRUE); }
 459
 460 private2
 461  : constDeclaration
 462    { declarePrivConstant ($1); $$ =  interfaceNode_makePrivConst ($1); }
 463  | varDeclaration
 464    { declarePrivVar ($1); $$ = interfaceNode_makePrivVar ($1); }
 465  | type
 466    { declarePrivType ($1); $$ = interfaceNode_makePrivType ($1); }
 467  | fcn
 468    { declarePrivFcn ($1, typeId_invalid); $$ = interfaceNode_makePrivFcn ($1); }
 469
 470 constDeclaration
 471  : LLT_CONSTANT lclTypeSpec initDecls LLT_SEMI
 472    { $$ = makeConstDeclarationNode ($2, $3); }
 473
 474 varDeclaration
 475  : lclTypeSpec initDecls LLT_SEMI
 476    { $$ = makeVarDeclarationNode ($1, $2, FALSE, FALSE); $$->qualifier = QLF_NONE; }
 477  | LLT_CONST lclTypeSpec initDecls LLT_SEMI
 478    { $$ = makeVarDeclarationNode ($2, $3, FALSE, FALSE); $$->qualifier = QLF_CONST; }
 479  | LLT_VOLATILE lclTypeSpec initDecls LLT_SEMI
 480    { $$ = makeVarDeclarationNode ($2, $3, FALSE, FALSE); $$->qualifier = QLF_VOLATILE; }
 481
 482 type
 483  : abstract                     { $$ = makeAbstractTypeNode ($1); }
 484  | exposed                      { $$ = makeExposedTypeNode ($1); }
 485
 486 special
 487  : LLT_PRINTFLIKE  { $$ = qual_createPrintfLike (); }
 488  | LLT_SCANFLIKE   { $$ = qual_createScanfLike (); }
 489  | LLT_MESSAGELIKE { $$ = qual_createMessageLike (); }
 490
 491 fcn
 492  : lclTypeSpec declarator globals { enteringFcnScope ($1, $2, $3); } LLT_LBRACE
 493    privateInits optLetDecl optChecks optRequire optModify optEnsure optClaim LLT_RBRACE
 494    { $$ = makeFcnNode (qual_createUnknown (),  $1, $2, $3, $6, $7,
 495                        $8, $9, $10, $11, $12);
 496      /* type, declarator, glovbls, privateinits,
 497         lets, checks, requires, modifies, ensures, claims */
 498      symtable_exitScope (g_symtab);
 499    }
 500  | special lclTypeSpec declarator globals { enteringFcnScope ($2, $3, $4); }
 501    LLT_LBRACE
 502    privateInits optLetDecl optChecks optRequire optModify optEnsure optClaim
 503    LLT_RBRACE
 504    { $$ = makeFcnNode ($1, $2, $3, $4, $7,
 505                        $8, $9, $10, $11, $12, $13);
 506      /* type, declarator, glovbls, privateinits,
 507         lets, checks, requires, modifies, ensures, claims */
 508      symtable_exitScope (g_symtab);
 509    }
 510
 511
 512 claim
 513  : LLT_CLAIMS claimId LLT_LPAR optParamList LLT_RPAR globals
 514    { enteringClaimScope ($4, $6); }
 515    LLT_LBRACE optLetDecl optRequire optBody optEnsure LLT_RBRACE
 516    {      $$ = makeClaimNode ($2, $4, $6, $9, $10, $11, $12);
 517      symtable_exitScope (g_symtab); }
 518  | LLT_CLAIMS fcnId claimId LLT_SEMI
 519    { $$ = (claimNode) 0; }
 520
 521 abstract
 522  : LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_TYPE LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
 523    { $$ = makeAbstractNode ($1, $4, TRUE, FALSE, $6); }
 524  | LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_REFCOUNTED LLT_TYPE
 525    LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
 526    { $$ = makeAbstractNode ($1, $5, TRUE, TRUE, $7); }
 527  | LLT_REFCOUNTED LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_TYPE
 528    LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
 529    { $$ = makeAbstractNode ($2, $5, TRUE, TRUE, $7); }
 530  | LLT_IMMUTABLE {g_inTypeDef = TRUE; } LLT_TYPE LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
 531    { $$ = makeAbstractNode ($1, $4, FALSE, FALSE, $6); }
 532
 533 exposed
 534  : LLT_TYPEDEF lclTypeSpec { g_inTypeDef = TRUE; setExposedType ($2); } declaratorInvs
 535    { g_inTypeDef = FALSE; } LLT_SEMI
 536    { $$ = makeExposedNode ($1, $2, $4); /* to support mutually recursive types */ }
 537  | structOrUnionSpec LLT_SEMI
 538    { $$ = makeExposedNode ($2, makeLclTypeSpecNodeSU ($1), declaratorInvNodeList_new ()); }
 539  | enumSpec LLT_SEMI
 540    { $$ = makeExposedNode ($2, makeLclTypeSpecNodeEnum ($1), declaratorInvNodeList_new ()); }
 541
 542 /* evs - 26 Feb 1995 (changed to be consistent with C grammar)
 543  | STRUCT tagId LLT_SEMI
 544    { (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy ($2));
 545      lhForwardStruct ($2); $$ = (exposedNode)0;
 546    }
 547  | UNION tagId LLT_SEMI
 548    { (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy ($2));
 549      lhForwardUnion ($2);
 550      $$ = (exposedNode)0;
 551    }
 552 */
 553
 554 importNameList
 555  : importName
 556    { $$ = importNodeList_add (importNodeList_new (),  $1); }
 557  | importNameList LLT_COMMA importName
 558    { $$ = importNodeList_add ($1, $3); }
 559
 560 importName
 561  : interfaceName      { $$ = importNode_makePlain ($1); }
 562  | simpleOp interfaceName simpleOp
 563    { checkBrackets ($1, $3); $$ = importNode_makeBracketed ($2); }
 564  | LLT_LCSTRING           { $$ = importNode_makeQuoted ($1); }
 565
 566 interfaceNameList
 567  : interfaceName                         { $$ = ltokenList_singleton ($1); }
 568  | interfaceNameList LLT_COMMA interfaceName { $$ = ltokenList_push ($1, $3); }
 569
 570 interfaceName
 571  : simpleIdOrTypedefName
 572    /* to allow module names to be the same as LCL type names */
 573
 574 traitRefNodeList
 575  : traitRef
 576    { $$ = traitRefNodeList_add (traitRefNodeList_new (),  $1); }
 577  | traitRefNodeList LLT_COMMA traitRef
 578    { $$ = traitRefNodeList_add ($1, $3); }
 579
 580 traitRef
 581  : traitId
 582    { $$ = makeTraitRefNode (ltokenList_singleton ($1), (renamingNode)0); }
 583  | traitId LLT_LPAR renaming LLT_RPAR
 584    { $$ = makeTraitRefNode (ltokenList_singleton ($1), $3); }
 585  | LLT_LPAR traitIdList LLT_RPAR
 586    { $$ = makeTraitRefNode ($2, (renamingNode)0); }
 587  | LLT_LPAR traitIdList LLT_RPAR LLT_LPAR renaming LLT_RPAR
 588    { $$ = makeTraitRefNode ($2, $5); }
 589
 590 traitIdList
 591  : traitId                     { $$ = ltokenList_singleton ($1); }
 592  | traitIdList LLT_COMMA traitId   { $$ = ltokenList_push ($1, $3); }
 593
 594 renaming
 595  : replaceNodeList
 596    { $$ = makeRenamingNode (typeNameNodeList_new (),  $1); }
 597  | nameList
 598    { $$ = makeRenamingNode ($1, replaceNodeList_new ()); }
 599  | nameList LLT_COMMA replaceNodeList { $$ = makeRenamingNode ($1, $3); }
 600
 601 nameList
 602  : typeName
 603    { $$ = typeNameNodeList_add (typeNameNodeList_new (),  $1); }
 604  | nameList LLT_COMMA typeName       { $$ = typeNameNodeList_add ($1, $3); }
 605
 606 replaceNodeList
 607  : replace
 608    { $$ = replaceNodeList_add (replaceNodeList_new (),  $1); }
 609  | replaceNodeList LLT_COMMA replace { $$ = replaceNodeList_add ($1, $3); }
 610
 611 replace
 612  : typeName LLT_FOR CType            { $$ = makeReplaceNode ($2, $1, TRUE, $3, NULL, NULL); }
 613  | typeName LLT_FOR name             { $$ = makeReplaceNameNode ($2, $1, $3); }
 614  | typeName LLT_FOR name signature   { $$ = makeReplaceNode ($2, $1, FALSE, ltoken_undefined,
 615                                                          $3, $4); }
 616
 617 name
 618  : opId                          { $$ = makeNameNodeId ($1); }
 619  | opForm                        { $$ = makeNameNodeForm ($1); }
 620
 621 initializer : constLclExpr
 622
 623 constLclExpr : term
 624
 625 initDecls
 626  : initDecl
 627    { $$ = initDeclNodeList_add (initDeclNodeList_new (),  $1); }
 628  | initDecls LLT_COMMA initDecl
 629    { $$ = initDeclNodeList_add ($1, $3); }
 630
 631 initDecl
 632  : declarator                    { $$ = makeInitDeclNode ($1, (termNode)0); }
 633  | declarator LLT_EQUALS initializer { $$ = makeInitDeclNode ($1, $3); }
 634
 635 globals
 636  : /* empty */ /* has the same structure */
 637    { $$ = varDeclarationNodeList_new (); }
 638  | globals globalDecl
 639    { varDeclarationNodeList_addh ($1, $2); $$ = $1; }
 640
 641 globalDecl
 642  : lclTypeSpec initDecls LLT_SEMI    { $$ = makeVarDeclarationNode ($1, $2, TRUE, FALSE); }
 643  | LLT_INTERNAL LLT_SEMI                 { $$ = makeInternalStateNode (); }
 644  | LLT_FILESYS LLT_SEMI                  { $$ = makeFileSystemNode (); }
 645
 646 privateInits
 647  : /* empty */                  { $$ = varDeclarationNodeList_new (); }
 648  | privateInits privateInit     { varDeclarationNodeList_addh ($1, $2); $$ = $1; }
 649
 650 privateInit
 651  : LLT_PRIVATE lclTypeSpec initDecls LLT_SEMI
 652    { $$ = makeVarDeclarationNode ($2, $3, FALSE, TRUE); }
 653
 654 optLetDecl
 655  : /* empty */                 { $$ = letDeclNodeList_new (); }
 656  | LLT_LET beDeclList LLT_SEMI         { $$ = $2; }
 657
 658 beDeclList
 659  : beDecl                      { $$ = letDeclNodeList_add (letDeclNodeList_new (),  $1); }
 660  | beDeclList LLT_COMMA beDecl     { $$ = letDeclNodeList_add ($1, $3); }
 661
 662 beDecl
 663  : varId LLT_COLON sortSpec LLT_BE term { $$ = makeLetDeclNode ($1, $3, $5); }
 664  | varId                LLT_BE term { $$ = makeLetDeclNode ($1, (lclTypeSpecNode)0, $3); }
 665
 666 sortSpec : lclTypeSpec
 667
 668 optChecks
 669  : /* empty */                  { $$ = (lclPredicateNode)0; }
 670  | LLT_CHECKS lclPredicate LLT_SEMI     { checkLclPredicate ($1, $2); $$ = makeChecksNode ($1, $2); }
 671
 672 optRequire
 673  : /* empty */                  { $$ = (lclPredicateNode)0; }
 674  | LLT_REQUIRES lclPredicate LLT_SEMI   { checkLclPredicate ($1, $2); $$ = makeRequiresNode ($1, $2);}
 675
 676 optModify
 677  : /* empty */                  { $$ = (modifyNode)0; }
 678  | LLT_MODIFIES LLT_NOTHING LLT_SEMI        { $$ = makeModifyNodeSpecial ($1, TRUE); }
 679  | LLT_MODIFIES LLT_ANYTHING LLT_SEMI       { $$ = makeModifyNodeSpecial ($1, FALSE); }
 680  | LLT_MODIFIES storeRefList LLT_SEMI   { $$ = makeModifyNodeRef ($1, $2); }
 681
 682 storeRefList
 683  : storeRef                     { $$ = storeRefNodeList_add (storeRefNodeList_new (),  $1); }
 684  | storeRefList LLT_COMMA storeRef  { $$ = storeRefNodeList_add ($1, $3); }
 685
 686 storeRef
 687  : term                         { $$ = makeStoreRefNodeTerm ($1); }
 688  | lclType                      { $$ = makeStoreRefNodeType ($1, FALSE); }
 689  | LLT_OBJ lclType                  { $$ = makeStoreRefNodeType ($2, TRUE); }
 690  | LLT_INTERNAL                     { $$ = makeStoreRefNodeInternal (); }
 691  | LLT_FILESYS                      { $$ = makeStoreRefNodeSystem (); }
 692
 693 optEnsure
 694  : /* empty */                  { $$ = (lclPredicateNode)0; }
 695  | LLT_ENSURES lclPredicate LLT_SEMI    { checkLclPredicate ($1, $2); $$ = makeEnsuresNode ($1, $2);}
 696
 697 optClaim
 698  : /* empty */                  { $$ = (lclPredicateNode)0; }
 699  | LLT_CLAIMS lclPredicate LLT_SEMI     { checkLclPredicate ($1, $2); $$ = makeIntraClaimNode ($1, $2);}
 700
 701 optParamList
 702  : /* empty */                  { $$ = paramNodeList_new (); }
 703  | realParamList                { $$ = $1; }
 704
 705 realParamList
 706  : paramList
 707  | LLT_TELIPSIS                  { $$ = paramNodeList_add (paramNodeList_new (),  paramNode_elipsis ()); }
 708  | paramList LLT_COMMA LLT_TELIPSIS  { $$ = paramNodeList_add ($1, paramNode_elipsis ()); }
 709
 710 paramList
 711  : param                     { $$ = paramNodeList_single ($1); }
 712  | paramList LLT_COMMA param     { $$ = paramNodeList_add ($1, $3); }
 713
 714 optBody
 715  : /* empty */                      { $$ = (programNode)0; }
 716  | LLT_BODY LLT_LBRACE callExpr LLT_RBRACE      { $$ = $3; }
 717  | LLT_BODY LLT_LBRACE callExpr LLT_SEMI LLT_RBRACE { $$ = $3; }
 718
 719 callExpr
 720  : stmt                             { $$ = makeProgramNode ($1); }
 721  | LLT_LPAR callExpr LLT_RPAR
 722    /* may need to make a copy of $2 */
 723    { $$ = $2; $$->wrapped = $$->wrapped + 1; }
 724  | callExpr LLT_MULOP        %prec ITERATION_OP
 725    { programNodeList x = programNodeList_new ();
 726      programNodeList_addh (x, $1);
 727      $$ = makeProgramNodeAction (x, ACT_ITER);
 728    }
 729  | callExpr LLT_VERTICALBAR callExpr
 730    { programNodeList x = programNodeList_new ();
 731      programNodeList_addh (x, $1);
 732      programNodeList_addh (x, $3);
 733      $$ = makeProgramNodeAction (x, ACT_ALTERNATE);
 734    }
 735  | callExpr LLT_SEMI callExpr
 736    { programNodeList x = programNodeList_new ();
 737      programNodeList_addh (x, $1);
 738      programNodeList_addh (x, $3);
 739      $$ = makeProgramNodeAction (x, ACT_SEQUENCE);
 740    }
 741
 742 stmt
 743  : fcnId LLT_LPAR valueList LLT_RPAR
 744    { $$ = makeStmtNode (ltoken_undefined, $1, $3); }
 745  | fcnId LLT_LPAR LLT_RPAR
 746    { $$ = makeStmtNode (ltoken_undefined, $1, termNodeList_new ()); }
 747  | varId LLT_EQUALS fcnId LLT_LPAR LLT_RPAR
 748    { $$ = makeStmtNode ($1, $3, termNodeList_new ()); }
 749  | varId LLT_EQUALS fcnId LLT_LPAR valueList LLT_RPAR
 750    { $$ = makeStmtNode ($1, $3, $5); }
 751
 752 valueList
 753  : value                 { $$ = termNodeList_push (termNodeList_new (),  $1); }
 754  | valueList LLT_COMMA value { $$ = termNodeList_push ($1, $3); }
 755
 756 value
 757  : cLiteral
 758  | varId                            { $$ = makeSimpleTermNode ($1); }
 759  | simpleOp value %prec PREFIX_OP   { $$ = makePrefixTermNode ($1, $2); }
 760  | value simpleOp  %prec POSTFIX_OP { $$ = makePostfixTermNode2 ($1, $2); }
 761  | value simpleOp value /* infix */ { $$ = makeInfixTermNode ($1, $2, $3); }
 762  | LLT_LPAR value LLT_RPAR                  { $$ = $2; $$->wrapped = $$->wrapped + 1; }
 763  | fcnId LLT_LPAR LLT_RPAR
 764    { $$ = makeOpCallTermNode ($1, $2, termNodeList_new (),  $3); }
 765  | fcnId LLT_LPAR valueList LLT_RPAR
 766    { $$ = makeOpCallTermNode ($1, $2, $3, $4); }
 767
 768 abstBody
 769  : LLT_SEMI                                  { $$ = (abstBodyNode)0; }
 770  | LLT_LBRACE fcns LLT_RBRACE                    { $$ = makeAbstBodyNode ($1, $2); }
 771  | LLT_LBRACE interfaceNameList LLT_RBRACE LLT_SEMI  { $$ = makeAbstBodyNode2 ($1, $2); }
 772  | LLT_LBRACE LLT_RBRACE LLT_SEMI                    { $$ = (abstBodyNode)0; }
 773
 774 fcns
 775  : /* empty */                           { $$ = fcnNodeList_new (); }
 776  | fcns fcn                              { $$ = fcnNodeList_add ($1, $2); }
 777
 778 optTypeInv
 779  : /* empty */                           { $$ = (lclPredicateNode)0; }
 780  | typeInv
 781
 782 typeInv
 783  : LLT_CONSTRAINT { g_inTypeDef = FALSE; } quantifier LLT_LPAR lclPredicate LLT_RPAR
 784    { $5->tok = $1; $5->kind = LPD_CONSTRAINT;
 785      checkLclPredicate ($1, $5);
 786      $$ = $5;
 787      symtable_exitScope (g_symtab);
 788      g_inTypeDef = TRUE;
 789    }
 790
 791 declaratorInvs
 792  : declaratorInv        { $$ = declaratorInvNodeList_add (declaratorInvNodeList_new (),  $1); }
 793  | declaratorInvs LLT_COMMA declaratorInv
 794    { $$ = declaratorInvNodeList_add ($1, $3); }
 795
 796 declaratorInv
 797  : declarator { declareForwardType ($1); } optExposedBody
 798    { $$ = makeDeclaratorInvNode ($1, $3); }
 799
 800 optExposedBody
 801  : /* empty */                  { $$ = (abstBodyNode)0; }
 802  | LLT_LBRACE optTypeInv LLT_RBRACE     { $$ = makeExposedBodyNode ($1, $2); }
 803
 804 CType
 805  : LLT_VOID           { $$ = $1; ltoken_setIntField ($$, fixBits (TS_VOID, 0)); }
 806  | LLT_CHAR           { $$ = $1; ltoken_setIntField ($$, fixBits (TS_CHAR, 0)); }
 807  | LLT_DOUBLE         { $$ = $1; ltoken_setIntField ($$, fixBits (TS_DOUBLE, 0)); }
 808  | LLT_FLOAT          { $$ = $1; ltoken_setIntField ($$, fixBits (TS_FLOAT, 0)); }
 809  | LLT_INT            { $$ = $1; ltoken_setIntField ($$, fixBits (TS_INT, 0)); }
 810  | LLT_LONG           { $$ = $1; ltoken_setIntField ($$, fixBits (TS_LONG, 0)); }
 811  | LLT_SHORT          { $$ = $1; ltoken_setIntField ($$, fixBits (TS_SHORT, 0)); }
 812  | LLT_SIGNED         { $$ = $1; ltoken_setIntField ($$, fixBits (TS_SIGNED, 0)); }
 813  | LLT_UNSIGNED       { $$ = $1; ltoken_setIntField ($$, fixBits (TS_UNSIGNED, 0)); }
 814  | LLT_UNKNOWN        { $$ = $1; ltoken_setIntField ($$, fixBits (TS_UNKNOWN, 0)); }
 815
 816 /*
 817 ** CTypes allow "unsigned short int" but we drop all C type qualifiers
 818 ** and storage class except TYPEDEF
 819 */
 820
 821 CTypes
 822  : CType                       { $$ = makeCTypesNode ((CTypesNode)0, $1); }
 823  | CTypes CType                { $$ = makeCTypesNode ($1, $2); }
 824
 825 /* Add abstract type names and typedef names */
 826
 827 typeSpecifier
 828  : LLT_TYPEDEF_NAME
 829    { $$ = makeTypeSpecifier ($1); }
 830  | CTypes
 831    { $$ = $1; $$->sort = sort_lookupName (lclctype_toSort ($1->intfield)); }
 832
 833 /* Add struct and enum types */
 834
 835 specialQualifier
 836  : LLT_OUT       { $$ = qual_createOut (); }
 837  | LLT_UNUSED { $$ = qual_createUnused (); }
 838  | LLT_SEF       { $$ = qual_createSef (); }
 839  | LLT_ONLY      { $$ = qual_createOnly (); }
 840  | LLT_OWNED     { $$ = qual_createOwned (); }
 841  | LLT_DEPENDENT { $$ = qual_createDependent (); }
 842  | LLT_KEEP      { $$ = qual_createKeep (); }
 843  | LLT_KEPT      { $$ = qual_createKept (); }
 844  | LLT_OBSERVER  { $$ = qual_createObserver (); }
 845  | LLT_EXITS     { $$ = qual_createExits (); }
 846  | LLT_MAYEXIT   { $$ = qual_createMayExit (); }
 847  | LLT_TRUEEXIT  { $$ = qual_createTrueExit (); }
 848  | LLT_FALSEEXIT { $$ = qual_createFalseExit (); }
 849  | LLT_NEVEREXIT { $$ = qual_createNeverExit (); }
 850  | LLT_TEMP      { $$ = qual_createOnly (); }
 851  | LLT_SHARED    { $$ = qual_createShared (); }
 852  | LLT_UNIQUE    { $$ = qual_createUnique (); }
 853  | LLT_CHECKED   { $$ = qual_createChecked (); }
 854  | LLT_UNCHECKED { $$ = qual_createUnchecked (); }
 855  | LLT_CHECKEDSTRICT { $$ = qual_createCheckedStrict (); }
 856  | LLT_TRUENULL  { $$ = qual_createTrueNull (); }
 857  | LLT_FALSENULL { $$ = qual_createFalseNull (); }
 858  | LLT_RELNULL   { $$ = qual_createRelNull (); }
 859  | LLT_RELDEF    { $$ = qual_createRelDef (); }
 860  | LLT_REFCOUNTED{ $$ = qual_createRefCounted (); }
 861  | LLT_REFS      { $$ = qual_createRefs (); }
 862  | LLT_NEWREF    { $$ = qual_createNewRef (); }
 863  | LLT_KILLREF   { $$ = qual_createKillRef (); }
 864  | LLT_LNULL     { $$ = qual_createNull (); }
 865  | LLT_LNOTNULL  { $$ = qual_createNotNull (); }
 866  | LLT_RETURNED  { $$ = qual_createReturned (); }
 867  | LLT_EXPOSED   { $$ = qual_createExposed (); }
 868  | LLT_PARTIAL   { $$ = qual_createPartial (); }
 869  | LLT_NULLTERMINATED { $$ = qual_createNullTerminated () ; }
 870  | LLT_UNDEF { $$ = qual_createUndef (); }
 871  | LLT_KILLED { $$ = qual_createKilled (); }
 872
 873 lclTypeSpec
 874  : typeSpecifier
 875    { $$ = makeLclTypeSpecNodeType ($1); } /* does not process CONST at all */
 876  | structOrUnionSpec
 877    { $$ = makeLclTypeSpecNodeSU ($1); }
 878  | enumSpec
 879    { $$ = makeLclTypeSpecNodeEnum ($1); }
 880  | specialQualifier lclTypeSpec
 881    { $$ = lclTypeSpecNode_addQual ($2, $1); }
 882  | LLT_VERTICALBAR lclType LLT_COLON lclType LLT_VERTICALBAR
 883    { $$ = makeLclTypeSpecNodeConj ($2, $4); }
 884
 885 /*
 886 ** Add pointers to the right, only used in StoreRef, maybe should throw
 887 ** out and replace its use in StoreRef by CTypeName
 888 */
 889
 890 lclType
 891  : lclTypeSpec
 892  | lclTypeSpec pointers
 893    { llassert (lclTypeSpecNode_isDefined ($1));
 894      $1->pointers = $2; $$ = $1; }
 895
 896 pointers
 897  : LLT_MULOP          { $$ = 1; }
 898  | pointers LLT_MULOP { $$ = $1 + 1; }
 899
 900 structOrUnionSpec
 901  : LLT_STRUCT optTagId
 902    { (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy ($2)); }
 903    LLT_LBRACE structDecls LLT_RBRACE
 904    { $$ = makestrOrUnionNode ($1, SU_STRUCT, $2, $5); }
 905  | LLT_UNION optTagId
 906    { (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy ($2)); }
 907    LLT_LBRACE structDecls LLT_RBRACE
 908    { $$ = makestrOrUnionNode ($1, SU_UNION, $2, $5); }
 909  | LLT_STRUCT tagId
 910    { $$ = makeForwardstrOrUnionNode ($1, SU_STRUCT, $2); }
 911  | LLT_UNION tagId
 912    { $$ = makeForwardstrOrUnionNode ($1, SU_UNION, $2); }
 913
 914 optTagId
 915  : /* empty */ { $$ = ltoken_undefined; }
 916  | tagId
 917
 918 structDecls
 919  : structDecl               { $$ = stDeclNodeList_add (stDeclNodeList_new (),  $1); }
 920  | structDecls structDecl   { $$ = stDeclNodeList_add ($1, $2); }
 921
 922 /* We don't allow specification of field size */
 923
 924 structDecl
 925  : lclTypeSpec declaratorList LLT_SEMI { $$ = makestDeclNode ($1, $2); }
 926
 927 declaratorList
 928  : declarator
 929    { $$ = declaratorNodeList_add (declaratorNodeList_new (),  $1); }
 930  | declaratorList LLT_COMMA declarator
 931    { $$ = declaratorNodeList_add ($1, $3); }
 932
 933 optCOMMA
 934  : /* empty */ { ; }
 935  | LLT_COMMA       { ; }
 936
 937 enumSpec
 938  : LLT_ENUM optTagId LLT_LBRACE enumeratorList optCOMMA LLT_RBRACE
 939    { $$ = makeEnumSpecNode ($1, $2, $4); }
 940  | LLT_ENUM tagId
 941    { $$ = makeEnumSpecNode2 ($1, $2); }
 942
 943 enumeratorList
 944  : simpleId                             { $$ = ltokenList_singleton ($1); }
 945  | enumeratorList LLT_COMMA simpleId        { $$ = ltokenList_push ($1, $3); }
 946
 947 /* This part of declarator rules is adapted from GCC (2.2.1)'s C grammar */
 948
 949 /* An after_type_decl is a declarator that is allowed only after an explicit
 950    typeSpecifier, an id can be typedef'd here.
 951    A notype_decl is a declarator that may not have seen a typeSpecifier
 952    preceding it; it cannot typedef'd an id.  */
 953
 954 declarator
 955  : after_type_decl                      { $$ = makeDeclaratorNode ($1); }
 956  | notype_decl                          { $$ = makeDeclaratorNode ($1); }
 957
 958 notype_decl
 959  : varId                                { $$ = makeTypeExpr ($1); }
 960  | LLT_LPAR notype_decl LLT_RPAR        { $$ = $2; $$->wrapped = $$->wrapped + 1; }
 961  | LLT_MULOP notype_decl                { $$ = makePointerNode ($1, $2); }
 962  | notype_decl arrayQual                { $$ = makeArrayNode ($1, $2); }
 963  | notype_decl LLT_LPAR LLT_RPAR                { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
 964  | notype_decl LLT_LPAR realParamList LLT_RPAR  { $$ = makeFunctionNode ($1, $3); }
 965
 966 after_type_decl
 967  : LLT_TYPEDEF_NAME                         { $$ = makeTypeExpr ($1); }
 968  | LLT_LPAR after_type_decl LLT_RPAR        { $$ = $2; $$->wrapped = $$->wrapped + 1; }
 969  | LLT_MULOP after_type_decl                { $$ = makePointerNode ($1, $2); }
 970  | after_type_decl arrayQual                { $$ = makeArrayNode ($1, $2); }
 971  | after_type_decl LLT_LPAR LLT_RPAR                { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
 972  | after_type_decl LLT_LPAR realParamList LLT_RPAR  { $$ = makeFunctionNode ($1, $3); }
 973
 974 /* A parameter_decl is a decl that can appear in a parameter list.
 975    We disallow the old C way of giving only the id names without types.
 976    A parameter_decl is like an after_type_decl except that it does not
 977    allow a TYPEDEF_NAME to appear in parens.  It will conflict with a
 978    a function with that typedef as an argument */
 979
 980 parameter_decl
 981  : LLT_TYPEDEF_NAME                             { $$ = makeTypeExpr ($1); }
 982  | LLT_MULOP parameter_decl /* %prec UNARY */   { $$ = makePointerNode ($1, $2); }
 983  | parameter_decl arrayQual                 { $$ = makeArrayNode ($1, $2); }
 984  | parameter_decl LLT_LPAR LLT_RPAR                 { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
 985  | parameter_decl LLT_LPAR realParamList LLT_RPAR   { $$ = makeFunctionNode ($1, $3); }
 986
 987 /* param : the last production allows C types to be generated without the
 988    parameter name */
 989
 990 param
 991  : lclTypeSpec parameter_decl               { $$ = makeParamNode ($1, $2); }
 992  | lclTypeSpec notype_decl                  { $$ = makeParamNode ($1, $2); }
 993  | lclTypeSpec optAbstDeclarator            { $$ = makeParamNode ($1, $2); }
 994 /*
 995 ** | OUT lclTypeSpec parameter_decl           { $$ = makeOutParamNode ($1, $2, $3); }
 996 ** | OUT lclTypeSpec notype_decl              { $$ = makeOutParamNode ($1, $2, $3); }
 997 ** | OUT lclTypeSpec optAbstDeclarator        { $$ = makeOutParamNode ($1, $2, $3); }
 998 */
 999
1000 /* typeName is only used in trait parameter renaming */
1001
1002 typeName
1003  : lclTypeSpec optAbstDeclarator           { $$ = makeTypeNameNode (FALSE, $1, $2); }
1004  | LLT_OBJ lclTypeSpec optAbstDeclarator       { $$ = makeTypeNameNode (TRUE, $2, $3); }
1005  | opForm                                  { $$ = makeTypeNameNodeOp ($1); }
1006
1007 /* Abstract declarator is like a declarator, but with no identifier */
1008
1009 optAbstDeclarator
1010  : /* empty */                            { $$ = (abstDeclaratorNode)0; }
1011  | abstDeclarator                         { $$ = (abstDeclaratorNode)$1; }
1012
1013 abstDeclarator
1014  : LLT_LPAR abstDeclarator LLT_RPAR               { $$ = $2; $$->wrapped = $$->wrapped + 1; }
1015  | LLT_MULOP abstDeclarator                   { $$ = makePointerNode ($1, $2); }
1016  | LLT_MULOP                                  { $$ = makePointerNode ($1, (typeExpr)0); }
1017  | arrayQual                              { $$ = makeArrayNode ((typeExpr)0, $1); }
1018  | abstDeclarator arrayQual               { $$ = makeArrayNode ($1, $2); }
1019  | abstDeclarator LLT_LPAR LLT_RPAR               { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
1020  | LLT_LPAR realParamList LLT_RPAR                { $$ = makeFunctionNode ((typeExpr)0, $2); }
1021  | abstDeclarator LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
1022
1023 arrayQual
1024  : LLT_LBRACKET LLT_RBRACKET                     { $$ = makeArrayQualNode ($1, (termNode)0); }
1025  | LLT_LBRACKET constLclExpr LLT_RBRACKET        { $$ = makeArrayQualNode ($1, $2); }
1026
1027 opForm
1028  : LLT_IF markerSym LLT_THEN markerSym LLT_ELSE markerSym
1029    { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); }
1030  | anyOp
1031    { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); }
1032  | markerSym anyOp
1033    { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); }
1034  | anyOp markerSym
1035    { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); }
1036  | markerSym anyOp markerSym
1037    { $$ = makeOpFormNode ($1, OPF_MANYOPM,
1038                           opFormUnion_createAnyOp ($2), ltoken_undefined); }
1039  | open middle close
1040    { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); }
1041  | markerSym open middle close
1042    { $$ = makeOpFormNode ($1, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); }
1043  | open middle close markerSym
1044    { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); }
1045  | markerSym open middle close markerSym
1046    { $$ = makeOpFormNode ($2, OPF_MMIDDLEM, opFormUnion_createMiddle ($3), $4); }
1047  | LLT_LBRACKET middle LLT_RBRACKET
1048    { $$ = makeOpFormNode ($1, OPF_BMIDDLE, opFormUnion_createMiddle ($2), $3); }
1049  | LLT_LBRACKET middle LLT_RBRACKET markerSym
1050    { $$ = makeOpFormNode ($1, OPF_BMIDDLEM, opFormUnion_createMiddle ($2), $3); }
1051
1052    /* added the next 6 productions (wrt old checker) to complete LSL grammar
1053    ** LSL treats '[' and '{' as openSym but LCL treats them as LLT_LBRACKET and
1054    ** LLT_LBRACE, and hence the need for these separate productions
1055    */
1056
1057  | markerSym LLT_LBRACKET middle LLT_RBRACKET
1058    { $$ = makeOpFormNode ($2, OPF_BMMIDDLE, opFormUnion_createMiddle ($3), $4); }
1059  | markerSym LLT_LBRACKET middle LLT_RBRACKET markerSym
1060    { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM, opFormUnion_createMiddle ($3), $4); }
1061  | selectSym simpleIdOrTypedefName
1062    { $$ = makeOpFormNode ($1, OPF_SELECT,
1063                           opFormUnion_createAnyOp ($2), ltoken_undefined); }
1064  | mapSym simpleIdOrTypedefName
1065    { $$ = makeOpFormNode ($1, OPF_MAP,
1066                           opFormUnion_createAnyOp ($2), ltoken_undefined); }
1067  | markerSym selectSym simpleIdOrTypedefName
1068    { $$ = makeOpFormNode ($1, OPF_MSELECT,
1069                           opFormUnion_createAnyOp ($3), ltoken_undefined); }
1070  | markerSym mapSym simpleIdOrTypedefName
1071    { $$ = makeOpFormNode ($1, OPF_MMAP,
1072                           opFormUnion_createAnyOp ($3), ltoken_undefined); }
1073
1074 open
1075  : openSym
1076  | LLT_LBRACE
1077
1078 close
1079  : closeSym
1080  | LLT_RBRACE
1081
1082 anyOp
1083  : simpleOp2
1084  | logicalOp
1085  | eqOp
1086
1087 middle
1088  : /* empty */               { $$ = 0; }
1089  | placeList
1090
1091 placeList
1092  : markerSym                      { $$ = 1; }
1093  | placeList separator markerSym  { $$ = $1 + 1; }
1094
1095 separator
1096  : LLT_COMMA
1097  | sepSym
1098
1099 signature
1100  : LLT_COLON domain mapSym sortId   { $$ = makesigNode ($1, $2, $4); }
1101
1102 domain
1103  : /* empty */               { $$ = ltokenList_new (); }
1104  | sortList
1105
1106 sortList
1107  : sortId                    { $$ = ltokenList_singleton ($1); }
1108  | sortList LLT_COMMA sortId     { $$ = ltokenList_push ($1, $3); }
1109
1110 lclPredicate
1111  : term                      { $$ = makeLclPredicateNode (ltoken_undefined, $1, LPD_PLAIN);}
1112
1113 term
1114  : term0                     { $$ = checkSort ($1); }
1115
1116 /* When "if <term> then <term> else <term> . <logicalOp> <term>"
1117    shift instead of reduce */
1118
1119 term0
1120  : LLT_IF term0 LLT_THEN term0 LLT_ELSE term0 %prec LLT_IF_THEN_ELSE
1121    { $$ = makeIfTermNode ($1,$2,$3,$4,$5,$6); }
1122  | equalityTerm
1123  | term0 logicalOp term0          { $$ = makeInfixTermNode ($1, $2, $3); }
1124
1125 equalityTerm
1126  : simpleOpTerm   /* was   | quantifiers LLT_LPAR term LLT_RPAR */
1127  | quantifiers LLT_LPAR lclPredicate LLT_RPAR
1128    /* temp fix, should change interface in future, add lclPredicateKind too */
1129    { checkLclPredicate ($2, $3); $$ = makeQuantifiedTermNode ($1, $2, $3->predicate, $4);
1130      symtable_exitScope (g_symtab);
1131    }
1132  | simpleOpTerm eqOp simpleOpTerm
1133    { $$ = makeInfixTermNode ($1, $2, $3);}
1134  | simpleOpTerm LLT_EQUALS simpleOpTerm
1135    { $$ = makeInfixTermNode ($1, $2, $3);}
1136
1137 simpleOpTerm
1138  : prefixOpTerm
1139  | secondary postfixOps          { $$ = makePostfixTermNode ($1, $2); }
1140  | secondary infixOpPart         { $$ = CollapseInfixTermNode ($1, $2); }
1141
1142 simpleOp2
1143  : simpleOp
1144  | LLT_MULOP
1145
1146 prefixOpTerm
1147  : secondary
1148  | simpleOp2 prefixOpTerm          { $$ = makePrefixTermNode ($1, $2); }
1149
1150 postfixOps
1151  : simpleOp2                       { $$ = ltokenList_singleton ($1); }
1152  | postfixOps simpleOp2            { $$ = ltokenList_push ($1, $2); }
1153
1154 infixOpPart
1155  : simpleOp2 secondary             { $$ = pushInfixOpPartNode (termNodeList_new (),  $1, $2); }
1156  | infixOpPart simpleOp2 secondary { $$ = pushInfixOpPartNode ($1, $2, $3); }
1157
1158 secondary
1159  : primary
1160  | bracketed                 { $$ = computePossibleSorts ($1); }
1161  | bracketed primary         { $$ = updateMatchedNode ((termNode)0, $1, $2); }
1162  | primary bracketed         { $$ = updateMatchedNode ($1, $2, (termNode)0); }
1163  | primary bracketed primary { $$ = updateMatchedNode ($1, $2, $3); }
1164  | sqBracketed               { $$ = computePossibleSorts ($1); }
1165  | sqBracketed primary       { $$ = updateSqBracketedNode ((termNode)0, $1, $2); }
1166
1167 bracketed
1168  : matched LLT_COLON sortId    { $$ = $1; $$->sort = sort_lookupName (ltoken_getText ($3)); }
1169  | matched
1170
1171 sqBracketed
1172  : LLT_LBRACKET args LLT_RBRACKET LLT_COLON sortId
1173    { $$ = makeSqBracketedNode ($1, $2, $3);
1174      $$->given = sort_lookupName (ltoken_getText ($5)); }
1175  | LLT_LBRACKET args LLT_RBRACKET
1176    { $$ = makeSqBracketedNode ($1, $2, $3); }
1177  | LLT_LBRACKET  LLT_RBRACKET LLT_COLON sortId
1178    { $$ = makeSqBracketedNode ($1, termNodeList_new (),  $2);
1179      $$->given = sort_lookupName (ltoken_getText ($4));
1180    }
1181  | LLT_LBRACKET  LLT_RBRACKET
1182    { $$ = makeSqBracketedNode ($1, termNodeList_new (),  $2); }
1183
1184 matched
1185  : open args  close          { $$ = makeMatchedNode ($1, $2, $3); }
1186  | open close                { $$ = makeMatchedNode ($1, termNodeList_new (),  $2); }
1187
1188 args
1189  : term                      { $$ = termNodeList_push (termNodeList_new (),  $1); }
1190  | args separator term       { $$ = termNodeList_push ($1, $3); }
1191
1192 primary
1193  : LLT_LPAR term0 LLT_RPAR           /* may need to make a copy of $2 */
1194    { $$ = $2; $$->wrapped = $$->wrapped + 1; }
1195  | varId
1196    { $$ = makeSimpleTermNode ($1); }
1197  | opId LLT_LPAR termList LLT_RPAR
1198    { $$ = makeOpCallTermNode ($1, $2, $3, $4); }
1199  | lclPrimary
1200  | primary stateFcn
1201    { $$ = makePostfixTermNode2 ($1, $2); }
1202  | primary selectSym simpleIdOrTypedefName
1203    { ltoken_markOwned ($3); $$ = makeSelectTermNode ($1, $2, $3); }
1204  | primary mapSym simpleIdOrTypedefName
1205    { ltoken_markOwned ($3); $$ = makeMapTermNode ($1, $2, $3); }
1206  | primary LLT_LBRACKET LLT_RBRACKET
1207    { $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, termNodeList_new (),  $3),
1208                                 (termNode)0); }
1209  | primary LLT_LBRACKET termList LLT_RBRACKET
1210    { $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, $3, $4), (termNode)0); }
1211  | primary LLT_COLON sortId
1212    { $$ = $1; $$->given = sort_lookupName (ltoken_getText ($3)); }
1213
1214 termList
1215  : term0                  { $$ = termNodeList_push (termNodeList_new (),  $1); }
1216  | termList LLT_COMMA term0   { $$ = termNodeList_push ($1, $3); }
1217
1218 stateFcn
1219  : preSym
1220  | postSym
1221  | anySym
1222  | LLT_QUOTE
1223
1224 lclPrimary
1225  : cLiteral
1226  | LLT_RESULT                           { $$ = makeSimpleTermNode ($1); }
1227  | LLT_FRESH LLT_LPAR termList LLT_RPAR         { $$ = makeOpCallTermNode ($1, $2, $3, $4); }
1228  | LLT_UNCHANGED LLT_LPAR LLT_ALL LLT_RPAR          { $$ = makeUnchangedTermNode1 ($1, $3); }
1229  | LLT_UNCHANGED LLT_LPAR storeRefList LLT_RPAR { $$ = makeUnchangedTermNode2 ($1, $3); }
1230  | LLT_SIZEOF LLT_LPAR term LLT_RPAR
1231    { termNodeList x = termNodeList_new ();
1232      termNodeList_addh (x, $3);
1233      $$ = makeOpCallTermNode ($1, $2, x, $4);
1234    }
1235  | LLT_ISSUB LLT_LPAR term LLT_COMMA term LLT_RPAR
1236    { termNodeList x = termNodeList_new ();
1237      termNodeList_addh (x, $3);
1238      termNodeList_addh (x, $5);
1239      $$ = makeOpCallTermNode ($1, $2, x, $6);
1240    }
1241  | LLT_SIZEOF LLT_LPAR lclTypeSpec LLT_RPAR       { $$ = makeSizeofTermNode ($1, $3); }
1242
1243 /* removed 94-Mar-25:
1244 **   | MODIFIES LLT_LPAR term LLT_RPAR
1245 **                             {termNodeList x = termNodeList_new ();
1246 **          termNodeList_addh (x, $3);
1247 **        $$ = makeOpCallTermNode ($1, $2, x, $4); }
1248 */
1249
1250 cLiteral
1251  : LLT_CINTEGER  { $$ = makeLiteralTermNode ($1, sort_int); }
1252  | LLT_LCSTRING  { $$ = makeLiteralTermNode ($1, sort_cstring); }
1253  | LLT_CCHAR     { $$ = makeLiteralTermNode ($1, sort_char); }
1254  | LLT_CFLOAT    { $$ = makeLiteralTermNode ($1, sort_double); }
1255
1256 quantifiers
1257  : quantifier
1258    { $$ = quantifierNodeList_add (quantifierNodeList_new (),  $1); }
1259  | quantifiers quantifier
1260    { $$ = quantifierNodeList_add ($1, $2); }
1261
1262 quantifier
1263  : quantifierSym { scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
1264                    si->kind = SPE_QUANT;
1265                    symtable_enterScope (g_symtab, si); }
1266    quantifiedList
1267    { $$ = makeQuantifierNode ($3, $1); }
1268
1269 quantifiedList
1270  : quantified                         { $$ = varNodeList_add (varNodeList_new (),  $1); }
1271  | quantifiedList LLT_COMMA quantified    { $$ = varNodeList_add ($1, $3); }
1272
1273 quantified
1274  : varId LLT_COLON sortSpec     { $$ = makeVarNode ($1, FALSE, $3); }
1275  | varId LLT_COLON LLT_OBJ sortSpec { $$ = makeVarNode ($1, TRUE, $4); }
1276
1277 simpleIdOrTypedefName
1278  : simpleId
1279  | LLT_TYPEDEF_NAME
1280
1281 /* a different name space from varId/fcnId/typeId */
1282 fcnId : simpleId
1283 varId : simpleId
1284 tagId : simpleIdOrTypedefName
1285 claimId : simpleIdOrTypedefName
1286 sortId : simpleIdOrTypedefName
1287 traitId : simpleIdOrTypedefName
1288 opId : simpleIdOrTypedefName
1289
1290 %%
1291
1292 # include "bison.reset"
1293
1294 /*
1295 ** yytext is set in lex scanner
1296 ** extern YYSTYPE yylval;
1297 ** yylval is defined by code generated by bison
1298 */
1299
1300 void ylerror (char *s)
1301 {
1302   /*
1303   ** This resetting of the left context is very important when multiple
1304   ** files are to be parsed.  We do not want failures to propagate.
1305   ** Lex/Yacc does not reset the flags when the parsing goes bad.
1306   ** BEGIN 0;
1307   **/
1308
1309   /*@-mustfree@*/
1310   lclfatalerror (yllval.ltok,
1311                  message ("%s: Token code: %s, Token String: %s",
1312                           cstring_fromChars (s),
1313                           ltoken_unparseCodeName (yllval.ltok),
1314                           ltoken_getRawString (yllval.ltok)));
1315   /*@=mustfree@*/
1316 }
1317
1318 static void yyprint (FILE *f, int t, YYSTYPE value)
1319 {
1320   fprintf (f, " type: %d (%s)", t,
1321            cstring_toCharsSafe (ltoken_getRawString (value.ltok)));
1322 }
1323
1324
1325
1326
1327
1328
1329