2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: splint@cs.virginia.edu
21 ** To report a bug: splint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
27 ** Grammar for .mts files.
32 # include "bison.reset"
33 # include "splintMacros.nf"
37 extern ctype mtscanner_lookupType (mttok p_tok) /*@modifies p_tok@*/ ;
40 /*@i523@*/ /* can't include these here
41 # include "mtgrammar.h"
42 # include "mtscanner.h"
45 static /*@noreturn@*/ void mterror (char *);
47 /*@-noparams@*/ /* Can't list params since YYSTYPE isn't defined yet. */
49 static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */);
52 # define YYPRINT(file, type, value) yyprint (file, type, value)
56 # include "bison.head"
64 mtDeclarationNode mtdecl;
65 mtDeclarationPiece mtpiece;
66 mtDeclarationPieces mtpieces;
67 mtContextNode mtcontext;
68 mtValuesNode mtvalues;
69 mtDefaultsNode mtdefaults;
70 mtDefaultsDeclList mtdeflist;
71 mtAnnotationsNode mtannotations;
72 mtAnnotationList mtannotlist;
73 mtAnnotationDecl mtannotdecl;
75 mtMergeItem mtmergeitem;
76 mtMergeClauseList mtmergeclauselist;
77 mtMergeClause mtmergeclause;
78 mtTransferClauseList mttransferclauselist;
79 mtTransferClause mttransferclause;
80 mtTransferAction mttransferaction;
81 mtLoseReferenceList mtlosereferencelist;
82 mtLoseReference mtlosereference;
84 /*@only@*/ cstringList cstringlist;
86 /*@only@*/ qtype qtyp;
91 /* Don't forget to enter all tokens in mtscanner.c */
92 %token <tok> MT_BADTOK
95 %token <tok> MT_STATE MT_GLOBAL
97 %token <tok> MT_CONTEXT
100 %token <tok> MT_DEFAULTS MT_DEFAULT
101 %token <tok> MT_REFERENCE MT_PARAMETER MT_RESULT MT_CLAUSE MT_LITERAL MT_NULL
103 %token <tok> MT_ANNOTATIONS
104 %token <tok> MT_ARROW
106 %token <tok> MT_MERGE
107 %token <tok> MT_TRANSFERS MT_PRECONDITIONS MT_POSTCONDITIONS
108 %token <tok> MT_LOSEREFERENCE
111 %token <tok> MT_ERROR
113 %token <tok> MT_PLUS MT_STAR MT_BAR
114 %token <tok> MT_LPAREN MT_RPAREN
115 %token <tok> MT_LBRACKET MT_RBRACKET
116 %token <tok> MT_LBRACE MT_RBRACE
117 %token <tok> MT_COMMA
119 %token <tok> MT_CHAR MT_INT MT_FLOAT MT_DOUBLE MT_VOID MT_ANYTYPE MT_INTEGRALTYPE MT_UNSIGNEDINTEGRALTYPE
120 %token <tok> MT_SIGNEDINTEGRALTYPE
121 %token <tok> MT_CONST MT_VOLATILE MT_RESTRICT
122 %token <tok> MT_STRINGLIT
123 %token <tok> MT_IDENT
125 %type <pointers> pointers
126 %type <ctyp> optType typeSpecifier typeName abstractDecl abstractDeclBase
127 %type <qtyp> typeExpression
128 %type <qtyp> completeType completeTypeAux optCompleteType
129 %type <mtpiece> declarationPiece
130 %type <mtcontext> contextDeclaration
131 %type <mtcontext> contextSelection optContextSelection
132 %type <mtvalues> valuesDeclaration
133 %type <tok> defaultNode
134 %type <mtdefaults> defaultsDeclaration
135 %type <mtdeflist> defaultDeclarationList
136 %type <mtannotations> annotationsDeclaration
137 %type <mtannotlist> annotationsDeclarationList
138 %type <mtannotdecl> annotationDeclaration
139 %type <mtmerge> mergeDeclaration
140 %type <mtmergeitem> mergeItem
141 %type <mtmergeclauselist> mergeClauses
142 %type <mtmergeclause> mergeClause
143 %type <mttransferclauselist> transfersDeclaration transferClauses preconditionsDeclaration postconditionsDeclaration
144 %type <mttransferclause> transferClause
145 %type <mttransferaction> transferAction errorAction
146 %type <mtlosereferencelist> loseReferenceDeclaration lostClauses
147 %type <mtlosereference> lostClause
148 %type <cstringlist> valuesList
149 %type <mtdecl> declarationNode
150 %type <mtpieces> declarationPieces
151 %type <tok> valueChoice
152 %type <quals> innerModsList
153 %type <qual> innerMods
164 : MT_STATE declarationNode MT_END
165 { mtreader_processDeclaration ($2); }
166 | MT_GLOBAL MT_STATE declarationNode MT_END
167 { mtreader_processGlobalDeclaration ($3); }
170 : MT_IDENT declarationPieces
171 { $$ = mtDeclarationNode_create ($1, $2); }
174 : { $$ = mtDeclarationPieces_create (); }
175 | declarationPiece declarationPieces
176 { $$ = mtDeclarationPieces_append ($2, $1); }
179 : contextDeclaration { $$ = mtDeclarationPiece_createContext ($1); }
180 | valuesDeclaration { $$ = mtDeclarationPiece_createValues ($1); }
181 | defaultsDeclaration { $$ = mtDeclarationPiece_createDefaults ($1); }
182 | defaultNode { $$ = mtDeclarationPiece_createValueDefault ($1); }
183 | annotationsDeclaration { $$ = mtDeclarationPiece_createAnnotations ($1); }
184 | mergeDeclaration { $$ = mtDeclarationPiece_createMerge ($1); }
185 | transfersDeclaration { $$ = mtDeclarationPiece_createTransfers ($1); }
186 | preconditionsDeclaration { $$ = mtDeclarationPiece_createPreconditions ($1); }
187 | postconditionsDeclaration { $$ = mtDeclarationPiece_createPostconditions ($1); }
188 | loseReferenceDeclaration { $$ = mtDeclarationPiece_createLosers ($1); }
191 : MT_CONTEXT contextSelection { $$ = $2; }
192 /* ??? should it be a list? */
195 : /* empty */ { $$ = mtContextNode_createAny (); }
199 : MT_PARAMETER optType { $$ = mtContextNode_createParameter ($2); }
200 | MT_REFERENCE optType { $$ = mtContextNode_createReference ($2); }
201 | MT_RESULT optType { $$ = mtContextNode_createResult ($2); }
202 | MT_CLAUSE optType { $$ = mtContextNode_createClause ($2); }
203 | MT_LITERAL optType { $$ = mtContextNode_createLiteral ($2); }
204 | MT_NULL optType { $$ = mtContextNode_createNull ($2); }
207 ** Wish I could share the C grammar here...cut-and-paste instead.
211 : /* empty */ { $$ = ctype_unknown; }
212 | typeExpression { DPRINTF (("Type: %s", qtype_unparse ($1))); $$ = qtype_getType ($1); }
216 | completeType abstractDecl { $$ = qtype_newBase ($1, $2); }
219 : completeTypeAux { $$ = $1; }
220 | completeType MT_BAR typeExpression
221 { $$ = qtype_mergeAlt ($1, $3); }
224 : typeSpecifier optCompleteType { $$ = qtype_combine ($2, $1); }
227 : /* empty */ { $$ = qtype_unknown (); }
228 | completeType { $$ = $1; }
232 : pointers { $$ = ctype_adjustPointers ($1, ctype_unknown); }
234 | pointers abstractDeclBase { $$ = ctype_adjustPointers ($1, $2); }
237 : MT_STAR { $$ = pointers_createMt ($1); }
238 | MT_STAR innerModsList { $$ = pointers_createModsMt ($1, $2); }
239 | MT_STAR pointers { $$ = pointers_extend (pointers_createMt ($1), $2); }
240 | MT_STAR innerModsList pointers { $$ = pointers_extend (pointers_createModsMt ($1, $2), $3); }
243 : MT_CONST { $$ = qual_createConst (); }
244 | MT_VOLATILE { $$ = qual_createVolatile (); }
245 | MT_RESTRICT { $$ = qual_createRestrict (); }
248 : innerMods { $$ = qualList_single ($1); }
249 | innerModsList innerMods { $$ = qualList_add ($1, $2); }
252 : MT_LPAREN abstractDecl MT_RPAREN { $$ = ctype_expectFunction ($2); }
253 | MT_LBRACKET MT_RBRACKET { $$ = ctype_makeArray (ctype_unknown); }
254 | abstractDeclBase MT_LBRACKET MT_RBRACKET { $$ = ctype_makeArray ($1); }
256 | abstractDeclBase MT_LBRACKET constantExpr MT_RBRACKET
257 { $$ = ctype_makeFixedArray ($1, exprNode_getLongValue ($3)); }
261 : MT_CHAR { $$ = ctype_char; }
262 | MT_INT { $$ = ctype_int; }
263 | MT_FLOAT { $$ = ctype_float; }
264 | MT_DOUBLE { $$ = ctype_double; }
265 | MT_VOID { $$ = ctype_void; }
266 | MT_ANYTYPE { $$ = ctype_unknown; }
267 | MT_INTEGRALTYPE { $$ = ctype_anyintegral; }
268 | MT_UNSIGNEDINTEGRALTYPE { $$ = ctype_unsignedintegral; }
269 | MT_SIGNEDINTEGRALTYPE { $$ = ctype_signedintegral; }
273 | typeModifier NotType { $$ = ctype_fromQual ($1); } */
276 : MT_IDENT { $$ = mtscanner_lookupType ($1); }
279 : MT_ONEOF valuesList { $$ = mtValuesNode_create ($2); }
282 : MT_IDENT { $$ = cstringList_single (mttok_getText ($1)); }
283 | MT_IDENT MT_COMMA valuesList
284 { $$ = cstringList_prepend ($3, mttok_getText ($1)); }
287 : MT_DEFAULT valueChoice { $$ = $2; }
290 : MT_DEFAULTS defaultDeclarationList { $$ = mtDefaultsNode_create ($1, $2); }
292 defaultDeclarationList
293 : contextSelection MT_ARROW valueChoice
294 { $$ = mtDefaultsDeclList_single (mtDefaultsDecl_create ($1, $3)); }
295 | contextSelection MT_ARROW valueChoice defaultDeclarationList
296 { $$ = mtDefaultsDeclList_prepend ($4, mtDefaultsDecl_create ($1, $3)); }
298 annotationsDeclaration
299 : MT_ANNOTATIONS annotationsDeclarationList { $$ = mtAnnotationsNode_create ($2); }
301 annotationsDeclarationList
302 : annotationDeclaration { $$ = mtAnnotationList_single ($1); }
303 | annotationDeclaration annotationsDeclarationList
304 { $$ = mtAnnotationList_prepend ($2, $1); }
306 annotationDeclaration
307 : MT_IDENT optContextSelection MT_ARROW valueChoice
308 { $$ = mtAnnotationDecl_create ($1, $2, $4); }
311 : MT_MERGE mergeClauses { $$ = mtMergeNode_create ($2); }
314 : mergeClause { $$ = mtMergeClauseList_single ($1); }
315 | mergeClause mergeClauses { $$ = mtMergeClauseList_prepend ($2, $1); }
318 : mergeItem MT_PLUS mergeItem MT_ARROW transferAction
319 { $$ = mtMergeClause_create ($1, $3, $5); }
322 : valueChoice { $$ = mtMergeItem_createValue ($1); }
323 | MT_STAR { $$ = mtMergeItem_createStar ($1); }
325 preconditionsDeclaration
326 : MT_PRECONDITIONS transferClauses { $$ = $2; }
328 postconditionsDeclaration
329 : MT_POSTCONDITIONS transferClauses { $$ = $2; }
332 : MT_TRANSFERS transferClauses { $$ = $2; }
334 loseReferenceDeclaration
335 : MT_LOSEREFERENCE lostClauses { $$ = $2; }
338 : lostClause { $$ = mtLoseReferenceList_single ($1); }
339 | lostClause lostClauses { $$ = mtLoseReferenceList_prepend ($2, $1); }
342 : valueChoice MT_ARROW errorAction { $$ = mtLoseReference_create ($1, $3); }
345 : transferClause { $$ = mtTransferClauseList_single ($1); }
346 | transferClause transferClauses { $$ = mtTransferClauseList_prepend ($2, $1); }
349 : valueChoice MT_AS valueChoice MT_ARROW transferAction
350 { $$ = mtTransferClause_create ($1, $3, $5); }
353 : valueChoice { $$ = mtTransferAction_createValue ($1); }
354 | errorAction { $$ = $1; }
357 : MT_ERROR { $$ = mtTransferAction_createError ($1); }
358 | MT_ERROR MT_STRINGLIT { $$ = mtTransferAction_createErrorMessage ($2); }
365 # include "bison.reset"
369 static void mterror (char *s)
375 (message ("Parse error in meta-state file: %s", cstring_fromChars (s)));
380 (message ("Parse error in meta-state file"));
385 static void yyprint (FILE *file, int type, YYSTYPE value)
387 cstring tname = mttok_unparse (value.tok);
388 fprintf (file, " (%s)", cstring_toCharsSafe (tname));
389 cstring_free (tname);