src/Headers/abstract.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 # ifndef ABSTRACT_H
   7 # define ABSTRACT_H
   8
   9 # ifdef NOLCL
  10 # error "Bad include"
  11 # endif
  12
  13 /*
  14 **  These two are needed in symtable.c
  15 */
  16
  17 /*@constant int HT_MAXINDEX; @*/
  18 # define HT_MAXINDEX 255
  19
  20 /* simply use the lower-order bits by masking out the higher order bits */
  21
  22 # include "ltoken.h"
  23 # include "ltokenList.h"
  24
  25 /*
  26 ** forward declarations for structures
  27 */
  28
  29 struct _lclTypeSpecNode;
  30 struct _opFormNode;
  31 struct _strOrUnionNode;
  32 struct _stmtNode;
  33 struct _lclPredicateNode;
  34 struct _typeExpr;
  35 struct _declaratorNode;
  36 struct _abstBodyNode;
  37 struct _functionTermNode;
  38 struct _quantifiedTermNode;
  39 struct _sigNode;
  40 struct _termNode;
  41 struct _nameNode;
  42 struct _importNode;
  43 struct _pairNode;
  44
  45 typedef enum
  46 {
  47   TAG_ENUM, TAG_STRUCT, TAG_UNION, TAG_FWDSTRUCT, TAG_FWDUNION
  48 } tagKind;
  49
  50 # include "importNode.h"
  51 # include "importNodeList.h"
  52
  53 extern void checkBrackets (ltoken p_lb, ltoken p_rb);
  54
  55 # include "sortList.h"
  56 # include "lsymbolList.h"
  57
  58 # include "lsymbolSet.h"
  59 # include "sortSet.h"
  60
  61 /*
  62 ** added pointer indirects to all typedefs, except as noted
  63 ** evs 94-01-05
  64 */
  65
  66 # include "pairNode.h"
  67 # include "pairNodeList.h"
  68
  69 # include "declaratorInvNode.h"
  70 # include "declaratorInvNodeList.h"
  71
  72 # include "typeExpr.h"  /* also defines abstDeclaratorNode */
  73
  74 # include "declaratorNode.h"
  75 # include "declaratorNodeList.h"
  76
  77 # include "arrayQualNode.h"
  78
  79 # include "varNode.h"
  80 # include "varNodeList.h"
  81
  82 # include "quantifierNode.h"
  83 # include "quantifierNodeList.h"
  84
  85 # include "storeRefNode.h"
  86 # include "storeRefNodeList.h"
  87
  88 # include "modifyNode.h"
  89
  90 # include "letDeclNode.h"
  91 # include "letDeclNodeList.h"
  92
  93 # include "programNode.h"
  94 # include "programNodeList.h"
  95
  96 # include "lclPredicateNode.h"
  97 # include "exposedNode.h"
  98
  99 typedef enum {
 100   TK_ABSTRACT, TK_EXPOSED, TK_UNION
 101   } typeKind ;
 102
 103 # include "CTypesNode.h"
 104
 105 # include "initDeclNode.h"
 106 # include "initDeclNodeList.h"
 107
 108 # include "constDeclarationNode.h"
 109
 110 typedef enum {
 111   QLF_NONE, QLF_CONST, QLF_VOLATILE
 112   } qualifierKind;
 113
 114 # include "varDeclarationNode.h"
 115 # include "varDeclarationNodeList.h"
 116
 117 # include "globalList.h"
 118
 119 # include "claimNode.h"
 120
 121 # include "fcnNode.h"
 122 # include "fcnNodeList.h"
 123
 124 # include "iterNode.h"
 125
 126 # include "abstBodyNode.h"
 127 # include "abstractNode.h"
 128
 129 # include "stDeclNode.h"
 130 # include "stDeclNodeList.h"
 131
 132 # include "taggedUnionNode.h"
 133 # include "typeNode.h"
 134
 135 # include "strOrUnionNode.h"
 136 # include "enumSpecNode.h"
 137
 138 # include "lclTypeSpecNode.h"
 139 # include "typeNamePack.h"
 140
 141 # include "typeNameNode.h"
 142 # include "typeNameNodeList.h"              /* this is a list of typeNameNode's */
 143
 144 # include "opFormNode.h"
 145
 146 # include "quantifiedTermNode.h"
 147
 148 typedef enum {
 149   TRM_LITERAL, TRM_CONST, TRM_VAR,
 150   TRM_ZEROARY, TRM_APPLICATION, TRM_QUANTIFIER,
 151   TRM_UNCHANGEDALL, TRM_UNCHANGEDOTHERS,
 152   TRM_SIZEOF
 153   } termKIND;
 154
 155 # include "sigNode.h"
 156 # include "sigNodeSet.h"
 157
 158 # include "signNode.h"
 159 # include "nameNode.h"
 160
 161 # include "lslOp.h"
 162 # include "lslOpSet.h"
 163
 164 # include "replaceNode.h"
 165 # include "replaceNodeList.h"
 166
 167 # include "renamingNode.h"
 168
 169 # include "traitRefNode.h"
 170 # include "traitRefNodeList.h"
 171
 172 # include "exportNode.h"
 173 # include "privateNode.h"
 174
 175 # include "interfaceNode.h"
 176 # include "interfaceNodeList.h" /* note: interfaceList --> interfaceNodeList */
 177
 178 # include "termNode.h"
 179 # include "termNodeList.h"
 180 # include "stmtNode.h"
 181
 182 /* The following are for parsing LSL signatures */
 183
 184 # include "sortSetList.h"
 185 # include "lslOpList.h"
 186
 187 /* function prototypes for parsing LSL signatures */
 188
 189 extern /*@only@*/ lslOp
 190   makelslOpNode (/*@only@*/ /*@null@*/ nameNode p_name,
 191                  /*@dependent@*/ sigNode p_s);
 192
 193 extern /*@only@*/ cstring lslOp_unparse (lslOp p_x);
 194
 195 /*@notfunction@*/
 196 # define MASH(x,y) \
 197   (/*@+enumint@*/ (((unsigned) ((x)+1) << 1) + (y)) & HT_MAXINDEX /*@=enumint@*/)
 198
 199 extern void abstract_init (void);
 200 extern void resetImports (cstring p_current) ;
 201
 202 extern interfaceNodeList
 203   consInterfaceNode (/*@only@*/ interfaceNode p_n, /*@returned@*/ interfaceNodeList p_ns);
 204
 205 /* evs 8 Sept 1993       changed to importNodeList */
 206 extern /*@only@*/ interfaceNode
 207   makeInterfaceNodeImports (/*@only@*/ importNodeList p_x);
 208
 209 extern /*@only@*/ nameNode
 210   makeNameNodeForm (/*@only@*/ /*@null@*/ opFormNode p_opform) /*@*/ ;
 211 extern /*@only@*/ nameNode
 212   makeNameNodeId (/*@only@*/ ltoken p_opid) /*@*/ ;
 213 extern /*@only@*/ interfaceNode
 214   makeInterfaceNodeUses (/*@only@*/ traitRefNodeList p_x) /*@*/ ;
 215 extern /*@only@*/ interfaceNode
 216   interfaceNode_makeConst (/*@only@*/ constDeclarationNode p_x) /*@*/ ;
 217 extern /*@only@*/ interfaceNode
 218   interfaceNode_makeVar (/*@only@*/ varDeclarationNode p_x) /*@*/ ;
 219 extern /*@only@*/ interfaceNode
 220   interfaceNode_makeType (/*@only@*/ typeNode p_x) /*@*/ ;
 221 extern /*@only@*/ interfaceNode
 222   interfaceNode_makeFcn (/*@only@*/ fcnNode p_x) /*@*/ ;
 223 extern /*@only@*/ interfaceNode
 224   interfaceNode_makeClaim (/*@only@*/ claimNode p_x) /*@*/ ;
 225 extern /*@only@*/ interfaceNode interfaceNode_makeIter (/*@only@*/ iterNode p_x) /*@*/ ;
 226 extern /*@only@*/ interfaceNode interfaceNode_makePrivConst(/*@only@*/ constDeclarationNode p_x) /*@*/ ;
 227 extern /*@only@*/ interfaceNode
 228   interfaceNode_makePrivVar(/*@only@*/ varDeclarationNode p_x) /*@*/ ;
 229 extern /*@only@*/ interfaceNode
 230   interfaceNode_makePrivType(/*@only@*/ typeNode p_x) /*@*/ ;
 231 extern /*@only@*/ interfaceNode
 232   interfaceNode_makePrivFcn(/*@only@*/ fcnNode p_x) /*@*/ ;
 233 extern /*@only@*/ typeNode makeAbstractTypeNode (/*@only@*/ abstractNode p_x) /*@*/ ;
 234 extern /*@only@*/ typeNode makeExposedTypeNode (/*@only@*/ exposedNode p_x) /*@*/ ;
 235
 236 extern /*@only@*/ traitRefNode
 237   makeTraitRefNode(/*@only@*/ ltokenList p_fl, /*@null@*/ /*@only@*/ renamingNode p_r) /*@*/ ;
 238
 239 extern /*@only@*/ cstring printLeaves2 (ltokenList p_f) /*@*/ ;
 240 extern /*@only@*/ cstring printRawLeaves2 (ltokenList p_f) /*@*/ ;
 241 extern /*@only@*/ cstring sigNode_unparseText (/*@null@*/ sigNode p_n) /*@*/ ;
 242
 243 extern /*@only@*/ renamingNode
 244   makeRenamingNode (/*@only@*/ typeNameNodeList p_n,
 245                     /*@only@*/ replaceNodeList p_r) /*@*/ ;
 246 extern /*@only@*/ replaceNode
 247   makeReplaceNode (/*@only@*/ ltoken p_t, /*@only@*/ typeNameNode p_tn, bool p_is_ctype,
 248                    /*@only@*/ ltoken p_ct,
 249                    /*@null@*/ /*@only@*/ nameNode p_nn,
 250                    /*@null@*/ /*@only@*/ sigNode p_sn) /*@*/ ;
 251
 252 extern /*@only@*/ sigNode
 253   makesigNode (/*@only@*/ ltoken p_t, /*@only@*/ ltokenList p_domain, /*@only@*/ ltoken p_range) /*@*/ ;
 254
 255 extern /*@only@*/ replaceNode
 256   makeReplaceNameNode (/*@only@*/ ltoken p_t, /*@only@*/ typeNameNode p_tn,
 257                        /*@only@*/ nameNode p_nn) /*@*/ ;
 258
 259 extern /*@only@*/ opFormNode
 260   makeOpFormNode(/*@only@*/ ltoken p_t, opFormKind p_k,
 261                  opFormUnion p_u, /*@only@*/ ltoken p_close) /*@*/ ;
 262
 263 extern /*@only@*/ typeNameNode
 264   makeTypeNameNode (bool p_isObj, /*@only@*/ lclTypeSpecNode p_t,
 265                     /*@only@*/ abstDeclaratorNode p_n) /*@*/ ;
 266 extern /*@only@*/ typeNameNode
 267   makeTypeNameNodeOp (/*@only@*/ opFormNode p_n) /*@*/ ;
 268
 269 extern /*@only@*/ lclTypeSpecNode
 270   makeLclTypeSpecNodeConj (/*@only@*/ /*@null@*/ lclTypeSpecNode p_a,
 271                            /*@only@*/ /*@null@*/ lclTypeSpecNode p_b) /*@*/ ;
 272
 273 extern /*@only@*/ lclTypeSpecNode
 274   makeLclTypeSpecNodeType(/*@only@*/ /*@null@*/ CTypesNode p_x) /*@*/ ;
 275
 276 extern /*@only@*/ lclTypeSpecNode
 277   makeLclTypeSpecNodeSU(/*@only@*/ /*@null@*/ strOrUnionNode p_x) /*@*/ ;
 278
 279 extern /*@only@*/ lclTypeSpecNode
 280   makeLclTypeSpecNodeEnum(/*@only@*/ /*@null@*/ enumSpecNode p_x) /*@*/ ;
 281
 282 extern /*@only@*/ lclTypeSpecNode
 283   lclTypeSpecNode_addQual (/*@only@*/ lclTypeSpecNode p_n, qual p_q)
 284   /*@modifies p_n@*/ ;
 285
 286 extern /*@only@*/ enumSpecNode
 287   makeEnumSpecNode (/*@only@*/ ltoken p_t, /*@only@*/ ltoken p_optTagId, /*@owned@*/ ltokenList p_enums);
 288
 289 extern /*@only@*/ enumSpecNode
 290   makeEnumSpecNode2 (/*@only@*/ ltoken p_t, /*@only@*/ ltoken p_tagid);
 291
 292 extern /*@only@*/ strOrUnionNode
 293   makestrOrUnionNode (/*@only@*/ ltoken p_str, suKind p_k,
 294                          /*@only@*/ ltoken p_opttagid, /*@only@*/ stDeclNodeList p_x);
 295
 296 extern /*@only@*/ strOrUnionNode
 297   makeForwardstrOrUnionNode (/*@only@*/ ltoken p_str, suKind p_k,
 298                                 /*@only@*/ ltoken p_tagid);
 299
 300 extern /*@only@*/ stDeclNode
 301   makestDeclNode (/*@only@*/ lclTypeSpecNode p_s,
 302                   /*@only@*/ declaratorNodeList p_x);
 303 extern /*@only@*/ constDeclarationNode
 304   makeConstDeclarationNode (/*@only@*/ lclTypeSpecNode p_t,
 305                             /*@only@*/ initDeclNodeList p_decls);
 306 extern /*@only@*/ varDeclarationNode
 307   makeVarDeclarationNode (/*@only@*/ lclTypeSpecNode p_t,
 308                           /*@only@*/ initDeclNodeList p_x,
 309                           bool p_isGlobal, bool p_isPrivate);
 310
 311 extern varDeclarationNode makeFileSystemNode (void);
 312 extern varDeclarationNode makeInternalStateNode (void);
 313
 314 extern /*@only@*/ initDeclNode
 315   makeInitDeclNode (/*@only@*/ declaratorNode p_d, /*@null@*/ /*@only@*/ termNode p_x);
 316
 317 extern /*@only@*/ abstractNode
 318   makeAbstractNode (/*@only@*/ ltoken p_t, /*@only@*/ ltoken p_name,
 319                     bool p_isMutable, bool p_isRefCounted,
 320                     /*@only@*/ abstBodyNode p_a);
 321
 322 extern /*@unused@*/ /*@only@*/ cstring abstBodyNode_unparseExposed (abstBodyNode p_n);
 323
 324 extern /*@only@*/ exposedNode
 325   makeExposedNode (/*@only@*/ ltoken p_t, /*@only@*/ lclTypeSpecNode p_s,
 326                    /*@only@*/ declaratorInvNodeList p_d);
 327
 328 extern /*@only@*/ declaratorInvNode
 329   makeDeclaratorInvNode (/*@only@*/ declaratorNode p_d,
 330                          /*@only@*/ abstBodyNode p_b);
 331
 332 extern /*@only@*/ fcnNode
 333   fcnNode_fromDeclarator (/*@only@*/ /*@null@*/ lclTypeSpecNode p_t,
 334                           /*@only@*/ declaratorNode p_d);
 335
 336 extern /*@only@*/ fcnNode
 337   makeFcnNode (qual p_specQual,
 338                /*@only@*/ /*@null@*/ lclTypeSpecNode p_t,
 339                /*@only@*/ declaratorNode p_d,
 340                /*@only@*/ /*@null@*/ globalList p_g,
 341                /*@only@*/ /*@null@*/ varDeclarationNodeList p_privateinits,
 342                /*@only@*/ /*@null@*/ letDeclNodeList p_lets,
 343                /*@only@*/ /*@null@*/ lclPredicateNode p_checks,
 344                /*@only@*/ /*@null@*/ lclPredicateNode p_requires,
 345                /*@only@*/ /*@null@*/ modifyNode p_m,
 346                /*@only@*/ /*@null@*/ lclPredicateNode p_ensures,
 347                /*@only@*/ /*@null@*/ lclPredicateNode p_claims);
 348
 349 extern /*@only@*/ iterNode
 350   makeIterNode (/*@only@*/ ltoken p_id, /*@only@*/ paramNodeList p_p);
 351
 352 extern /*@only@*/ claimNode
 353   makeClaimNode (/*@only@*/ ltoken p_id,
 354                  /*@only@*/ paramNodeList p_p,
 355                  /*@only@*/ /*@null@*/ globalList p_g,
 356                  /*@only@*/ /*@null@*/ letDeclNodeList p_lets,
 357                  /*@only@*/ /*@null@*/ lclPredicateNode p_requires,
 358                  /*@only@*/ /*@null@*/ programNode p_b,
 359                  /*@only@*/ /*@null@*/ lclPredicateNode p_ensures);
 360
 361 extern /*@only@*/ lclPredicateNode
 362   makeIntraClaimNode (/*@only@*/ ltoken p_t, /*@only@*/ lclPredicateNode p_n);
 363
 364 extern /*@only@*/ lclPredicateNode
 365   makeRequiresNode (/*@only@*/ ltoken p_t, /*@only@*/ lclPredicateNode p_n);
 366
 367 extern /*@only@*/ lclPredicateNode
 368   makeChecksNode (/*@only@*/ ltoken p_t, /*@only@*/ lclPredicateNode p_n);
 369
 370 extern /*@only@*/ lclPredicateNode
 371   makeEnsuresNode (/*@only@*/ ltoken p_t, /*@only@*/ lclPredicateNode p_n);
 372
 373 extern /*@only@*/ lclPredicateNode
 374   makeLclPredicateNode (/*@only@*/ ltoken p_t, /*@only@*/ termNode p_n,
 375                         lclPredicateKind p_k);
 376
 377 extern /*@only@*/ stmtNode
 378   makeStmtNode (/*@only@*/ ltoken p_varId,
 379                 /*@only@*/ ltoken p_fcnId, /*@only@*/ termNodeList p_v);
 380
 381 extern /*@only@*/ programNode
 382   makeProgramNodeAction (/*@only@*/ programNodeList p_x, actionKind p_k);
 383
 384 extern /*@only@*/ programNode
 385   makeProgramNode (/*@only@*/ stmtNode p_x);
 386
 387 extern /*@only@*/ storeRefNode
 388   makeStoreRefNodeTerm (/*@only@*/ termNode p_t);
 389
 390 extern /*@only@*/ storeRefNode
 391   makeStoreRefNodeType (/*@only@*/ lclTypeSpecNode p_t, bool p_isObj);
 392
 393 extern /*@only@*/ modifyNode
 394   makeModifyNodeSpecial (/*@only@*/ ltoken p_t, bool p_modifiesNothing);
 395
 396 extern storeRefNode makeStoreRefNodeInternal (void);
 397 extern storeRefNode makeStoreRefNodeSystem (void);
 398
 399 extern /*@only@*/ modifyNode
 400   makeModifyNodeRef (/*@only@*/ ltoken p_t, /*@only@*/ storeRefNodeList p_y);
 401
 402 extern /*@only@*/ letDeclNode
 403   makeLetDeclNode(/*@only@*/ ltoken p_varid, /*@null@*/ /*@only@*/ lclTypeSpecNode p_t,
 404                   /*@only@*/ termNode p_term);
 405
 406 extern /*@only@*/ abstBodyNode
 407   makeAbstBodyNode (/*@only@*/ ltoken p_t, /*@only@*/ fcnNodeList p_f);
 408
 409 extern /*@only@*/ abstBodyNode
 410   makeExposedBodyNode (/*@only@*/ ltoken p_t, /*@only@*/ lclPredicateNode p_inv);
 411
 412 extern /*@only@*/ abstBodyNode
 413   makeAbstBodyNode2 (/*@only@*/ ltoken p_t, /*@only@*/ ltokenList p_ops);
 414
 415 extern paramNode markYieldParamNode (/*@returned@*/ paramNode p_p);
 416
 417 extern /*@only@*/ arrayQualNode
 418   makeArrayQualNode (/*@only@*/ ltoken p_t, /*@null@*/ /*@only@*/ termNode p_term);
 419
 420 extern /*@only@*/ quantifierNode
 421   makeQuantifierNode (/*@only@*/ varNodeList p_v, /*@only@*/ ltoken p_quant);
 422
 423 extern /*@only@*/ varNode
 424   makeVarNode (/*@only@*/ ltoken p_varid, bool p_isObj, /*@only@*/ lclTypeSpecNode p_t);
 425
 426 extern /*@only@*/ typeExpr makeTypeExpr (/*@only@*/ ltoken p_t);
 427
 428 extern /*@only@*/ declaratorNode
 429   makeDeclaratorNode (/*@only@*/ typeExpr p_t);
 430
 431 extern /*@only@*/ typeExpr
 432   makeFunctionNode (/*@null@*/ /*@only@*/ typeExpr p_x, /*@only@*/ paramNodeList p_p);
 433
 434 extern /*@only@*/ typeExpr
 435   makePointerNode (/*@only@*/ ltoken p_star, /*@null@*/ /*@only@*/ /*@returned@*/ typeExpr p_x);
 436
 437 extern /*@only@*/ typeExpr
 438   makeArrayNode (/*@only@*/ /*@returned@*/ /*@null@*/ typeExpr p_x,
 439                  /*@only@*/ arrayQualNode p_a);
 440
 441 extern /*@only@*/ paramNode
 442   makeParamNode (/*@only@*/ lclTypeSpecNode p_t, /*@only@*/ typeExpr p_d);
 443
 444 extern /*@only@*/ termNode
 445   makeIfTermNode (/*@only@*/ ltoken p_ift, /*@only@*/ termNode p_ifn,
 446                   /*@only@*/ ltoken p_thent, /*@only@*/ termNode p_thenn,
 447                   /*@only@*/ ltoken p_elset, /*@only@*/ termNode p_elsen);
 448
 449 extern /*@only@*/ termNode
 450   makeQuantifiedTermNode (/*@only@*/ quantifierNodeList p_qn,
 451                           /*@only@*/ ltoken p_open,
 452                           /*@only@*/ termNode p_t, /*@only@*/ ltoken p_close);
 453
 454 extern /*@only@*/ termNode
 455   makeInfixTermNode (/*@only@*/ termNode p_x, /*@only@*/ ltoken p_op,
 456                      /*@only@*/ termNode p_y);
 457
 458 extern /*@only@*/ termNode
 459   makePostfixTermNode (/*@returned@*/ /*@only@*/ termNode p_secondary,
 460                        /*@only@*/ ltokenList p_postfixops);
 461
 462 extern /*@only@*/ termNode
 463   makePostfixTermNode2 (/*@only@*/ /*@returned@*/ termNode p_secondary,
 464                         /*@only@*/ ltoken p_postfixop);
 465
 466 extern /*@only@*/ termNode
 467   makePrefixTermNode (/*@only@*/ ltoken p_op, /*@only@*/ termNode p_arg);
 468
 469 extern /*@exposed@*/ termNode
 470   CollapseInfixTermNode (/*@returned@*/ termNode p_secondary, termNodeList p_infix);
 471
 472 extern /*@only@*/ termNode
 473   makeMatchedNode (/*@only@*/ ltoken p_open,
 474                    /*@only@*/ termNodeList p_args, /*@only@*/ ltoken p_close);
 475
 476 extern /*@only@*/ termNode
 477   makeSqBracketedNode (/*@only@*/ ltoken p_lbracket,
 478                        /*@only@*/ termNodeList p_args,
 479                        /*@only@*/ ltoken p_rbracket);
 480
 481 extern /*@only@*/ termNode
 482   updateSqBracketedNode (/*@null@*/ /*@only@*/ termNode p_left,
 483                          /*@only@*/ /*@returned@*/ termNode p_t,
 484                          /*@null@*/ /*@only@*/ termNode p_right);
 485
 486 extern termNode
 487   updateMatchedNode (/*@null@*/ /*@only@*/ termNode p_left, /*@returned@*/ termNode p_t,
 488                      /*@null@*/ /*@only@*/ termNode p_right);
 489
 490 extern /*@only@*/ termNode
 491   makeSimpleTermNode (/*@only@*/ ltoken p_varid);
 492 extern /*@only@*/ termNode
 493   makeSelectTermNode (/*@only@*/ termNode p_pri, /*@only@*/ ltoken p_select,
 494                       /*@dependent@*/ ltoken p_id);
 495 extern /*@only@*/ termNode
 496   makeMapTermNode (/*@only@*/ termNode p_pri, /*@only@*/ ltoken p_map,
 497                    /*@dependent@*/ ltoken p_id);
 498 extern /*@only@*/ termNode
 499   makeLiteralTermNode (/*@only@*/ ltoken p_tok, sort p_s);
 500
 501 extern /*@only@*/ termNode
 502   makeUnchangedTermNode1 (/*@only@*/ ltoken p_op, /*@only@*/ ltoken p_all);
 503 extern /*@only@*/ termNode
 504   makeUnchangedTermNode2 (/*@only@*/ ltoken p_op, /*@only@*/ storeRefNodeList p_x);
 505 extern /*@only@*/ termNode
 506   makeSizeofTermNode(/*@only@*/ ltoken p_op, /*@only@*/ lclTypeSpecNode p_type);
 507 extern /*@only@*/ termNode
 508   makeOpCallTermNode (/*@only@*/ ltoken p_op, /*@only@*/ ltoken p_open,
 509                       /*@only@*/ termNodeList p_args, /*@only@*/ ltoken p_close);
 510
 511 extern sort sigNode_rangeSort (sigNode p_sig);
 512
 513 extern /*@only@*/ sortList sigNode_domain (sigNode p_sig);
 514
 515 extern bool sameNameNode (/*@null@*/ nameNode p_n1, /*@null@*/ nameNode p_n2);
 516
 517 extern /*@only@*/ CTypesNode
 518   makeCTypesNode (/*@null@*/ /*@only@*/ CTypesNode p_ctypes, /*@only@*/ ltoken p_ct);
 519
 520 extern /*@only@*/ CTypesNode
 521   makeTypeSpecifier (/*@only@*/ ltoken p_typedefname) ;
 522
 523 extern bool sigNode_equal (sigNode p_n1, sigNode p_n2);
 524
 525 extern sort lclTypeSpecNode2sort(lclTypeSpecNode p_type);
 526
 527 extern sort typeExpr2ptrSort(sort p_base, /*@null@*/ typeExpr p_t);
 528
 529 /* should be tagKind, instead of int */
 530 extern lsymbol checkAndEnterTag(tagKind p_k, /*@only@*/ ltoken p_opttagid);
 531 extern void enteringFcnScope(lclTypeSpecNode p_t, declaratorNode p_d, globalList p_g);
 532 extern void enteringClaimScope (paramNodeList p_params, globalList p_g);
 533
 534 extern /*@observer@*/ ltoken nameNode_errorToken (/*@null@*/ nameNode p_nn);
 535 extern /*@observer@*/ ltoken termNode_errorToken (/*@null@*/ termNode p_n);
 536 extern /*@observer@*/ ltoken lclTypeSpecNode_errorToken (/*@null@*/ lclTypeSpecNode p_t);
 537
 538 extern opFormUnion opFormUnion_createAnyOp (ltoken p_t);
 539 extern opFormUnion opFormUnion_createMiddle (int p_middle);
 540 extern void LCLBuiltins (void);
 541 extern /*@only@*/ paramNode paramNode_elipsis (void);
 542 extern termNodeList
 543   pushInfixOpPartNode (/*@returned@*/ termNodeList p_x, /*@only@*/ ltoken p_op,
 544                        /*@only@*/ termNode p_secondary);
 545 extern /*@only@*/ cstring declaratorNode_unparseCode (declaratorNode p_x);
 546
 547 extern /*@only@*/ cstring typeExpr_name (/*@null@*/ typeExpr p_x);
 548
 549 extern void setExposedType (lclTypeSpecNode p_s);
 550 extern void declareForwardType (declaratorNode p_declare);
 551
 552 extern /*@only@*/ declaratorNode declaratorNode_copy (declaratorNode p_x);
 553
 554 extern bool lslOp_equal (lslOp p_x, lslOp p_y);
 555
 556 extern void lsymbol_setbool (lsymbol p_s) /*@modifies internalState@*/ ;
 557 extern lsymbol lsymbol_getbool (void);
 558 extern lsymbol lsymbol_getBool (void);
 559 extern lsymbol lsymbol_getTRUE (void);
 560 extern lsymbol lsymbol_getFALSE (void);
 561
 562
 563 # else
 564 # error "Multiple include"
 565 # endif