]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
616915dd | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
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. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
616915dd | 23 | */ |
24 | /* | |
25 | ** ltoken.c | |
26 | */ | |
27 | ||
1b8ae690 | 28 | # include "splintMacros.nf" |
616915dd | 29 | # include "llbasic.h" |
30 | # include "llgrammar.h" | |
31 | # include "scanline.h" | |
32 | # include "lclscanline.h" | |
33 | ||
34 | /* | |
35 | ** Place to store the \keyword (\forall ...) tokens. These tokens will | |
36 | ** have to be modified when the extensionChar ("\") changes. | |
37 | ** set in LCLScanLineInit of lclscanline.c or in scanline.c | |
38 | */ | |
39 | ||
2a6e9c30 | 40 | /*@-namechecks@*/ /* These should all start with g_ */ |
616915dd | 41 | ltoken ltoken_forall; |
42 | ltoken ltoken_exists; | |
43 | ltoken ltoken_true; | |
44 | ltoken ltoken_false; | |
45 | ltoken ltoken_not; | |
46 | ltoken ltoken_and; | |
47 | ltoken ltoken_or; | |
48 | ltoken ltoken_implies; | |
49 | ltoken ltoken_eq; | |
50 | ltoken ltoken_neq; | |
51 | ltoken ltoken_equals; | |
52 | ltoken ltoken_eqsep; | |
53 | ltoken ltoken_select; | |
54 | ltoken ltoken_open; | |
55 | ltoken ltoken_sep; | |
56 | ltoken ltoken_close; | |
57 | ltoken ltoken_id; | |
58 | ltoken ltoken_arrow; | |
59 | ltoken ltoken_marker; | |
60 | ltoken ltoken_pre; | |
61 | ltoken ltoken_post; | |
62 | ltoken ltoken_comment; | |
63 | ltoken ltoken_any; | |
64 | ltoken ltoken_compose; | |
65 | ltoken ltoken_if; | |
66 | ltoken ltoken_result; | |
67 | ltoken ltoken_typename; | |
68 | ltoken ltoken_bool; | |
69 | ltoken ltoken_farrow; | |
70 | ltoken ltoken_lbracked; | |
71 | ltoken ltoken_rbracket; | |
72 | /*@=namechecks@*/ | |
73 | ||
74 | static /*@notnull@*/ ltoken ltoken_new (void) | |
75 | { | |
76 | ltoken tok = (ltoken) dmalloc (sizeof (*tok)); | |
77 | ||
78 | tok->code = NOTTOKEN; | |
79 | tok->col = 0; | |
80 | tok->line = 0; | |
81 | tok->text = lsymbol_undefined; | |
82 | tok->fname = lsymbol_undefined; | |
83 | tok->rawText = lsymbol_undefined; | |
84 | tok->defined = FALSE; | |
85 | tok->hasSyn = FALSE; | |
86 | ||
87 | return tok; | |
88 | } | |
89 | ||
28bf4b0b | 90 | ltoken ltoken_create (ltokenCode code, lsymbol text) |
616915dd | 91 | { |
92 | ltoken tok = ltoken_new (); | |
93 | ||
94 | tok->code = code; | |
95 | tok->text = text; | |
96 | ||
97 | return tok; | |
98 | } | |
99 | ||
28bf4b0b | 100 | ltoken ltoken_createRaw (ltokenCode code, lsymbol text) |
616915dd | 101 | { |
102 | ltoken tok = ltoken_new (); | |
103 | ||
104 | tok->code = code; | |
105 | tok->rawText = text; | |
106 | ||
107 | return tok; | |
108 | } | |
109 | ||
28bf4b0b | 110 | ltoken ltoken_createType (ltokenCode code, SimpleIdCode idtype, lsymbol text) |
616915dd | 111 | { |
112 | ltoken tok = ltoken_new (); | |
113 | ||
114 | /* no...what's the real llassert (code == simpleId); */ | |
115 | ||
116 | tok->code = code; | |
117 | tok->idtype = idtype; | |
118 | tok->text = text; | |
119 | ||
120 | return tok; | |
121 | } | |
122 | ||
28bf4b0b | 123 | ltoken ltoken_createFull (ltokenCode code, lsymbol text, |
124 | cstring file, int line, | |
125 | int col) | |
616915dd | 126 | { |
127 | ltoken tok = (ltoken) dmalloc (sizeof (*tok)); | |
128 | ||
129 | tok->code = code; | |
130 | tok->text = text; | |
131 | tok->fname = lsymbol_fromString (file); | |
132 | tok->line = line; | |
133 | tok->col = col; | |
134 | tok->rawText = lsymbol_undefined; | |
135 | tok->defined = FALSE; | |
136 | tok->hasSyn = FALSE; | |
137 | ||
138 | return tok; | |
139 | } | |
140 | ||
28bf4b0b | 141 | static /*@only@*/ cstring LCLTokenCode_unparseCodeName (ltokenCode t) |
616915dd | 142 | { |
143 | switch (t) | |
144 | { | |
145 | case NOTTOKEN: return cstring_makeLiteral ("*** NOTTOKEN ***"); | |
146 | case quantifierSym: return cstring_makeLiteral ("QUANTIFIERSYM"); | |
147 | case logicalOp: return cstring_makeLiteral ("LOGICALOP"); | |
148 | case selectSym: return cstring_makeLiteral ("SELECTSYM"); | |
149 | case openSym: return cstring_makeLiteral ("OPENSYM"); | |
150 | case preSym: return cstring_makeLiteral ("\\pre"); | |
151 | case postSym: return cstring_makeLiteral ("\\post"); | |
152 | case anySym: return cstring_makeLiteral ("\\any"); | |
153 | case sepSym: return cstring_makeLiteral ("SEPSYM"); | |
154 | case closeSym: return cstring_makeLiteral ("CLOSESYM"); | |
155 | case simpleId: return cstring_makeLiteral ("simpleId"); | |
156 | case LLT_TYPEDEF_NAME: return cstring_makeLiteral ("TYPEDEF_NAME"); | |
157 | case mapSym: return cstring_makeLiteral ("MAPSYM"); | |
158 | case markerSym: return cstring_makeLiteral ("MARKERSYM"); | |
159 | case commentSym: return cstring_makeLiteral ("COMMENTSYM"); | |
160 | case simpleOp: return cstring_makeLiteral ("SIMPLEOP"); | |
161 | case LLT_COLON: return cstring_makeLiteral ("COLON"); | |
162 | case LLT_COMMA: return cstring_makeLiteral ("COMMA"); | |
163 | case LLT_EQUALS: return cstring_makeLiteral ("LLT_EQUALS"); | |
164 | case LLT_LBRACE: return cstring_makeLiteral ("LBRACE"); | |
165 | case LLT_LBRACKET: return cstring_makeLiteral ("LBRACKET"); | |
166 | case LLT_LPAR: return cstring_makeLiteral ("LPAR"); | |
167 | case LLT_QUOTE: return cstring_makeLiteral ("QUOTE"); | |
168 | case LLT_RBRACE: return cstring_makeLiteral ("RBRACE"); | |
169 | case LLT_RBRACKET: return cstring_makeLiteral ("RBRACKET"); | |
170 | case LLT_RPAR: return cstring_makeLiteral ("RPAR"); | |
171 | case LLT_SEMI: return cstring_makeLiteral ("SEMI"); | |
172 | case LLT_VERTICALBAR: return cstring_makeLiteral ("VERTICALBAR"); | |
173 | case eqOp: return cstring_makeLiteral ("EQOP"); | |
174 | case LLT_MULOP: return cstring_makeLiteral ("MULOP"); | |
175 | case LLT_WHITESPACE: return cstring_makeLiteral ("WHITESPACE,"); | |
176 | case LEOFTOKEN: return cstring_makeLiteral ("EOFTOKEN"); | |
177 | case LLT_EOL: return cstring_makeLiteral ("LLT_EOL"); | |
178 | case LLT_CCHAR: return cstring_makeLiteral ("CCHAR"); | |
179 | case LLT_CFLOAT: return cstring_makeLiteral ("CFLOAT"); | |
180 | case LLT_CINTEGER: return cstring_makeLiteral ("CINTEGER"); | |
181 | case LLT_LCSTRING: return cstring_makeLiteral ("CSTRING"); | |
182 | case LLT_ALL: return cstring_makeLiteral ("allTOKEN"); | |
183 | case LLT_ANYTHING: return cstring_makeLiteral ("anythingTOKEN"); | |
184 | case LLT_BE: return cstring_makeLiteral ("beTOKEN"); | |
185 | case LLT_CONSTANT: return cstring_makeLiteral ("constantTOKEN"); | |
186 | case LLT_ELSE: return cstring_makeLiteral ("elseTOKEN"); | |
187 | case LLT_ENSURES: return cstring_makeLiteral ("ensuresTOKEN"); | |
188 | case LLT_IF: return cstring_makeLiteral ("ifTOKEN"); | |
189 | case LLT_IMMUTABLE: return cstring_makeLiteral ("immutableTOKEN"); | |
190 | case LLT_OBJ: return cstring_makeLiteral ("objTOKEN"); | |
191 | case LLT_IMPORTS: return cstring_makeLiteral ("importsTOKEN"); | |
192 | case LLT_CONSTRAINT: return cstring_makeLiteral ("constraintTOKEN"); | |
193 | case LLT_LET: return cstring_makeLiteral ("letTOKEN"); | |
194 | case LLT_MODIFIES: return cstring_makeLiteral ("modifiesTOKEN"); | |
195 | case LLT_CLAIMS: return cstring_makeLiteral ("claimsTOKEN"); | |
196 | case LLT_MUTABLE: return cstring_makeLiteral ("mutableTOKEN"); | |
197 | case LLT_FRESH: return cstring_makeLiteral ("freshTOKEN"); | |
198 | case LLT_NOTHING: return cstring_makeLiteral ("nothingTOKEN"); | |
199 | case LLT_PRIVATE: return cstring_makeLiteral ("privateTOKEN"); | |
200 | case LLT_SPEC: return cstring_makeLiteral ("specTOKEN"); | |
201 | case LLT_REQUIRES: return cstring_makeLiteral ("requiresTOKEN"); | |
202 | case LLT_BODY: return cstring_makeLiteral ("bodyTOKEN"); | |
203 | case LLT_RESULT: return cstring_makeLiteral ("resultTOKEN"); | |
204 | case LLT_SIZEOF: return cstring_makeLiteral ("sizeofTOKEN"); | |
205 | case LLT_THEN: return cstring_makeLiteral ("thenTOKEN"); | |
206 | case LLT_TYPE: return cstring_makeLiteral ("typeTOKEN"); | |
207 | case LLT_TYPEDEF: return cstring_makeLiteral ("typedefTOKEN"); | |
208 | case LLT_UNCHANGED: return cstring_makeLiteral ("unchangedTOKEN"); | |
209 | case LLT_USES: return cstring_makeLiteral ("usesTOKEN"); | |
210 | case LLT_CHAR: return cstring_makeLiteral ("charTOKEN"); | |
211 | case LLT_CONST: return cstring_makeLiteral ("constTOKEN"); | |
212 | case LLT_DOUBLE: return cstring_makeLiteral ("doubleTOKEN"); | |
213 | case LLT_ENUM: return cstring_makeLiteral ("enumTOKEN"); | |
214 | case LLT_FLOAT: return cstring_makeLiteral ("floatTOKEN"); | |
215 | case LLT_INT: return cstring_makeLiteral ("intTOKEN"); | |
216 | case LLT_LONG: return cstring_makeLiteral ("longTOKEN"); | |
217 | case LLT_SHORT: return cstring_makeLiteral ("shortTOKEN"); | |
218 | case LLT_STRUCT: return cstring_makeLiteral ("structTOKEN"); | |
219 | case LLT_SIGNED: return cstring_makeLiteral ("signedTOKEN"); | |
220 | case LLT_UNION: return cstring_makeLiteral ("unionTOKEN"); | |
221 | case LLT_UNKNOWN: return cstring_makeLiteral ("unknownTOKEN"); | |
222 | case LLT_UNSIGNED: return cstring_makeLiteral ("unsignedTOKEN"); | |
223 | case LLT_VOID: return cstring_makeLiteral ("voidTOKEN"); | |
224 | case LLT_VOLATILE: return cstring_makeLiteral ("volatileTOKEN"); | |
225 | case LLT_TELIPSIS: return cstring_makeLiteral ("elipsisTOKEN"); | |
226 | case LLT_ITER: return cstring_makeLiteral ("iterTOKEN"); | |
227 | case LLT_YIELD: return cstring_makeLiteral ("yieldTOKEN"); | |
228 | default: return cstring_makeLiteral ("*** invalid token code ***"); | |
229 | } /* end switch */ | |
230 | } | |
231 | ||
232 | cstring ltoken_unparseCodeName (ltoken tok) | |
233 | { | |
234 | return LCLTokenCode_unparseCodeName (ltoken_getCode (tok)); | |
235 | } | |
236 | ||
237 | /*@observer@*/ cstring ltoken_unparse (ltoken s) | |
238 | { | |
239 | if (ltoken_isValid (s)) | |
240 | { | |
241 | return (lsymbol_toString (s->text)); | |
242 | } | |
243 | else | |
244 | { | |
245 | return cstring_undefined; | |
246 | } | |
247 | } | |
248 | ||
249 | ltoken ltoken_copy (ltoken tok) | |
250 | { | |
251 | if (ltoken_isValid (tok)) | |
252 | { | |
253 | ltoken ret = (ltoken) dmalloc (sizeof (*ret)); | |
254 | ||
255 | ret->code = tok->code; | |
256 | ret->text = tok->text; | |
257 | ret->fname = tok->fname; | |
258 | ret->line = tok->line; | |
259 | ret->col = tok->col; | |
260 | ret->rawText = tok->rawText; | |
261 | ret->defined = tok->defined; | |
262 | ret->hasSyn = tok->hasSyn; | |
263 | ret->idtype = tok->idtype; | |
264 | ret->intfield = tok->intfield; | |
265 | ||
266 | return ret; | |
267 | } | |
268 | else | |
269 | { | |
270 | return ltoken_undefined; | |
271 | } | |
272 | } | |
273 | ||
274 | lsymbol ltoken_getRawText (ltoken tok) | |
275 | { | |
276 | if (ltoken_isValid (tok)) | |
277 | { | |
278 | lsymbol ret = tok->rawText; | |
279 | ||
280 | if (lsymbol_isUndefined (ret)) | |
281 | { | |
282 | ret = tok->text; | |
283 | } | |
284 | ||
285 | return ret; | |
286 | } | |
287 | else | |
288 | { | |
289 | return lsymbol_undefined; | |
290 | } | |
291 | } | |
292 | ||
293 | /*@only@*/ cstring ltoken_unparseLoc (ltoken t) | |
294 | { | |
295 | if (ltoken_getCode (t) != NOTTOKEN) | |
296 | { | |
28bf4b0b | 297 | cstring res = fileloc_unparseRawCol (ltoken_fileName (t), |
298 | ltoken_getLine (t), | |
299 | ltoken_getCol (t)); | |
300 | return res; | |
616915dd | 301 | } |
302 | else | |
303 | { | |
304 | return cstring_makeLiteral ("*** Not Token ***"); | |
305 | } | |
306 | } | |
307 | ||
308 | void ltoken_markOwned (/*@owned@*/ ltoken tok) | |
309 | { | |
310 | sfreeEventually (tok); | |
311 | } | |
312 | ||
313 | void ltoken_free (/*@only@*/ ltoken tok) | |
314 | { | |
315 | sfree (tok); | |
316 | } | |
317 | ||
318 | bool ltoken_isSingleChar (char c) | |
319 | { | |
320 | return (LCLScanCharClass (c) == SINGLECHAR); | |
321 | } |