]> andersk Git - splint.git/blobdiff - src/cgrammar.y
Fixed problem with loop guards in loop test effects. New test case
[splint.git] / src / cgrammar.y
index acfa463825893dc0f8f6c749c2b29a172145d763..5c4f2d8cebf4a6bb51313191a87637f1b7291de7 100644 (file)
@@ -1,32 +1,37 @@
 /*;-*-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-2002 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 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.
 **
-** This code is distributed freely and may be used freely under the 
-** following conditions:
-**
-**     1. This notice may not be removed or altered.
-**
-**     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: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
 */
 %{
 /*
 **
 ** cgrammar.y
 **
-** Yacc/Bison grammar for extended ANSI C used by LCLint.
+** Yacc/Bison grammar for extended ANSI C used by Splint.
 **
 ** original grammar by Nate Osgood ---
 **    hacrat@catfish.lcs.mit.edu Mon Jun 14 13:06:32 1993
 **
-** changes for LCLint --- handle typedef names correctly
+** changes for Splint --- handle typedef names correctly
 ** fix struct/union parsing bug (empty struct is accepted)
 ** add productions to handle macros --- require
 ** error correction --- main source of conflicts in grammar.
 
 extern int yylex ();
 extern void swallowMacro (void);
+extern void yyerror (char *);
 
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
+# include "cscanner.h"
 # include "cgrammar.h"
 # include "exprChecks.h"
 
@@ -53,7 +60,6 @@ extern void swallowMacro (void);
 /*@-matchfields@*/
 
 # define SHOWCSYM FALSE
-void yyerror (char *);
 
 /*
 ** This is necessary, or else when the bison-generated code #include's malloc.h,
@@ -79,6 +85,7 @@ void yyerror (char *);
   qualList tquallist;
   ctype ctyp;
   /*@dependent@*/ sRef sr;
+  /*@only@*/ sRef osr;
 
   /*@only@*/ functionClauseList funcclauselist;
   /*@only@*/ functionClause funcclause;  
@@ -88,6 +95,13 @@ void yyerror (char *);
   /*@only@*/ warnClause warnclause;
   /*@only@*/ stateClause stateclause;
 
+  /*@only@*/ functionConstraint fcnconstraint; 
+
+  /*@only@*/ metaStateConstraint msconstraint;
+  /*@only@*/ metaStateSpecifier msspec;
+  /*@only@*/ metaStateExpression msexpr;
+  /*@observer@*/ metaStateInfo msinfo;
+
   /*@only@*/ sRefList srlist;
   /*@only@*/ globSet globset;
   /*@only@*/ qtype qtyp;
@@ -101,9 +115,10 @@ void yyerror (char *);
   /*@only@*/ uentry oentry;
   /*@only@*/ exprNode expr;
   /*@only@*/ enumNameList enumnamelist;
-  /*@only@*/ exprNodeList alist;
+  /*@only@*/ exprNodeList exprlist;
   /*@only@*/ sRefSet srset; 
   /*@only@*/ cstringList cstringlist;
+
   /*drl
     added 1/19/2001
   */
@@ -121,7 +136,7 @@ void yyerror (char *);
 %token <tok> TSEMI TLBRACE TRBRACE TCOMMA TCOLON TASSIGN TLPAREN 
 %token <tok> TRPAREN TLSQBR TRSQBR TDOT TAMPERSAND TEXCL TTILDE
 %token <tok> TMINUS TPLUS TMULT TDIV TPERCENT TLT TGT TCIRC TBAR TQUEST
-%token <tok> CSIZEOF CALIGNOF ARROW_OP CTYPEDEF COFFSETOF
+%token <tok> CSIZEOF CALIGNOF CTYPEOF ARROW_OP CTYPEDEF COFFSETOF
 %token <tok> INC_OP DEC_OP LEFT_OP RIGHT_OP
 %token <tok> LE_OP GE_OP EQ_OP NE_OP AND_OP OR_OP
 %token <tok> MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN
@@ -141,12 +156,13 @@ void yyerror (char *);
 %token <tok> QSETS
 %token <tok> QRELEASES 
 %token <tok> QPRECLAUSE 
-%token <tok> QPOSTCLAUSE 
+%token <tok> QPOSTCLAUSE
+%token <tok> QINVARIANT
 %token <tok> QALT 
 %token <tok> QUNDEF QKILLED
 %token <tok> QENDMACRO
 
-/* additional tokens introduced by lclint pre-processor. */
+/* additional tokens introduced by splint pre-processor. */
 %token <tok> LLMACRO LLMACROITER LLMACROEND TENDMACRO
 
 /* break comments: */
@@ -180,11 +196,8 @@ void yyerror (char *);
 %token <ctyp> CGCHAR CBOOL CINT CGFLOAT CDOUBLE CVOID 
 %token <tok> QANYTYPE QINTEGRALTYPE QUNSIGNEDINTEGRALTYPE QSIGNEDINTEGRALTYPE
 
-%type <typequal> nullterminatedQualifier
 %token <tok> QNULLTERMINATED
 %token <tok> QSETBUFFERSIZE
-%token <tok> QBUFFERCONSTRAINT
-%token <tok> QENSURESCONSTRAINT
 %token <tok> QSETSTRINGLENGTH
 %token <tok> QMAXSET
 %token <tok> QMAXREAD
@@ -209,18 +222,24 @@ void yyerror (char *);
 
 %type <globsclause> globalsClause globalsClausePlain
 %type <modsclause> modifiesClause modifiesClausePlain nomodsClause
-%type <warnclause> warnClause warnClausePlain
-%type <stateclause> conditionClause conditionClausePlain
+%type <warnclause> warnClause warnClausePlain optWarnClause
+%type <funcclause> conditionClause conditionClausePlain
 %type <stateclause> stateClause stateClausePlain
+%type <msconstraint> metaStateConstraint 
+%type <fcnconstraint> functionConstraint
+%type <msspec> metaStateSpecifier
+%type <msexpr> metaStateExpression
 
 %type <sr> globId globIdListExpr
 %type <globset> globIdList
 
 %token <ctyp>  TYPE_NAME 
+%token <msinfo> METASTATE_NAME 
+%type <msinfo> metaStateName
 %type <cname> enumerator newId  /*@-varuse@*/ /* yacc declares yytranslate here */
 %type <count> pointers /*@=varuse@*/
 
-%type <tok> doHeader stateTag conditionTag 
+%type <tok> doHeader stateTag conditionTag startConditionClause
 %type <typequal> exitsQualifier checkQualifier stateQualifier 
                  paramQualifier returnQualifier visibilityQualifier
                  typedefQualifier refcountQualifier definedQualifier
@@ -240,14 +259,14 @@ void yyerror (char *);
 %type <ntyplist> structNamedDeclList
 
 %type <entrylist> genericParamList paramTypeList paramList idList paramIdList
-%type <alist> argumentExprList iterArgList
-%type <alist> initList
+%type <exprlist> argumentExprList iterArgList
+%type <exprlist> initList namedInitializerList namedInitializerListAux
 %type <flist> structDeclList structDecl
 %type <srset> locModifies modList specClauseList optSpecClauseList
 %type <sr>    mExpr modListExpr specClauseListExpr
 
 /*drl*/
-%type <con>    BufConstraint
+%type <con> BufConstraint
 %type <tok> relationalOp
 %type <tok> BufBinaryOp
 %type <tok> bufferModifier
@@ -257,10 +276,15 @@ void yyerror (char *);
 %type <conE> BufConstraintTerm
 %type <sr> BufConstraintSrefExpr
 
-%type <conL>    BufConstraintList
+%type <conL> BufConstraintList
+
+%type <conL> optStructInvariant
 
 %type <tok>  BufUnaryOp
 
+/*drl 1/6/2002 either /\ or && */
+%type <tok> constraintSeperator
+
 %type <enumnamelist> enumeratorList 
 %type <cstringlist> fieldDesignator
 
@@ -283,13 +307,15 @@ void yyerror (char *);
 %type <expr> compoundStmt compoundStmtAux compoundStmtRest compoundStmtAuxErr
 %type <expr> expressionStmt selectionStmt iterationStmt jumpStmt iterDefIterationStmt 
 %type <expr> stmtErr stmtListErr compoundStmtErr expressionStmtErr 
-%type <expr> iterationStmtErr initializerList initializer ifPred whilePred forPred iterWhilePred
+%type <expr> iterationStmtErr initializerList typeInitializerList initializer
+%type <expr> ifPred whilePred forPred iterWhilePred typeInitializer
+
+%type <expr> designator designatorList designation
 
 %type <typequal> storageSpecifier typeQualifier typeModifier globQual
 %type <tquallist> optGlobQuals
 %type <qtyp> completeType completeTypeSpecifier optCompleteType
 %type <qtyp> completeTypeSpecifierAux altType typeExpression 
-/*%type <expr> lclintassertion*/
 
 %start file
 
@@ -300,8 +326,8 @@ file
  | externalDefs
 
 externalDefs
- : externalDef
- | externalDefs externalDef 
+ : externalDef { context_checkGlobalScope (); }
+ | externalDefs externalDef { context_checkGlobalScope (); }
 
 externalDef
  : fcnDef optSemi { uentry_clearDecl (); } 
@@ -310,6 +336,7 @@ externalDef
  | iterDecl       { uentry_clearDecl (); } 
  | macroDef       { uentry_clearDecl (); } 
  | initializer    { uentry_checkDecl (); exprNode_free ($1); }
+ | TSEMI          { uentry_clearDecl (); /* evans 2002-02-08: okay to have a null statement */ }  
  | error          { uentry_clearDecl (); } 
 
 constantDecl
@@ -345,27 +372,38 @@ namedDeclBase
  | IsType TLPAREN NotType namedDecl IsType TRPAREN
    { $$ = idDecl_expectFunction ($4); }
  | namedDeclBase TLSQBR TRSQBR 
-   { $$ = idDecl_replaceCtype ($1, ctype_makeArray (idDecl_getCtype ($1))); }
+   { $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); }
  | namedDeclBase TLSQBR IsType constantExpr TRSQBR NotType
