[splint.git] / src / qual.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2003 University of Virginia,
**         Massachusetts Institute of Technology
**
** 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.
**
** For information on splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** qual.c
**
** representation of type qualifiers
*/

# include "splintMacros.nf"
# include "basic.h"

static qual qual_createPlainAux (int i) /*@*/ 
{
  qual res = (qual) dmalloc (sizeof (*res));
  res->kind = (quenum) i;
  res->info = annotationInfo_undefined;

  sfreeEventually (res); /* stored in qtable */
  return res;
}

static qual qtable[QU_LAST];
static bool isinit = FALSE;

extern void qual_initMod (void)
{
  int i = (int) QU_UNKNOWN;
  llassert (!isinit);

  while (i < (int) QU_LAST) {
    qtable[i] = qual_createPlainAux (i);
    i++;
  }
  
  isinit = TRUE;
}

static void qual_free (qual p_q) ;

extern void qual_destroyMod (void)
{
  if (isinit)
    {
      int i = (int) QU_UNKNOWN;
      isinit = FALSE;

      while (i < (int) QU_LAST) {
	qual_free (qtable[i]);
	i++;
      }
    }
}

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];
}

extern qual qual_createMetaState (annotationInfo info)
{
  qual res;

  res = (qual) dmalloc (sizeof (*res));
  res->kind = QU_USERANNOT;
  res->info = info;

  sfreeEventually (res); /* Memory leak */
  return res;
}
  
static bool quenum_isValid (int q)
{
  return ((quenum) q >= QU_UNKNOWN 
	  && ((quenum) q < QU_LAST));
}

qual qual_fromInt (int q)
{
  llassertprint (quenum_isValid (q), ("Invalid qual: %d", q));
  return (qual_createPlain ((quenum) 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_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;
  }
}

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)
{
  if (q1->kind == q2->kind) {
    if (q1->kind == QU_USERANNOT) {
      return (annotationInfo_equal (q1->info, q2->info));
    } else {
      return TRUE;
    }
  }
  
  return FALSE;
}

extern annotationInfo qual_getAnnotationInfo (qual q)
{
  llassert (qual_isMetaState (q));
  return q->info;
}

extern cstring qual_dump (qual q)
{
  llassert (isinit);

  if (q->kind == QU_USERANNOT)
    {
      return message ("%d.%s",
		      (int) q->kind,
		      annotationInfo_dump (q->info));
    }
  else
    {
      return message ("%d", (int) q->kind);
    }
}


extern qual qual_undump (char **s)
{
  quenum q = (quenum) reader_getInt (s); 
  llassert (isinit);

  if (q == QU_USERANNOT)
    {
      annotationInfo ai;

      reader_checkChar (s, '.');
      ai = annotationInfo_undump (s);

      return qual_createMetaState (ai);
    }
  else
    {
      return qual_createPlain (q);
    }
}
Commit	Line	Data
616915dd	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
c59f5181	3	** Copyright (C) 1994-2003 University of Virginia,
616915dd	4	** Massachusetts Institute of Technology
	5	**
	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.
	10	**
	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.
	15	**
	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.
	19	**
155af98d	20	** For information on splint: info@splint.org
155af98d	21	** To report a bug: splint-bug@splint.org
11db3170	22	** For more information: http://www.splint.org
616915dd	23	*/
	24	/*
	25	** qual.c
	26	**
	27	** representation of type qualifiers
	28	*/
	29
1b8ae690	30	# include "splintMacros.nf"
616915dd	31	# include "basic.h"
616915dd	32
6fcd0b1e	33	static qual qual_createPlainAux (int i) /@/
616915dd	34	{
28bf4b0b	35	qual res = (qual) dmalloc (sizeof (*res));
	36	res->kind = (quenum) i;
	37	res->info = annotationInfo_undefined;
	38
15b3d2b2	39	sfreeEventually (res); /* stored in qtable */
15b3d2b2	40	return res;
28bf4b0b	41	}
28bf4b0b	42
6fcd0b1e	43	static qual qtable[QU_LAST];
	44	static bool isinit = FALSE;
	45
	46	extern void qual_initMod (void)
28bf4b0b	47	{
6fcd0b1e	48	int i = (int) QU_UNKNOWN;
	49	llassert (!isinit);
	50
	51	while (i < (int) QU_LAST) {
	52	qtable[i] = qual_createPlainAux (i);
	53	i++;
	54	}
	55
	56	isinit = TRUE;
	57	}
28bf4b0b	58
6fcd0b1e	59	static void qual_free (qual p_q) ;
28bf4b0b	60
6fcd0b1e	61	extern void qual_destroyMod (void)
	62	{
	63	if (isinit)
	64	{
	65	int i = (int) QU_UNKNOWN;
	66	isinit = FALSE;
	67
	68	while (i < (int) QU_LAST) {
	69	qual_free (qtable[i]);
	70	i++;
	71	}
28bf4b0b	72	}
6fcd0b1e	73	}
28bf4b0b	74
6fcd0b1e	75	static void qual_free (qual q)
	76	{
	77	llassert (!isinit);
	78	sfree (q);
	79	}
