/*;-*-C-*-;
-** Copyright (c) Massachusetts Institute of Technology 1994-1998.
-** All Rights Reserved.
-** Unpublished rights reserved under the copyright laws of
-** the United States.
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 University of Virginia,
+** Massachusetts Institute of Technology
**
-** THIS MATERIAL IS PROVIDED AS IS, WITH ABSOLUTELY NO WARRANTY EXPRESSED
-** OR IMPLIED. ANY USE IS AT YOUR OWN RISK.
-**
-** This code is distributed freely and may be used freely under the
-** following conditions:
-**
-** 1. This notice may not be removed or altered.
+** This program is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by the
+** Free Software Foundation; either version 2 of the License, or (at your
+** option) any later version.
+**
+** This program is distributed in the hope that it will be useful, but
+** WITHOUT ANY WARRANTY; without even the implied warranty of
+** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+** General Public License for more details.
+**
+** The GNU General Public License is available from http://www.gnu.org/ or
+** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+** MA 02111-1307, USA.
**
-** 2. Works derived from this code are not distributed for
-** commercial gain without explicit permission from MIT
-** (for permission contact lclint-request@sds.lcs.mit.edu).
+** For information on splint: splint@cs.virginia.edu
+** To report a bug: splint-bug@cs.virginia.edu
+** For more information: http://www.splint.org
*/
/*
-** Copyright (c) Massachusetts Institute of Technology, 1993
-** All Rights Reserved. Unpublished rights reserved
-** under the copyright laws of the United States.
-**++
-** FACILITY: LSLC
-**
-** MODULE DESCRIPTION:
-**
-** FILENAME: llgramar.y
-**
-** PURPOSE: bison grammar for LCL language.
-**
-** AUTHORS:
-** Yang Meng Tan, Massachusetts Institute of Technology
+** Original author: Yang Meng Tan, Massachusetts Institute of Technology
*/
-
%{
-# include "lclintMacros.nf"
-# include "llbasic.h"
+# include "splintMacros.nf"
+# include "basic.h"
# include "lclscan.h"
# include "checking.h"
# include "lslparse.h"
/*@=noparams@*/
/*@-redecl@*/
-void ylerror (char *) /*@modifies *g_msgstream@*/ ;
+void ylerror (char *) /*@modifies *g_warningstream@*/ ;
/*@=redecl@*/
bool g_inTypeDef = FALSE;
%}
+/*@-readonlytrans@*/
+
%union
{
ltoken ltok; /* a leaf is also an ltoken */
/*@only@*/ abstBodyNode abstbody;
/*@only@*/ abstractNode abstract;
/*@only@*/ exposedNode exposed;
+ /*@only@*/ pointers pointers;
/* taggedUnionNode taggedunion; */
/*@only@*/ globalList globals;
/*@only@*/ constDeclarationNode constdeclaration;
/*@only@*/ interfaceNode iface;
/*@only@*/ interfaceNodeList interfacelist;
/*@only@*/ CTypesNode ctypes;
-}
+ /*@-redef@*/
+} /*@=redef@*/
/* Order of precedence is increasing going down the list */
%type <opform> opForm
%type <signature> signature
%type <typname> typeName
-%type <count> middle placeList pointers
+%type <count> middle placeList
+%type <pointers> pointers
%type <abstDecl> optAbstDeclarator
%type <lcltypespec> lclTypeSpec lclType sortSpec
%type <ltokenList> enumeratorList postfixOps
** the call to the static semantic routine.
*/
+/*@=redef@*/
+/*@=readonlytrans@*/
+
%%
interface
: externals { lhExternals ($1); } optDeclarations
{ interfaceNodeList_free ($1); interfaceNodeList_free ($3); }
+;
externals
: /* empty */ { $$ = interfaceNodeList_new (); }
| externals external { $$ = interfaceNodeList_addh ($1, $2);}
+;
external
: imports
| uses
+;
optDeclarations
: /* empty */ { $$ = interfaceNodeList_new (); }
| export declarations { $$ = consInterfaceNode ($1, $2);}
| private declarations { $$ = consInterfaceNode ($1, $2);}
+;
declarations
: /* empty */ { $$ = interfaceNodeList_new (); }
| declarations declaration { $$ = interfaceNodeList_addh ($1, $2);}
+;
declaration
: export
| private
| uses
+;
imports
: LLT_IMPORTS importNameList LLT_SEMI
{ $$ = makeInterfaceNodeImports ($2);
/* assume subspecs are already processed, symbol table info in external file */
}
+;
uses
: LLT_USES traitRefNodeList LLT_SEMI
{ $$ = makeInterfaceNodeUses ($2); readlsignatures ($$);}
+;
export
: constDeclaration
{ $$ = interfaceNode_makeClaim ($1); }
| iter
{ declareIter ($1); $$ = interfaceNode_makeIter ($1); }
+;
iter
: LLT_ITER varId LLT_LPAR iterParamList LLT_RPAR LLT_SEMI
{ $$ = makeIterNode ($2, $4); }
+;
iterParamList
: /* empty */ { $$ = paramNodeList_new (); }
| realIterParamList { $$ = $1; }
+;
realIterParamList
: iterParam
- { $$ = paramNodeList_add (paramNodeList_new (), $1); }
+ { $$ = paramNodeList_add (paramNodeList_new (), $1); }
| realIterParamList LLT_COMMA iterParam
{ $$ = paramNodeList_add ($1,$3); }
-
+;
+
iterParam
: LLT_YIELD param { $$ = markYieldParamNode ($2); }
| param { $$ = $1; }
+;
private
: LLT_SPEC { symtable_export (g_symtab, FALSE); } private2
{ $$ = $3; symtable_export (g_symtab, TRUE); }
+;
private2
: constDeclaration
{ declarePrivType ($1); $$ = interfaceNode_makePrivType ($1); }
| fcn
{ declarePrivFcn ($1, typeId_invalid); $$ = interfaceNode_makePrivFcn ($1); }
+;
constDeclaration
: LLT_CONSTANT lclTypeSpec initDecls LLT_SEMI
{ $$ = makeConstDeclarationNode ($2, $3); }
+;
varDeclaration
: lclTypeSpec initDecls LLT_SEMI
{ $$ = makeVarDeclarationNode ($2, $3, FALSE, FALSE); $$->qualifier = QLF_CONST; }
| LLT_VOLATILE lclTypeSpec initDecls LLT_SEMI
{ $$ = makeVarDeclarationNode ($2, $3, FALSE, FALSE); $$->qualifier = QLF_VOLATILE; }
+;
type
: abstract { $$ = makeAbstractTypeNode ($1); }
| exposed { $$ = makeExposedTypeNode ($1); }
+;
special
: LLT_PRINTFLIKE { $$ = qual_createPrintfLike (); }
| LLT_SCANFLIKE { $$ = qual_createScanfLike (); }
| LLT_MESSAGELIKE { $$ = qual_createMessageLike (); }
+;
fcn
: lclTypeSpec declarator globals { enteringFcnScope ($1, $2, $3); } LLT_LBRACE
privateInits optLetDecl optChecks optRequire optModify optEnsure optClaim LLT_RBRACE
- { $$ = makeFcnNode (qual_createUnknown (), $1, $2, $3, $6, $7,
+ { $$ = makeFcnNode (qual_createUnknown (), $1, $2, $3, $6, $7,
$8, $9, $10, $11, $12);
/* type, declarator, glovbls, privateinits,
lets, checks, requires, modifies, ensures, claims */
lets, checks, requires, modifies, ensures, claims */
symtable_exitScope (g_symtab);
}
-
+;
claim
: LLT_CLAIMS claimId LLT_LPAR optParamList LLT_RPAR globals
symtable_exitScope (g_symtab); }
| LLT_CLAIMS fcnId claimId LLT_SEMI
{ $$ = (claimNode) 0; }
+;
abstract
: LLT_MUTABLE {g_inTypeDef = TRUE; } LLT_TYPE LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
{ $$ = makeAbstractNode ($2, $5, TRUE, TRUE, $7); }
| LLT_IMMUTABLE {g_inTypeDef = TRUE; } LLT_TYPE LLT_TYPEDEF_NAME {g_inTypeDef = FALSE; } abstBody
{ $$ = makeAbstractNode ($1, $4, FALSE, FALSE, $6); }
+;
exposed
: LLT_TYPEDEF lclTypeSpec { g_inTypeDef = TRUE; setExposedType ($2); } declaratorInvs
$$ = (exposedNode)0;
}
*/
+;
importNameList
: importName
- { $$ = importNodeList_add (importNodeList_new (), $1); }
+ { $$ = importNodeList_add (importNodeList_new (), $1); }
| importNameList LLT_COMMA importName
{ $$ = importNodeList_add ($1, $3); }
+;
importName
: interfaceName { $$ = importNode_makePlain ($1); }
| simpleOp interfaceName simpleOp
{ checkBrackets ($1, $3); $$ = importNode_makeBracketed ($2); }
| LLT_LCSTRING { $$ = importNode_makeQuoted ($1); }
+;
interfaceNameList
: interfaceName { $$ = ltokenList_singleton ($1); }
| interfaceNameList LLT_COMMA interfaceName { $$ = ltokenList_push ($1, $3); }
+;
interfaceName
: simpleIdOrTypedefName
/* to allow module names to be the same as LCL type names */
+;
traitRefNodeList
: traitRef
- { $$ = traitRefNodeList_add (traitRefNodeList_new (), $1); }
+ { $$ = traitRefNodeList_add (traitRefNodeList_new (), $1); }
| traitRefNodeList LLT_COMMA traitRef
{ $$ = traitRefNodeList_add ($1, $3); }
+;
traitRef
: traitId
{ $$ = makeTraitRefNode ($2, (renamingNode)0); }
| LLT_LPAR traitIdList LLT_RPAR LLT_LPAR renaming LLT_RPAR
{ $$ = makeTraitRefNode ($2, $5); }
+;
traitIdList
: traitId { $$ = ltokenList_singleton ($1); }
| traitIdList LLT_COMMA traitId { $$ = ltokenList_push ($1, $3); }
+;
renaming
: replaceNodeList
- { $$ = makeRenamingNode (typeNameNodeList_new (), $1); }
+ { $$ = makeRenamingNode (typeNameNodeList_new (), $1); }
| nameList
{ $$ = makeRenamingNode ($1, replaceNodeList_new ()); }
| nameList LLT_COMMA replaceNodeList { $$ = makeRenamingNode ($1, $3); }
+;
nameList
: typeName
- { $$ = typeNameNodeList_add (typeNameNodeList_new (), $1); }
+ { $$ = typeNameNodeList_add (typeNameNodeList_new (), $1); }
| nameList LLT_COMMA typeName { $$ = typeNameNodeList_add ($1, $3); }
+;
replaceNodeList
: replace
- { $$ = replaceNodeList_add (replaceNodeList_new (), $1); }
+ { $$ = replaceNodeList_add (replaceNodeList_new (), $1); }
| replaceNodeList LLT_COMMA replace { $$ = replaceNodeList_add ($1, $3); }
+;
replace
: typeName LLT_FOR CType { $$ = makeReplaceNode ($2, $1, TRUE, $3, NULL, NULL); }
| typeName LLT_FOR name { $$ = makeReplaceNameNode ($2, $1, $3); }
| typeName LLT_FOR name signature { $$ = makeReplaceNode ($2, $1, FALSE, ltoken_undefined,
$3, $4); }
+;
name
: opId { $$ = makeNameNodeId ($1); }
| opForm { $$ = makeNameNodeForm ($1); }
+;
initializer : constLclExpr
+;
constLclExpr : term
+;
initDecls
: initDecl
- { $$ = initDeclNodeList_add (initDeclNodeList_new (), $1); }
+ { $$ = initDeclNodeList_add (initDeclNodeList_new (), $1); }
| initDecls LLT_COMMA initDecl
{ $$ = initDeclNodeList_add ($1, $3); }
+;
initDecl
: declarator { $$ = makeInitDeclNode ($1, (termNode)0); }
| declarator LLT_EQUALS initializer { $$ = makeInitDeclNode ($1, $3); }
+;
globals
: /* empty */ /* has the same structure */
{ $$ = varDeclarationNodeList_new (); }
| globals globalDecl
{ varDeclarationNodeList_addh ($1, $2); $$ = $1; }
+;
globalDecl
: lclTypeSpec initDecls LLT_SEMI { $$ = makeVarDeclarationNode ($1, $2, TRUE, FALSE); }
| LLT_INTERNAL LLT_SEMI { $$ = makeInternalStateNode (); }
| LLT_FILESYS LLT_SEMI { $$ = makeFileSystemNode (); }
+;
privateInits
: /* empty */ { $$ = varDeclarationNodeList_new (); }
| privateInits privateInit { varDeclarationNodeList_addh ($1, $2); $$ = $1; }
+;
privateInit
: LLT_PRIVATE lclTypeSpec initDecls LLT_SEMI
{ $$ = makeVarDeclarationNode ($2, $3, FALSE, TRUE); }
+;
optLetDecl
: /* empty */ { $$ = letDeclNodeList_new (); }
| LLT_LET beDeclList LLT_SEMI { $$ = $2; }
+;
beDeclList
- : beDecl { $$ = letDeclNodeList_add (letDeclNodeList_new (), $1); }
+ : beDecl { $$ = letDeclNodeList_add (letDeclNodeList_new (), $1); }
| beDeclList LLT_COMMA beDecl { $$ = letDeclNodeList_add ($1, $3); }
+;
beDecl
: varId LLT_COLON sortSpec LLT_BE term { $$ = makeLetDeclNode ($1, $3, $5); }
| varId LLT_BE term { $$ = makeLetDeclNode ($1, (lclTypeSpecNode)0, $3); }
+;
sortSpec : lclTypeSpec
+;
optChecks
: /* empty */ { $$ = (lclPredicateNode)0; }
| LLT_CHECKS lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeChecksNode ($1, $2); }
+;
optRequire
: /* empty */ { $$ = (lclPredicateNode)0; }
| LLT_REQUIRES lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeRequiresNode ($1, $2);}
+;
optModify
: /* empty */ { $$ = (modifyNode)0; }
| LLT_MODIFIES LLT_NOTHING LLT_SEMI { $$ = makeModifyNodeSpecial ($1, TRUE); }
| LLT_MODIFIES LLT_ANYTHING LLT_SEMI { $$ = makeModifyNodeSpecial ($1, FALSE); }
| LLT_MODIFIES storeRefList LLT_SEMI { $$ = makeModifyNodeRef ($1, $2); }
+;
storeRefList
- : storeRef { $$ = storeRefNodeList_add (storeRefNodeList_new (), $1); }
+ : storeRef { $$ = storeRefNodeList_add (storeRefNodeList_new (), $1); }
| storeRefList LLT_COMMA storeRef { $$ = storeRefNodeList_add ($1, $3); }
+;
storeRef
: term { $$ = makeStoreRefNodeTerm ($1); }
| LLT_OBJ lclType { $$ = makeStoreRefNodeType ($2, TRUE); }
| LLT_INTERNAL { $$ = makeStoreRefNodeInternal (); }
| LLT_FILESYS { $$ = makeStoreRefNodeSystem (); }
+;
optEnsure
: /* empty */ { $$ = (lclPredicateNode)0; }
| LLT_ENSURES lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeEnsuresNode ($1, $2);}
+;
optClaim
: /* empty */ { $$ = (lclPredicateNode)0; }
| LLT_CLAIMS lclPredicate LLT_SEMI { checkLclPredicate ($1, $2); $$ = makeIntraClaimNode ($1, $2);}
+;
optParamList
: /* empty */ { $$ = paramNodeList_new (); }
| realParamList { $$ = $1; }
+;
realParamList
: paramList
- | LLT_TELIPSIS { $$ = paramNodeList_add (paramNodeList_new (), paramNode_elipsis ()); }
+ | LLT_TELIPSIS { $$ = paramNodeList_add (paramNodeList_new (), paramNode_elipsis ()); }
| paramList LLT_COMMA LLT_TELIPSIS { $$ = paramNodeList_add ($1, paramNode_elipsis ()); }
+;
paramList
: param { $$ = paramNodeList_single ($1); }
| paramList LLT_COMMA param { $$ = paramNodeList_add ($1, $3); }
+;
optBody
: /* empty */ { $$ = (programNode)0; }
| LLT_BODY LLT_LBRACE callExpr LLT_RBRACE { $$ = $3; }
| LLT_BODY LLT_LBRACE callExpr LLT_SEMI LLT_RBRACE { $$ = $3; }
+;
callExpr
: stmt { $$ = makeProgramNode ($1); }
programNodeList_addh (x, $3);
$$ = makeProgramNodeAction (x, ACT_SEQUENCE);
}
+;
stmt
: fcnId LLT_LPAR valueList LLT_RPAR
{ $$ = makeStmtNode ($1, $3, termNodeList_new ()); }
| varId LLT_EQUALS fcnId LLT_LPAR valueList LLT_RPAR
{ $$ = makeStmtNode ($1, $3, $5); }
+;
valueList
- : value { $$ = termNodeList_push (termNodeList_new (), $1); }
+ : value { $$ = termNodeList_push (termNodeList_new (), $1); }
| valueList LLT_COMMA value { $$ = termNodeList_push ($1, $3); }
+;
value
: cLiteral
| value simpleOp value /* infix */ { $$ = makeInfixTermNode ($1, $2, $3); }
| LLT_LPAR value LLT_RPAR { $$ = $2; $$->wrapped = $$->wrapped + 1; }
| fcnId LLT_LPAR LLT_RPAR
- { $$ = makeOpCallTermNode ($1, $2, termNodeList_new (), $3); }
+ { $$ = makeOpCallTermNode ($1, $2, termNodeList_new (), $3); }
| fcnId LLT_LPAR valueList LLT_RPAR
{ $$ = makeOpCallTermNode ($1, $2, $3, $4); }
+;
abstBody
: LLT_SEMI { $$ = (abstBodyNode)0; }
| LLT_LBRACE fcns LLT_RBRACE { $$ = makeAbstBodyNode ($1, $2); }
| LLT_LBRACE interfaceNameList LLT_RBRACE LLT_SEMI { $$ = makeAbstBodyNode2 ($1, $2); }
| LLT_LBRACE LLT_RBRACE LLT_SEMI { $$ = (abstBodyNode)0; }
+;
fcns
: /* empty */ { $$ = fcnNodeList_new (); }
| fcns fcn { $$ = fcnNodeList_add ($1, $2); }
+;
optTypeInv
: /* empty */ { $$ = (lclPredicateNode)0; }
| typeInv
+ ;
typeInv
: LLT_CONSTRAINT { g_inTypeDef = FALSE; } quantifier LLT_LPAR lclPredicate LLT_RPAR
symtable_exitScope (g_symtab);
g_inTypeDef = TRUE;
}
+;
declaratorInvs
- : declaratorInv { $$ = declaratorInvNodeList_add (declaratorInvNodeList_new (), $1); }
+ : declaratorInv { $$ = declaratorInvNodeList_add (declaratorInvNodeList_new (), $1); }
| declaratorInvs LLT_COMMA declaratorInv
{ $$ = declaratorInvNodeList_add ($1, $3); }
+;
declaratorInv
: declarator { declareForwardType ($1); } optExposedBody
{ $$ = makeDeclaratorInvNode ($1, $3); }
+;
optExposedBody
: /* empty */ { $$ = (abstBodyNode)0; }
| LLT_LBRACE optTypeInv LLT_RBRACE { $$ = makeExposedBodyNode ($1, $2); }
+;
CType
: LLT_VOID { $$ = $1; ltoken_setIntField ($$, fixBits (TS_VOID, 0)); }
| LLT_SIGNED { $$ = $1; ltoken_setIntField ($$, fixBits (TS_SIGNED, 0)); }
| LLT_UNSIGNED { $$ = $1; ltoken_setIntField ($$, fixBits (TS_UNSIGNED, 0)); }
| LLT_UNKNOWN { $$ = $1; ltoken_setIntField ($$, fixBits (TS_UNKNOWN, 0)); }
+;
/*
** CTypes allow "unsigned short int" but we drop all C type qualifiers
CTypes
: CType { $$ = makeCTypesNode ((CTypesNode)0, $1); }
| CTypes CType { $$ = makeCTypesNode ($1, $2); }
+;
/* Add abstract type names and typedef names */
{ $$ = makeTypeSpecifier ($1); }
| CTypes
{ $$ = $1; $$->sort = sort_lookupName (lclctype_toSort ($1->intfield)); }
+;
/* Add struct and enum types */
| LLT_NULLTERMINATED { $$ = qual_createNullTerminated () ; }
| LLT_UNDEF { $$ = qual_createUndef (); }
| LLT_KILLED { $$ = qual_createKilled (); }
+;
lclTypeSpec
: typeSpecifier
{ $$ = lclTypeSpecNode_addQual ($2, $1); }
| LLT_VERTICALBAR lclType LLT_COLON lclType LLT_VERTICALBAR
{ $$ = makeLclTypeSpecNodeConj ($2, $4); }
+;
/*
** Add pointers to the right, only used in StoreRef, maybe should throw
| lclTypeSpec pointers
{ llassert (lclTypeSpecNode_isDefined ($1));
$1->pointers = $2; $$ = $1; }
+;
pointers
- : LLT_MULOP { $$ = 1; }
- | pointers LLT_MULOP { $$ = $1 + 1; }
+ : LLT_MULOP { $$ = pointers_createLt ($1); }
+ | pointers LLT_MULOP { $$ = pointers_extend ($1, pointers_createLt ($2)); }
+;
structOrUnionSpec
: LLT_STRUCT optTagId
{ $$ = makeForwardstrOrUnionNode ($1, SU_STRUCT, $2); }
| LLT_UNION tagId
{ $$ = makeForwardstrOrUnionNode ($1, SU_UNION, $2); }
+;
optTagId
: /* empty */ { $$ = ltoken_undefined; }
| tagId
+ ;
structDecls
- : structDecl { $$ = stDeclNodeList_add (stDeclNodeList_new (), $1); }
+ : structDecl { $$ = stDeclNodeList_add (stDeclNodeList_new (), $1); }
| structDecls structDecl { $$ = stDeclNodeList_add ($1, $2); }
+;
/* We don't allow specification of field size */
structDecl
: lclTypeSpec declaratorList LLT_SEMI { $$ = makestDeclNode ($1, $2); }
+;
declaratorList
: declarator
- { $$ = declaratorNodeList_add (declaratorNodeList_new (), $1); }
+ { $$ = declaratorNodeList_add (declaratorNodeList_new (), $1); }
| declaratorList LLT_COMMA declarator
{ $$ = declaratorNodeList_add ($1, $3); }
+;
optCOMMA
: /* empty */ { ; }
| LLT_COMMA { ; }
+;
enumSpec
: LLT_ENUM optTagId LLT_LBRACE enumeratorList optCOMMA LLT_RBRACE
{ $$ = makeEnumSpecNode ($1, $2, $4); }
| LLT_ENUM tagId
{ $$ = makeEnumSpecNode2 ($1, $2); }
+;
enumeratorList
: simpleId { $$ = ltokenList_singleton ($1); }
| enumeratorList LLT_COMMA simpleId { $$ = ltokenList_push ($1, $3); }
+;
/* This part of declarator rules is adapted from GCC (2.2.1)'s C grammar */
declarator
: after_type_decl { $$ = makeDeclaratorNode ($1); }
| notype_decl { $$ = makeDeclaratorNode ($1); }
+;
notype_decl
: varId { $$ = makeTypeExpr ($1); }
| notype_decl arrayQual { $$ = makeArrayNode ($1, $2); }
| notype_decl LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
| notype_decl LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
+;
after_type_decl
: LLT_TYPEDEF_NAME { $$ = makeTypeExpr ($1); }
| after_type_decl arrayQual { $$ = makeArrayNode ($1, $2); }
| after_type_decl LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
| after_type_decl LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
+;
/* A parameter_decl is a decl that can appear in a parameter list.
We disallow the old C way of giving only the id names without types.
| parameter_decl arrayQual { $$ = makeArrayNode ($1, $2); }
| parameter_decl LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
| parameter_decl LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
+;
/* param : the last production allows C types to be generated without the
parameter name */
** | OUT lclTypeSpec notype_decl { $$ = makeOutParamNode ($1, $2, $3); }
** | OUT lclTypeSpec optAbstDeclarator { $$ = makeOutParamNode ($1, $2, $3); }
*/
+;
/* typeName is only used in trait parameter renaming */
: lclTypeSpec optAbstDeclarator { $$ = makeTypeNameNode (FALSE, $1, $2); }
| LLT_OBJ lclTypeSpec optAbstDeclarator { $$ = makeTypeNameNode (TRUE, $2, $3); }
| opForm { $$ = makeTypeNameNodeOp ($1); }
+;
/* Abstract declarator is like a declarator, but with no identifier */
optAbstDeclarator
: /* empty */ { $$ = (abstDeclaratorNode)0; }
| abstDeclarator { $$ = (abstDeclaratorNode)$1; }
+;
abstDeclarator
: LLT_LPAR abstDeclarator LLT_RPAR { $$ = $2; $$->wrapped = $$->wrapped + 1; }
| abstDeclarator LLT_LPAR LLT_RPAR { $$ = makeFunctionNode ($1, paramNodeList_new ()); }
| LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ((typeExpr)0, $2); }
| abstDeclarator LLT_LPAR realParamList LLT_RPAR { $$ = makeFunctionNode ($1, $3); }
+;
arrayQual
: LLT_LBRACKET LLT_RBRACKET { $$ = makeArrayQualNode ($1, (termNode)0); }
| LLT_LBRACKET constLclExpr LLT_RBRACKET { $$ = makeArrayQualNode ($1, $2); }
+;
opForm
: LLT_IF markerSym LLT_THEN markerSym LLT_ELSE markerSym
| markerSym mapSym simpleIdOrTypedefName
{ $$ = makeOpFormNode ($1, OPF_MMAP,
opFormUnion_createAnyOp ($3), ltoken_undefined); }
+;
open
: openSym
| LLT_LBRACE
+;
close
: closeSym
| LLT_RBRACE
+;
anyOp
: simpleOp2
| logicalOp
| eqOp
+;
middle
: /* empty */ { $$ = 0; }
| placeList
+ ;
placeList
: markerSym { $$ = 1; }
| placeList separator markerSym { $$ = $1 + 1; }
+;
separator
: LLT_COMMA
| sepSym
+;
signature
: LLT_COLON domain mapSym sortId { $$ = makesigNode ($1, $2, $4); }
+;
domain
: /* empty */ { $$ = ltokenList_new (); }
| sortList
+ ;
sortList
: sortId { $$ = ltokenList_singleton ($1); }
| sortList LLT_COMMA sortId { $$ = ltokenList_push ($1, $3); }
+;
lclPredicate
: term { $$ = makeLclPredicateNode (ltoken_undefined, $1, LPD_PLAIN);}
+;
term
: term0 { $$ = checkSort ($1); }
+;
/* When "if <term> then <term> else <term> . <logicalOp> <term>"
shift instead of reduce */
{ $$ = makeIfTermNode ($1,$2,$3,$4,$5,$6); }
| equalityTerm
| term0 logicalOp term0 { $$ = makeInfixTermNode ($1, $2, $3); }
+;
equalityTerm
: simpleOpTerm /* was | quantifiers LLT_LPAR term LLT_RPAR */
{ $$ = makeInfixTermNode ($1, $2, $3);}
| simpleOpTerm LLT_EQUALS simpleOpTerm
{ $$ = makeInfixTermNode ($1, $2, $3);}
+;
simpleOpTerm
: prefixOpTerm
| secondary postfixOps { $$ = makePostfixTermNode ($1, $2); }
| secondary infixOpPart { $$ = CollapseInfixTermNode ($1, $2); }
+;
simpleOp2
: simpleOp
| LLT_MULOP
+;
prefixOpTerm
: secondary
| simpleOp2 prefixOpTerm { $$ = makePrefixTermNode ($1, $2); }
+;
postfixOps
: simpleOp2 { $$ = ltokenList_singleton ($1); }
| postfixOps simpleOp2 { $$ = ltokenList_push ($1, $2); }
+;
infixOpPart
- : simpleOp2 secondary { $$ = pushInfixOpPartNode (termNodeList_new (), $1, $2); }
+ : simpleOp2 secondary { $$ = pushInfixOpPartNode (termNodeList_new (), $1, $2); }
| infixOpPart simpleOp2 secondary { $$ = pushInfixOpPartNode ($1, $2, $3); }
+;
secondary
: primary
| primary bracketed primary { $$ = updateMatchedNode ($1, $2, $3); }
| sqBracketed { $$ = computePossibleSorts ($1); }
| sqBracketed primary { $$ = updateSqBracketedNode ((termNode)0, $1, $2); }
+;
bracketed
: matched LLT_COLON sortId { $$ = $1; $$->sort = sort_lookupName (ltoken_getText ($3)); }
| matched
+ ;
sqBracketed
: LLT_LBRACKET args LLT_RBRACKET LLT_COLON sortId
| LLT_LBRACKET args LLT_RBRACKET
{ $$ = makeSqBracketedNode ($1, $2, $3); }
| LLT_LBRACKET LLT_RBRACKET LLT_COLON sortId
- { $$ = makeSqBracketedNode ($1, termNodeList_new (), $2);
+ { $$ = makeSqBracketedNode ($1, termNodeList_new (), $2);
$$->given = sort_lookupName (ltoken_getText ($4));
}
| LLT_LBRACKET LLT_RBRACKET
- { $$ = makeSqBracketedNode ($1, termNodeList_new (), $2); }
+ { $$ = makeSqBracketedNode ($1, termNodeList_new (), $2); }
+;
matched
: open args close { $$ = makeMatchedNode ($1, $2, $3); }
- | open close { $$ = makeMatchedNode ($1, termNodeList_new (), $2); }
+ | open close { $$ = makeMatchedNode ($1, termNodeList_new (), $2); }
+;
args
- : term { $$ = termNodeList_push (termNodeList_new (), $1); }
+ : term { $$ = termNodeList_push (termNodeList_new (), $1); }
| args separator term { $$ = termNodeList_push ($1, $3); }
+;
primary
: LLT_LPAR term0 LLT_RPAR /* may need to make a copy of $2 */
| primary mapSym simpleIdOrTypedefName
{ ltoken_markOwned ($3); $$ = makeMapTermNode ($1, $2, $3); }
| primary LLT_LBRACKET LLT_RBRACKET
- { $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, termNodeList_new (), $3),
+ { $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, termNodeList_new (), $3),
(termNode)0); }
| primary LLT_LBRACKET termList LLT_RBRACKET
{ $$ = updateSqBracketedNode ($1, makeSqBracketedNode ($2, $3, $4), (termNode)0); }
| primary LLT_COLON sortId
{ $$ = $1; $$->given = sort_lookupName (ltoken_getText ($3)); }
+;
termList
- : term0 { $$ = termNodeList_push (termNodeList_new (), $1); }
+ : term0 { $$ = termNodeList_push (termNodeList_new (), $1); }
| termList LLT_COMMA term0 { $$ = termNodeList_push ($1, $3); }
+;
stateFcn
: preSym
| postSym
| anySym
| LLT_QUOTE
+;
lclPrimary
: cLiteral
$$ = makeOpCallTermNode ($1, $2, x, $6);
}
| LLT_SIZEOF LLT_LPAR lclTypeSpec LLT_RPAR { $$ = makeSizeofTermNode ($1, $3); }
+;
/* removed 94-Mar-25:
** | MODIFIES LLT_LPAR term LLT_RPAR
*/
cLiteral
- : LLT_CINTEGER { $$ = makeLiteralTermNode ($1, sort_int); }
- | LLT_LCSTRING { $$ = makeLiteralTermNode ($1, sort_cstring); }
- | LLT_CCHAR { $$ = makeLiteralTermNode ($1, sort_char); }
- | LLT_CFLOAT { $$ = makeLiteralTermNode ($1, sort_double); }
+ : LLT_CINTEGER { $$ = makeLiteralTermNode ($1, g_sortInt); }
+ | LLT_LCSTRING { $$ = makeLiteralTermNode ($1, g_sortCstring); }
+ | LLT_CCHAR { $$ = makeLiteralTermNode ($1, g_sortChar); }
+ | LLT_CFLOAT { $$ = makeLiteralTermNode ($1, g_sortDouble); }
+;
quantifiers
: quantifier
- { $$ = quantifierNodeList_add (quantifierNodeList_new (), $1); }
+ { $$ = quantifierNodeList_add (quantifierNodeList_new (), $1); }
| quantifiers quantifier
{ $$ = quantifierNodeList_add ($1, $2); }
+;
quantifier
: quantifierSym { scopeInfo si = (scopeInfo) dmalloc (sizeof (*si));
symtable_enterScope (g_symtab, si); }
quantifiedList
{ $$ = makeQuantifierNode ($3, $1); }
+;
quantifiedList
- : quantified { $$ = varNodeList_add (varNodeList_new (), $1); }
+ : quantified { $$ = varNodeList_add (varNodeList_new (), $1); }
| quantifiedList LLT_COMMA quantified { $$ = varNodeList_add ($1, $3); }
+;
quantified
: varId LLT_COLON sortSpec { $$ = makeVarNode ($1, FALSE, $3); }
| varId LLT_COLON LLT_OBJ sortSpec { $$ = makeVarNode ($1, TRUE, $4); }
+;
simpleIdOrTypedefName
: simpleId
| LLT_TYPEDEF_NAME
+;
/* a different name space from varId/fcnId/typeId */
-fcnId : simpleId
-varId : simpleId
-tagId : simpleIdOrTypedefName
-claimId : simpleIdOrTypedefName
-sortId : simpleIdOrTypedefName
-traitId : simpleIdOrTypedefName
-opId : simpleIdOrTypedefName
+fcnId : simpleId ;
+varId : simpleId ;
+tagId : simpleIdOrTypedefName ;
+claimId : simpleIdOrTypedefName ;
+sortId : simpleIdOrTypedefName ;
+traitId : simpleIdOrTypedefName ;
+opId : simpleIdOrTypedefName ;
%%
andersk / splint.git / blobdiff