[splint.git] / src / mtContextNode.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
*/
/*
** mtContextNode.c
*/

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

static bool mtContextNode_matchesType (mtContextNode, ctype) /*@*/ ;

static /*@observer@*/ cstring mtContextKind_unparse (mtContextKind ck)
{
  switch (ck)
    {
    case MTC_ANY: return cstring_makeLiteralTemp ("any");
    case MTC_PARAM: return cstring_makeLiteralTemp ("parameter"); 
    case MTC_RESULT: return cstring_makeLiteralTemp ("result"); 
    case MTC_REFERENCE: return cstring_makeLiteralTemp ("reference");
    case MTC_CLAUSE: return cstring_makeLiteralTemp ("clause");
    case MTC_LITERAL: return cstring_makeLiteralTemp ("literal");
    case MTC_NULL: return cstring_makeLiteralTemp ("null");
    }

  BADBRANCHRET (cstring_undefined);
}
 
static mtContextNode mtContextNode_create (mtContextKind context, ctype ct) 
{
  mtContextNode res = (mtContextNode) dmalloc (sizeof (*res));
  res->context = context;
  res->type = ct;
  DPRINTF (("Create: %s", mtContextNode_unparse (res)));
  return res;
}

extern mtContextNode mtContextNode_createAny ()
{
  return mtContextNode_create (MTC_ANY, ctype_unknown);
}

extern mtContextNode mtContextNode_createParameter (ctype ct) 
{
  return mtContextNode_create (MTC_PARAM, ct);
}

extern mtContextNode mtContextNode_createResult (ctype ct) 
{
  return mtContextNode_create (MTC_RESULT, ct);
}

extern mtContextNode mtContextNode_createReference (ctype ct) 
{
  return mtContextNode_create (MTC_REFERENCE, ct);
}

extern mtContextNode mtContextNode_createClause (ctype ct) 
{
  return mtContextNode_create (MTC_CLAUSE, ct);
}

extern mtContextNode mtContextNode_createLiteral (ctype ct) 
{
  return mtContextNode_create (MTC_LITERAL, ct);
}

extern mtContextNode mtContextNode_createNull (ctype ct) 
{
  return mtContextNode_create (MTC_NULL, ct);
}

extern void mtContextNode_free (/*@only@*/ mtContextNode node) 
{
  sfree (node);
}

bool mtContextNode_matchesEntry (mtContextNode context, uentry ue)
{
  ctype ct;

  llassert (mtContextNode_isDefined (context));

  DPRINTF (("Matches context: %s / %s",
	    mtContextNode_unparse (context), uentry_unparse (ue)));

  switch (context->context)
    {
    case MTC_ANY: break; /* everything matches */
    case MTC_RESULT:
      if (!uentry_isFunction (ue))
	{
	  return FALSE;
	}
      break;
    case MTC_PARAM: 
      if (!uentry_isAnyParam (ue))
	{
	  DPRINTF (("not param: %s", uentry_unparseFull (ue)));
	  return FALSE;
	}
      break;
    case MTC_LITERAL:
    case MTC_NULL:
      return FALSE;
    case MTC_REFERENCE:
      break;
    case MTC_CLAUSE:
      BADBRANCH;
    }

  if (uentry_isFunction (ue))
    {
      ct = ctype_getReturnType (uentry_getType (ue));
    }
  else
    {
      ct = uentry_getType (ue);
    }

  return mtContextNode_matchesType (context, ct);
}

bool mtContextNode_matchesRef (mtContextNode context, sRef sr)
{
  ctype ct;

  llassert (mtContextNode_isDefined (context));

  DPRINTF (("Matches context: %s / %s",
	    mtContextNode_unparse (context), sRef_unparse (sr)));

  switch (context->context)
    {
    case MTC_ANY: break; /* everything matches */
    case MTC_RESULT:
      DPRINTF (("Result? %s / %s",
		sRef_unparseFull (sr),
		bool_unparse (sRef_isResult (sr))));
      return sRef_isResult (sr);
    case MTC_PARAM: 
      if (!sRef_isParam (sr))
	{
	  return FALSE;
	}
      break;
    case MTC_LITERAL:
      DPRINTF (("Literal: %s", sRef_unparse (sr)));
      if (!sRef_isConst (sr))
	{
	  return FALSE;
	}
      break;
    case MTC_NULL:
    case MTC_REFERENCE:
      break;
    case MTC_CLAUSE:
      BADBRANCH;
    }

  ct = sRef_getType (sr);
  return mtContextNode_matchesType (context, ct);
}

