/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "portab.h"
-static /*@only@*/ fileloc fileloc_createPrim (flkind p_kind, fileId p_fid, int p_line, int p_col);
+static /*@only@*/ fileloc fileloc_createPrim (flkind p_kind, fileId p_fid, int p_line, int p_col) /*@*/ ;
+
+/*
+** builtin locs are never free'd
+*/
+
+static /*@owned@*/ fileloc s_builtinLoc = fileloc_undefined;
+static /*@owned@*/ fileloc s_externalLoc = fileloc_undefined;
+
+void fileloc_destroyMod ()
+{
+ if (fileloc_isDefined (s_builtinLoc))
+ {
+ sfree (s_builtinLoc);
+ s_builtinLoc = fileloc_undefined;
+ }
+
+ if (fileloc_isDefined (s_externalLoc))
+ {
+ sfree (s_externalLoc);
+ s_externalLoc = fileloc_undefined;
+ }
+}
static flkind fileId_kind (fileId s)
{
/*@noaccess fileId@*/
}
-# ifndef NOLCL
bool
fileloc_isStandardLibrary (fileloc f)
{
|| cstring_equalLit (s, LLPOSIXSTRICTLIBS_NAME)
|| cstring_equalLit (s, LLPOSIXLIBS_NAME));
}
-# endif
bool
fileloc_sameFileAndLine (fileloc f1, fileloc f2)
}
}
-# ifndef NOLCL
/*@only@*/ fileloc
fileloc_fromTok (ltoken t)
{
return (fl);
}
-# endif
/*@only@*/ fileloc
fileloc_createLib (cstring ln)
fileloc fileloc_getExternal (void)
{
- static /*@owned@*/ fileloc res = fileloc_undefined;
-
- if (res == fileloc_undefined)
+ if (s_externalLoc == fileloc_undefined)
{
- res = fileloc_createPrim (FL_EXTERNAL, fileId_invalid, 0, 0);
+ s_externalLoc = fileloc_createPrim (FL_EXTERNAL, fileId_invalid, 0, 0);
}
- return res;
+ return s_externalLoc;
}
fileloc fileloc_observeBuiltin ()
return (fileloc_createPrim (FL_PREPROC, fileId_invalid, 0, 0));
}
+/* We pretend the result is only, because fileloc_free doesn't free it! */
/*@only@*/ fileloc
fileloc_createBuiltin ()
{
- return (fileloc_createPrim (FL_BUILTIN, fileId_invalid, 0, 0));
+ if (fileloc_isUndefined (s_builtinLoc))
+ {
+ s_builtinLoc = fileloc_createPrim (FL_BUILTIN, fileId_invalid, 0, 0);
+ }
+
+ /*@-globstate@*/ /*@-retalias@*/
+ return s_builtinLoc;
+ /*@=globstate@*/ /*@=retalias@*/
}
-# ifndef NOLCL
/*@only@*/ fileloc
fileloc_createImport (cstring fname, int lineno)
{
return (fileloc_createPrim (FL_IMPORT, fid, lineno, 0));
}
-# endif
static /*@only@*/ fileloc
fileloc_createPrim (flkind kind, fileId fid, int line, int col)
return (f);
}
-# ifndef NOLCL
/*@only@*/ fileloc
fileloc_createSpec (fileId fid, int line, int col)
{
return (fileloc_createPrim (FL_SPEC, fid, line, col));
}
-# endif
fileloc fileloc_create (fileId fid, int line, int col)
{
/*@only@*/ cstring
fileloc_unparse (fileloc f)
{
- static in_funparse = FALSE;
+ static bool in_funparse = FALSE;
bool parenFormat = context_getFlag (FLG_PARENFILEFORMAT);
bool htmlFormat = context_getFlag (FLG_HTMLFILEFORMAT);
cstring res = cstring_undefined;
if (f->kind == FL_LIB)
{
fname = message ("load file %q", fileloc_outputFilename (f));
+
+ if (!context_getFlag (FLG_SHOWLOADLOC))
+ {
+ res = fname;
+ break;
+ }
}
else
{
else
{
res = fname;
+ /*@-branchstate@*/ /* spurious warnings reporteded because of break above */
}
}
else if (fileloc_linenoDefined (f))
{
res = cstring_makeLiteral ("< Location unknown >");
}
-
+ /*@=branchstate@*/ /* this is a spurious warning because of the break */
+
in_funparse = FALSE;
return res;
}