extern int yylex ();
extern void swallowMacro (void);
+extern void yyerror (char *);
# include "lclintMacros.nf"
# include "basic.h"
+# include "cscanner.h"
+# include "mtincludes.h"
# include "cgrammar.h"
# include "exprChecks.h"
/*@-matchfields@*/
# define SHOWCSYM FALSE
-void yyerror (char *);
/*
** This is necessary, or else when the bison-generated code #include's malloc.h,
qualList tquallist;
ctype ctyp;
/*@dependent@*/ sRef sr;
+ /*@only@*/ sRef osr;
/*@only@*/ functionClauseList funcclauselist;
/*@only@*/ functionClause funcclause;
/*@only@*/ warnClause warnclause;
/*@only@*/ stateClause stateclause;
+ /*@only@*/ metaStateConstraint msconstraint;
+ /*@only@*/ metaStateSpecifier msspec;
+ /*@only@*/ metaStateExpression msexpr;
+ /*@observer@*/ metaStateInfo msinfo;
+
/*@only@*/ sRefList srlist;
/*@only@*/ globSet globset;
/*@only@*/ qtype qtyp;
/*@only@*/ exprNodeList alist;
/*@only@*/ sRefSet srset;
/*@only@*/ cstringList cstringlist;
+
/*drl
added 1/19/2001
*/
%type <typequal> nullterminatedQualifier
%token <tok> QNULLTERMINATED
%token <tok> QSETBUFFERSIZE
-%token <tok> QBUFFERCONSTRAINT
-%token <tok> QENSURESCONSTRAINT
%token <tok> QSETSTRINGLENGTH
%token <tok> QMAXSET
%token <tok> QMAXREAD
%type <globsclause> globalsClause globalsClausePlain
%type <modsclause> modifiesClause modifiesClausePlain nomodsClause
%type <warnclause> warnClause warnClausePlain
-%type <stateclause> conditionClause conditionClausePlain
+%type <funcclause> conditionClause conditionClausePlain
%type <stateclause> stateClause stateClausePlain
+%type <msconstraint> metaStateConstraint
+%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
%type <sr> mExpr modListExpr specClauseListExpr
/*drl*/
-%type <con> BufConstraint
+%type <con> BufConstraint
%type <tok> relationalOp
%type <tok> BufBinaryOp
%type <tok> bufferModifier
| 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 ());
| namedDeclBase PushType TLPAREN genericParamList TRPAREN
{ setCurrentParams ($4); }
functionClauses
- optGlobBufConstraints
{ setImplictfcnConstraints ();
clearCurrentParams ();
$$ = idDecl_replaceCtype ($1, ctype_makeFunction (idDecl_getCtype ($1), $4));
| LLMACRO TENDMACRO /* no stmt */ { exprChecks_checkEmptyMacroBody (); }
fcnDefHdr
- : fcnDefHdrAux { clabstract_declareFunction ($1); }
+ : fcnDefHdrAux { clabstract_declareFunction ($1); }
-/*drl*/
+metaStateConstraint
+ : metaStateSpecifier TASSIGN metaStateExpression
+ { $$ = metaStateConstraint_create ($1, $3); }
-optGlobBufConstraints
- : { setProcessingGlobMods (); } optGlobBufConstraintsRest
- { clearProcessingGlobMods (); }
+metaStateSpecifier
+ : BufConstraintSrefExpr { cscanner_expectingMetaStateName (); } TCOLON metaStateName
+ { cscanner_clearExpectingMetaStateName ();
+ $$ = metaStateSpecifier_create ($1, $4); }
-optGlobBufConstraintsRest
- : optGlobBufConstraintsAux optGlobEnsuresConstraintsAux
+metaStateExpression
+: metaStateSpecifier { $$ = metaStateExpression_create ($1); }
+| metaStateSpecifier TBAR metaStateExpression { $$ = metaStateExpression_createMerge ($1, $3); }
+metaStateName
+: METASTATE_NAME
-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*/
-
-
-optGlobBufConstraintsAux
-: {
- DPRINTF ( ("doing optGlobBufConstraintsAux\n") );
-context_setProtectVars (); enterParamsTemp ();
- sRef_setGlobalScopeSafe ();
-
-} QBUFFERCONSTRAINT BufConstraintList optSemi QENDMACRO
-{
- setFunctionConstraints ($3);
- exitParamsTemp ();
- sRef_clearGlobalScopeSafe ();
- context_releaseVars ();
- DPRINTF (("done optGlobBufConstraintsAux\n"));}
- | /*empty*/
+/*drl*/
BufConstraintList
: BufConstraint TCAND BufConstraintList { $$ = constraintList_add ($3, $1); }
bufferModifier
: QMAXSET
- |QMAXREAD
+ | QMAXREAD
relationalOp
: GE_OP
$$ = 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
+ {
+ /* char *t; int c;
+ t = cstring_toCharsSafe (exprNode_unparse($1));
+ c = atoi( t );
+ */
+
+ $$ = 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); }
| modifiesClause { $$ = functionClause_createModifies ($1); }
| nomodsClause { $$ = functionClause_createModifies ($1); }
| stateClause { $$ = functionClause_createState ($1); }
- | conditionClause { $$ = functionClause_createState ($1); }
+ | conditionClause { $$ = $1; }
| warnClause { $$ = functionClause_createWarn ($1); }
functionClausePlain
| modifiesClausePlain { $$ = functionClause_createModifies ($1); }
| nomodsClause { $$ = functionClause_createModifies ($1); }
| stateClausePlain { $$ = functionClause_createState ($1); }
- | conditionClausePlain { $$ = functionClause_createState ($1); }
+ | conditionClausePlain { $$ = $1; }
| warnClausePlain { $$ = functionClause_createWarn ($1); }
globalsClause
conditionClause
: conditionClausePlain QENDMACRO { $$ = $1; }
+startConditionClause
+: conditionTag NotType { $$ = $1; context_enterFunctionHeader (); }
+
conditionClausePlain
- : conditionTag { context_enterFunctionHeader (); } NotType stateQualifier
+ : startConditionClause stateQualifier
{
context_exitFunctionHeader ();
context_setProtectVars ();
exitParamsTemp ();
sRef_clearGlobalScopeSafe ();
context_releaseVars ();
- $$ = stateClause_create ($1, $4, $6);
+ $$ = functionClause_createState (stateClause_create ($1, $2, $4));
+ }
+ | startConditionClause
+ {
+ context_setProtectVars ();
+ enterParamsTemp ();
+ sRef_setGlobalScopeSafe ();
+ }
+ BufConstraintList 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;
+ }
+ }
+ | startConditionClause
+ {
+ context_setProtectVars ();
+ enterParamsTemp ();
+ sRef_setGlobalScopeSafe ();
+ }
+ metaStateConstraint optSemi IsType
+ {
+ context_exitFunctionHeader ();
+ exitParamsTemp ();
+ sRef_clearGlobalScopeSafe ();
+ context_releaseVars ();
+ DPRINTF (("done optGlobBufConstraintsAux\n"));
+
+ if (lltok_isEnsures ($1))
+ {
+ $$ = functionClause_createMetaEnsures ($3);
+ }
+ else if (lltok_isRequires ($1))
+ {
+ $$ = functionClause_createMetaRequires ($3);
+ }
+ else
+ {
+ BADBRANCH;
+ }
}
exitsQualifier
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
%%
-/*@-redecl@*/
+/*@-redecl@*/ /*@-namechecks@*/
extern char *yytext;
-/*@=redecl@*/
+/*@=redecl@*/ /*@=namechecks@*/
# include "bison.reset"
andersk / splint.git / blobdiff