-   { 
-     $$ = idDecl_replaceCtype ($1, ctype_makeFixedArray (idDecl_getCtype ($1), exprNode_getLongValue ($4)));
+   {
+     exprNode_findValue ($4);
+     idDecl_notExpectingFunction ($1);
+
+     if (exprNode_hasValue ($4)) 
+       {
+        $$ = idDecl_replaceCtype ($1, ctype_makeInnerFixedArray (idDecl_getCtype ($1), 
+                                                                 exprNode_getLongValue ($4)));
+       } 
+     else
+       {
+        $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); 
+       }
    }
  | namedDeclBase PushType TLPAREN TRPAREN 
    { setCurrentParams (uentryList_missingParams); }
    functionClauses
-   optGlobBufConstraints
    { /* need to support globals and modifies here! */
      ctype ct = ctype_makeFunction (idDecl_getCtype ($1), 
                                    uentryList_makeMissingParams ());
      
      $$ = idDecl_replaceCtype ($1, ct);
      idDecl_addClauses ($$, $6);
-     context_popLoc (); 
+     context_popLoc ();
+     /*drl 7/25/01 added*/
+     setImplictfcnConstraints();
    }
  | namedDeclBase PushType TLPAREN genericParamList TRPAREN 
    { setCurrentParams ($4); } 
    functionClauses