28bf4b0b	80
6fcd0b1e	81	extern qual qual_createPlain (quenum q)
	82	{
	83	llassert (isinit);
28bf4b0b	84	llassert (q != QU_USERANNOT && q < QU_LAST);
	85	return qtable[(int) q];
	86	}
	87
	88	extern qual qual_createMetaState (annotationInfo info)
	89	{
	90	qual res;
	91
	92	res = (qual) dmalloc (sizeof (*res));
	93	res->kind = QU_USERANNOT;
15b3d2b2	94	res->info = info;
28bf4b0b	95
15b3d2b2	96	sfreeEventually (res); /* Memory leak */
15b3d2b2	97	return res;
28bf4b0b	98	}
	99
	100	static bool quenum_isValid (int q)
	101	{
	102	return ((quenum) q >= QU_UNKNOWN
	103	&& ((quenum) q < QU_LAST));
616915dd	104	}
	105
	106	qual qual_fromInt (int q)
	107	{
28bf4b0b	108	llassertprint (quenum_isValid (q), ("Invalid qual: %d", q));
28bf4b0b	109	return (qual_createPlain ((quenum) q));
616915dd	110	}
	111
	112	cstring qual_unparse (qual q)
	113	{
f9264521	114	if (q->kind == QU_USERANNOT)
	115	{
	116	return (annotationInfo_unparse (q->info));
	117	}
	118	else
	119	{
	120	switch (q->kind)
	121	{
	122	case QU_UNKNOWN: return cstring_makeLiteralTemp ("unknown");
	123	case QU_ABSTRACT: return cstring_makeLiteralTemp ("abstract");
e5081f8c	124	case QU_NUMABSTRACT:return cstring_makeLiteralTemp ("numabstract");
f9264521	125	case QU_CONCRETE: return cstring_makeLiteralTemp ("concrete");
	126	case QU_MUTABLE: return cstring_makeLiteralTemp ("mutable");
	127	case QU_IMMUTABLE: return cstring_makeLiteralTemp ("immutable");
	128	case QU_SHORT: return cstring_makeLiteralTemp ("short");
	129	case QU_LONG: return cstring_makeLiteralTemp ("long");
	130	case QU_SIGNED: return cstring_makeLiteralTemp ("signed");
	131	case QU_UNSIGNED: return cstring_makeLiteralTemp ("unsigned");
	132	case QU_CONST: return cstring_makeLiteralTemp ("const");
	133	case QU_RESTRICT: return cstring_makeLiteralTemp ("restrict");
	134	case QU_VOLATILE: return cstring_makeLiteralTemp ("volatile");
	135	case QU_INLINE: return cstring_makeLiteralTemp ("inline");
	136	case QU_EXTERN: return cstring_makeLiteralTemp ("extern");
	137	case QU_STATIC: return cstring_makeLiteralTemp ("static");
	138	case QU_AUTO: return cstring_makeLiteralTemp ("auto");
	139	case QU_REGISTER: return cstring_makeLiteralTemp ("register");
	140	case QU_OUT: return cstring_makeLiteralTemp ("out");
	141	case QU_IN: return cstring_makeLiteralTemp ("in");
	142	case QU_RELDEF: return cstring_makeLiteralTemp ("reldef");
	143	case QU_ONLY: return cstring_makeLiteralTemp ("only");
	144	case QU_IMPONLY: return cstring_makeLiteralTemp ("only");
	145	case QU_PARTIAL: return cstring_makeLiteralTemp ("partial");
	146	case QU_SPECIAL: return cstring_makeLiteralTemp ("special");
	147	case QU_KEEP: return cstring_makeLiteralTemp ("keep");
	148	case QU_KEPT: return cstring_makeLiteralTemp ("kept");
	149	case QU_YIELD: return cstring_makeLiteralTemp ("yield");
	150	case QU_TEMP: return cstring_makeLiteralTemp ("temp");
	151	case QU_SHARED: return cstring_makeLiteralTemp ("shared");
	152	case QU_UNIQUE: return cstring_makeLiteralTemp ("unique");
	153	case QU_UNCHECKED: return cstring_makeLiteralTemp ("unchecked");
	154	case QU_CHECKED: return cstring_makeLiteralTemp ("checked");
	155	case QU_CHECKMOD: return cstring_makeLiteralTemp ("checkmod");
	156	case QU_CHECKEDSTRICT: return cstring_makeLiteralTemp ("checkedstrict");
	157	case QU_TRUENULL: return cstring_makeLiteralTemp ("truenull");
	158	case QU_FALSENULL: return cstring_makeLiteralTemp ("falsenull");
	159	case QU_NULL: return cstring_makeLiteralTemp ("null");
	160	case QU_ISNULL: return cstring_makeLiteralTemp ("isnull");
	161	case QU_RELNULL: return cstring_makeLiteralTemp ("relnull");
	162	case QU_NOTNULL: return cstring_makeLiteralTemp ("notnull");
	163	case QU_NULLTERMINATED: return cstring_makeLiteralTemp ("nullterminated");
	164	case QU_RETURNED: return cstring_makeLiteralTemp ("returned");
	165	case QU_EXPOSED: return cstring_makeLiteralTemp ("exposed");
	166	case QU_EXITS: return cstring_makeLiteralTemp ("noreturn");
	167	case QU_MAYEXIT: return cstring_makeLiteralTemp ("maynotreturn");
	168	case QU_UNUSED: return cstring_makeLiteralTemp ("unused");
	169	case QU_EXTERNAL: return cstring_makeLiteralTemp ("external");
	170	case QU_SEF: return cstring_makeLiteralTemp ("sef");
	171	case QU_OBSERVER: return cstring_makeLiteralTemp ("observer");
	172	case QU_REFCOUNTED: return cstring_makeLiteralTemp ("refcounted");
	173	case QU_REFS: return cstring_makeLiteralTemp ("refs");
	174	case QU_NEWREF: return cstring_makeLiteralTemp ("newref");
	175	case QU_KILLREF: return cstring_makeLiteralTemp ("killref");
	176	case QU_TEMPREF: return cstring_makeLiteralTemp ("tempref");
	177	case QU_OWNED: return cstring_makeLiteralTemp ("owned");
	178	case QU_DEPENDENT: return cstring_makeLiteralTemp ("dependent");
	179	case QU_NEVEREXIT: return cstring_makeLiteralTemp ("alwaysreturns");
	180	case QU_TRUEEXIT: return cstring_makeLiteralTemp ("noreturnwhentrue");
	181	case QU_FALSEEXIT: return cstring_makeLiteralTemp ("noreturnwhenfalse");
	182	case QU_UNDEF: return cstring_makeLiteralTemp ("undef");
	183	case QU_KILLED: return cstring_makeLiteralTemp ("killed");
	184	case QU_PRINTFLIKE: return cstring_makeLiteralTemp ("printflike");
	185	case QU_SCANFLIKE: return cstring_makeLiteralTemp ("scanflike");
	186	case QU_MESSAGELIKE:return cstring_makeLiteralTemp ("messagelike");
	187	case QU_SETBUFFERSIZE: return cstring_makeLiteralTemp("<qsetbuffersize>");
	188	case QU_LAST: return cstring_makeLiteralTemp ("< last >");
189	case QU_USERANNOT: return cstring_makeLiteralTemp ("<user>");
190	}
191	}
192
28bf4b0b	193	BADEXIT;
	194	}
	195