bool mtContextNode_matchesRefStrict (mtContextNode context, sRef s)
{
  if (mtContextNode_isDefined (context)
      && mtContextNode_matchesRef (context, s))
    {
      if (ctype_isKnown (context->type) 
	  && (ctype_isUnknown (sRef_getType (s))
	      || ctype_isVoidPointer (sRef_getType (s))))
	{
	  return FALSE;
	}
      else
	{
	  return TRUE;
	}
    }
  
  return FALSE;
}

bool mtContextNode_matchesType (mtContextNode context, ctype ct)
{
  DPRINTF (("Context type..."));
  llassert (mtContextNode_isDefined (context));
  
  if (!ctype_match (context->type, ct))
    {
      DPRINTF (("Type mismatch: %s / %s",
		ctype_unparse (context->type),
		ctype_unparse (ct)));
      return FALSE;
    }
  else
    {
      /* evans 2001-08-21 - don't match if only one type is unknown */
      if (ctype_isUnknown (ct) && !ctype_isUnknown (context->type))
	{
	  return FALSE;
	}

      DPRINTF (("Type okay: %s / %s",
		ctype_unparse (context->type),
		ctype_unparse (ct)));
    }
  
  return TRUE;
}

cstring mtContextNode_unparse (mtContextNode node)
{
  llassert (mtContextNode_isDefined (node));

  if (ctype_isKnown (node->type))
    {
      return message ("%s %s", mtContextKind_unparse (node->context),
		      ctype_unparse (node->type));
    }
  else
    {
      return message ("%s", mtContextKind_unparse (node->context));
    }
}

bool mtContextNode_isClause (mtContextNode n)
{
  llassert (mtContextNode_isDefined (n));
  return (n->context == MTC_CLAUSE);
}

bool mtContextNode_isParameter (mtContextNode n)
{
  llassert (mtContextNode_isDefined (n));
  return (n->context == MTC_PARAM);
}

bool mtContextNode_isReference (mtContextNode n)
{
  llassert (mtContextNode_isDefined (n));
  return (n->context == MTC_REFERENCE);
}

bool mtContextNode_isResult (mtContextNode n)
{
  llassert (mtContextNode_isDefined (n));
  return (n->context == MTC_RESULT);
}

bool mtContextNode_isLiteral (mtContextNode n)
{
  llassert (mtContextNode_isDefined (n));
  return (n->context == MTC_LITERAL);
}

bool mtContextNode_isNull (mtContextNode n)
{
  llassert (mtContextNode_isDefined (n));
  return (n->context == MTC_NULL);
}

void mtContextNode_showRefError (mtContextNode context, sRef sr)
{
  ctype ct;

  llassert (mtContextNode_isDefined (context));
  llassert (!mtContextNode_matchesRef (context, sr));

  DPRINTF (("Matches context: %s / %s",
	    mtContextNode_unparse (context), sRef_unparse (sr)));

  switch (context->context)
    {
    case MTC_ANY: break; /* everything matches */
    case MTC_RESULT:
      if (!sRef_isResult (sr))
	{
	  llgenindentmsgnoloc 
	    (message ("Context is result, doesn't match %q", sRef_unparse (sr)));
	  return;
	}
      break;
    case MTC_PARAM: 
      if (!sRef_isResult (sr))
	{
	  llgenindentmsgnoloc 
	    (message ("Context is parameter, doesn't match %q", sRef_unparse (sr)));
	  return;
	}
      break;
    case MTC_LITERAL:
      DPRINTF (("Literal: %s", sRef_unparse (sr)));
      if (!sRef_isConst (sr))
	{
	  llgenindentmsgnoloc
	    (message ("Context is literal, doesn't match %q", sRef_unparse (sr)));
	  return;
	}
      break;
    case MTC_NULL:
    case MTC_REFERENCE:
      break;
    case MTC_CLAUSE:
      BADBRANCH;
    }

  ct = sRef_getType (sr);
  
  if (!mtContextNode_matchesType (context, ct))
    {
      llgenindentmsgnoloc
	(message ("Context type is %s, doesn't match type %s", 
		  ctype_unparse (context->type),
		  ctype_unparse (ct)));
    }
  else
    {
      BADBRANCH;
    }
}
Commit	Line	Data
28bf4b0b	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
c59f5181	3	** Copyright (C) 1994-2003 University of Virginia,
28bf4b0b	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
28bf4b0b	23	*/
	24	/*
	25	** mtContextNode.c
	26	*/
	27