-   optGlobBufConstraints
    { setImplictfcnConstraints ();
      clearCurrentParams ();
      $$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4));
@@ -378,7 +416,7 @@ plainNamedDeclBase
  | IsType TLPAREN NotType plainNamedDecl IsType TRPAREN
    { $$ = idDecl_expectFunction ($4); }
  | plainNamedDeclBase TLSQBR TRSQBR 
-   { $$ = idDecl_replaceCtype ($1, ctype_makeArray (idDecl_getCtype ($1))); }
+   { $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); }
  | plainNamedDeclBase TLSQBR IsType constantExpr TRSQBR NotType
    { 
      int value;
@@ -393,7 +431,7 @@ plainNamedDeclBase
         value = 0;
        }
 
-     $$ = idDecl_replaceCtype ($1, ctype_makeFixedArray (idDecl_getCtype ($1), value));
+     $$ = idDecl_replaceCtype ($1, ctype_makeInnerFixedArray (idDecl_getCtype ($1), value));
    }
  | plainNamedDeclBase PushType TLPAREN TRPAREN 
    { setCurrentParams (uentryList_missingParams); }
@@ -429,52 +467,36 @@ macroDef
  | LLMACRO TENDMACRO /* no stmt */ { exprChecks_checkEmptyMacroBody (); } 
 
 fcnDefHdr
-  : fcnDefHdrAux { clabstract_declareFunction ($1); }
-
-/*drl*/
+ : fcnDefHdrAux { clabstract_declareFunction ($1); }
 
-optGlobBufConstraints
- : { setProcessingGlobMods (); } optGlobBufConstraintsRest
-   { clearProcessingGlobMods (); }
+metaStateConstraint
+ : metaStateSpecifier TASSIGN metaStateExpression 
+   { $$ = metaStateConstraint_create ($1, $3); }
 
-optGlobBufConstraintsRest
- : optGlobBufConstraintsAux optGlobEnsuresConstraintsAux
+metaStateSpecifier
+  : BufConstraintSrefExpr { cscanner_expectingMetaStateName (); } TCOLON metaStateName
+    { cscanner_clearExpectingMetaStateName ();
+      $$ = metaStateSpecifier_create ($1, $4); }
+  | CTOK_ELIPSIS { cscanner_expectingMetaStateName (); } TCOLON metaStateName
+    { cscanner_clearExpectingMetaStateName ();
+      $$ = metaStateSpecifier_createElipsis ($4); }
 
+metaStateExpression
+: metaStateSpecifier { $$ = metaStateExpression_create ($1); }
+| metaStateSpecifier TBAR metaStateExpression { $$ = metaStateExpression_createMerge ($1, $3); }
 
