Fixed problem with loop guards in loop test effects. New test case

[splint.git] / src / cgrammar.y

diff --git a/src/cgrammar.y b/src/cgrammar.y
index eb78741b4536f67d33f004e4c7a5e6b0fa7b4664..5c4f2d8cebf4a6bb51313191a87637f1b7291de7 100644 (file)
--- a/src/cgrammar.y
+++ b/src/cgrammar.y
@@ -17,8 +17,8 @@
 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 ** MA 02111-1307, USA.
 **
-** For information on splint: splint@cs.virginia.edu
-** To report a bug: splint-bug@cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
 ** For more information: http://www.splint.org
 */
 %{
@@ -136,7 +136,7 @@ extern 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
@@ -156,7 +156,8 @@ extern 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
@@ -195,7 +196,6 @@ extern 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> QSETSTRINGLENGTH
@@ -278,8 +278,13 @@ extern void yyerror (char *);
 
 %type <conL> BufConstraintList
 
+%type <conL> optStructInvariant
+
 %type <tok>  BufUnaryOp
 
+/*drl 1/6/2002 either /\ or && */
+%type <tok> constraintSeperator
+
 %type <enumnamelist> enumeratorList 
 %type <cstringlist> fieldDesignator
 
@@ -302,7 +307,10 @@ extern 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
@@ -328,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
@@ -363,17 +372,20 @@ 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
    {
-     exprNode_findValue($4);
+     exprNode_findValue ($4);
+     idDecl_notExpectingFunction ($1);
+
      if (exprNode_hasValue ($4)) 
        {
-        $$ = idDecl_replaceCtype ($1, ctype_makeFixedArray (idDecl_getCtype ($1), exprNode_getLongValue ($4)));
+        $$ = idDecl_replaceCtype ($1, ctype_makeInnerFixedArray (idDecl_getCtype ($1), 
+                                                                 exprNode_getLongValue ($4)));
        } 
      else
        {
-        $$ = idDecl_replaceCtype ($1, ctype_makeArray (idDecl_getCtype ($1))); 
+        $$ = idDecl_replaceCtype ($1, ctype_makeInnerArray (idDecl_getCtype ($1))); 
        }
    }
  | namedDeclBase PushType TLPAREN TRPAREN 
@@ -404,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;
@@ -419,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); }
@@ -478,8 +490,12 @@ metaStateName
 
 /*drl*/
 
+constraintSeperator
+: TCAND
+| AND_OP
+
 BufConstraintList
-: BufConstraint TCAND BufConstraintList { $$ = constraintList_add ($3, $1); }
+: BufConstraint constraintSeperator BufConstraintList { $$ = constraintList_add ($3, $1); }
 | BufConstraint { $$ = constraintList_single ($1); } 
 
 BufConstraint
@@ -779,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 
@@ -790,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); }
@@ -1005,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 
@@ -1025,9 +1063,6 @@ storageSpecifier
  | QAUTO     { $$ = qual_createAuto (); }
  | QREGISTER { $$ = qual_createRegister (); }
 
-nullterminatedQualifier:
- QNULLTERMINATED IsType { $$ = qual_createNullTerminated (); }
-
 stateClause
  : stateClausePlain QENDMACRO { $$ = $1; }
 
@@ -1228,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 (); } 
@@ -1413,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 
@@ -1438,6 +1481,7 @@ stmt
  | iterStmt
  | jumpStmt 
 
+
 iterBody
  : iterDefStmtList { $$ = $1; }
 
@@ -1605,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); }
@@ -1833,6 +1885,10 @@ optSemi
  : 
  | TSEMI { ; } 
 
+optComma
+ : 
+ | TCOMMA { ; } 
+
 id
  : IDENTIFIER 
 
@@ -1846,6 +1902,8 @@ 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); } 
 
 %%