/*;-*-C-*-;
-** Copyright (c) Massachusetts Institute of Technology 1994-1998.
-** All Rights Reserved.
-** Unpublished rights reserved under the copyright laws of
-** the United States.
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
+** Massachusetts Institute of Technology
**
-** THIS MATERIAL IS PROVIDED AS IS, WITH ABSOLUTELY NO WARRANTY EXPRESSED
-** OR IMPLIED. ANY USE IS AT YOUR OWN RISK.
+** This program is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by the
+** Free Software Foundation; either version 2 of the License, or (at your
+** option) any later version.
+**
+** This program is distributed in the hope that it will be useful, but
+** WITHOUT ANY WARRANTY; without even the implied warranty of
+** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+** General Public License for more details.
+**
+** The GNU General Public License is available from http://www.gnu.org/ or
+** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+** MA 02111-1307, USA.
**
-** This code is distributed freely and may be used freely under the
-** following conditions:
-**
-** 1. This notice may not be removed or altered.
+** For information on splint: splint@cs.virginia.edu
+** To report a bug: splint-bug@cs.virginia.edu
+** For more information: http://www.splint.org
+*/
+/*
+** cscanner.l
**
-** 2. Works derived from this code are not distributed for
-** commercial gain without explicit permission from MIT
-** (for permission contact lclint-request@sds.lcs.mit.edu).
+** Flex lexer for C.
+** Based on a C lexer by Nate Osgood
+** from hacrat@catfish.lcs.mit.edu Mon Jun 14 13:06:32 1993
*/
/*
- * Modified by Herbert 08/19/97:
- * - added #include for IBM's OS/2 compiler.
- * - fixed weird bug with lookup of tmp files (OS/2 and MSDOS only).
- */
-
+** Modified by Herbert 08/19/97:
+** - added #include for IBM's OS/2 compiler.
+** - fixed weird bug with lookup of tmp files (OS/2 and MSDOS only).
+*/
/*
- * Modified by Mike Smith
- * Corrected missing 'line' in scanf() calls in handleSpecial().
- * Without this, I get an error when LCLint hits a '#line' directive
- * in the pre-pre-processed source files. For safety, I have made these
- * conditional on OS2 and MSDOS because I don't understand why noone else
- * has seen this problem.
- *
- * Modified by Mike Smith, 4th June 1997
- * Finally resolved the #line problem. The scanf() calls have been fixed to
- * allow the following #line forms:-
- *
- * #line 123 "filename"
- * #line 123
- * # 123 "filename"
- * # 123
- *
- * The last two are generated by the GNU pre-processor, apparently
- */
+** Modified by Mike Smith
+** Corrected missing 'line' in scanf() calls in handleSpecial().
+** Without this, I get an error when Splint hits a '#line' directive
+** in the pre-pre-processed source files. For safety, I have made these
+** conditional on OS2 and MSDOS because I don't understand why noone else
+** has seen this problem.
+**
+** Modified by Mike Smith, 4th June 1997
+** Finally resolved the #line problem. The scanf() calls have been fixed to
+** allow the following #line forms:-
+**
+** #line 123 "filename"
+** #line 123
+** # 123 "filename"
+** # 123
+**
+** The last two are generated by the GNU pre-processor, apparently
+*/
Digit [0-9]
Letter [a-zA-Z_$]
ULSuffix ({U}{L}|{L}{U})
%{
-/*
-** based on original C lexer by Nate Osgood
-** from hacrat@catfish.lcs.mit.edu Mon Jun 14 13:06:32 1993
-**
-*/
-
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# if defined(OS2) && defined(__IBMC__)
/* needed for isatty()... */
# include <io.h>
# else
+
+/*
+** Win32 doesn't have unistd.h
+*/
+
+# ifndef WIN32
# include <unistd.h>
# endif
+# endif
+
# include "basic.h"
# include "cgrammar.h"
static int ninput (void);
static char processChar (void);
static double processFloat (void);
-static /*@only@*/ exprNode processString (void);
+static /*@only@*/ exprNode processString (void) ;
+static /*@only@*/ exprNode processWideString (void) ;
static long processDec (void);
static long processHex (void);
static long processOctal (void);
"static" { setTokLength (6); RETURN_TOK (QSTATIC); }
\"(\\.|[^\\"])*\"([ \t\n]*\"(\\.|[^\\"])*\")* { RETURN_EXPR (processString ()); }
-L\"(\\.|[^\\"])*\"([ \t\n]*\"(\\.|[^\\"])*\")* { RETURN_EXPR (processString ()); }
+L\"(\\.|[^\\"])*\"([ \t\n]*\"(\\.|[^\\"])*\")* { RETURN_EXPR (processWideString ()); }
"out" { return (processSpec (QOUT)); }
"in" { return (processSpec (QIN)); }
"partial" { return (processSpec (QPARTIAL)); }
"isnull" { return (processSpec (QISNULL)); }
"truenull" { return (processSpec (QTRUENULL)); }
"falsenull" { return (processSpec (QFALSENULL)); }
+"nullwhentrue" { return (processSpec (QTRUENULL)); }
+"nullwhenfalse" { return (processSpec (QFALSENULL)); }
"relnull" { return (processSpec (QRELNULL)); }
"reldef" { return (processSpec (QRELDEF)); }
"exposed" { return (processSpec (QEXPOSED)); }
if (processMacro ())
{
+ DPRINTF (("Here we are: %s", context_unparse ()));
+
if (context_inIterDef ())
{
RETURN_TOK (LLMACROITER);
{ "testinRange", QTESTINRANGE},
{ "requires", QPRECLAUSE } ,
{ "ensures", QPOSTCLAUSE } ,
+ { "invariant", QINVARIANT} ,
{ NULL, BADTOK }
} ;
{ "special", QSPECIAL } ,
{ "truenull", QTRUENULL } ,
{ "falsenull", QFALSENULL } ,
+ { "nullwhentrue", QTRUENULL } ,
+ { "falsewhennull", QFALSENULL } ,
{ "keep", QKEEP } ,
{ "kept", QKEPT } ,
{ "notnull", QNOTNULL } ,
{ "reldef", QRELDEF } ,
{ "observer", QOBSERVER } ,
{ "exits", QEXITS } ,
+ { "noreturn", QEXITS } ,
{ "mayexit", QMAYEXIT } ,
+ { "maynotreturn", QMAYEXIT } ,
{ "trueexit", QTRUEEXIT } ,
{ "falseexit", QFALSEEXIT } ,
+ { "noreturnwhentrue", QTRUEEXIT } ,
+ { "noreturnwhenfalse", QFALSEEXIT } ,
{ "neverexit", QNEVEREXIT } ,
+ { "alwaysreturns", QNEVEREXIT } ,
{ "temp", QTEMP } ,
{ "shared", QSHARED } ,
{ "ref", QREF } ,
voptgenerror
(FLG_WARNLINTCOMMENTS,
cstring_makeLiteral
- ("Traditional lint comment /*FALLTHROUGH*/ used. "
- "This is interpreted by "
- "LCLint in the same way as most Unix lints, but it is "
+ ("Traditional lint comment /*FALLTHROUGH*/ used. "
+ "Splint interprets this in the same way as most Unix lints, but it is "
"preferable to replace it with the /*@fallthrough@*/ "
"semantic comment"),
g_currentloc);
voptgenerror
(FLG_WARNLINTCOMMENTS,
cstring_makeLiteral
- ("Traditional lint comment /*FALLTHRU*/ used. "
- "This is interpreted by "
- "LCLint in the same way as most Unix lints, but it is "
+ ("Traditional lint comment /*FALLTHRU*/ used. "
+ "Splint interprets this in the same way as most Unix lints, but it is "
"preferable to replace it with the /*@fallthrough@*/ "
"semantic comment"),
g_currentloc);
voptgenerror
(FLG_WARNLINTCOMMENTS,
cstring_makeLiteral
- ("Traditional lint comment /*NOTREACHED*/ used. "
- "This is interpreted by "
- "LCLint in the same way as most Unix lints, but it is "
+ ("Traditional lint comment /*NOTREACHED*/ used. "
+ "Splint interprets this in the same way as most Unix lints, but it is "
"preferable to replace it with the /*@notreached@*/ "
"semantic comment."),
g_currentloc);
voptgenerror
(FLG_WARNLINTCOMMENTS,
cstring_makeLiteral
- ("Traditional lint comment /*PRINTFLIKE*/ used. "
- "This is interpreted by "
- "LCLint in the same way as most Unix lints, but it is "
+ ("Traditional lint comment /*PRINTFLIKE*/ used. "
+ "Splint interprets this in the same way as most Unix lints, but it is "
"preferable to replace it with either /*@printflike@*/, "
"/*@scanflike@*/ or /*@messagelike@*/."),
g_currentloc);
voptgenerror
(FLG_WARNLINTCOMMENTS,
cstring_makeLiteral
- ("Traditional lint comment /*ARGSUSED*/ used. "
- "This is interpreted by "
- "LCLint in the same way as most Unix lints, but it is "
+ ("Traditional lint comment /*ARGSUSED*/ used. "
+ "Splint interprets this in the same way as most Unix lints, but it is "
"preferable to use /*@unused@*/ annotations on "
"the unused parameters."),
g_currentloc);
static bool handleSpecial (char *yyt)
{
char *l = mstring_create (MAX_NAME_LENGTH);
- static bool reportcpp = FALSE;
int lineno = 0;
char c;
char *ol;
cstring olc;
-
- strcpy (l, yyt + 1);
- /* Need to safe original l for deallocating. */
- ol = l;
+ int len_yyt;
+
+ len_yyt = strlen (yyt +1) ;
- l += strlen (yyt) - 1;
+ l = mstring_copy (yyt + 1);
while ((c = char_fromInt (lminput ())) != '\n' && c != '\0')
{
- *l++ = c;
+ l = mstring_append(l, c);
}
- *l = '\0';
+ /* Need to safe original l for deallocating. */
+ ol = l;
+
+ l += strlen (l);
+
olc = cstring_fromChars (ol);
if (cstring_equalPrefixLit (olc, "pragma"))
mstring_free (ol);
return FALSE;
} else {
- if (!reportcpp)
- {
-
- } else {
- llbug (message ("File contains preprocessor command: #%s",
- cstring_fromChars (ol)));
- reportcpp = TRUE;
- }
+ voptgenerror
+ (FLG_UNRECOGDIRECTIVE,
+ message ("Unrecognized pre-processor directive: #%s",
+ cstring_fromChars (ol)),
+ g_currentloc);
}
sfree (ol);
- return TRUE;
+ return FALSE; /* evans 2001-12-30: was: TRUE; */
}
sfree (ol);
(FLG_SYNTAX,
message ("Likely parse error: syntactic comment token spans multiple lines: %s",
cstring_fromChars (s)),
- g_currentloc);
+ loc);
}
s = mstring_append (s, c);
if (!context_getFlag (FLG_NOCOMMENTS))
{
cstring flagname = thisflag;
- flagcode fflag = identifyFlag (flagname);
-
+ flagcode fflag = flags_identifyFlag (flagname);
+
if (flagcode_isSkip (fflag))
{
;
(FLG_UNRECOGFLAGCOMMENTS,
message ("Unrecognized option in semantic comment: %s",
flagname),
- g_currentloc);
+ loc);
}
}
else if (flagcode_isGlobalFlag (fflag))
("Semantic comment attempts to set global flag %s. "
"A global flag cannot be set locally.",
flagname),
- g_currentloc);
+ loc);
}
else
{
- context_fileSetFlag (fflag, set);
+ context_fileSetFlag (fflag, set, loc);
if (flagcode_hasArgument (fflag))
{
("Semantic comment attempts to restore flag %s. "
"A flag for setting a value cannot be restored.",
flagname),
- g_currentloc);
+ loc);
}
else
{ /* cut-and-pastied from llmain...blecch */
{
s--;
- if (flagcode_hasValue (fflag))
+ if (flagcode_hasNumber (fflag))
+ {
+ setValueFlag (fflag, extra);
+ }
+ else if (flagcode_hasChar (fflag))
{
setValueFlag (fflag, extra);
}
if (context_inHeader () && !isArtificial (cstring_fromChars (os)))
{
DPRINTF (("Here adding comment: %s", os));
- context_addComment (cstring_fromCharsNew (os));
+ context_addComment (cstring_fromCharsNew (os), loc);
}
else
{
&& macrocode != SKIPTOK
&& !isArtificial (cstring_fromChars (os)))
{
- DPRINTF (("Add comment: %s", os));
- context_addComment (cstring_fromCharsNew (os));
+ if (context_processingMacros ())
+ {
+ /* evans 2002-02-24: don't add comments when procssing macros */
+ }
+ else
+ {
+ context_addComment (cstring_fromCharsNew (os), loc);
+ }
}
else
{
{
if (!context_getFlag (FLG_NOCOMMENTS))
{
- context_enterSuppressRegion ();
+ context_enterSuppressRegion (loc);
}
}
else if ((*t == 'i' || *t == 't')
if (!context_getFlag (FLG_NOCOMMENTS)
&& (*t == 'i' || context_getFlag (FLG_TMPCOMMENTS)))
{
- context_enterSuppressLine (-1); /* infinite suppression */
+ context_enterSuppressLine (-1, loc); /* infinite suppression */
}
}
else if (((*t == 'i') || (*t == 't'))
lc = *(++tt);
}
}
-
if (!context_getFlag (FLG_NOCOMMENTS)
&& (!tmpcomment || context_getFlag (FLG_TMPCOMMENTS)))
{
- context_enterSuppressLine (val);
+ DPRINTF (("Here: enter suppress: %s", fileloc_unparse (loc)));
+ context_enterSuppressLine (val, loc);
}
}
else if (mstring_equal (t, "end"))
{
if (!context_getFlag (FLG_NOCOMMENTS))
{
- context_exitSuppressRegion ();
+ context_exitSuppressRegion (loc);
}
}
else if (mstring_equal (t, "notfunction"))
message
("Non-abstract type %s used in access comment",
tname),
- g_currentloc);
+ loc);
}
}
else
{
if (!(context_inSuppressRegion ()
- || context_inSuppressZone (g_currentloc)))
+ || context_inSuppressZone (loc)))
{
voptgenerror
(FLG_COMMENTERROR,
message
("Unrecognized type %s used in access comment",
tname),
- g_currentloc);
+ loc);
}
}
}
else
{
if (!(context_inSuppressRegion ()
- || context_inSuppressZone (g_currentloc)))
+ || context_inSuppressZone (loc)))
{
uentry ue = usymtab_getTypeEntry (tuid);
message
("Non-accessible abstract type %s used in noaccess comment",
tname),
- g_currentloc);
+ loc);
}
else
{
message
("Non-abstract type %s used in noaccess comment",
tname),
- g_currentloc);
+ loc);
}
}
}
else
{
if (!(context_inSuppressRegion ()
- || context_inSuppressZone (g_currentloc)))
+ || context_inSuppressZone (loc)))
{
voptgenerror
(FLG_COMMENTERROR,
message
("Unrecognized type %s used in noaccess comment",
tname),
- g_currentloc);
+ loc);
}
}
}
{
voptgenerror (FLG_UNRECOGCOMMENTS,
message ("Semantic comment unrecognized: %s",
- cstring_fromChars (os)), loc);
+ cstring_fromChars (os)),
+ loc);
}
-
+
sfree (t);
}
{
tok = CALIGNOF; /* alignof is parsed like sizeof */
}
+ else if (cstring_equalLit (id, "__typeof__"))
+ {
+ tok = CTYPEOF;
+ }
+ else if (cstring_equalLit (id, "typeof"))
+ {
+ tok = CTYPEOF;
+ }
else if (cstring_equalLit (id, "__FUNCTION__")
|| cstring_equalLit (id, "__PRETTY_FUNCTION__"))
{
/* These tokens hold the name of the current function as strings */
- yylval.expr = exprNode_stringLiteral (id, fileloc_copy (g_currentloc));
+ /* evans 2001-12-30: changed from exprNode_stringLiteral; bug reported by Jim Zelenka. */
+ yylval.expr = exprNode_makeConstantString (id, fileloc_copy (g_currentloc));
tokLength = 0;
lastWasString = TRUE;
tok = CCONSTANT;
}
else
{
+ /*
+ ** Will be handled by handleLlSpecial
+ */
+
cstring_free (id);
return FALSE;
}
return (res);
}
+/*
+** process a wide character string L"...."
+*/
+
+static /*@only@*/ exprNode processWideString ()
+{
+ exprNode res;
+ fileloc loc;
+ char *nl = strchr (yytext, '\n');
+ cstring ns;
+
+ llassert (*yytext == 'L');
+ yytext++;
+
+ ns = cstring_fromCharsNew (yytext);
+
+ if (nl == NULL)
+ {
+ loc = fileloc_copy (g_currentloc);
+ addColumn (cstring_length (ns));
+ }
+ else
+ {
+ char *lastnl = nl;
+
+ loc = fileloc_copy (g_currentloc);
+
+ context_incLineno ();
+
+ while ((nl = strchr ((nl + 1), '\n')) != NULL)
+ {
+ context_incLineno ();
+ lastnl = nl;
+ }
+ }
+
+ res = exprNode_wideStringLiteral (ns, loc);
+ return (res);
+}
+
static
char processChar ()
{
andersk / splint.git / blobdiff