-optGlobEnsuresConstraintsAux
-: {
-  DPRINTF ( ("doing optGlobEnsuresConstraintsAux\n") );
-context_setProtectVars (); enterParamsTemp (); 
-     sRef_setGlobalScopeSafe (); 
-
-}  QENSURESCONSTRAINT BufConstraintList optSemi QENDMACRO
-{
-  setEnsuresConstraints ($3);
-  exitParamsTemp ();
-     sRef_clearGlobalScopeSafe (); 
-     context_releaseVars ();
-  DPRINTF (("done optGlobBufConstraintsAux\n"));}
- | /*empty*/
-
+metaStateName
+: METASTATE_NAME
 
-optGlobBufConstraintsAux
-: {
-  DPRINTF ( ("doing optGlobBufConstraintsAux\n") );
-context_setProtectVars (); enterParamsTemp (); 
-     sRef_setGlobalScopeSafe (); 
+/*drl*/
 
-}  QBUFFERCONSTRAINT BufConstraintList optSemi QENDMACRO
-{
-  setFunctionConstraints ($3);
-  exitParamsTemp ();
-     sRef_clearGlobalScopeSafe (); 
-     context_releaseVars ();
-  DPRINTF (("done optGlobBufConstraintsAux\n"));}
- | /*empty*/
+constraintSeperator
+: TCAND
+| AND_OP
 
 BufConstraintList
-: BufConstraint TCAND BufConstraintList { $$ = constraintList_add ($3, $1); }
-| BufConstraint {constraintList c; c = constraintList_makeNew(); c = constraintList_add (c, $1); $$ = c}
+: BufConstraint constraintSeperator BufConstraintList { $$ = constraintList_add ($3, $1); }
+| BufConstraint { $$ = constraintList_single ($1); } 
 
 BufConstraint
 :  BufConstraintExpr relationalOp BufConstraintExpr {
@@ -483,7 +505,7 @@ BufConstraint
 
 bufferModifier
  : QMAXSET
- |QMAXREAD
+ | QMAXREAD
 
 relationalOp
  : GE_OP
@@ -498,32 +520,33 @@ BufConstraintExpr
    $$ = constraintExpr_parseMakeBinaryOp ($2, $3, $4); }
 
 BufConstraintTerm
-: BufConstraintSrefExpr { $$ =  constraintExpr_makeTermsRef($1);} 
- | CCONSTANT {  char *t; int c;
-  t =  cstring_toCharsSafe (exprNode_unparse($1));
-  c = atoi( t );
-  $$ = constraintExpr_makeIntLiteral (c);
-}
-
+ : BufConstraintSrefExpr { $$ =  constraintExpr_makeTermsRef ($1);} 
+ | CCONSTANT { $$ = constraintExpr_makeIntLiteral (exprNode_getLongValue ($1)); }
 
 BufConstraintSrefExpr
-: id                              {
-   $$ =
-     checkbufferConstraintClausesId ($1);}
- | NEW_IDENTIFIER                  { $$ = fixStateClausesId ($1); }
-
- | BufConstraintSrefExpr TLSQBR TRSQBR       { $$ = sRef_makeAnyArrayFetch ($1); }
- |  BufConstraintSrefExpr  TLSQBR CCONSTANT TRSQBR {
-     char *t; int c;
-  t =  cstring_toCharsSafe (exprNode_unparse($3));
-  c = atoi( t );
-   $$ = sRef_makeArrayFetchKnown($1, c); }
- | TMULT  BufConstraintSrefExpr               { $$ = sRef_constructPointer ($2); }
- | TLPAREN BufConstraintSrefExpr TRPAREN     { $$ = $2; }  
- |  BufConstraintSrefExpr TDOT newId          { cstring_markOwned ($3);
-                                           $$ = sRef_buildField ($1, $3); }
- |  BufConstraintSrefExpr ARROW_OP newId      { cstring_markOwned ($3);
-                                            $$ = sRef_makeArrow ($1, $3); }
+: id            
+  { /*@-onlytrans@*/ $$ = checkbufferConstraintClausesId ($1); /*@=onlytrans@*/ /*@i523@*/ }
+| NEW_IDENTIFIER                   
+  { $$ = fixStateClausesId ($1); }
+| BufConstraintSrefExpr TLSQBR TRSQBR       
+  { $$ = sRef_makeAnyArrayFetch ($1); }
+| BufConstraintSrefExpr  TLSQBR CCONSTANT TRSQBR 
+  {
+    /*
+    char *t; int c; 
+    t =  cstring_toCharsSafe (exprNode_unparse($3)); 
+    c = atoi( t );
+    */
+    $$ = sRef_makeArrayFetchKnown ($1, exprNode_getLongValue ($3));
+  }
+| TMULT  BufConstraintSrefExpr               
+  { $$ = sRef_constructPointer ($2); }
+| TLPAREN BufConstraintSrefExpr TRPAREN     
+  { $$ = $2; }  
+| BufConstraintSrefExpr TDOT newId          
+  { cstring_markOwned ($3); $$ = sRef_buildField ($1, $3); }
+| BufConstraintSrefExpr ARROW_OP newId      
+  { cstring_markOwned ($3); $$ = sRef_makeArrow ($1, $3); }
 
 /*
 | BufConstraintTerm TLSQBR TRSQBR       { $$ = sRef_makeAnyArrayFetch ($1); }
@@ -569,7 +592,7 @@ functionClause
  | modifiesClause  { $$ = functionClause_createModifies ($1); }
  | nomodsClause    { $$ = functionClause_createModifies ($1); }
  | stateClause     { $$ = functionClause_createState ($1); }  
- | conditionClause { $$ = functionClause_createState ($1); }
+ | conditionClause { $$ = $1; }
  | warnClause      { $$ = functionClause_createWarn ($1); }
 
 functionClausePlain
@@ -577,7 +600,7 @@ functionClausePlain
  | modifiesClausePlain  { $$ = functionClause_createModifies ($1); }
  | nomodsClause         { $$ = functionClause_createModifies ($1); }
  | stateClausePlain     { $$ = functionClause_createState ($1); }  
- | conditionClausePlain { $$ = functionClause_createState ($1); }
+ | conditionClausePlain { $$ = $1; }
  | warnClausePlain      { $$ = functionClause_createWarn ($1); }
 
 globalsClause
@@ -620,14 +643,22 @@ flagSpec
 flagId
  : NEW_IDENTIFIER
 
+optWarnClause
+ : warnClause
+ | /* empty */ { $$ = warnClause_undefined; }
+
 warnClause
  : warnClausePlain QENDMACRO { $$ = $1; }
 
 warnClausePlain
  : QWARN flagSpec cconstantExpr