e5081f8c	196	qual qual_abstractFromCodeChar (char c)
	197	{
	198	switch (c) {
	199	case '-': return qual_createUnknown ();
	200	case 'a': return qual_createAbstract ();
	201	case 'n': return qual_createNumAbstract ();
	202	case 'c': return qual_createConcrete ();
	203	BADDEFAULT;
	204	}
	205	}
	206
	207	char qual_abstractCode (qual q)
	208	{
	209	switch (q->kind) {
	210	case QU_UNKNOWN: return '-';
	211	case QU_ABSTRACT: return 'a';
	212	case QU_NUMABSTRACT: return 'n';
	213	case QU_CONCRETE: return 'c';
	214	BADDEFAULT;
	215	}
	216	}
	217
28bf4b0b	218	extern bool qual_match (qual q1, qual q2)
	219	{
	220	if (q1->kind == q2->kind) {
	221	if (q1->kind == QU_USERANNOT) {
	222	return (annotationInfo_equal (q1->info, q2->info));
	223	} else {
	224	return TRUE;
	225	}
	226	}
	227
	228	return FALSE;
	229	}
	230
	231	extern annotationInfo qual_getAnnotationInfo (qual q)
	232	{
	233	llassert (qual_isMetaState (q));
	234	return q->info;
	235	}
	236
28bf4b0b	237	extern cstring qual_dump (qual q)
28bf4b0b	238	{
6fcd0b1e	239	llassert (isinit);
6fcd0b1e	240
28bf4b0b	241	if (q->kind == QU_USERANNOT)
616915dd	242	{
28bf4b0b	243	return message ("%d.%s",
	244	(int) q->kind,
	245	annotationInfo_dump (q->info));
616915dd	246	}
28bf4b0b	247	else
	248	{
	249	return message ("%d", (int) q->kind);
	250	}
	251	}
616915dd	252
28bf4b0b	253
	254	extern qual qual_undump (char **s)
	255	{
	256	quenum q = (quenum) reader_getInt (s);
6fcd0b1e	257	llassert (isinit);
28bf4b0b	258
	259	if (q == QU_USERANNOT)
	260	{
	261	annotationInfo ai;
	262
	263	reader_checkChar (s, '.');
	264	ai = annotationInfo_undump (s);
	265
	266	return qual_createMetaState (ai);
	267	}
	268	else
	269	{
	270	return qual_createPlain (q);
	271	}
616915dd	272	}
616915dd	273
28bf4b0b	274