]> andersk Git - splint.git/blame - src/signature.y
Renaming - LCLint => Splint
[splint.git] / src / signature.y
CommitLineData
885824d3 1/*;-*-C-*-;
11db3170 2** Splint - annotation-assisted static program checker
3** Copyright (C) 1994-2001 University of Virginia,
4** Massachusetts Institute of Technology
885824d3 5**
11db3170 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.
885824d3 19**
11db3170 20** For information on lclint: lclint-request@cs.virginia.edu
21** To report a bug: lclint-bug@cs.virginia.edu
22** For more information: http://www.splint.org
885824d3 23*/
24/*
11db3170 25** signature.y
885824d3 26**
11db3170 27** Grammar for parsing LSL signatures.
885824d3 28**
11db3170 29** Original author: Yang Meng Tan, Massachusetts Institute of Technology
885824d3 30*/
31
32%{
33
885824d3 34# include <stdio.h>
35# include "lclintMacros.nf"
36# include "llbasic.h"
37# include "lslparse.h"
38# include "signature.h"
39
40void lslerror (char *);
41/*@dependent@*/ /*@null@*/ lslOp importedlslOp;
42
43/*@-noparams@*/ /* Can't list params since YYSTYPE isn't defined yet. */
44static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */);
45/*@=noparams@*/
46
47# define YYPRINT(file, type, value) yyprint (file, type, value)
48
49# define YYDEBUG 1
50
60eced23 51/*@-redef@*/
52/*@-readonlytrans@*/
53/*@-nullassign@*/
885824d3 54
55%}
56
57%pure_parser
58
59/* CONVENTIONS: Reserved words are in ALL CAPS (plus markerSym)
60 Characters appearing in the grammar are reserved:
61 % ( ) , : \ */
62
63/* Changes made
64 - added LBRACKET stuff in OpForm (missing in LSL)
65 - dif from LCL: open vs openSym, close vs closeSym
66 - yylval vs yylval.tok
67*/
68
69%union {
70 ltoken ltok; /* a leaf is also an ltoken */
71 unsigned int count;
72 /*@only@*/ ltokenList ltokenList;
73 /*@only@*/ opFormNode opform;
74 /*@owned@*/ sigNode signature;
75 /*@only@*/ nameNode name;
76 /*@owned@*/ lslOp operator;
77 /*@only@*/ lslOpList operators;
60eced23 78 /*@-redef@*/ /*@-matchfields@*/
79}
80/*@=redef@*/ /*@=matchfields@*/
885824d3 81
82%token <ltok> LST_SIMPLEID
83%token <ltok> LST_LOGICALOP /* \implies, \and, \not, \or */
84%token <ltok> LST_EQOP /* \eq, \neq, ==, != */
85%token <ltok> LST_SIMPLEOP /* opSym - reserved */
86%token <ltok> LST_MAPSYM /* LSL's -> */
87 /* FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */
88%token <ltok> LST_FIELDMAPSYM /* LCL's struct field operator -> */
89%token <ltok> LST_MARKERSYM /* \marker, __ */
90%token <ltok> LST_ifTOKEN LST_thenTOKEN LST_elseTOKEN
91 /* different from LSL: separate LBRACKET from openSym and
92 RBRACKET from closeSym */
93%token <ltok> LST_LBRACKET LST_RBRACKET
94%token <ltok> LST_SELECTSYM /* \select or . */
95%token <ltok> LST_SEPSYM LST_OPENSYM LST_CLOSESYM
96%token <ltok> LST_COLON /* : */
97%token <ltok> LST_COMMA /* , */
98%token <ltok> LST_EOL LST_COMMENTSYM LST_WHITESPACE
99
100%token LST_WHITESPACE
101%token LST_QUANTIFIERSYM
102%token LST_EQUATIONSYM
103%token LST_EQSEPSYM
104%token LST_COMPOSESYM
105%token LST_LPAR
106%token LST_RPAR
107%token LST_assertsTOKEN
108%token LST_assumesTOKEN
109%token LST_byTOKEN
110%token LST_convertsTOKEN
111%token LST_enumerationTOKEN
112%token LST_equationsTOKEN
113%token LST_exemptingTOKEN
114%token LST_forTOKEN
115%token LST_generatedTOKEN
116%token LST_impliesTOKEN
117%token LST_includesTOKEN
118%token LST_introducesTOKEN
119%token LST_ofTOKEN
120%token LST_partitionedTOKEN
121%token LST_traitTOKEN
122%token LST_tupleTOKEN
123%token LST_unionTOKEN
124%token LST_BADTOKEN
125
126%type <ltok> anyOp separator sortId opId
127%type <count> middle placeList
128%type <ltokenList> domain sortList
129%type <opform> opForm
130%type <signature> signature
131%type <name> name
132%type <operator> operator
133%type <operators> operatorList top
134
135%%
136
137top: operatorList { lslOpList_free ($1); }
138
139operatorList: operator
140 { lslOpList x = lslOpList_new ();
141 g_importedlslOp = $1;
142 lslOpList_add (x, $1);
143 $$ = x; }
144 | operatorList operator
145 { lslOpList_add ($1, $2);
146 $$ = $1; }
147
148operator: name LST_COLON signature
149 { $$ = makelslOpNode ($1, $3); }
150/* The next production is never used in the output of lsl -syms
151 | name
152 { $$ = makelslOpNode ($1, (sigNode)0); } */
153
154name: opId /* check for the case of if_then_else */
155 { $$ = makeNameNodeId ($1); }
156 | opForm
157 { $$ = makeNameNodeForm ($1); }
158
159opForm
160 : LST_ifTOKEN LST_MARKERSYM LST_thenTOKEN LST_MARKERSYM LST_elseTOKEN LST_MARKERSYM
161 { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); }
162 | anyOp
163 { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); }
164 | LST_MARKERSYM anyOp
165 { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); }
166 | anyOp LST_MARKERSYM
167 { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); }
168 | LST_MARKERSYM anyOp LST_MARKERSYM
169 { $$ = makeOpFormNode ($1, OPF_MANYOPM, opFormUnion_createAnyOp ($2), ltoken_undefined); }
170 | LST_OPENSYM middle LST_CLOSESYM
171 { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); }
172 | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM
173 { $$ = makeOpFormNode ($2, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); }
174 | LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM
175 { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); }
176 | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM
177 { $$ = makeOpFormNode ($2, OPF_MMIDDLEM,
178 opFormUnion_createMiddle ($3), $4); }
179 | LST_LBRACKET middle LST_RBRACKET
180 { $$ = makeOpFormNode ($1, OPF_BMIDDLE,
181 opFormUnion_createMiddle ($2), $3); }
182 | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET
183 { $$ = makeOpFormNode ($2, OPF_BMMIDDLE,
184 opFormUnion_createMiddle ($3), $4); }
185 | LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM
186 { $$ = makeOpFormNode ($1, OPF_BMIDDLEM,
187 opFormUnion_createMiddle ($2), $3); }
188 | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM
189 { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM,
190 opFormUnion_createMiddle ($3), $4); }
191 | LST_SELECTSYM LST_SIMPLEID
192 { $$ = makeOpFormNode ($1, OPF_SELECT,
193 opFormUnion_createAnyOp ($2), ltoken_undefined); }
194 | LST_MARKERSYM LST_SELECTSYM LST_SIMPLEID
195 { $$ = makeOpFormNode ($1, OPF_MSELECT,
196 opFormUnion_createAnyOp ($3), ltoken_undefined); }
197 /* not in LSL, need FILEDMAPSYM to distinguish it from MAPSYM */
198 /* LST_FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */
199 | LST_MARKERSYM LST_FIELDMAPSYM LST_SIMPLEID
200 { $$ = makeOpFormNode ($1, OPF_MMAP,
201 opFormUnion_createAnyOp ($3), ltoken_undefined); }
202
203
204anyOp: LST_SIMPLEOP
205 { $$ = $1; }
206 | LST_LOGICALOP
207 { $$ = $1; }
208 | LST_EQOP
209 { $$ = $1; }
210
211middle: /* empty */
212 { $$ = 0; }
213 | placeList
214 { $$ = $1; }
215
216placeList: LST_MARKERSYM
217 { $$ = 1; }
218 | placeList separator LST_MARKERSYM
219 { $$ = $1 + 1; }
220
221separator: LST_COMMA
222 { $$ = $1; }
223 | LST_SEPSYM
224 { $$ = $1; }
225
226signature: domain LST_MAPSYM sortId
227 { $$ = makesigNode ($2, $1, $3); }
228
229domain: /* empty */
230 { $$ = ltokenList_new (); }
231 | sortList
232 { $$ = $1; }
233
234sortList: sortId
235 { $$ = ltokenList_singleton ($1); }
236 | sortList LST_COMMA sortId
237 { $$ = ltokenList_push ($1, $3); }
238
239sortId: LST_SIMPLEID
240 {
241 $$ = $1;
242 ltoken_setText ($$, processTraitSortId (ltoken_getText ($1)));
243 }
244
245opId: LST_SIMPLEID
246 { $$ = $1; }
247%%
248
249# include "bison.reset"
250
251extern char *yytext;
252
253void lslerror (char *s)
254{
a0a162cd 255 llfatalbug
256 (cstring_makeLiteral
28bf4b0b 257 ("There has been a problem in the parser with LSL signatures. This is believed to result "
258 "from a problem with bison v. 1.25. Please try rebuidling LCLint "
259 "using the pre-compiled grammar files by commenting out the "
260 "BISON= line in the top-level Makefile."));
885824d3 261}
262
263static void yyprint (FILE *file, int type, YYSTYPE value)
264{
265 fprintf (file, " (%u:%u type: %d; text: %s) ",
266 ltoken_getLine (value.ltok),
267 ltoken_getCol (value.ltok),
268 type,
269 ltoken_getRawTextChars (value.ltok));
270}
271
272extern void PrintToken (ltoken tok) {
273 char *codStr;
274
275 switch (ltoken_getCode (tok))
276 {
277 case NOTTOKEN: codStr = "*** NOTTOKEN ***"; break;
278 case LST_QUANTIFIERSYM: codStr = "QUANTIFIERSYM"; break;
279 case LST_LOGICALOP: codStr = "LOGICALOP: "; break;
280 case LST_SELECTSYM: codStr = "LST_SELECTSYM"; break;
281 case LST_OPENSYM: codStr = "LST_OPENSYM"; break;
282 case LST_SEPSYM: codStr = "SEPSYM"; break;
283 case LST_CLOSESYM: codStr = "LST_CLOSESYM"; break;
284 case LST_SIMPLEID: codStr = "LST_SIMPLEID"; break;
285 case LST_MAPSYM: codStr = "MAPSYM"; break;
286 case LST_MARKERSYM: codStr = "LST_MARKERSYM"; break;
287 case LST_COMMENTSYM: codStr = "COMMENTSYM"; break;
288 case LST_SIMPLEOP: codStr = "SIMPLEOP"; break;
289 case LST_COLON: codStr = "LST_COLON"; break;
290 case LST_COMMA: codStr = "COMMA"; break;
291 case LST_LBRACKET: codStr = "LST_LBRACKET"; break;
292 case LST_LPAR: codStr = "LST_LPAR"; break;
293 case LST_RBRACKET: codStr = "LST_RBRACKET"; break;
294 case LST_RPAR: codStr = "LST_RPAR"; break;
295 case LST_EQOP: codStr = "LST_EQOP"; break;
296 case LST_WHITESPACE: codStr = "WHITESPACE,"; break;
297 case LST_EOL: codStr = "LST_EOL"; break;
298 case LST_elseTOKEN: codStr = "elseTOKEN"; break;
299 case LST_ifTOKEN: codStr = "ifTOKEN"; break;
300 case LST_thenTOKEN: codStr = "thenTOKEN"; break;
301 case LST_BADTOKEN: codStr = "*** BADTOKEN ***"; break;
302 case LEOFTOKEN: /* can't reach LEOFTOKEN easily */
303 codStr = "LEOFTOKEN"; break;
304 default:
305 codStr = "*** invalid token code ***";
306 break;
307 } /* end switch */
308
309 /* only used for debugging */
310 printf ("%u:%u: Token Code (%u): %s",
311 ltoken_getLine (tok), ltoken_getCol (tok),
312 ltoken_getCode (tok), codStr);
313 if (ltoken_getRawText (tok) != 0)
314 {
315 printf (", Token String (%lu): %s\n",
316 ltoken_getRawText (tok), ltoken_getRawTextChars (tok));
317 }
318 else printf ("\n");
319}
320
321
322
323
This page took 0.11207 seconds and 5 git commands to generate.