-   { $$ = warnClause_create ($1, $2, $3); }
+   {      
+     llassert (exprNode_knownStringValue ($3));
+     $$ = warnClause_create ($1, $2, cstring_copy (multiVal_forceString (exprNode_getValue ($3)))); 
+     exprNode_free ($3);
+   }
  | QWARN flagSpec
-   { $$ = warnClause_create ($1, $2, exprNode_undefined); }
+   { $$ = warnClause_create ($1, $2, cstring_undefined); }
 
 globIdList
  : globIdListExpr                     { $$ = globSet_single ($1); }
@@ -680,20 +711,20 @@ fcnBody
      exprNode_checkFunctionBody ($3); $$ = $3; 
      context_exitInner ($3); 
    }
- | initializerList 
-   { doneParams (); context_enterInnerContext (); }
+ | { context_enterOldStyleScope (); } initializerList 
+   { oldStyleDoneParams (); context_enterInnerContext (); } 
    compoundStmt 
    {
-     context_exitInner ($3);
-     exprNode_checkFunctionBody ($3); 
-     $$ = $3; /* old style */ 
+     exprNode_checkFunctionBody ($4); 
+     $$ = $4; /* oldstyle */ 
+     context_exitInner ($4);
    } 
  
 fcnDef
  : fcnDefHdr fcnBody 
    { 
      context_setFunctionDefined (exprNode_loc ($2)); 
-     exprNode_checkFunction (context_getHeader (), $2); 
+     exprNode_checkFunction (context_getHeader (),  $2); 
      /* DRL 8 8 2000 */
      
      context_exitFunction ();
@@ -764,6 +795,9 @@ primaryExpr
  | TLPAREN expr TRPAREN { $$ = exprNode_addParens ($1, $2); }
  | TYPE_NAME_OR_ID { $$ = exprNode_fromIdentifier (coerceId ($1)); } 
  | QEXTENSION { $$ = exprNode_makeError (); }
+ | TLPAREN { exprChecks_inCompoundStatementExpression (); } 
+   compoundStmt TRPAREN 
+   { exprChecks_leaveCompoundStatementExpression (); $$ = exprNode_compoundStatementExpression ($1, $3); }
  
 postfixExpr
  : primaryExpr 
@@ -775,7 +809,9 @@ postfixExpr
  | postfixExpr NotType ARROW_OP newId IsType { $$ = exprNode_arrowAccess ($1, $3, $4); }
  | postfixExpr INC_OP { $$ = exprNode_postOp ($1, $2); }
  | postfixExpr DEC_OP { $$ = exprNode_postOp ($1, $2); }
+ | TLPAREN typeExpression TRPAREN TLBRACE typeInitializerList optComma TRBRACE 
+   { /* added for C99 */ $$ = exprNode_undefined; /*@i87 no checking */ }
+
 argumentExprList
  : assignExpr { $$ = exprNodeList_singleton ($1); }
  | argumentExprList TCOMMA assignExpr { $$ = exprNodeList_push ($1, $3); }
@@ -964,7 +1000,8 @@ namedInitializer
 
 typeDecl
  : CTYPEDEF completeTypeSpecifier { setProcessingTypedef ($2); } 
-   NotType namedInitializerList IsType TSEMI { unsetProcessingTypedef (); } 
+   NotType namedInitializerList IsType optWarnClause TSEMI 
+   { clabstract_declareType ($5, $7); }
  | CTYPEDEF completeTypeSpecifier IsType TSEMI { /* in the ANSI grammar, semantics unclear */ }
  | CTYPEDEF namedInitializerList IsType TSEMI { /* in the ANSI grammar, semantics unclear */ } 
 
@@ -975,11 +1012,11 @@ PushType
  : { g_expectingTypeName = TRUE; context_pushLoc (); }
 
 namedInitializerList
- :  namedInitializerListAux IsType { ; }
+ :  namedInitializerListAux IsType { $$ = $1; }
 
 namedInitializerListAux
- : namedInitializer { ; }
- | namedInitializerList TCOMMA NotType namedInitializer { ; }
+ : namedInitializer { $$ = exprNodeList_singleton ($1); }
+ | namedInitializerList TCOMMA NotType namedInitializer { $$ = exprNodeList_push ($1, $4); }
 
 optDeclarators
  : /* empty */      { $$ = exprNode_makeError (); }
@@ -989,7 +1026,24 @@ init
  : assignExpr                      
  | TLBRACE initList TRBRACE        { $$ = exprNode_makeInitBlock ($1, $2); }
  | TLBRACE initList TCOMMA TRBRACE { $$ = exprNode_makeInitBlock ($1, $2); }
+ | designation init                { $$ = exprNode_undefined; }
 
+/*
+** Splint parses these (added in ISO C99), but no checking yet...
+*/
+
+designation
+ : designatorList TASSIGN          { $$ = $1; }
+ | newId TCOLON                    { $$ = exprNode_undefined; 
+                                     /* gcc extension, obsolete since 2.5 */ }
+
+designatorList
+ : designator                      { $$ = exprNode_undefined; } 
+ | designatorList designator       { $$ = exprNode_undefined; }
+
+designator
+ : TLSQBR constantExpr TRSQBR      { $$ = exprNode_undefined; }
+ | TDOT newId                      { $$ = exprNode_undefined; }
 
 initList
  : init 
@@ -1009,9 +1063,6 @@ storageSpecifier
  | QAUTO     { $$ = qual_createAuto (); }
  | QREGISTER { $$ = qual_createRegister (); }
 
-nullterminatedQualifier:
- QNULLTERMINATED IsType { $$ = qual_createNullTerminated (); }
-
 stateClause
  : stateClausePlain QENDMACRO { $$ = $1; }
 
@@ -1033,8 +1084,11 @@ stateClausePlain
 conditionClause
  : conditionClausePlain QENDMACRO { $$ = $1; }
 
+startConditionClause
+: conditionTag NotType { $$ = $1; context_enterFunctionHeader (); } 
+
 conditionClausePlain
- : conditionTag { context_enterFunctionHeader (); } NotType stateQualifier
+ : startConditionClause stateQualifier
    {
      context_exitFunctionHeader ();
      context_setProtectVars (); 
@@ -1046,8 +1100,41 @@ conditionClausePlain
      exitParamsTemp ();
      sRef_clearGlobalScopeSafe (); 
      context_releaseVars ();
-     $$ = stateClause_create ($1, $4, $6);
+     $$ = functionClause_createState (stateClause_create ($1, $2, $4));
    }
+ | startConditionClause
+   {
+     context_setProtectVars (); 
+     enterParamsTemp (); 
+     sRef_setGlobalScopeSafe (); 
+   } 
+   functionConstraint optSemi IsType
+   {
+     context_exitFunctionHeader ();
+     exitParamsTemp ();
+     sRef_clearGlobalScopeSafe (); 
+     context_releaseVars ();
+     DPRINTF (("done optGlobBufConstraintsAux\n"));
+
+     if (lltok_isEnsures ($1)) 
+       {
+        $$ = functionClause_createEnsures ($3);
+       }
+     else if (lltok_isRequires ($1))
+       {
+        $$ = functionClause_createRequires ($3);
+       }
+     else
+       {
+        BADBRANCH;
+       }
+
+     DPRINTF (("FunctionclauseS: %s", functionClause_unparse ($$)));
+   }
+
+functionConstraint
+ : BufConstraintList   { $$ = functionConstraint_createBufferConstraint ($1); }
+ | metaStateConstraint { $$ = functionConstraint_createMetaStateConstraint ($1); DPRINTF (("Made constraint: %s", functionConstraint_unparse ($$))); } 
  
 exitsQualifier
  : QEXITS        { $$ = qual_createExits (); }
@@ -1078,8 +1165,10 @@ stateQualifier
  | QNOTNULL      { $$ = qual_createNotNull (); }
  | QEXPOSED      { $$ = qual_createExposed (); }
  | QOBSERVER     { $$ = qual_createObserver (); }
+ | QNULLTERMINATED { $$ = qual_createNullTerminated (); } 
  | CANNOTATION   { $$ = qual_createMetaState ($1); }
 
+
 paramQualifier
  : QRETURNED     { $$ = qual_createReturned (); }
  | QSEF          { $$ = qual_createSef (); }
@@ -1174,12 +1263,20 @@ optCompleteType
  : /* empty */                             { $$ = qtype_unknown (); }
  | completeTypeSpecifier                   { $$ = $1; }
 
+
+optStructInvariant
+: /* empty */ { $$ = constraintList_undefined; }
+/* don't want to have support for structure invariant until we're
+   sure it's stable
+   |  QINVARIANT BufConstraintList QENDMACRO { $$ = $2 }
+*/
+
 suSpc
  : NotType CSTRUCT newId IsType TLBRACE { sRef_setGlobalScopeSafe (); } 
    CreateStructInnerScope 
-   structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
+   structDeclList  DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
    TRBRACE 
-   { $$ = declareStruct ($3, $8); }
+   optStructInvariant { {ctype ct; ct = declareStruct ($3, $8); /* setGlobalStructInfo(ct, $12);*/ $$ = ct;} } 
  | NotType CUNION  newId IsType TLBRACE { sRef_setGlobalScopeSafe (); } 
    CreateStructInnerScope 
    structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); } 
