src/llgrammar.y

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