1b8ae690	28	# include "splintMacros.nf"
28bf4b0b	29	# include "basic.h"
28bf4b0b	30
	31	static bool mtContextNode_matchesType (mtContextNode, ctype) /@/ ;
	32
	33	static /@observer@/ cstring mtContextKind_unparse (mtContextKind ck)
	34	{
	35	switch (ck)
	36	{
	37	case MTC_ANY: return cstring_makeLiteralTemp ("any");
12f2ffe9	38	case MTC_PARAM: return cstring_makeLiteralTemp ("parameter");
b072092f	39	case MTC_RESULT: return cstring_makeLiteralTemp ("result");
28bf4b0b	40	case MTC_REFERENCE: return cstring_makeLiteralTemp ("reference");
28bf4b0b	41	case MTC_CLAUSE: return cstring_makeLiteralTemp ("clause");
12f2ffe9	42	case MTC_LITERAL: return cstring_makeLiteralTemp ("literal");
12f2ffe9	43	case MTC_NULL: return cstring_makeLiteralTemp ("null");
28bf4b0b	44	}
28bf4b0b	45
8250fa4a	46	BADBRANCHRET (cstring_undefined);
28bf4b0b	47	}
	48
	49	static mtContextNode mtContextNode_create (mtContextKind context, ctype ct)
	50	{
	51	mtContextNode res = (mtContextNode) dmalloc (sizeof (*res));
	52	res->context = context;
	53	res->type = ct;
	54	DPRINTF (("Create: %s", mtContextNode_unparse (res)));
	55	return res;
	56	}
	57
	58	extern mtContextNode mtContextNode_createAny ()
	59	{
	60	return mtContextNode_create (MTC_ANY, ctype_unknown);
	61	}
	62
	63	extern mtContextNode mtContextNode_createParameter (ctype ct)
	64	{
	65	return mtContextNode_create (MTC_PARAM, ct);
	66	}
	67
b072092f	68	extern mtContextNode mtContextNode_createResult (ctype ct)
	69	{
	70	return mtContextNode_create (MTC_RESULT, ct);
	71	}
	72
28bf4b0b	73	extern mtContextNode mtContextNode_createReference (ctype ct)
	74	{
	75	return mtContextNode_create (MTC_REFERENCE, ct);
	76	}
	77
	78	extern mtContextNode mtContextNode_createClause (ctype ct)
	79	{
	80	return mtContextNode_create (MTC_CLAUSE, ct);
	81	}
	82
12f2ffe9	83	extern mtContextNode mtContextNode_createLiteral (ctype ct)
	84	{
	85	return mtContextNode_create (MTC_LITERAL, ct);
	86	}
	87
	88	extern mtContextNode mtContextNode_createNull (ctype ct)
	89	{
	90	return mtContextNode_create (MTC_NULL, ct);
	91	}
	92
