/*;-*-C-*-;
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "splintMacros.nf"
# include "basic.h"
# include "cscanner.h"
+# include "cscannerHelp.h"
# include "cgrammar.h"
# include "exprChecks.h"
/* additional tokens introduced by splint pre-processor. */
%token <tok> LLMACRO LLMACROITER LLMACROEND TENDMACRO
+/* For debugging purposes */
+%token <tok> QDREVEALSTATE
+
/* break comments: */
%token <tok> QSWITCHBREAK QLOOPBREAK QINNERBREAK QSAFEBREAK
%token <tok> QINNERCONTINUE
%token <tok> QRETURNED QEXPOSED QNULL QOBSERVER QISNULL
%token <tok> QEXITS QMAYEXIT QNEVEREXIT QTRUEEXIT QFALSEEXIT
%token <tok> QLONG QSIGNED QUNSIGNED QSHORT QUNUSED QSEF QNOTNULL QRELNULL
-%token <tok> QABSTRACT QCONCRETE QMUTABLE QIMMUTABLE
+%token <tok> QABSTRACT QNUMABSTRACT QCONCRETE QMUTABLE QIMMUTABLE
%token <tok> QTRUENULL QFALSENULL QEXTERNAL
%token <tok> QREFCOUNTED QREFS QNEWREF QTEMPREF QKILLREF QRELDEF
%token <ctyp> CGCHAR CBOOL CINT CGFLOAT CDOUBLE CVOID
%type <entry> endIter
%type <funcclauselist> functionClauses functionClausesPlain
-%type <funcclause> functionClause functionClause functionClausePlain
+%type <funcclause> functionClause functionClausePlain
%type <globsclause> globalsClause globalsClausePlain
%type <modsclause> modifiesClause modifiesClausePlain nomodsClause
%type <entrylist> genericParamList paramTypeList paramList idList paramIdList
%type <exprlist> argumentExprList iterArgList
-%type <exprlist> initList namedInitializerList namedInitializerListAux
+%type <exprlist> initList namedInitializerList namedInitializerListAux namedInitializerTypeList namedInitializerTypeListAux
%type <flist> structDeclList structDecl
%type <srset> locModifies modList specClauseList optSpecClauseList
%type <sr> mExpr modListExpr specClauseListExpr
%type <expr> sizeofExpr sizeofExprAux offsetofExpr
%type <expr> openScope closeScope
-%type <expr> instanceDecl namedInitializer optDeclarators
+%type <expr> instanceDecl namedInitializer optDeclarators namedInitializerType
%type <expr> primaryExpr postfixExpr primaryIterExpr postfixIterExpr
%type <expr> unaryExpr castExpr timesExpr plusExpr
%type <expr> unaryIterExpr castIterExpr timesIterExpr plusIterExpr
%type <expr> orIterExpr conditionalIterExpr assignIterExpr iterArgExpr
%type <expr> expr optExpr constantExpr
%type <expr> init macroBody iterBody endBody partialIterStmt iterSelectionStmt
-%type <expr> stmt stmtList fcnBody iterStmt iterDefStmt iterDefStmtList
+%type <expr> stmt stmtList fcnBody iterStmt iterDefStmt iterDefStmtList debugStmt
%type <expr> labeledStmt caseStmt defaultStmt
%type <expr> compoundStmt compoundStmtAux compoundStmtRest compoundStmtAuxErr
%type <expr> expressionStmt selectionStmt iterationStmt jumpStmt iterDefIterationStmt
{ setCurrentParams (uentryList_missingParams); }
functionClauses
{ /* need to support globals and modifies here! */
+ functionClauseList fcl;
ctype ct = ctype_makeFunction (idDecl_getCtype ($1),
uentryList_makeMissingParams ());
$$ = idDecl_replaceCtype ($1, ct);
/*drl 7/25/01 added*/
- setImplictfcnConstraints();
+ setImplicitfcnConstraints();
+
+ DPRINTF((message("namedDeclBase PushType TLPAREN TRPAREN...:\n adding implict constraints to functionClause List: %s",
+ functionClauseList_unparse($6)
+ )
+ ));
+
+ fcl = functionClauseList_setImplicitConstraints($6);
- /* functionClauseList_ImplictConstraints($6); */
+ idDecl_addClauses ($$, fcl);
- idDecl_addClauses ($$, $6);
+ DPRINTF((message("1 added fuctionClause List: %s to the Id",
+ functionClauseList_unparse(fcl)
+ )
+ ));
+
+
context_popLoc ();
lltok_free2 ($3, $4);
}
{ setCurrentParams ($4); }
functionClauses
{
- setImplictfcnConstraints ();
- /* functionClauseList_ImplictConstraints($7);*/
+ functionClauseList fcl;
+ setImplicitfcnConstraints ();
clearCurrentParams ();
$$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4));
- idDecl_addClauses ($$, $7);
+
+ DPRINTF((message("namedDeclBase PushType TLPAREN genericParamList TRPAREN...:\n adding implict constraints to functionClause List: %s",
+ functionClauseList_unparse($7)
+ )
+ )) ;
+
+ fcl = functionClauseList_setImplicitConstraints($7);
+
+ idDecl_addClauses ($$, fcl);
+
+ DPRINTF((message("added fuctionClause List: %s to the Id",
+ functionClauseList_unparse(fcl)
+ )
+ ));
+
+
context_popLoc ();
lltok_free2 ($3, $5);
}
;
metaStateSpecifier
- : BufConstraintSrefExpr { cscanner_expectingMetaStateName (); } TCOLON metaStateName
- { cscanner_clearExpectingMetaStateName ();
+ : BufConstraintSrefExpr { cscannerHelp_expectingMetaStateName (); } TCOLON metaStateName
+ { cscannerHelp_clearExpectingMetaStateName ();
$$ = metaStateSpecifier_create ($1, $4);
lltok_free ($3);
}
- | CTOK_ELIPSIS { cscanner_expectingMetaStateName (); } TCOLON metaStateName
- { cscanner_clearExpectingMetaStateName ();
+ | CTOK_ELIPSIS { cscannerHelp_expectingMetaStateName (); } TCOLON metaStateName
+ { cscannerHelp_clearExpectingMetaStateName ();
$$ = metaStateSpecifier_createElipsis ($4);
lltok_free2 ($1, $3);
}
;
optSpecClauseList
- : /* empty */ { $$ = sRefSet_undefined }
+ : /* empty */ { DPRINTF ((message("Empty optSpecClauseList") )); $$ = sRefSet_undefined }
| specClauseList
;
specClauseList
: specClauseListExpr
{ if (sRef_isValid ($1)) { $$ = sRefSet_single ($1); }
- else { $$ = sRefSet_undefined; }
+ else {
+ DPRINTF((message("returning sRefSEt_undefined ") ));
+ $$ = sRefSet_undefined; }
}
| specClauseList TCOMMA specClauseListExpr
{ if (sRef_isValid ($3))
| NEW_IDENTIFIER { $$ = exprNode_fromUIO ($1); }
| cconstantExpr
| TLPAREN expr TRPAREN { $$ = exprNode_addParens ($1, $2); }
- | TYPE_NAME_OR_ID { $$ = exprNode_fromIdentifier (coerceId ($1)); }
+ | TYPE_NAME_OR_ID { $$ = exprNode_fromIdentifier (cscannerHelp_coerceId ($1)); }
| QEXTENSION { $$ = exprNode_makeError (); }
| TLPAREN { exprChecks_inCompoundStatementExpression (); }
compoundStmt TRPAREN
| TMINUS castExpr { $$ = exprNode_preOp ($2, $1); }
| TTILDE castExpr { $$ = exprNode_preOp ($2, $1); }
| TEXCL castExpr { $$ = exprNode_preOp ($2, $1); }
- | sizeofExpr { $$ = $1; }
+ | processSizeof sizeofExpr endprocessSizeof { $$ = $2; }
| offsetofExpr { $$ = $1; }
;
sizeofExprAux { context_sizeofReleaseVars (); $$ = $3; }
;
+processSizeof: {context_enterSizeof()};
+
+
+endprocessSizeof: {context_leaveSizeof()};
+
+
sizeofExprAux
- : CSIZEOF TLPAREN typeExpression TRPAREN { $$ = exprNode_sizeofType ($3); lltok_free3 ($1, $2, $4); }
- | CSIZEOF unaryExpr { $$ = exprNode_sizeofExpr ($2); lltok_free ($1); }
+ : CSIZEOF TLPAREN typeExpression TRPAREN { $$ = exprNode_sizeofType ($3); lltok_free3 ($1, $2, $4); }
+ | CSIZEOF unaryExpr { $$ = exprNode_sizeofExpr ($2); lltok_free ($1); }
| CALIGNOF TLPAREN typeExpression TRPAREN { $$ = exprNode_alignofType ($3); lltok_free3 ($1, $2, $4); }
| CALIGNOF unaryExpr { $$ = exprNode_alignofExpr ($2); lltok_free ($1); }
;
-
+
+
+
castExpr
: unaryExpr
| TLPAREN typeExpression TRPAREN castExpr
conditionalExpr
: orExpr
+ | orExpr TQUEST
+ { /* GCC extension: conditional with empty if */
+ exprNode_produceGuards ($1); context_enterTrueClause ($1); } TCOLON
+ { context_enterFalseClause ($1); } conditionalExpr
+ { $$ = exprNode_condIfOmit ($1, $6); context_exitClause ($1, exprNode_undefined, $6); }
| orExpr TQUEST { exprNode_produceGuards ($1); context_enterTrueClause ($1); } expr TCOLON
{ context_enterFalseClause ($1); } conditionalExpr
{ $$ = exprNode_cond ($1, $4, $7); context_exitClause ($1, $4, $7); }
}
;
+namedInitializerType
+ : namedInitializer { $$ = $1; }
+ | TYPE_NAME { $$ = exprNode_fromIdentifier (usymtab_getTypeEntry (ctype_typeId ($1))); }
+;
+
namedInitializer
: namedDecl NotType
{
typeDecl
: CTYPEDEF completeTypeSpecifier { setProcessingTypedef ($2); }
- NotType namedInitializerList IsType optWarnClause TSEMI
+ NotType namedInitializerTypeList 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 */ }
;
IsType
- : { g_expectingTypeName = TRUE; }
+ : { cscannerHelp_setExpectingTypeName (); }
;
PushType
- : { g_expectingTypeName = TRUE; context_pushLoc (); }
+ : { cscannerHelp_setExpectingTypeName (); context_pushLoc (); }
;
namedInitializerList
| namedInitializerList TCOMMA NotType namedInitializer { $$ = exprNodeList_push ($1, $4); }
;
+namedInitializerTypeList
+ : namedInitializerTypeListAux IsType { $$ = $1; }
+;
+
+namedInitializerTypeListAux
+ : namedInitializerType { $$ = exprNodeList_singleton ($1); }
+ | namedInitializerTypeList TCOMMA NotType namedInitializerType { $$ = exprNodeList_push ($1, $4); }
+;
+
optDeclarators
: /* empty */ { $$ = exprNode_makeError (); }
| optDeclarators TCOMMA NotType namedInitializer { $$ = exprNode_concat ($1, $4); }
typedefQualifier
: QABSTRACT { $$ = qual_createAbstract (); }
+ | QNUMABSTRACT { $$ = qual_createNumAbstract (); }
| QCONCRETE { $$ = qual_createConcrete (); }
| QMUTABLE { $$ = qual_createMutable (); }
| QIMMUTABLE { $$ = qual_createImmutable (); }
structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
TRBRACE
optStructInvariant
- { ctype ct; ct = declareStruct ($3, $8); context_setGlobalStructInfo(ct, $12); $$ = ct; }
+ { ctype ct; ct = declareStruct ($3, $8); /* context_setGlobalStructInfo(ct, $12); */ $$ = ct; }
| NotType CUNION newId IsType TLBRACE { sRef_setGlobalScopeSafe (); }
CreateStructInnerScope
structDeclList DeleteStructInnerScope { sRef_clearGlobalScopeSafe (); }
;
NotType
- : { g_expectingTypeName = FALSE; }
+: { cscannerHelp_clearExpectingTypeName (); }
;
structDeclList
{
qtype qt = qtype_unknown ();
qtype_adjustPointers ($1, qt);
- $$ = idDecl_create (cstring_copy (cscanner_observeLastIdentifier ()), qt);
+ $$ = idDecl_create (cstring_copy (cscannerHelp_observeLastIdentifier ()), qt);
}
| pointers optNamedDecl
{ $$ = $2; qtype_adjustPointers ($1, idDecl_getTyp ($$)); }
| iterationStmt
| iterStmt
| jumpStmt
+ | debugStmt
;
+debugStmt
+ : QDREVEALSTATE TLPAREN expr TRPAREN { exprNode_revealState ($3); $$ = exprNode_undefined; }
+;
iterBody
: iterDefStmtList { $$ = $1; }
| iterationStmtErr
| TLPAREN stmtErr TRPAREN { $$ = exprNode_addParens ($1, $2); }
| jumpStmt
+ | debugStmt
| error { $$ = exprNode_makeError (); }
;
iterArgExpr
: assignIterExpr { $$ = exprNode_iterExpr ($1); }
| id { $$ = exprNode_iterId ($1); }
- | TYPE_NAME_OR_ID { uentry ue = coerceIterId ($1);
+ | TYPE_NAME_OR_ID { uentry ue = cscannerHelp_coerceIterId ($1);
if (uentry_isValid (ue))
{
}
else
{
- $$ = exprNode_iterNewId (cstring_copy (cscanner_observeLastIdentifier ()));
+ $$ = exprNode_iterNewId (cstring_copy (cscannerHelp_observeLastIdentifier ()));
}
}
| NEW_IDENTIFIER { $$ = exprNode_iterNewId ($1); }
conditionalIterExpr
: orIterExpr
+ | orExpr TQUEST { context_enterTrueClause ($1); }
+ TCOLON { context_enterFalseClause ($1); } conditionalExpr
+ { $$ = exprNode_condIfOmit ($1, $6); }
| orExpr TQUEST { context_enterTrueClause ($1); }
expr TCOLON { context_enterFalseClause ($1); } conditionalExpr
{ $$ = exprNode_cond ($1, $4, $7); }
}
}
- cscanner_swallowMacro ();
+ cscannerHelp_swallowMacro ();
context_exitAllClausesQuiet ();
}
else
andersk / splint.git / blobdiff