2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 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: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
28 # include "splintMacros.nf"
30 # include "llgrammar.h"
31 # include "lslscanline.h"
32 # include "lclscanline.h"
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
40 /*@-namechecks@*/ /* These should all start with g_ */
48 ltoken ltoken_implies
;
62 ltoken ltoken_comment
;
64 ltoken ltoken_compose
;
67 ltoken ltoken_typename
;
70 ltoken ltoken_lbracked
;
71 ltoken ltoken_rbracket
;
74 static /*@notnull@*/ ltoken
ltoken_new (void)
76 ltoken tok
= (ltoken
) dmalloc (sizeof (*tok
));
81 tok
->text
= lsymbol_undefined
;
82 tok
->fname
= lsymbol_undefined
;
83 tok
->rawText
= lsymbol_undefined
;
90 ltoken
ltoken_create (ltokenCode code
, lsymbol text
)
92 ltoken tok
= ltoken_new ();
100 ltoken
ltoken_createRaw (ltokenCode code
, lsymbol text
)
102 ltoken tok
= ltoken_new ();
110 ltoken
ltoken_createType (ltokenCode code
, SimpleIdCode idtype
, lsymbol text
)
112 ltoken tok
= ltoken_new ();
114 /* no...what's the real llassert (code == simpleId); */
117 tok
->idtype
= idtype
;
123 ltoken
ltoken_createFull (ltokenCode code
, lsymbol text
,
124 cstring file
, int line
,
127 ltoken tok
= (ltoken
) dmalloc (sizeof (*tok
));
131 tok
->fname
= lsymbol_fromString (file
);
134 tok
->rawText
= lsymbol_undefined
;
135 tok
->defined
= FALSE
;
141 static /*@only@*/ cstring
LCLTokenCode_unparseCodeName (ltokenCode t
)
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 ***");
232 cstring
ltoken_unparseCodeName (ltoken tok
)
234 return LCLTokenCode_unparseCodeName (ltoken_getCode (tok
));
237 /*@observer@*/ cstring
ltoken_unparse (ltoken s
)
239 if (ltoken_isValid (s
))
241 return (lsymbol_toString (s
->text
));
245 return cstring_undefined
;
249 ltoken
ltoken_copy (ltoken tok
)
251 if (ltoken_isValid (tok
))
253 ltoken ret
= (ltoken
) dmalloc (sizeof (*ret
));
255 ret
->code
= tok
->code
;
256 ret
->text
= tok
->text
;
257 ret
->fname
= tok
->fname
;
258 ret
->line
= tok
->line
;
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
;
270 return ltoken_undefined
;
274 lsymbol
ltoken_getRawText (ltoken tok
)
276 if (ltoken_isValid (tok
))
278 lsymbol ret
= tok
->rawText
;
280 if (lsymbol_isUndefined (ret
))
289 return lsymbol_undefined
;
293 /*@only@*/ cstring
ltoken_unparseLoc (ltoken t
)
295 if (ltoken_getCode (t
) != NOTTOKEN
)
297 cstring res
= fileloc_unparseRawCol (ltoken_fileName (t
),
304 return cstring_makeLiteral ("*** Not Token ***");
308 void ltoken_markOwned (/*@owned@*/ ltoken tok
)
310 sfreeEventually (tok
);
313 void ltoken_free (/*@only@*/ ltoken tok
)
318 bool ltoken_isSingleChar (char c
)
320 return (LCLScanCharClass (c
) == SINGLECHAR
);