28bf4b0b	93	extern void mtContextNode_free (/@only@/ mtContextNode node)
	94	{
	95	sfree (node);
	96	}
	97
	98	bool mtContextNode_matchesEntry (mtContextNode context, uentry ue)
	99	{
	100	ctype ct;
	101
	102	llassert (mtContextNode_isDefined (context));
	103
	104	DPRINTF (("Matches context: %s / %s",
	105	mtContextNode_unparse (context), uentry_unparse (ue)));
	106
	107	switch (context->context)
	108	{
	109	case MTC_ANY: break; /* everything matches */
b072092f	110	case MTC_RESULT:
	111	if (!uentry_isFunction (ue))
	112	{
	113	return FALSE;
	114	}
	115	break;
28bf4b0b	116	case MTC_PARAM:
6970c11b	117	if (!uentry_isAnyParam (ue))
28bf4b0b	118	{
6970c11b	119	DPRINTF (("not param: %s", uentry_unparseFull (ue)));
28bf4b0b	120	return FALSE;
	121	}
	122	break;
12f2ffe9	123	case MTC_LITERAL:
	124	case MTC_NULL:
	125	return FALSE;
28bf4b0b	126	case MTC_REFERENCE:
	127	break;
	128	case MTC_CLAUSE:
	129	BADBRANCH;
	130	}
	131
	132	if (uentry_isFunction (ue))
	133	{
	134	ct = ctype_getReturnType (uentry_getType (ue));
	135	}
	136	else
	137	{
	138	ct = uentry_getType (ue);
	139	}
	140
	141	return mtContextNode_matchesType (context, ct);
	142	}
	143
	144	bool mtContextNode_matchesRef (mtContextNode context, sRef sr)
	145	{
	146	ctype ct;
	147
	148	llassert (mtContextNode_isDefined (context));
	149
	150	DPRINTF (("Matches context: %s / %s",
	151	mtContextNode_unparse (context), sRef_unparse (sr)));
	152
	153	switch (context->context)
	154	{
	155	case MTC_ANY: break; /* everything matches */
b072092f	156	case MTC_RESULT:
	157	DPRINTF (("Result? %s / %s",
	158	sRef_unparseFull (sr),
	159	bool_unparse (sRef_isResult (sr))));
	160	return sRef_isResult (sr);
28bf4b0b	161	case MTC_PARAM:
	162	if (!sRef_isParam (sr))
	163	{
	164	return FALSE;
	165	}
	166	break;
12f2ffe9	167	case MTC_LITERAL:
	168	DPRINTF (("Literal: %s", sRef_unparse (sr)));
	169	if (!sRef_isConst (sr))
	170	{
	171	return FALSE;
	172	}
	173	break;
	174	case MTC_NULL:
28bf4b0b	175	case MTC_REFERENCE:
	176	break;
	177	case MTC_CLAUSE:
	178	BADBRANCH;
	179	}
	180
	181	ct = sRef_getType (sr);
	182	return mtContextNode_matchesType (context, ct);
	183	}
	184
	185	bool mtContextNode_matchesRefStrict (mtContextNode context, sRef s)
	186	{
abd7f895	187	if (mtContextNode_isDefined (context)
abd7f895	188	&& mtContextNode_matchesRef (context, s))
28bf4b0b	189	{
	190	if (ctype_isKnown (context->type)
	191	&& (ctype_isUnknown (sRef_getType (s))
	192	\|\| ctype_isVoidPointer (sRef_getType (s))))
	193	{
	194	return FALSE;
	195	}
	196	else
	197	{
	198	return TRUE;
	199	}
	200	}
	201
	202	return FALSE;
	203	}
	204
	205	bool mtContextNode_matchesType (mtContextNode context, ctype ct)
	206	{
	207	DPRINTF (("Context type..."));
abd7f895	208	llassert (mtContextNode_isDefined (context));
28bf4b0b	209
	210	if (!ctype_match (context->type, ct))
	211	{
	212	DPRINTF (("Type mismatch: %s / %s",
	213	ctype_unparse (context->type),
	214	ctype_unparse (ct)));
	215	return FALSE;
	216	}
	217	else
	218	{
b7e84605	219	/* evans 2001-08-21 - don't match if only one type is unknown */
	220	if (ctype_isUnknown (ct) && !ctype_isUnknown (context->type))
	221	{
	222	return FALSE;
	223	}
	224
28bf4b0b	225	DPRINTF (("Type okay: %s / %s",
	226	ctype_unparse (context->type),
	227	ctype_unparse (ct)));
	228	}
	229
	230	return TRUE;
	231	}
	232
	233	cstring mtContextNode_unparse (mtContextNode node)
	234	{
abd7f895	235	llassert (mtContextNode_isDefined (node));
abd7f895	236
28bf4b0b	237	if (ctype_isKnown (node->type))
	238	{
	239	return message ("%s %s", mtContextKind_unparse (node->context),
	240	ctype_unparse (node->type));
	241	}
	242	else
	243	{
	244	return message ("%s", mtContextKind_unparse (node->context));
	245	}
	246	}
	247
	248	bool mtContextNode_isClause (mtContextNode n)
	249	{
	250	llassert (mtContextNode_isDefined (n));
	251	return (n->context == MTC_CLAUSE);
	252	}
	253
	254	bool mtContextNode_isParameter (mtContextNode n)
	255	{
	256	llassert (mtContextNode_isDefined (n));
	257	return (n->context == MTC_PARAM);
	258	}
	259
