/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 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
** 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 information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** representation of type qualifiers
*/
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
-static qual qual_createPlainAux (int i)
+static qual qual_createPlainAux (int i) /*@*/
{
qual res = (qual) dmalloc (sizeof (*res));
res->kind = (quenum) i;
return res;
}
-extern qual qual_createPlain (quenum q)
+static qual qtable[QU_LAST];
+static bool isinit = FALSE;
+
+extern void qual_initMod (void)
{
- static bool isinit = FALSE;
- static qual qtable[QU_LAST];
+ int i = (int) QU_UNKNOWN;
+ llassert (!isinit);
+
+ while (i < (int) QU_LAST) {
+ qtable[i] = qual_createPlainAux (i);
+ i++;
+ }
+
+ isinit = TRUE;
+}
- if (!isinit) {
- int i = (int) QU_UNKNOWN;
+static void qual_free (qual p_q) ;
- while (i < (int) QU_LAST) {
- qtable[i] = qual_createPlainAux (i);
- i++;
+extern void qual_destroyMod (void)
+{
+ if (isinit)
+ {
+ int i = (int) QU_UNKNOWN;
+ isinit = FALSE;
+
+ while (i < (int) QU_LAST) {
+ qual_free (qtable[i]);
+ i++;
+ }
}
+}
- isinit = TRUE;
- }
+static void qual_free (qual q)
+{
+ llassert (!isinit);
+ sfree (q);
+}
+extern qual qual_createPlain (quenum q)
+{
+ llassert (isinit);
llassert (q != QU_USERANNOT && q < QU_LAST);
return qtable[(int) q];
}
cstring qual_unparse (qual q)
{
- if (q->kind == QU_USERANNOT) {
- return (annotationInfo_unparse (q->info));
- } else {
- switch (q->kind)
- {
- case QU_UNKNOWN: return cstring_makeLiteralTemp ("unknown");
- case QU_ABSTRACT: return cstring_makeLiteralTemp ("abstract");
- case QU_CONCRETE: return cstring_makeLiteralTemp ("concrete");
- case QU_MUTABLE: return cstring_makeLiteralTemp ("mutable");
- case QU_IMMUTABLE: return cstring_makeLiteralTemp ("immutable");
- case QU_SHORT: return cstring_makeLiteralTemp ("short");
- case QU_LONG: return cstring_makeLiteralTemp ("long");
- case QU_SIGNED: return cstring_makeLiteralTemp ("signed");
- case QU_UNSIGNED: return cstring_makeLiteralTemp ("unsigned");
- case QU_CONST: return cstring_makeLiteralTemp ("const");
- case QU_VOLATILE: return cstring_makeLiteralTemp ("volatile");
- case QU_INLINE: return cstring_makeLiteralTemp ("inline");
- case QU_EXTERN: return cstring_makeLiteralTemp ("extern");
- case QU_STATIC: return cstring_makeLiteralTemp ("static");
- case QU_AUTO: return cstring_makeLiteralTemp ("auto");
- case QU_REGISTER: return cstring_makeLiteralTemp ("register");
- case QU_OUT: return cstring_makeLiteralTemp ("out");
- case QU_IN: return cstring_makeLiteralTemp ("in");
- case QU_RELDEF: return cstring_makeLiteralTemp ("reldef");
- case QU_ONLY: return cstring_makeLiteralTemp ("only");
- case QU_IMPONLY: return cstring_makeLiteralTemp ("only");
- case QU_PARTIAL: return cstring_makeLiteralTemp ("partial");
- case QU_SPECIAL: return cstring_makeLiteralTemp ("special");
- case QU_KEEP: return cstring_makeLiteralTemp ("keep");
- case QU_KEPT: return cstring_makeLiteralTemp ("kept");
- case QU_YIELD: return cstring_makeLiteralTemp ("yield");
- case QU_TEMP: return cstring_makeLiteralTemp ("temp");
- case QU_SHARED: return cstring_makeLiteralTemp ("shared");
- case QU_UNIQUE: return cstring_makeLiteralTemp ("unique");
- case QU_UNCHECKED: return cstring_makeLiteralTemp ("unchecked");
- case QU_CHECKED: return cstring_makeLiteralTemp ("checked");
- case QU_CHECKMOD: return cstring_makeLiteralTemp ("checkmod");
- case QU_CHECKEDSTRICT: return cstring_makeLiteralTemp ("checkedstrict");
- case QU_TRUENULL: return cstring_makeLiteralTemp ("truenull");
- case QU_FALSENULL: return cstring_makeLiteralTemp ("falsenull");
- case QU_NULL: return cstring_makeLiteralTemp ("null");
- case QU_ISNULL: return cstring_makeLiteralTemp ("isnull");
- case QU_RELNULL: return cstring_makeLiteralTemp ("relnull");
- case QU_NOTNULL: return cstring_makeLiteralTemp ("notnull");
- case QU_NULLTERMINATED: return cstring_makeLiteralTemp ("nullterminated");
- case QU_RETURNED: return cstring_makeLiteralTemp (" returned");
- case QU_EXPOSED: return cstring_makeLiteralTemp ("exposed");
- case QU_EXITS: return cstring_makeLiteralTemp ("exits");
- case QU_MAYEXIT: return cstring_makeLiteralTemp ("mayexit");
- case QU_UNUSED: return cstring_makeLiteralTemp ("unused");
- case QU_EXTERNAL: return cstring_makeLiteralTemp ("external");
- case QU_SEF: return cstring_makeLiteralTemp ("sef");
- case QU_OBSERVER: return cstring_makeLiteralTemp ("observer");
- case QU_REFCOUNTED: return cstring_makeLiteralTemp ("refcounted");
- case QU_REFS: return cstring_makeLiteralTemp ("refs");
- case QU_NEWREF: return cstring_makeLiteralTemp ("newref");
- case QU_KILLREF: return cstring_makeLiteralTemp ("killref");
- case QU_TEMPREF: return cstring_makeLiteralTemp ("tempref");
- case QU_OWNED: return cstring_makeLiteralTemp ("owned");
- case QU_DEPENDENT: return cstring_makeLiteralTemp ("dependent");
- case QU_NEVEREXIT: return cstring_makeLiteralTemp ("neverexit");
- case QU_TRUEEXIT: return cstring_makeLiteralTemp ("trueexit");
- case QU_FALSEEXIT: return cstring_makeLiteralTemp ("falseexit");
- case QU_UNDEF: return cstring_makeLiteralTemp ("undef");
- case QU_KILLED: return cstring_makeLiteralTemp ("killed");
- case QU_PRINTFLIKE: return cstring_makeLiteralTemp ("printflike");
- case QU_SCANFLIKE: return cstring_makeLiteralTemp ("scanflike");
- case QU_MESSAGELIKE:return cstring_makeLiteralTemp ("messagelike");
- case QU_SETBUFFERSIZE: return cstring_makeLiteralTemp("<qsetbuffersize>");
- case QU_LAST: return cstring_makeLiteralTemp ("< last >");
- case QU_USERANNOT: return cstring_makeLiteralTemp ("<user>");
- }
+ if (q->kind == QU_USERANNOT)
+ {
+ return (annotationInfo_unparse (q->info));
+ }
+ else
+ {
+ switch (q->kind)
+ {
+ case QU_UNKNOWN: return cstring_makeLiteralTemp ("unknown");
+ case QU_ABSTRACT: return cstring_makeLiteralTemp ("abstract");
+ case QU_NUMABSTRACT:return cstring_makeLiteralTemp ("numabstract");
+ case QU_CONCRETE: return cstring_makeLiteralTemp ("concrete");
+ case QU_MUTABLE: return cstring_makeLiteralTemp ("mutable");
+ case QU_IMMUTABLE: return cstring_makeLiteralTemp ("immutable");
+ case QU_SHORT: return cstring_makeLiteralTemp ("short");
+ case QU_LONG: return cstring_makeLiteralTemp ("long");
+ case QU_SIGNED: return cstring_makeLiteralTemp ("signed");
+ case QU_UNSIGNED: return cstring_makeLiteralTemp ("unsigned");
+ case QU_CONST: return cstring_makeLiteralTemp ("const");
+ case QU_RESTRICT: return cstring_makeLiteralTemp ("restrict");
+ case QU_VOLATILE: return cstring_makeLiteralTemp ("volatile");
+ case QU_INLINE: return cstring_makeLiteralTemp ("inline");
+ case QU_EXTERN: return cstring_makeLiteralTemp ("extern");
+ case QU_STATIC: return cstring_makeLiteralTemp ("static");
+ case QU_AUTO: return cstring_makeLiteralTemp ("auto");
+ case QU_REGISTER: return cstring_makeLiteralTemp ("register");
+ case QU_OUT: return cstring_makeLiteralTemp ("out");
+ case QU_IN: return cstring_makeLiteralTemp ("in");
+ case QU_RELDEF: return cstring_makeLiteralTemp ("reldef");
+ case QU_ONLY: return cstring_makeLiteralTemp ("only");
+ case QU_IMPONLY: return cstring_makeLiteralTemp ("only");
+ case QU_PARTIAL: return cstring_makeLiteralTemp ("partial");
+ case QU_SPECIAL: return cstring_makeLiteralTemp ("special");
+ case QU_KEEP: return cstring_makeLiteralTemp ("keep");
+ case QU_KEPT: return cstring_makeLiteralTemp ("kept");
+ case QU_YIELD: return cstring_makeLiteralTemp ("yield");
+ case QU_TEMP: return cstring_makeLiteralTemp ("temp");
+ case QU_SHARED: return cstring_makeLiteralTemp ("shared");
+ case QU_UNIQUE: return cstring_makeLiteralTemp ("unique");
+ case QU_UNCHECKED: return cstring_makeLiteralTemp ("unchecked");
+ case QU_CHECKED: return cstring_makeLiteralTemp ("checked");
+ case QU_CHECKMOD: return cstring_makeLiteralTemp ("checkmod");
+ case QU_CHECKEDSTRICT: return cstring_makeLiteralTemp ("checkedstrict");
+ case QU_TRUENULL: return cstring_makeLiteralTemp ("truenull");
+ case QU_FALSENULL: return cstring_makeLiteralTemp ("falsenull");
+ case QU_NULL: return cstring_makeLiteralTemp ("null");
+ case QU_ISNULL: return cstring_makeLiteralTemp ("isnull");
+ case QU_RELNULL: return cstring_makeLiteralTemp ("relnull");
+ case QU_NOTNULL: return cstring_makeLiteralTemp ("notnull");
+ case QU_NULLTERMINATED: return cstring_makeLiteralTemp ("nullterminated");
+ case QU_RETURNED: return cstring_makeLiteralTemp ("returned");
+ case QU_EXPOSED: return cstring_makeLiteralTemp ("exposed");
+ case QU_EXITS: return cstring_makeLiteralTemp ("noreturn");
+ case QU_MAYEXIT: return cstring_makeLiteralTemp ("maynotreturn");
+ case QU_UNUSED: return cstring_makeLiteralTemp ("unused");
+ case QU_EXTERNAL: return cstring_makeLiteralTemp ("external");
+ case QU_SEF: return cstring_makeLiteralTemp ("sef");
+ case QU_OBSERVER: return cstring_makeLiteralTemp ("observer");
+ case QU_REFCOUNTED: return cstring_makeLiteralTemp ("refcounted");
+ case QU_REFS: return cstring_makeLiteralTemp ("refs");
+ case QU_NEWREF: return cstring_makeLiteralTemp ("newref");
+ case QU_KILLREF: return cstring_makeLiteralTemp ("killref");
+ case QU_TEMPREF: return cstring_makeLiteralTemp ("tempref");
+ case QU_OWNED: return cstring_makeLiteralTemp ("owned");
+ case QU_DEPENDENT: return cstring_makeLiteralTemp ("dependent");
+ case QU_NEVEREXIT: return cstring_makeLiteralTemp ("alwaysreturns");
+ case QU_TRUEEXIT: return cstring_makeLiteralTemp ("noreturnwhentrue");
+ case QU_FALSEEXIT: return cstring_makeLiteralTemp ("noreturnwhenfalse");
+ case QU_UNDEF: return cstring_makeLiteralTemp ("undef");
+ case QU_KILLED: return cstring_makeLiteralTemp ("killed");
+ case QU_PRINTFLIKE: return cstring_makeLiteralTemp ("printflike");
+ case QU_SCANFLIKE: return cstring_makeLiteralTemp ("scanflike");
+ case QU_MESSAGELIKE:return cstring_makeLiteralTemp ("messagelike");
+ case QU_SETBUFFERSIZE: return cstring_makeLiteralTemp("<qsetbuffersize>");
+ case QU_LAST: return cstring_makeLiteralTemp ("< last >");
+ case QU_USERANNOT: return cstring_makeLiteralTemp ("<user>");
+ }
+ }
+
+ BADEXIT;
+}
+
+qual qual_abstractFromCodeChar (char c)
+{
+ switch (c) {
+ case '-': return qual_createUnknown ();
+ case 'a': return qual_createAbstract ();
+ case 'n': return qual_createNumAbstract ();
+ case 'c': return qual_createConcrete ();
+ BADDEFAULT;
}
+}
- BADEXIT;
+char qual_abstractCode (qual q)
+{
+ switch (q->kind) {
+ case QU_UNKNOWN: return '-';
+ case QU_ABSTRACT: return 'a';
+ case QU_NUMABSTRACT: return 'n';
+ case QU_CONCRETE: return 'c';
+ BADDEFAULT;
+ }
}
extern bool qual_match (qual q1, qual q2)
return q->info;
}
-/* Cannot call qual_create after this... */
-
-# if 0
-static void qual_free (qual q)
-{
- llassert (FALSE);
- sfree (q);
-}
-# endif
-
extern cstring qual_dump (qual q)
{
+ llassert (isinit);
+
if (q->kind == QU_USERANNOT)
{
return message ("%d.%s",
extern qual qual_undump (char **s)
{
quenum q = (quenum) reader_getInt (s);
+ llassert (isinit);
if (q == QU_USERANNOT)
{
andersk / splint.git / blobdiff