]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 1 | /*;-*-C-*-; |
1b8ae690 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
1b8ae690 | 4 | ** Massachusetts Institute of Technology |
28bf4b0b | 5 | ** |
1b8ae690 | 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. | |
10 | ** | |
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. | |
15 | ** | |
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. | |
28bf4b0b | 19 | ** |
1b8ae690 | 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 | |
28bf4b0b | 23 | */ |
24 | /* | |
25 | ** mtgrammar.y | |
26 | ** | |
27 | ** Grammar for .mts files. | |
28 | */ | |
29 | ||
30 | %{ | |
31 | ||
32 | # include "bison.reset" | |
1b8ae690 | 33 | # include "splintMacros.nf" |
b73d1009 | 34 | # include "basic.h" |
28bf4b0b | 35 | |
3e3ec469 | 36 | # ifndef S_SPLINT_S |
b7b694d6 | 37 | extern ctype mtscanner_lookupType (mttok p_tok) /*@modifies p_tok@*/ ; |
38 | # endif | |
39 | ||
68de3f33 | 40 | /*@i523@*/ /* can't include these here |
b7b694d6 | 41 | # include "mtgrammar.h" |
42 | # include "mtscanner.h" | |
43 | */ | |
44 | ||
4dd72714 | 45 | static /*@noreturn@*/ void mterror (char *); |
28bf4b0b | 46 | |
47 | /*@-noparams@*/ /* Can't list params since YYSTYPE isn't defined yet. */ | |
4dd72714 | 48 | extern int mtlex () ; |
28bf4b0b | 49 | static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */); |
50 | /*@=noparams@*/ | |
51 | ||
52 | # define YYPRINT(file, type, value) yyprint (file, type, value) | |
53 | ||
54 | # define YYDEBUG 1 | |
55 | ||
56 | # include "bison.head" | |
57 | ||
58 | %} | |
59 | ||
60 | %pure_parser | |
61 | ||
62 | %union { | |
63 | mttok tok; | |
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; | |
74 | mtMergeNode mtmerge; | |
75 | mtMergeItem mtmergeitem; | |
76 | mtMergeClauseList mtmergeclauselist; | |
77 | mtMergeClause mtmergeclause; | |
78 | mtTransferClauseList mttransferclauselist; | |
79 | mtTransferClause mttransferclause; | |
80 | mtTransferAction mttransferaction; | |
81 | mtLoseReferenceList mtlosereferencelist; | |
82 | mtLoseReference mtlosereference; | |
f9264521 | 83 | pointers pointers; |
28bf4b0b | 84 | /*@only@*/ cstringList cstringlist; |
85 | ctype ctyp; | |
86 | /*@only@*/ qtype qtyp; | |
f9264521 | 87 | qual qual; |
88 | qualList quals; | |
28bf4b0b | 89 | } |
90 | ||
91 | /* Don't forget to enter all tokens in mtscanner.c */ | |
92 | %token <tok> MT_BADTOK | |
93 | ||
94 | %token <tok> MT_END | |
95 | %token <tok> MT_STATE MT_GLOBAL | |
96 | ||
97 | %token <tok> MT_CONTEXT | |
98 | %token <tok> MT_ONEOF | |
99 | ||
100 | %token <tok> MT_DEFAULTS MT_DEFAULT | |
12f2ffe9 | 101 | %token <tok> MT_REFERENCE MT_PARAMETER MT_RESULT MT_CLAUSE MT_LITERAL MT_NULL |
28bf4b0b | 102 | |
103 | %token <tok> MT_ANNOTATIONS | |
104 | %token <tok> MT_ARROW | |
105 | ||
106 | %token <tok> MT_MERGE | |
107 | %token <tok> MT_TRANSFERS MT_PRECONDITIONS MT_POSTCONDITIONS | |
108 | %token <tok> MT_LOSEREFERENCE | |
109 | ||
110 | %token <tok> MT_AS | |
111 | %token <tok> MT_ERROR | |
112 | ||
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 | |
118 | ||
119 | %token <tok> MT_CHAR MT_INT MT_FLOAT MT_DOUBLE MT_VOID MT_ANYTYPE MT_INTEGRALTYPE MT_UNSIGNEDINTEGRALTYPE | |
120 | %token <tok> MT_SIGNEDINTEGRALTYPE | |
f9264521 | 121 | %token <tok> MT_CONST MT_VOLATILE MT_RESTRICT |
28bf4b0b | 122 | %token <tok> MT_STRINGLIT |
123 | %token <tok> MT_IDENT | |
124 | ||
f9264521 | 125 | %type <pointers> pointers |
28bf4b0b | 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 | |
f9264521 | 152 | %type <quals> innerModsList |
153 | %type <qual> innerMods | |
28bf4b0b | 154 | |
155 | %start file | |
156 | ||
157 | %% | |
158 | ||
159 | file | |
160 | : {} | |
161 | | mtsDeclaration {} | |
2f2892c2 | 162 | ; |
28bf4b0b | 163 | |
164 | mtsDeclaration | |
165 | : MT_STATE declarationNode MT_END | |
166 | { mtreader_processDeclaration ($2); } | |
167 | | MT_GLOBAL MT_STATE declarationNode MT_END | |
168 | { mtreader_processGlobalDeclaration ($3); } | |
2f2892c2 | 169 | ; |
28bf4b0b | 170 | |
171 | declarationNode | |
172 | : MT_IDENT declarationPieces | |
173 | { $$ = mtDeclarationNode_create ($1, $2); } | |
2f2892c2 | 174 | ; |
28bf4b0b | 175 | |
176 | declarationPieces | |
177 | : { $$ = mtDeclarationPieces_create (); } | |
178 | | declarationPiece declarationPieces | |
179 | { $$ = mtDeclarationPieces_append ($2, $1); } | |
2f2892c2 | 180 | ; |
28bf4b0b | 181 | |
182 | declarationPiece | |
183 | : contextDeclaration { $$ = mtDeclarationPiece_createContext ($1); } | |
184 | | valuesDeclaration { $$ = mtDeclarationPiece_createValues ($1); } | |
185 | | defaultsDeclaration { $$ = mtDeclarationPiece_createDefaults ($1); } | |
186 | | defaultNode { $$ = mtDeclarationPiece_createValueDefault ($1); } | |
187 | | annotationsDeclaration { $$ = mtDeclarationPiece_createAnnotations ($1); } | |
188 | | mergeDeclaration { $$ = mtDeclarationPiece_createMerge ($1); } | |
189 | | transfersDeclaration { $$ = mtDeclarationPiece_createTransfers ($1); } | |
190 | | preconditionsDeclaration { $$ = mtDeclarationPiece_createPreconditions ($1); } | |
191 | | postconditionsDeclaration { $$ = mtDeclarationPiece_createPostconditions ($1); } | |
192 | | loseReferenceDeclaration { $$ = mtDeclarationPiece_createLosers ($1); } | |
2f2892c2 | 193 | ; |
28bf4b0b | 194 | |
195 | contextDeclaration | |
196 | : MT_CONTEXT contextSelection { $$ = $2; } | |
197 | /* ??? should it be a list? */ | |
2f2892c2 | 198 | ; |
28bf4b0b | 199 | |
200 | optContextSelection | |
201 | : /* empty */ { $$ = mtContextNode_createAny (); } | |
202 | | contextSelection | |
2f2892c2 | 203 | ; |
28bf4b0b | 204 | |
205 | contextSelection | |
206 | : MT_PARAMETER optType { $$ = mtContextNode_createParameter ($2); } | |
207 | | MT_REFERENCE optType { $$ = mtContextNode_createReference ($2); } | |
b072092f | 208 | | MT_RESULT optType { $$ = mtContextNode_createResult ($2); } |
28bf4b0b | 209 | | MT_CLAUSE optType { $$ = mtContextNode_createClause ($2); } |
12f2ffe9 | 210 | | MT_LITERAL optType { $$ = mtContextNode_createLiteral ($2); } |
211 | | MT_NULL optType { $$ = mtContextNode_createNull ($2); } | |
2f2892c2 | 212 | ; |
28bf4b0b | 213 | |
214 | /* | |
215 | ** Wish I could share the C grammar here...cut-and-paste instead. | |
216 | */ | |
217 | ||
218 | optType | |
219 | : /* empty */ { $$ = ctype_unknown; } | |
220 | | typeExpression { DPRINTF (("Type: %s", qtype_unparse ($1))); $$ = qtype_getType ($1); } | |
2f2892c2 | 221 | ; |
28bf4b0b | 222 | |
223 | typeExpression | |
224 | : completeType | |
225 | | completeType abstractDecl { $$ = qtype_newBase ($1, $2); } | |
2f2892c2 | 226 | ; |
28bf4b0b | 227 | |
228 | completeType | |
229 | : completeTypeAux { $$ = $1; } | |
230 | | completeType MT_BAR typeExpression | |
231 | { $$ = qtype_mergeAlt ($1, $3); } | |
2f2892c2 | 232 | ; |
28bf4b0b | 233 | |
234 | completeTypeAux | |
235 | : typeSpecifier optCompleteType { $$ = qtype_combine ($2, $1); } | |
2f2892c2 | 236 | ; |
28bf4b0b | 237 | |
238 | optCompleteType | |
239 | : /* empty */ { $$ = qtype_unknown (); } | |
240 | | completeType { $$ = $1; } | |
2f2892c2 | 241 | ; |
28bf4b0b | 242 | |
243 | abstractDecl | |
244 | : pointers { $$ = ctype_adjustPointers ($1, ctype_unknown); } | |
245 | | abstractDeclBase | |
246 | | pointers abstractDeclBase { $$ = ctype_adjustPointers ($1, $2); } | |
2f2892c2 | 247 | ; |
28bf4b0b | 248 | |
249 | pointers | |
f9264521 | 250 | : MT_STAR { $$ = pointers_createMt ($1); } |
251 | | MT_STAR innerModsList { $$ = pointers_createModsMt ($1, $2); } | |
252 | | MT_STAR pointers { $$ = pointers_extend (pointers_createMt ($1), $2); } | |
253 | | MT_STAR innerModsList pointers { $$ = pointers_extend (pointers_createModsMt ($1, $2), $3); } | |
2f2892c2 | 254 | ; |
28bf4b0b | 255 | |
256 | innerMods | |
f9264521 | 257 | : MT_CONST { $$ = qual_createConst (); } |
258 | | MT_VOLATILE { $$ = qual_createVolatile (); } | |
259 | | MT_RESTRICT { $$ = qual_createRestrict (); } | |
2f2892c2 | 260 | ; |
28bf4b0b | 261 | |
262 | innerModsList | |
f9264521 | 263 | : innerMods { $$ = qualList_single ($1); } |
264 | | innerModsList innerMods { $$ = qualList_add ($1, $2); } | |
2f2892c2 | 265 | ; |
28bf4b0b | 266 | |
267 | abstractDeclBase | |
268 | : MT_LPAREN abstractDecl MT_RPAREN { $$ = ctype_expectFunction ($2); } | |
269 | | MT_LBRACKET MT_RBRACKET { $$ = ctype_makeArray (ctype_unknown); } | |
270 | | abstractDeclBase MT_LBRACKET MT_RBRACKET { $$ = ctype_makeArray ($1); } | |
271 | /* | |
272 | | abstractDeclBase MT_LBRACKET constantExpr MT_RBRACKET | |
273 | { $$ = ctype_makeFixedArray ($1, exprNode_getLongValue ($3)); } | |
274 | */ | |
2f2892c2 | 275 | ; |
28bf4b0b | 276 | |
277 | typeSpecifier | |
278 | : MT_CHAR { $$ = ctype_char; } | |
279 | | MT_INT { $$ = ctype_int; } | |
280 | | MT_FLOAT { $$ = ctype_float; } | |
281 | | MT_DOUBLE { $$ = ctype_double; } | |
282 | | MT_VOID { $$ = ctype_void; } | |
283 | | MT_ANYTYPE { $$ = ctype_unknown; } | |
284 | | MT_INTEGRALTYPE { $$ = ctype_anyintegral; } | |
285 | | MT_UNSIGNEDINTEGRALTYPE { $$ = ctype_unsignedintegral; } | |
286 | | MT_SIGNEDINTEGRALTYPE { $$ = ctype_signedintegral; } | |
287 | | typeName | |
288 | /* | suSpc | |
289 | | enumSpc | |
290 | | typeModifier NotType { $$ = ctype_fromQual ($1); } */ | |
2f2892c2 | 291 | ; |
28bf4b0b | 292 | |
293 | typeName | |
294 | : MT_IDENT { $$ = mtscanner_lookupType ($1); } | |
2f2892c2 | 295 | ; |
28bf4b0b | 296 | |
297 | valuesDeclaration | |
298 | : MT_ONEOF valuesList { $$ = mtValuesNode_create ($2); } | |
2f2892c2 | 299 | ; |
28bf4b0b | 300 | |
301 | valuesList | |
302 | : MT_IDENT { $$ = cstringList_single (mttok_getText ($1)); } | |
303 | | MT_IDENT MT_COMMA valuesList | |
304 | { $$ = cstringList_prepend ($3, mttok_getText ($1)); } | |
2f2892c2 | 305 | ; |
28bf4b0b | 306 | |
307 | defaultNode | |
308 | : MT_DEFAULT valueChoice { $$ = $2; } | |
2f2892c2 | 309 | ; |
28bf4b0b | 310 | |
311 | defaultsDeclaration | |
312 | : MT_DEFAULTS defaultDeclarationList { $$ = mtDefaultsNode_create ($1, $2); } | |
2f2892c2 | 313 | ; |
28bf4b0b | 314 | |
315 | defaultDeclarationList | |
316 | : contextSelection MT_ARROW valueChoice | |
317 | { $$ = mtDefaultsDeclList_single (mtDefaultsDecl_create ($1, $3)); } | |
318 | | contextSelection MT_ARROW valueChoice defaultDeclarationList | |
319 | { $$ = mtDefaultsDeclList_prepend ($4, mtDefaultsDecl_create ($1, $3)); } | |
2f2892c2 | 320 | ; |
28bf4b0b | 321 | |
322 | annotationsDeclaration | |
323 | : MT_ANNOTATIONS annotationsDeclarationList { $$ = mtAnnotationsNode_create ($2); } | |
2f2892c2 | 324 | ; |
28bf4b0b | 325 | |
326 | annotationsDeclarationList | |
327 | : annotationDeclaration { $$ = mtAnnotationList_single ($1); } | |
328 | | annotationDeclaration annotationsDeclarationList | |
329 | { $$ = mtAnnotationList_prepend ($2, $1); } | |
2f2892c2 | 330 | ; |
28bf4b0b | 331 | |
332 | annotationDeclaration | |
333 | : MT_IDENT optContextSelection MT_ARROW valueChoice | |
334 | { $$ = mtAnnotationDecl_create ($1, $2, $4); } | |
2f2892c2 | 335 | ; |
28bf4b0b | 336 | |
337 | mergeDeclaration | |
338 | : MT_MERGE mergeClauses { $$ = mtMergeNode_create ($2); } | |
2f2892c2 | 339 | ; |
28bf4b0b | 340 | |
341 | mergeClauses | |
342 | : mergeClause { $$ = mtMergeClauseList_single ($1); } | |
343 | | mergeClause mergeClauses { $$ = mtMergeClauseList_prepend ($2, $1); } | |
2f2892c2 | 344 | ; |
28bf4b0b | 345 | |
346 | mergeClause | |
347 | : mergeItem MT_PLUS mergeItem MT_ARROW transferAction | |
348 | { $$ = mtMergeClause_create ($1, $3, $5); } | |
2f2892c2 | 349 | ; |
28bf4b0b | 350 | |
351 | mergeItem | |
352 | : valueChoice { $$ = mtMergeItem_createValue ($1); } | |
353 | | MT_STAR { $$ = mtMergeItem_createStar ($1); } | |
2f2892c2 | 354 | ; |
28bf4b0b | 355 | |
356 | preconditionsDeclaration | |
357 | : MT_PRECONDITIONS transferClauses { $$ = $2; } | |
2f2892c2 | 358 | ; |
28bf4b0b | 359 | |
360 | postconditionsDeclaration | |
361 | : MT_POSTCONDITIONS transferClauses { $$ = $2; } | |
2f2892c2 | 362 | ; |
28bf4b0b | 363 | |
364 | transfersDeclaration | |
365 | : MT_TRANSFERS transferClauses { $$ = $2; } | |
2f2892c2 | 366 | ; |
28bf4b0b | 367 | |
368 | loseReferenceDeclaration | |
369 | : MT_LOSEREFERENCE lostClauses { $$ = $2; } | |
2f2892c2 | 370 | ; |
28bf4b0b | 371 | |
372 | lostClauses | |
373 | : lostClause { $$ = mtLoseReferenceList_single ($1); } | |
374 | | lostClause lostClauses { $$ = mtLoseReferenceList_prepend ($2, $1); } | |
2f2892c2 | 375 | ; |
28bf4b0b | 376 | |
377 | lostClause | |
378 | : valueChoice MT_ARROW errorAction { $$ = mtLoseReference_create ($1, $3); } | |
2f2892c2 | 379 | ; |
28bf4b0b | 380 | |
381 | transferClauses | |
382 | : transferClause { $$ = mtTransferClauseList_single ($1); } | |
383 | | transferClause transferClauses { $$ = mtTransferClauseList_prepend ($2, $1); } | |
2f2892c2 | 384 | ; |
28bf4b0b | 385 | |
386 | transferClause | |
387 | : valueChoice MT_AS valueChoice MT_ARROW transferAction | |
388 | { $$ = mtTransferClause_create ($1, $3, $5); } | |
2f2892c2 | 389 | ; |
28bf4b0b | 390 | |
391 | transferAction | |
392 | : valueChoice { $$ = mtTransferAction_createValue ($1); } | |
393 | | errorAction { $$ = $1; } | |
2f2892c2 | 394 | ; |
28bf4b0b | 395 | |
396 | errorAction | |
397 | : MT_ERROR { $$ = mtTransferAction_createError ($1); } | |
398 | | MT_ERROR MT_STRINGLIT { $$ = mtTransferAction_createErrorMessage ($2); } | |
2f2892c2 | 399 | ; |
28bf4b0b | 400 | |
401 | valueChoice | |
b072092f | 402 | : MT_IDENT |
2f2892c2 | 403 | ; |
28bf4b0b | 404 | |
405 | %% | |
406 | ||
407 | # include "bison.reset" | |
408 | ||
409 | extern char *yytext; | |
410 | ||
411 | static void mterror (char *s) | |
412 | { | |
b072092f | 413 | |
414 | if (s != NULL) | |
415 | { | |
416 | llparseerror | |
417 | (message ("Parse error in meta-state file: %s", cstring_fromChars (s))); | |
418 | } | |
419 | else | |
420 | { | |
421 | llparseerror | |
422 | (message ("Parse error in meta-state file")); | |
423 | } | |
424 | ||
28bf4b0b | 425 | } |
426 | ||
427 | static void yyprint (FILE *file, int type, YYSTYPE value) | |
428 | { | |
429 | cstring tname = mttok_unparse (value.tok); | |
430 | fprintf (file, " (%s)", cstring_toCharsSafe (tname)); | |
431 | cstring_free (tname); | |
432 | } | |
433 | ||
434 | ||
435 | ||
436 |