b072092f	260	bool mtContextNode_isReference (mtContextNode n)
28bf4b0b	261	{
	262	llassert (mtContextNode_isDefined (n));
	263	return (n->context == MTC_REFERENCE);
	264	}
	265
b072092f	266	bool mtContextNode_isResult (mtContextNode n)
	267	{
	268	llassert (mtContextNode_isDefined (n));
	269	return (n->context == MTC_RESULT);
	270	}
	271
12f2ffe9	272	bool mtContextNode_isLiteral (mtContextNode n)
	273	{
	274	llassert (mtContextNode_isDefined (n));
	275	return (n->context == MTC_LITERAL);
	276	}
	277
	278	bool mtContextNode_isNull (mtContextNode n)
	279	{
	280	llassert (mtContextNode_isDefined (n));
	281	return (n->context == MTC_NULL);
	282	}
	283
b7e84605	284	void mtContextNode_showRefError (mtContextNode context, sRef sr)
	285	{
	286	ctype ct;
	287
	288	llassert (mtContextNode_isDefined (context));
	289	llassert (!mtContextNode_matchesRef (context, sr));
	290
	291	DPRINTF (("Matches context: %s / %s",
	292	mtContextNode_unparse (context), sRef_unparse (sr)));
	293
	294	switch (context->context)
	295	{
	296	case MTC_ANY: break; /* everything matches */
	297	case MTC_RESULT:
	298	if (!sRef_isResult (sr))
	299	{
	300	llgenindentmsgnoloc
	301	(message ("Context is result, doesn't match %q", sRef_unparse (sr)));
	302	return;
	303	}
	304	break;
	305	case MTC_PARAM:
	306	if (!sRef_isResult (sr))
	307	{
	308	llgenindentmsgnoloc
	309	(message ("Context is parameter, doesn't match %q", sRef_unparse (sr)));
	310	return;
	311	}
	312	break;
	313	case MTC_LITERAL:
	314	DPRINTF (("Literal: %s", sRef_unparse (sr)));
	315	if (!sRef_isConst (sr))
	316	{
	317	llgenindentmsgnoloc
	318	(message ("Context is literal, doesn't match %q", sRef_unparse (sr)));
	319	return;
	320	}
	321	break;
	322	case MTC_NULL:
	323	case MTC_REFERENCE:
	324	break;
	325	case MTC_CLAUSE:
	326	BADBRANCH;
	327	}
	328
	329	ct = sRef_getType (sr);
	330
	331	if (!mtContextNode_matchesType (context, ct))
	332	{
	333	llgenindentmsgnoloc
	334	(message ("Context type is %s, doesn't match type %s",
	335	ctype_unparse (context->type),
	336	ctype_unparse (ct)));
	337	}
	338	else
	339	{
	340	BADBRANCH;
	341	}
	342	}
28bf4b0b	343
	344
	345