@@ -1195,8 +1292,8 @@ suSpc
    TRBRACE 
    { $$ = declareUnnamedStruct ($7); }
  | NotType CUNION IsType TLBRACE { sRef_setGlobalScopeSafe (); } 
-   CreateStructInnerScope 
-   structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
+   CreateStructInnerScope structDeclList DeleteStructInnerScope 
+   { sRef_clearGlobalScopeSafe (); }
    TRBRACE 
    { $$ = declareUnnamedUnion ($7); } 
  | NotType CSTRUCT IsType TLBRACE TRBRACE
@@ -1359,9 +1456,9 @@ abstractDeclBase
  | TLSQBR TRSQBR { $$ = ctype_makeArray (ctype_unknown); }
  | TLSQBR constantExpr TRSQBR 
    { $$ = ctype_makeFixedArray (ctype_unknown, exprNode_getLongValue ($2)); }
- | abstractDeclBase TLSQBR TRSQBR { $$ = ctype_makeArray ($1); }
+ | abstractDeclBase TLSQBR TRSQBR { $$ = ctype_makeInnerArray ($1); }
  | abstractDeclBase TLSQBR constantExpr TRSQBR 
-   { $$ = ctype_makeFixedArray ($1, exprNode_getLongValue ($3)); }
+   { $$ = ctype_makeInnerFixedArray ($1, exprNode_getLongValue ($3)); }
  | IsType TLPAREN TRPAREN 
    { $$ = ctype_makeFunction (ctype_unknown, uentryList_makeMissingParams ()); }
  | IsType TLPAREN paramTypeList TRPAREN 
