/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
*/
/*
** llmain.c
**
-** Main module for LCLint checker
+** Main module for Splint annotation-assisted program checker
*/
# include <signal.h>
# include <process.h>
# endif
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "llbasic.h"
# include "osd.h"
# include "imports.h"
# endif
-# include "version.h"
+# include "Headers/version.h" /* Visual C++ finds the wrong version.h */
# include "fileIdList.h"
# include "lcllib.h"
# include "cgrammar.h"
static void showHelp (void);
static void interrupt (int p_i);
+static bool readOptionsFile (cstring p_fname,
+ cstringSList *p_passThroughArgs,
+ bool p_report)
+ /*@modifies fileSystem, internalState, *p_passThroughArgs@*/ ;
+
static void loadrc (FILE *p_rcfile, cstringSList *p_passThroughArgs)
- /*@ensures closed p_rcfile@*/ ;
+ /*@modifies *p_passThroughArgs, p_rcfile@*/
+ /*@ensures closed p_rcfile@*/ ;
static void describeVars (void);
static bool specialFlagsHelp (char *p_next);
static fileIdList preprocessFiles (fileIdList, bool)
/*@modifies fileSystem@*/ ;
+static void warnSysFiles(fileIdList p_files) /*@modifies fileSystem@*/;
+
# ifndef NOLCL
static
fileIdList_elements (lclfiles, fid)
{
cstring actualName = cstring_undefined;
- cstring fname = fileName (fid);
+ cstring fname = fileTable_fileName (fid);
if (osd_getPath (cstring_fromChars (g_localSpecPath),
fname, &actualName) == OSD_FILENOTFOUND)
{
if (mstring_equal (g_localSpecPath, "."))
{
- lldiagmsg (message ("Spec file not found: %s", fname));
+ lldiagmsg (message ("Spec file not found: %q", osd_outputPath (fname)));
}
else
{
- lldiagmsg (message ("Spec file not found: %s (on %s)",
- fname,
+ lldiagmsg (message ("Spec file not found: %q (on %s)",
+ osd_outputPath (fname),
cstring_fromChars (g_localSpecPath)));
}
}
setSpecFileId (fid);
- if (context_getFlag (FLG_SHOWSCAN))
- {
- lldiagmsg (message ("< reading spec %s >", g_currentSpec));
- }
+ displayScan (message ("reading spec %s", g_currentSpec));
- /* Open source file */
+ /* Open the source file */
if (!inputStream_open (specFile))
{
- lldiagmsg (message ("Cannot open file: %s",
- inputStream_fileName (specFile)));
+ lldiagmsg (message ("Cannot open file: %q",
+ osd_outputPath (inputStream_fileName (specFile))));
inputStream_free (specFile);
}
else
void showHerald (void)
{
- if (hasShownHerald || context_getFlag (FLG_QUIET)) return;
-
+ if (hasShownHerald || context_getFlag (FLG_QUIET))
+ {
+ return;
+ }
else
{
- fprintf (g_msgstream, "%s\n\n", LCL_VERSION);
+ fprintf (g_messagestream, "%s\n\n", SPLINT_VERSION);
hasShownHerald = TRUE;
llflush ();
}
}
-static void addFile (fileIdList files, /*@only@*/ cstring s)
+static cstring findLarchPathFile (/*@temp@*/ cstring s)
{
- if (fileTable_exists (context_fileTable (), s))
+ cstring pathName;
+ filestatus status;
+
+ status = osd_getPath (context_getLarchPath (), s, &pathName);
+
+ if (status == OSD_FILEFOUND)
+ {
+ return pathName;
+ }
+ else if (status == OSD_FILENOTFOUND)
{
showHerald ();
- lldiagmsg (message ("File listed multiple times: %s", s));
- cstring_free (s);
+ lldiagmsg (message ("Cannot find file on LARCH_PATH: %s", s));
+ }
+ else if (status == OSD_PATHTOOLONG)
+ {
+ /* Directory and filename are too long. Report error. */
+ llbuglit ("soure_getPath: Filename plus directory from search path too long");
}
else
{
- fileIdList_add (files, fileTable_addFileOnly (context_fileTable (), s));
+ BADBRANCH;
}
+
+ return cstring_undefined;
}
-static void addXHFile (fileIdList files, /*@only@*/ cstring s)
+static void addLarchPathFile (fileIdList files, /*@temp@*/ cstring s)
+{
+ cstring pathName = findLarchPathFile (s);
+
+ if (cstring_isDefined (pathName))
+ {
+ if (fileTable_exists (context_fileTable (), pathName))
+ {
+ showHerald ();
+ lldiagmsg (message ("File listed multiple times: %s", pathName));
+ cstring_free (pathName);
+ }
+ else
+ {
+ fileIdList_add (files, fileTable_addFileOnly (context_fileTable (), pathName));
+ }
+ }
+}
+
+static void addFile (fileIdList files, /*@only@*/ cstring s)
{
if (fileTable_exists (context_fileTable (), s))
{
}
else
{
- fileIdList_add (files, fileTable_addXHFile (context_fileTable (), s));
- cstring_free (s);
+ fileIdList_add (files, fileTable_addFileOnly (context_fileTable (), s));
+ }
+}
+
+static void addXHFile (fileIdList files, /*@temp@*/ cstring s)
+{
+ cstring pathName = findLarchPathFile (s);
+
+ if (cstring_isDefined (pathName))
+ {
+ if (fileTable_exists (context_fileTable (), pathName))
+ {
+ showHerald ();
+ lldiagmsg (message ("File listed multiple times: %s", s));
+ }
+ else
+ {
+ fileIdList_add (files, fileTable_addXHFile (context_fileTable (), pathName));
+ }
}
+
+ cstring_free (pathName);
}
/*
-** Disable MSVC++ warning about return value. Methinks humbly lclint control
+** Disable MSVC++ warning about return value. Methinks humbly splint control
** comments are a mite more legible.
*/
# ifdef NOLCL
/*@globals killed undef g_currentloc,
killed undef yyin,
- undef g_msgstream;
+ undef g_warningstream, g_messagestream, g_errorstream;
@*/
/*@modifies g_currentloc, fileSystem,
yyin;
killed undef g_currentSpec,
killed undef g_currentSpecName,
killed undef yyin,
- undef g_msgstream;
+ undef g_warningstream, g_messagestream, g_errorstream;
@*/
/*@modifies g_currentloc, initFile,
g_localSpecPath, g_currentSpec, g_currentSpecName, fileSystem,
# endif
{
bool first_time = TRUE;
- bool showhelp = FALSE;
- bool allhelp = TRUE;
bool expsuccess;
inputStream sourceFile = inputStream_undefined;
_wildcard (&argc, &argv);
# endif
- g_msgstream = stdout;
+ g_warningstream = stdout;
+ g_messagestream = stderr;
+ g_errorstream = stderr;
(void) signal (SIGINT, interrupt);
(void) signal (SIGSEGV, interrupt);
clabstract_initMod ();
typeIdSet_initMod ();
cppReader_initMod ();
+ osd_initMod ();
+
setCodePoint ();
g_currentloc = fileloc_createBuiltin ();
-
+
before = clock ();
context_initMod ();
if (argc <= 1)
{
showHelp ();
- llexit (LLGIVEUP);
+ llexit (LLSUCCESS);
+ }
+
+ /* -help must be the first flag to get help */
+ if (flagcode_isHelpFlag (flags_identifyFlag (argv[1])))
+ {
+ flags_processHelp (argc - 1, argv + 1);
+ llexit (LLSUCCESS);
}
setCodePoint ();
{
/* Put C_INCLUDE_PATH directories in sysdirs */
cstring cincval = osd_getEnvironmentVariable (cstring_makeLiteralTemp ("C_INCLUDE_PATH"));
+
if (cstring_isDefined (cincval))
{
context_setString (FLG_SYSTEMDIRS, cstring_copy (cincval));
{
cstring home = osd_getHomeDir ();
- char *fname = NULL;
- FILE *rcfile;
+ cstring fname = cstring_undefined;
bool defaultf = TRUE;
bool nof = FALSE;
if (*thisarg == '-' || *thisarg == '+')
{
+ bool set = (*thisarg == '+');
+ flagcode opt;
+
thisarg++;
- if (mstring_equal (thisarg, "nof"))
+ /*
+ ** Don't report warnings this time
+ */
+
+ opt = flags_identifyFlagQuiet (cstring_fromChars (thisarg));
+
+ if (opt == FLG_NOF)
{
nof = TRUE;
}
- else if (mstring_equal (thisarg, "f"))
+ else if (flagcode_isMessageControlFlag (opt))
{
- if (++i < argc)
- {
- defaultf = FALSE;
- fname = argv[i];
- rcfile = fileTable_openFile (context_fileTable (), cstring_fromChars (fname), "r");
+ /*
+ ** Need to set it immediately, so rc file scan is displayed
+ */
+
+ context_userSetFlag (opt, set);
- if (rcfile != NULL)
+ if (flagcode_hasArgument (opt))
+ {
+ llassert (flagcode_hasString (opt));
+
+ if (++i < argc)
{
- fileloc oloc = g_currentloc;
-
- g_currentloc = fileloc_createRc (cstring_fromChars (fname));
- loadrc (rcfile, &passThroughArgs);
- fileloc_reallyFree (g_currentloc);
- g_currentloc = oloc;
+ fname = cstring_fromChars (argv[i]);
+ setStringFlag (opt, fname);
}
- else
+ else
{
- showHerald ();
- lldiagmsg (message ("Options file not found: %s",
- cstring_fromChars (fname)));
+ llfatalerror
+ (message
+ ("Flag %s must be followed by a string",
+ flagcode_unparse (opt)));
}
}
+ }
+ else if (opt == FLG_OPTF)
+ {
+ if (++i < argc)
+ {
+ defaultf = FALSE;
+ fname = cstring_fromChars (argv[i]);
+ (void) readOptionsFile (fname, &passThroughArgs, TRUE);
+ }
else
llfatalerror
(cstring_makeLiteral ("Flag f to select options file "
}
}
}
-
- if (fname == NULL)
- {
- if (!cstring_isEmpty (home)) {
- fname = cstring_toCharsSafe (message ("%s%h%s", home, CONNECTCHAR,
- cstring_fromChars (RCFILE)));
- mstring_markFree (fname);
- }
- }
-
+
setCodePoint ();
if (!nof && defaultf)
{
- if (!mstring_isEmpty (fname)) {
- rcfile = fileTable_openFile (context_fileTable (), cstring_fromChars (fname), "r");
-
- if (rcfile != NULL)
- {
- fileloc oloc = g_currentloc;
-
- g_currentloc = fileloc_createRc (cstring_fromChars (fname));
- loadrc (rcfile, &passThroughArgs);
- fileloc_reallyFree (g_currentloc);
- g_currentloc = oloc;
- }
- }
-
-# if defined(MSDOS) || defined(OS2)
- fname = cstring_toCharsSafe (message ("%s",
- cstring_fromChars (RCFILE)));
-# else
- fname = cstring_toCharsSafe (message ("./%s",
- cstring_fromChars (RCFILE)));
-# endif
-
- rcfile = fileTable_openFile (context_fileTable (), cstring_fromChars (fname), "r");
+ /*
+ ** No explicit rc file, first try reading ~/.splintrc
+ */
- if (rcfile != NULL)
+ if (cstring_isUndefined (fname))
{
- fileloc oloc = g_currentloc;
+ if (!cstring_isEmpty (home))
+ {
+ bool readhomerc, readaltrc;
+ cstring homename, altname;
+
+ homename = message ("%s%h%s", home, CONNECTCHAR,
+ cstring_fromChars (RCFILE));
+ readhomerc = readOptionsFile (homename, &passThroughArgs, FALSE);
+
+ /*
+ ** Try ~/.splintrc also for historical accuracy
+ */
+
+ altname = message ("%s%h%s", home, CONNECTCHAR,
+ cstring_fromChars (ALTRCFILE));
+ readaltrc = readOptionsFile (altname, &passThroughArgs, FALSE);
+
+ if (readhomerc && readaltrc)
+ {
- g_currentloc = fileloc_createRc (cstring_fromChars (fname));
- loadrc (rcfile, &passThroughArgs);
- fileloc_reallyFree (g_currentloc);
- g_currentloc = oloc;
- }
+ voptgenerror
+ (FLG_WARNRC,
+ message ("Found both %s and %s files. Using both files, "
+ "but recommend using only %s to avoid confusion.",
+ homename, altname, homename),
+ g_currentloc);
+ }
- sfree (fname);
- }
- }
-
- setCodePoint ();
-
- for (i = 1; i < argc; i++)
- {
- char *thisarg;
- flagcode opt;
-
- thisarg = argv[i];
-
- if (showhelp)
+ cstring_free (homename);
+ cstring_free (altname);
+ }
+ }
+
+ /*
+ ** Next, read .splintrc in the current working directory
+ */
+
{
- if (allhelp)
- {
- showHerald ();
- }
+ cstring rcname = message ("%s%s",osd_getCurrentDirectory (), cstring_fromChars (RCFILE));
+ cstring altname = message ("%s%s",osd_getCurrentDirectory (), cstring_fromChars (ALTRCFILE));
+ bool readrc, readaltrc;
- allhelp = FALSE;
+ readrc = readOptionsFile (rcname, &passThroughArgs, FALSE);
+ readaltrc = readOptionsFile (altname, &passThroughArgs, FALSE);
- if (*thisarg == '-' || *thisarg == '+')
- {
- thisarg++; /* skip '-' */
- }
- if (mstring_equal (thisarg, "modes"))
- {
- llmsg (describeModes ());
- }
- else if (mstring_equal (thisarg, "vars")
- || mstring_equal (thisarg, "env"))
- {
- describeVars ();
- }
- else if (mstring_equal (thisarg, "annotations"))
- {
- printAnnotations ();
- }
- else if (mstring_equal (thisarg, "parseerrors"))
- {
- printParseErrors ();
- }
- else if (mstring_equal (thisarg, "comments"))
- {
- printComments ();
- }
- else if (mstring_equal (thisarg, "prefixcodes"))
- {
- describePrefixCodes ();
- }
- else if (mstring_equal (thisarg, "references")
- || mstring_equal (thisarg, "refs"))
- {
- printReferences ();
- }
- else if (mstring_equal (thisarg, "mail"))
- {
- printMail ();
- }
- else if (mstring_equal (thisarg, "maintainer")
- || mstring_equal (thisarg, "version"))
- {
- printMaintainer ();
- }
- else if (mstring_equal (thisarg, "flags"))
- {
- if (i + 1 < argc)
- {
- char *next = argv[i + 1];
-
- if (specialFlagsHelp (next))
- {
- i++;
- }
- else
- {
- flagkind k = identifyCategory (cstring_fromChars (next));
-
- if (k != FK_NONE)
- {
- printCategory (k);
- i++;
- }
- }
- }
- else
- {
- printFlags ();
- }
- }
- else
+ if (readrc && readaltrc)
{
- cstring s = describeFlag (cstring_fromChars (thisarg));
+ voptgenerror (FLG_WARNRC,
+ message ("Found both %s and %s files. Using both files, "
+ "but recommend using only %s to avoid confusion.",
+ rcname, altname, rcname),
+ g_currentloc);
- if (cstring_isDefined (s))
- {
- llmsg (s);
- }
}
- }
- else
- {
- if (*thisarg == '-' || *thisarg == '+')
- {
- bool set = (*thisarg == '+');
- cstring flagname;
-
- thisarg++; /* skip '-' */
- flagname = cstring_fromChars (thisarg);
- DPRINTF (("Flag: %s", flagname));
- opt = identifyFlag (flagname);
- DPRINTF (("Flag: %s", flagcode_unparse (opt)));
-
- if (flagcode_isSkip (opt))
- {
- DPRINTF (("Skipping!"));
- }
- else if (flagcode_isInvalid (opt))
- {
- DPRINTF (("Invalid: %s", flagname));
-
- if (isMode (flagname))
- {
- context_setMode (flagname);
- }
- else
- {
- DPRINTF (("Error!"));
- voptgenerror (FLG_BADFLAG,
- message ("Unrecognized option: %s",
- cstring_fromChars (thisarg)),
- g_currentloc);
- }
- }
- else
- {
- context_userSetFlag (opt, set);
-
- if (flagcode_hasArgument (opt))
- {
- if (opt == FLG_HELP)
- {
- showhelp = TRUE;
- }
- else if (flagcode_isPassThrough (opt)) /* -D or -U */
- {
- passThroughArgs = cstringSList_add
- (passThroughArgs, cstring_fromChars (thisarg));
- }
- else if (flagcode_hasValue (opt))
- {
- if (++i < argc)
- {
- setValueFlag (opt, cstring_fromChars (argv[i]));
- }
- else
- {
- llfatalerror
- (message
- ("Flag %s must be followed by a number",
- flagcode_unparse (opt)));
- }
- }
- else if (opt == FLG_INCLUDEPATH || opt == FLG_SPECPATH)
- {
- cstring dir = cstring_suffix (cstring_fromChars (thisarg), 1); /* skip over I */
-
- switch (opt)
- {
- case FLG_INCLUDEPATH:
- cppAddIncludeDir (dir);
- /*@switchbreak@*/ break;
- case FLG_SPECPATH:
- /*@-mustfree@*/
- g_localSpecPath = cstring_toCharsSafe
- (message ("%s%h%s",
- cstring_fromChars (g_localSpecPath),
- PATH_SEPARATOR,
- dir));
- /*@=mustfree@*/
- /*@switchbreak@*/ break;
- BADDEFAULT;
- }
- }
- else if (flagcode_hasString (opt)
- || opt == FLG_INIT || opt == FLG_OPTF)
- {
- if (++i < argc)
- {
- cstring arg = cstring_fromChars (argv[i]);
-
- if (opt == FLG_OPTF)
- {
- ; /* -f already processed */
- }
- else if (opt == FLG_INIT)
- {
-# ifndef NOLCL
- initFile = inputStream_create
- (arg,
- cstring_makeLiteralTemp (LCLINIT_SUFFIX),
- FALSE);
-# endif
- break;
- }
- else
- {
- DPRINTF (("String flag: %s / %s",
- flagcode_unparse (opt), arg));
- if (opt == FLG_MTSFILE)
- {
- /*
- ** arg identifies mts files
- */
-
- addFile (mtfiles, message ("%s%s", arg, MTS_EXTENSION));
- addXHFile (xfiles, message ("%s%s", arg, XH_EXTENSION));
- }
- else
- {
- setStringFlag (opt, arg);
- }
- }
- }
- else
- {
- llfatalerror
- (message
- ("Flag %s must be followed by a string",
- flagcode_unparse (opt)));
- }
- }
- else
- {
- /* no argument */
- }
- }
- }
- }
- else /* its a filename */
- {
- DPRINTF (("Adding filename: %s", thisarg));
- fl = cstringSList_add (fl, cstring_fromChars (thisarg));
- }
+ cstring_free (rcname);
+ cstring_free (altname);
}
- }
+ }
+ }
+
+ setCodePoint ();
- setCodePoint ();
+ /* argv[0] is the program name, don't pass it to flags_processFlags */
+ flags_processFlags (argc - 1, argv + 1);
+ showHerald ();
+
/*
** create lists of C and LCL files
*/
}
else if (cstring_equal (ext, XH_EXTENSION))
{
- addXHFile (xfiles, cstring_copy (current));
+ addXHFile (xfiles, current);
}
else if (cstring_equal (ext, PP_EXTENSION))
{
}
else if (cstring_equal (ext, MTS_EXTENSION))
{
- addFile (mtfiles, cstring_copy (current));
+ addLarchPathFile (mtfiles, current);
}
else
{
}
} end_cstringSList_elements;
- showHerald (); /*@i723 move earlier? */
-
if (showhelp)
{
if (allhelp)
{
showHelp ();
}
- fprintf (g_msgstream, "\n");
+ fprintf (g_warningstream, "\n");
fileIdList_free (cfiles);
fileIdList_free (xfiles);
{
cstring m = context_getMerge ();
- if (context_getFlag (FLG_SHOWSCAN))
- {
- fprintf (g_msgstream, "< loading %s ", cstring_toCharsSafe (m));
- }
-
+ displayScanOpen (message ("< loading %s ", m));
loadState (m);
-
- if (context_getFlag (FLG_SHOWSCAN))
- {
- fprintf (g_msgstream, " >\n");
- }
+ displayScanClose ();
if (!usymtab_existsType (context_getBoolName ()))
{
fileIdList_elements (mtfiles, mtfile)
{
context_setFileId (mtfile);
-
- if (context_getFlag (FLG_SHOWSCAN))
- {
- lldiagmsg (message ("< processing %s >", rootFileName (mtfile)));
- }
-
- mtreader_readFile (cstring_copy (fileName (mtfile)));
+ displayScan (message ("processing %s", fileTable_rootFileName (mtfile)));
+ mtreader_readFile (cstring_copy (fileTable_fileName (mtfile)));
} end_fileIdList_elements;
libtime = clock ();
if (anylcl)
{
# ifdef NOLCL
- llfatalerror (cstring_makeLiteral ("This version of LCLint does not handle LCL files."));
+ llfatalerror (cstring_makeLiteral ("This version of Splint does not handle LCL files."));
# else
lslProcess (lclfiles);
# endif
llflush ();
- if (context_getFlag (FLG_SHOWSCAN))
- {
- fprintf (stderr, "< preprocessing");
- }
+ displayScanOpen (cstring_makeLiteral ("preprocessing"));
lcltime = clock ();
context_setPreprocessing ();
dercfiles = preprocessFiles (xfiles, TRUE);
tfiles = preprocessFiles (cfiles, FALSE);
+ warnSysFiles(cfiles);
dercfiles = fileIdList_append (dercfiles, tfiles);
fileIdList_free (tfiles);
fileIdList_free (cfiles);
- if (context_getFlag (FLG_SHOWSCAN))
- {
- fprintf (stderr, " >\n");
- }
-
+ displayScanClose ();
pptime = clock ();
}
else
fileIdList_elements (dercfiles, fid)
{
- sourceFile = inputStream_create (cstring_copy (fileName (fid)), C_EXTENSION, TRUE);
+ sourceFile = inputStream_create (cstring_copy (fileTable_fileName (fid)), C_EXTENSION, TRUE);
context_setFileId (fid);
/* Open source file */
if (inputStream_isUndefined (sourceFile) || (!inputStream_open (sourceFile)))
{
/* previously, this was ignored ?! */
- llbug (message ("Could not open temp file: %s", fileName (fid)));
+ llbug (message ("Could not open temp file: %s", fileTable_fileName (fid)));
}
else
{
llassert (yyin != NULL);
- if (context_getFlag (FLG_SHOWSCAN))
- {
- lldiagmsg (message ("< checking %s >", rootFileName (fid)));
- }
+ displayScan (message ("checking %q", osd_outputPath (fileTable_rootFileName (fid))));
/*
** Every time, except the first time, through the loop,
** is this correct behaviour?
*/
- if (context_getFlag (FLG_SHOWSCAN))
- {
- lldiagmsg (cstring_makeLiteral ("< global checks >"));
- }
+ displayScan (cstring_makeLiteral ("global checks"));
cleanupMessages ();
expsuccess = TRUE;
if (context_neednl ())
- fprintf (g_msgstream, "\n");
+ fprintf (g_warningstream, "\n");
# ifndef NOLCL
if (nspecErrors > 0)
if (nspecErrors == context_getLCLExpect ())
{
specErrors =
- message ("%d spec error%& found, as expected\n ",
+ message ("%d spec warning%&, as expected\n ",
nspecErrors);
}
else
if (context_getLCLExpect () > 0)
{
specErrors =
- message ("%d spec error%& found, expected %d\n ",
+ message ("%d spec warning%&, expected %d\n ",
nspecErrors,
(int) context_getLCLExpect ());
}
else
{
- specErrors = message ("%d spec error%& found\n ",
+ specErrors = message ("%d spec warning%&\n ",
nspecErrors);
expsuccess = FALSE;
}
{
if (context_getLCLExpect () > 0)
{
- specErrors = message ("No spec errors found, expected %d\n ",
+ specErrors = message ("No spec warnings, expected %d\n ",
(int) context_getLCLExpect ());
expsuccess = FALSE;
}
if (context_numErrors () == context_getExpect ())
{
if (!isQuiet) {
- llmsg (message ("Finished LCLint checking --- "
- "%s%d code error%& found, as expected",
+ llmsg (message ("Finished checking --- "
+ "%s%d code warning%&, as expected",
specErrors, context_numErrors ()));
}
}
{
if (!isQuiet) {
llmsg (message
- ("Finished LCLint checking --- "
- "%s%d code error%& found, expected %d",
+ ("Finished checking --- "
+ "%s%d code warning%&, expected %d",
specErrors, context_numErrors (),
(int) context_getExpect ()));
}
if (!isQuiet)
{
- llmsg (message ("Finished LCLint checking --- "
- "%s%d code error%& found",
+ llmsg (message ("Finished checking --- "
+ "%s%d code warning%&",
specErrors, context_numErrors ()));
}
{
if (!isQuiet) {
llmsg (message
- ("Finished LCLint checking --- "
- "%sno code errors found, expected %d",
+ ("Finished checking --- "
+ "%sno code warnings, expected %d",
specErrors,
(int) context_getExpect ()));
}
{
if (context_getLinesProcessed () > 0)
{
- if (!isQuiet) {
- llmsg (message ("Finished LCLint checking --- %sno code errors found",
- specErrors));
- }
+ if (cstring_isEmpty (specErrors))
+ {
+ if (!isQuiet)
+ {
+ llmsg (message ("Finished checking --- no warnings"));
+ }
+ }
+ else
+ {
+ if (!isQuiet)
+ {
+ llmsg (message ("Finished checking --- %sno code warnings",
+ specErrors));
+ }
+ }
}
else
{
if (!isQuiet) {
- llmsg (message ("Finished LCLint checking --- %sno code processed",
+ llmsg (message ("Finished checking --- %sno code processed",
specErrors));
}
}
if (specLines > 0)
{
- fprintf (g_msgstream, "%d spec, ", specLines);
+ fprintf (g_warningstream, "%d spec, ", specLines);
}
# ifndef CLOCKS_PER_SEC
- fprintf (g_msgstream, "%d source lines in %ld time steps (steps/sec unknown)\n",
+ fprintf (g_warningstream, "%d source lines in %ld time steps (steps/sec unknown)\n",
context_getLinesProcessed (),
(long) ttime);
# else
- fprintf (g_msgstream, "%d source lines in %.2f s.\n",
+ fprintf (g_warningstream, "%d source lines in %.2f s.\n",
context_getLinesProcessed (),
(double) ttime / CLOCKS_PER_SEC);
# endif
llmsg (message ("Source files are .c, .h and %s files. If there is no suffix,",
LCL_EXTENSION));
- llmsg (message (" LCLint will look for <file>.c and <file>%s.", LCL_EXTENSION));
+ llmsg (message (" Splint will look for <file>.c and <file>%s.", LCL_EXTENSION));
llmsglit ("");
- llmsglit ("Use lclint -help <topic or flag name> for more information");
+ llmsglit ("Use splint -help <topic or flag name> for more information");
llmsglit ("");
llmsglit ("Topics:");
llmsglit ("");
printAllFlags (FALSE, TRUE);
return TRUE;
}
+ else if (mstring_equal (next, "manual"))
+ {
+ printFlagManual (FALSE);
+ return TRUE;
+ }
+ else if (mstring_equal (next, "webmanual"))
+ {
+ printFlagManual (TRUE);
+ return TRUE;
+ }
else
{
return FALSE;
llmsglit ("Parse Errors");
llmsglit ("------------");
llmsglit ("");
- llmsglit ("LCLint will sometimes encounter a parse error for code that "
+ llmsglit ("Splint will sometimes encounter a parse error for code that "
"can be parsed with a local compiler. There are a few likely "
"causes for this and a number of techniques that can be used "
"to work around the problem.");
"it is not advisible to use these, oftentimes one has no choice "
"when the system header files use compiler extensions. ");
llmsglit ("");
- llmsglit ("LCLint supports some of the GNU (gcc) compiler extensions, "
+ llmsglit ("Splint supports some of the GNU (gcc) compiler extensions, "
"if the +gnuextensions flag is set. You may be able to workaround "
"other compiler extensions by using a pre-processor define. "
"Alternately, you can surround the unparseable code with");
llmsglit ("");
- llmsglit (" # ifndef __LCLINT__");
+ llmsglit (" # ifndef S_SPLINT_S");
llmsglit (" ...");
llmsglit (" # endif");
llmsglit ("");
llmsglit ("Missing type definitions --- an undefined type name will usually "
"lead to a parse error. This often occurs when a standard header "
"file defines some type that is not part of the standard library. ");
- llmsglit ("By default, LCLint does not process the local files corresponding "
+ llmsglit ("By default, Splint does not process the local files corresponding "
"to standard library headers, but uses a library specification "
"instead so dependencies on local system headers can be detected. "
"If another system header file that does not correspond to a "
"a parse error will result.");
llmsglit ("");
llmsglit ("If the parse error is inside a posix standard header file, the "
- "first thing to try is +posixlib. This make LCLint use "
+ "first thing to try is +posixlib. This makes Splint use "
"the posix library specification instead of reading the posix "
"header files.");
llmsglit ("");
llmsglit ("Otherwise, you may need to either manually define the problematic "
- "type (e.g., add -Dmlink_t=int to your .lclintrc file) or force "
- "lclint to process the header file that defines it. This is done "
- "by setting -skipansiheaders or -skipposixheaders before "
+ "type (e.g., add -Dmlink_t=int to your .splintrc file) or force "
+ "splint to process the header file that defines it. This is done "
+ "by setting -skipisoheaders or -skipposixheaders before "
"the file that defines the type is #include'd.");
- llmsglit ("(See lclint -help "
- "skipansiheaders and lclint -help skipposixheaders for a list of "
+ llmsglit ("(See splint -help "
+ "skipisoheaders and splint -help skipposixheaders for a list of "
"standard headers.) For example, if <sys/local.h> uses a type "
"defined by posix header <sys/types.h> but not defined by the "
"posix library, we might do: ");
llmsglit (" /*@=skipposixheaders@*/");
llmsglit (" # include <sys/local.h>");
llmsglit ("");
- llmsglit ("to force LCLint to process <sys/types.h>.");
+ llmsglit ("to force Splint to process <sys/types.h>.");
llmsglit ("");
- llmsglit ("At last resort, +trytorecover can be used to make LCLint attempt "
+ llmsglit ("At last resort, +trytorecover can be used to make Splint attempt "
"to continue after a parse error. This is usually not successful "
"and the author does not consider assertion failures when +trytorecover "
"is used to be bugs.");
llmsglit ("");
llmsglit ("Null State:");
llmsglit (" /*@null@*/ - possibly null pointer");
- llmsglit (" /*@notnull@*/ - non-null pointer");
+ llmsglit (" /*@notnull@*/ - definitely non-null pointer");
llmsglit (" /*@relnull@*/ - relax null checking");
llmsglit ("");
llmsglit ("Null Predicates:");
- llmsglit (" /*@truenull@*/ - if result is TRUE, first parameter is NULL");
- llmsglit (" /*@falsenull@*/ - if result is TRUE, first parameter is not NULL");
+ llmsglit (" /*@nullwhentrue@*/ - if result is TRUE, first parameter is NULL");
+ llmsglit (" /*@falsewhennull@*/ - if result is TRUE, first parameter is not NULL");
llmsglit ("");
llmsglit ("Execution:");
- llmsglit (" /*@exits@*/ - function never returns");
- llmsglit (" /*@mayexit@*/ - function may or may not return");
- llmsglit (" /*@trueexit@*/ - function does not return if first parameter is TRUE");
- llmsglit (" /*@falseexit@*/ - function does not return if first parameter if FALSE");
- llmsglit (" /*@neverexit@*/ - function always returns");
+ llmsglit (" /*@noreturn@*/ - function never returns");
+ llmsglit (" /*@maynotreturn@*/ - function may or may not return");
+ llmsglit (" /*@noreturnwhentrue@*/ - function does not return if first parameter is TRUE");
+ llmsglit (" /*@noreturnwhenfalse@*/ - function does not return if first parameter if FALSE");
+ llmsglit (" /*@alwaysreturns@*/ - function always returns");
llmsglit ("");
llmsglit ("Side-Effects:");
llmsglit (" /*@sef@*/ - corresponding actual parameter has no side effects");
llmsglit ("/*@i<n>@*/");
llgenindentmsgnoloc
(cstring_makeLiteral
- ("No errors will be reported from an /*@i<n>@*/ (e.g., /*@i3@*/) comment to the end of the line. If there are not exactly n errors suppressed from the comment point to the end of the line, LCLint will report an error."));
+ ("No errors will be reported from an /*@i<n>@*/ (e.g., /*@i3@*/) comment to the end of the line. If there are not exactly n errors suppressed from the comment point to the end of the line, Splint will report an error."));
llmsglit ("/*@t@*/, /*@t<n>@*/");
llgenindentmsgnoloc
(cstring_makeLiteral
llmsglit ("Flag Categories");
llmsglit ("---------------");
listAllCategories ();
- llmsglit ("\nTo see the flags in a flag category, do\n lclint -help flags <category>");
- llmsglit ("To see a list of all flags in alphabetical order, do\n lclint -help flags alpha");
- llmsglit ("To see a full description of all flags, do\n lclint -help flags full");
+ llmsglit ("\nTo see the flags in a flag category, do\n splint -help flags <category>");
+ llmsglit ("To see a list of all flags in alphabetical order, do\n splint -help flags alpha");
+ llmsglit ("To see a full description of all flags, do\n splint -help flags full");
}
void
printMaintainer (void)
{
- llmsg (message ("Maintainer: %s", cstring_makeLiteralTemp (LCLINT_MAINTAINER)));
+ llmsg (message ("Maintainer: %s", cstring_makeLiteralTemp (SPLINT_MAINTAINER)));
llmsglit (LCL_COMPILE);
}
llmsglit ("Mailing Lists");
llmsglit ("-------------");
llmsglit ("");
- llmsglit ("There are two mailing lists associated with LCLint: ");
+ llmsglit ("There are two mailing lists associated with Splint: ");
llmsglit ("");
llmsglit (" lclint-announce@virginia.edu");
llmsglit ("");
llmsglit ("");
llmsglit (" lclint-interest@virginia.edu");
llmsglit ("");
- llmsglit (" Informal discussions on the use and development of lclint.");
+ llmsglit (" Informal discussions on the use and development of Splint.");
llmsglit (" To subscribe, send a message to majordomo@virginia.edu with body: ");
llmsglit (" subscribe lclint-interest");
}
llmsglit ("References");
llmsglit ("----------");
llmsglit ("");
- llmsglit ("The LCLint web site is http://lclint.cs.virginia.edu");
- llmsglit ("");
- llmsglit ("Technical papers relating to LCLint include:");
- llmsglit ("");
- llmsglit (" David Evans. \"Static Detection of Dynamic Memory Errors\".");
- llmsglit (" SIGPLAN Conference on Programming Language Design and ");
- llmsglit (" Implementation (PLDI '96), Philadelphia, PA, May 1996.");
- llmsglit ("");
- llmsglit (" David Evans, John Guttag, Jim Horning and Yang Meng Tan. ");
- llmsglit (" \"LCLint: A Tool for Using Specifications to Check Code\".");
- llmsglit (" SIGSOFT Symposium on the Foundations of Software Engineering,");
- llmsglit (" December 1994.");
- llmsglit ("");
- llmsglit ("A general book on Larch is:");
- llmsglit ("");
- llmsglit (" Guttag, John V., Horning, James J., (with Garland, S. J., Jones, ");
- llmsglit (" K. D., Modet, A., and Wing, J. M.), \"Larch: Languages and Tools ");
- llmsglit (" for Formal Specification\", Springer-Verlag, 1993.");
+ llmsglit ("For more information, see the Splint web site: http://www.splint.org");
}
void
switch (i)
{
case SIGINT:
- fprintf (stderr, "*** Interrupt\n");
+ fprintf (g_errorstream, "*** Interrupt\n");
llexit (LLINTERRUPT);
case SIGSEGV:
{
/* Cheat when there are parse errors */
checkParseError ();
- fprintf (stderr, "*** Segmentation Violation\n");
+ fprintf (g_errorstream, "*** Segmentation Violation\n");
/* Don't catch it if fileloc_unparse causes a signal */
(void) signal (SIGSEGV, NULL);
loc = fileloc_unparse (g_currentloc);
- fprintf (stderr, "*** Location (not trusted): %s\n",
+ fprintf (g_errorstream, "*** Location (not trusted): %s\n",
cstring_toCharsSafe (loc));
cstring_free (loc);
printCodePoint ();
- fprintf (stderr, "*** Please report bug to %s\n", LCLINT_MAINTAINER);
+ fprintf (g_errorstream, "*** Please report bug to %s\n", SPLINT_MAINTAINER);
exit (LLGIVEUP);
}
default:
- fprintf (stderr, "*** Signal: %d\n", i);
+ fprintf (g_errorstream, "*** Signal: %d\n", i);
/*@-mustfree@*/
- fprintf (stderr, "*** Location (not trusted): %s\n",
+ fprintf (g_errorstream, "*** Location (not trusted): %s\n",
cstring_toCharsSafe (fileloc_unparse (g_currentloc)));
/*@=mustfree@*/
printCodePoint ();
- fprintf (stderr, "*** Please report bug to %s ***\n", LCLINT_MAINTAINER);
+ fprintf (g_errorstream, "*** Please report bug to %s ***\n", SPLINT_MAINTAINER);
exit (LLGIVEUP);
}
}
if (context_getFlag (FLG_KEEP))
{
- check (fputs ("Temporary files kept:\n", stderr) != EOF);
+ check (fputs ("Temporary files kept:\n", g_messagestream) != EOF);
fileTable_printTemps (context_fileTable ());
}
else
}
/*
-** cleans up temp files (if necessary)
-** exits lclint
+** cleans up temp files (if necessary) and exits
*/
-/*@exits@*/ void
+/*@noreturn@*/ void
llexit (int status)
{
DPRINTF (("llexit: %d", status));
exit ((status == LLSUCCESS) ? EXIT_SUCCESS : EXIT_FAILURE);
}
+bool readOptionsFile (cstring fname, cstringSList *passThroughArgs, bool report)
+{
+ bool res = FALSE;
+
+ if (fileTable_exists (context_fileTable (), fname))
+ {
+ if (report)
+ {
+ voptgenerror
+ (FLG_WARNRC,
+ message ("Multiple attempts to read options file: %s", fname),
+ g_currentloc);
+ }
+ }
+ else
+ {
+ FILE *innerf = fileTable_openReadFile (context_fileTable (), fname);
+
+ if (innerf != NULL)
+ {
+ fileloc fc = g_currentloc;
+ g_currentloc = fileloc_createRc (fname);
+
+ displayScan (message ("< reading options from %q >",
+ fileloc_outputFilename (g_currentloc)));
+
+ loadrc (innerf, passThroughArgs);
+ fileloc_reallyFree (g_currentloc);
+ g_currentloc = fc;
+ res = TRUE;
+ }
+ else
+ {
+ if (report)
+ {
+ voptgenerror
+ (FLG_WARNRC,
+ message ("Cannot open options file: %s", fname),
+ g_currentloc);
+ }
+ }
+ }
+
+ return res;
+}
+
/*
** This shouldn't be necessary, but Apple Darwin can't handle '"''s.
*/
void
loadrc (/*:open:*/ FILE *rcfile, cstringSList *passThroughArgs)
+ /*@modifies rcfile@*/
/*@ensures closed rcfile@*/
{
char *s = mstring_create (MAX_LINE_LENGTH);
char *os = s;
-
+
DPRINTF (("Pass through: %s", cstringSList_unparse (*passThroughArgs)));
s = os;
DPRINTF (("Flag: %s", thisflag));
- opt = identifyFlag (cstring_fromChars (thisflag));
+ opt = flags_identifyFlag (cstring_fromChars (thisflag));
if (flagcode_isSkip (opt))
{
{
DPRINTF (("Invalid: %s", thisflag));
- if (isMode (cstring_fromChars (thisflag)))
+ if (flags_isModeName (cstring_fromChars (thisflag)))
{
context_setMode (cstring_fromChars (thisflag));
}
else if (opt == FLG_INCLUDEPATH
|| opt == FLG_SPECPATH)
{
- cstring dir = cstring_suffix (cstring_fromChars (thisflag), 1); /* skip over I/S */
+ cstring dir;
+
+ /*
+ ** Either -I<dir> or -I <dir>
+ */
+
+ if (cstring_length (thisflag) > 1)
+ {
+ dir = cstring_suffix (cstring_fromChars (thisflag), 1); /* skip over I/S */
+ }
+ else
+ {
+ BADBRANCH; /*@!!!!@*/
+ }
switch (opt)
{
}
}
else if (flagcode_hasString (opt)
- || flagcode_hasValue (opt)
+ || flagcode_hasNumber (opt)
+ || flagcode_hasChar (opt)
|| opt == FLG_INIT || opt == FLG_OPTF)
{
cstring extra = cstring_undefined;
DPRINTF (("Here we are: %s", extra));
- if (flagcode_hasValue (opt))
+ if (flagcode_hasNumber (opt) || flagcode_hasChar (opt))
{
DPRINTF (("Set value flag: %s", extra));
setValueFlag (opt, extra);
- cstring_free (extra);
}
else if (opt == FLG_OPTF)
{
- FILE *innerf = fileTable_openFile (context_fileTable (), extra, "r");
- cstring_markOwned (extra);
-
- if (innerf != NULL)
- {
- fileloc fc = g_currentloc;
- g_currentloc = fileloc_createRc (extra);
- loadrc (innerf, passThroughArgs);
- fileloc_reallyFree (g_currentloc);
- g_currentloc = fc;
- }
- else
- {
- showHerald ();
- voptgenerror
- (FLG_BADFLAG,
- message ("Options file not found: %s",
- extra),
- g_currentloc);
- }
+ (void) readOptionsFile (extra, passThroughArgs, TRUE);
}
else if (opt == FLG_INIT)
{
llassert (inputStream_isUndefined (initFile));
initFile = inputStream_create
- (extra,
+ (cstring_copy (extra),
cstring_makeLiteralTemp (LCLINIT_SUFFIX),
FALSE);
-# else
- cstring_free (extra);
# endif
}
else if (flagcode_hasString (opt))
{
+ DPRINTF (("Here: %s", extra));
+
+ /*
+ ** If it has "'s, we need to remove them.
+ */
+
if (cstring_firstChar (extra) == '\"')
{
if (cstring_lastChar (extra) == '\"')
{
- char *extras = cstring_toCharsSafe (extra);
-
- llassert (extras[strlen(extras) - 1] == '\"');
- extras[strlen(extras) - 1] = '\0';
- extra = cstring_fromChars (extras + 1);
- DPRINTF (("Remove quotes: %s", extra));
+ cstring unquoted = cstring_copyLength
+ (cstring_toCharsSafe (cstring_suffix (extra, 1)),
+ cstring_length (extra) - 2);
+
+ DPRINTF (("string flag: %s -> %s", extra, unquoted));
+ setStringFlag (opt, unquoted);
+ cstring_free (extra);
}
else
{
message ("Unmatched \" in option string: %s",
extra),
g_currentloc);
+ setStringFlag (opt, extra);
}
}
-
- setStringFlag (opt, extra);
+ else
+ {
+ DPRINTF (("No quotes: %s", extra));
+ setStringFlag (opt, extra);
+ }
+
+ extra = cstring_undefined;
}
else
{
- cstring_free (extra);
BADEXIT;
}
}
+
+ cstring_free (extra);
}
else
{
fileIdList_elements (fl, fid)
{
- cstring ppfname = fileName (fid);
+ cstring ppfname = fileTable_fileName (fid);
- if (xhfiles)
- {
- cstring fpath;
-
- if (osd_findOnLarchPath (ppfname, &fpath) == OSD_FILEFOUND)
- {
- if (cstring_equal (ppfname, fpath))
- {
- ;
- }
- else
- {
- DPRINTF (("xh file: %s", fpath));
- ppfname = fpath;
- fileTable_setFilePath (context_fileTable (), fid, fpath);
- }
- }
- else
- {
- lldiagmsg (message ("Cannot find .xh file on LARCH_PATH: %s", ppfname));
- lldiagmsg (cstring_makeLiteral (" Check LARCH_PATH environment variable."));
- ppfname = cstring_undefined;
- }
- }
- else
+ if (!(osd_fileIsReadable (ppfname)))
{
- if (!(osd_fileIsReadable (ppfname)))
- {
- lldiagmsg (message ("Cannot open file: %s", ppfname));
- ppfname = cstring_undefined;
- }
+ lldiagmsg (message ("Cannot open file: %q", osd_outputPath (ppfname)));
+ ppfname = cstring_undefined;
}
if (cstring_isDefined (ppfname))
{
fileId dfile = fileTable_addCTempFile (context_fileTable (), fid);
-
+
+ if (xhfiles)
+ {
+ llassert (fileTable_isXHFile (context_fileTable (), dfile));
+ }
+
llassert (cstring_isNonEmpty (ppfname));
if (msg)
if ((filesprocessed % skip) == 0)
{
if (filesprocessed == 0) {
- fprintf (stderr, " ");
+ fprintf (g_messagestream, " ");
}
else {
- fprintf (stderr, ".");
+ fprintf (g_messagestream, ".");
}
- (void) fflush (stderr);
+ (void) fflush (g_messagestream);
}
filesprocessed++;
}
- if (cppProcess (ppfname, fileName (dfile)) != 0)
+ DPRINTF (("outfile: %s", fileTable_fileName (dfile)));
+
+ if (cppProcess (ppfname, fileTable_fileName (dfile)) != 0)
{
llfatalerror (message ("Preprocessing error for file: %s",
- rootFileName (fid)));
+ fileTable_rootFileName (fid)));
}
fileIdList_add (dfiles, dfile);
return specname;
}
# endif
+
+void warnSysFiles(fileIdList files)
+{
+ fileIdList_elements (files, file)
+ {
+
+ if (fileTable_isSystemFile (context_fileTable (), file) )
+ {
+ if (!context_getFlag( FLG_SYSTEMDIRERRORS ) )
+ {
+ voptgenerror (FLG_WARNSYSFILES, message ("Warning %s is a considered a system file. No errors in this file will be reported.", fileTable_rootFileName (file) ), g_currentloc);
+ }
+ }
+ }
+ end_fileIdList_elements;
+}
andersk / splint.git / blobdiff