@@ -1383,18 +1480,7 @@ stmt
  | iterationStmt 
  | iterStmt
  | jumpStmt 
-/* | lclintassertion {$$ = $1; printf ("Doing stmt lclintassertion\n"); }*/
-
-/*
-lclintassertion
- : QSETBUFFERSIZE id CCONSTANT QENDMACRO { printf(" QSETBUFFERSIZE id CCONSTANT HEllo World\n");  uentry_setBufferSize($2, $3); $$ = exprNode_createTok ($4);
-  }
- | QSETSTRINGLENGTH id CCONSTANT QENDMACRO { printf(" QSETSTRINGLENGTH id CCONSTANT HEllo World\n");  uentry_setStringLength($2, $3); $$ = exprNode_createTok ($4);
-  }
- | QTESTINRANGE id CCONSTANT QENDMACRO {printf(" QTESTINRANGE\n");  uentry_testInRange($2, $3); $$ = exprNode_createTok ($4);
-  }
 
-/* | QSETBUFFERSIZE id id  {$$ = $2; printf(" QSETBUFFERSIZE id id HEllo World\n");} */
 
 iterBody
  : iterDefStmtList { $$ = $1; }
@@ -1447,9 +1533,9 @@ iterDefStmt
  | error { $$ = exprNode_makeError (); }
 
 iterSelectionStmt
- : ifPred iterDefStmt 
+ : ifPred { exprNode_checkIfPred ($1); } iterDefStmt 
    { /* don't: context_exitTrueClause ($1, $2); */
-     $$ = exprNode_if ($1, $2); 
+     $$ = exprNode_if ($1, $3); 
    }
 
 openScope
@@ -1479,20 +1565,28 @@ labeledStmt
  : newId TCOLON      { $$ = exprNode_labelMarker ($1); }
  | QNOTREACHED stmt  { $$ = exprNode_notReached ($2); }
 
+/*
+** We allow more than one QFALLTHROUGH token to support mixed lint/splint markers.
+*/
+
+optExtraFallThroughs
+ : /* empty */ { ; }
+ | QFALLTHROUGH optExtraFallThroughs { ; }
+
 /* Note that we can semantically check that the object to the case is
  indeed constant. In this case, we may not want to go through this effort */
 
 caseStmt
  : CASE constantExpr { context_enterCaseClause ($2); } 
    TCOLON            { $$ = exprNode_caseMarker ($2, FALSE); }
- | QFALLTHROUGH CASE constantExpr { context_enterCaseClause ($3); } 
-   TCOLON            { $$ = exprNode_caseMarker ($3, TRUE); }
+ | QFALLTHROUGH optExtraFallThroughs CASE constantExpr { context_enterCaseClause ($4); } 
+   TCOLON            { $$ = exprNode_caseMarker ($4, TRUE); }
 
 defaultStmt
  : DEFAULT { context_enterCaseClause (exprNode_undefined); } 
    TCOLON { $$ = exprNode_defaultMarker ($1, FALSE); }
- | QFALLTHROUGH DEFAULT { context_enterCaseClause (exprNode_undefined); } 
-   TCOLON { $$ = exprNode_defaultMarker ($2, TRUE); }
+ | QFALLTHROUGH optExtraFallThroughs DEFAULT { context_enterCaseClause (exprNode_undefined); } 
+   TCOLON { $$ = exprNode_defaultMarker ($3, TRUE); }
 
 compoundStmt
  : TLPAREN compoundStmt TRPAREN { $$ = $2; }
@@ -1533,7 +1627,6 @@ compoundStmtRest
                                                        lltok_getLoc ($3))); 
    }
 
-
 compoundStmtAux
  : TLBRACE compoundStmtRest 
    { $$ = exprNode_makeBlock ($2); }
@@ -1556,6 +1649,14 @@ initializerList
  : initializer { $$ = $1; }
  | initializerList initializer { $$ = exprNode_concat ($1, $2); }
 
+typeInitializerList
+ : typeInitializer { $$ = $1; }
+ | typeInitializerList TCOMMA typeInitializer { $$ = exprNode_concat ($1, $3); }
+
+typeInitializer
+ : assignExpr { $$ = $1; }
+ | TLBRACE typeInitializerList optComma TRBRACE { $$ = $2; } 
+
 stmtList
  : stmt { $$ = $1; }
  | stmtList stmt { $$ = exprNode_concat ($1, $2); }
@@ -1571,7 +1672,12 @@ expressionStmtErr
 
 ifPred
  : CIF TLPAREN expr TRPAREN 
-   { $$ = $3; exprNode_produceGuards ($3); context_enterTrueClause ($3); }
+   { 
+     exprNode_produceGuards ($3); context_enterTrueClause ($3); 
+     exprNode_checkIfPred ($3);
+     $$ = $3;
+   }
+
  /*
  ** not ANSI: | CIF TLPAREN compoundStmt TRPAREN 
  **             { $$ = $3; context_enterTrueClause (); } 
@@ -1583,7 +1689,7 @@ selectionStmt
      context_exitTrueClause ($1, $2);
      $$ = exprNode_if ($1, $2); 
    }
- | ifPred stmt CELSE { context_enterFalseClause ($1); } stmt 
+ | ifPred stmt CELSE  { context_enterFalseClause ($1); } stmt 
    {
      context_exitClause ($1, $2, $5);
      $$ = exprNode_ifelse ($1, $2, $5); 
@@ -1779,6 +1885,10 @@ optSemi
  : 
  | TSEMI { ; } 
 
+optComma
+ : 
+ | TCOMMA { ; } 
+
 id
  : IDENTIFIER 
 
@@ -1792,12 +1902,14 @@ newId
 typeName
  : TYPE_NAME
  | TYPE_NAME_OR_ID { $$ = ctype_unknown; }
+ | CTYPEOF TLPAREN expr TRPAREN { $$ = exprNode_getType ($3); exprNode_free ($3); }
+ | CTYPEOF TLPAREN typeExpression TRPAREN { $$ = qtype_getType ($3); } 
 
 %%
 
-/*@-redecl@*/
+/*@-redecl@*/ /*@-namechecks@*/
 extern char *yytext;
-/*@=redecl@*/
+/*@=redecl@*/ /*@=namechecks@*/
 
 # include "bison.reset"
 
@@ -1820,7 +1932,7 @@ void yyerror (/*@unused@*/ char *s)
       llerror (FLG_SYNTAX, message ("Macro syntax not parseable: %s", 
                                    context_inFunctionName ()));
       
-      if (context_inMacroUnknown ())
+      if (context_inUnknownMacro ())
        {
          if (!givehint)
            {
This page took 2.858879 seconds and 4 git commands to generate.