[splint.git] / src / mtContextNode.c

/*
** 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
** 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 lclint: lclint-request@cs.virginia.edu
** To report a bug: lclint-bug@cs.virginia.edu
** For more information: http://www.splint.org
*/
/*
** mtContextNode.c
*/

# include "lclintMacros.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_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..."));
  
  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)
{
  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
77d37419	3	** Copyright (C) 1994-2002 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	**
	20	** For information on lclint: lclint-request@cs.virginia.edu
	21	** To report a bug: lclint-bug@cs.virginia.edu
11db3170	22	** For more information: http://www.splint.org
28bf4b0b	23	*/
	24	/*
	25	** mtContextNode.c
	26	*/
	27
	28	# include "lclintMacros.nf"
	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	{
	187	if (mtContextNode_matchesRef (context, s))
	188	{
	189	if (ctype_isKnown (context->type)
	190	&& (ctype_isUnknown (sRef_getType (s))
	191	\|\| ctype_isVoidPointer (sRef_getType (s))))
	192	{
	193	return FALSE;
	194	}
	195	else
	196	{
	197	return TRUE;
	198	}
	199	}
	200
	201	return FALSE;
	202	}
	203
	204	bool mtContextNode_matchesType (mtContextNode context, ctype ct)
	205	{
	206	DPRINTF (("Context type..."));
	207
	208	if (!ctype_match (context->type, ct))
	209	{
	210	DPRINTF (("Type mismatch: %s / %s",
	211	ctype_unparse (context->type),
	212	ctype_unparse (ct)));
	213	return FALSE;
	214	}
	215	else
	216	{
b7e84605	217	/* evans 2001-08-21 - don't match if only one type is unknown */
	218	if (ctype_isUnknown (ct) && !ctype_isUnknown (context->type))
	219	{
	220	return FALSE;
	221	}
	222
28bf4b0b	223	DPRINTF (("Type okay: %s / %s",
	224	ctype_unparse (context->type),
	225	ctype_unparse (ct)));
	226	}
	227
	228	return TRUE;
	229	}
	230
	231	cstring mtContextNode_unparse (mtContextNode node)
	232	{
	233	if (ctype_isKnown (node->type))
	234	{
	235	return message ("%s %s", mtContextKind_unparse (node->context),
	236	ctype_unparse (node->type));
	237	}
	238	else
	239	{
	240	return message ("%s", mtContextKind_unparse (node->context));
	241	}
	242	}
	243
	244	bool mtContextNode_isClause (mtContextNode n)
	245	{
	246	llassert (mtContextNode_isDefined (n));
	247	return (n->context == MTC_CLAUSE);
	248	}
	249
	250	bool mtContextNode_isParameter (mtContextNode n)
	251	{
	252	llassert (mtContextNode_isDefined (n));
	253	return (n->context == MTC_PARAM);
	254	}
	255
b072092f	256	bool mtContextNode_isReference (mtContextNode n)
28bf4b0b	257	{
	258	llassert (mtContextNode_isDefined (n));
	259	return (n->context == MTC_REFERENCE);
	260	}
	261
b072092f	262	bool mtContextNode_isResult (mtContextNode n)
	263	{
	264	llassert (mtContextNode_isDefined (n));
	265	return (n->context == MTC_RESULT);
	266	}
	267
12f2ffe9	268	bool mtContextNode_isLiteral (mtContextNode n)
	269	{
	270	llassert (mtContextNode_isDefined (n));
	271	return (n->context == MTC_LITERAL);
	272	}
	273
	274	bool mtContextNode_isNull (mtContextNode n)
	275	{
	276	llassert (mtContextNode_isDefined (n));
	277	return (n->context == MTC_NULL);
	278	}
	279
b7e84605	280	void mtContextNode_showRefError (mtContextNode context, sRef sr)
	281	{
	282	ctype ct;
	283
	284	llassert (mtContextNode_isDefined (context));
	285	llassert (!mtContextNode_matchesRef (context, sr));
	286
	287	DPRINTF (("Matches context: %s / %s",
	288	mtContextNode_unparse (context), sRef_unparse (sr)));
	289
	290	switch (context->context)
	291	{
	292	case MTC_ANY: break; /* everything matches */
	293	case MTC_RESULT:
	294	if (!sRef_isResult (sr))
	295	{
	296	llgenindentmsgnoloc
	297	(message ("Context is result, doesn't match %q", sRef_unparse (sr)));
	298	return;
	299	}
	300	break;
	301	case MTC_PARAM:
	302	if (!sRef_isResult (sr))
	303	{
	304	llgenindentmsgnoloc
	305	(message ("Context is parameter, doesn't match %q", sRef_unparse (sr)));
	306	return;
	307	}
	308	break;
	309	case MTC_LITERAL:
	310	DPRINTF (("Literal: %s", sRef_unparse (sr)));
	311	if (!sRef_isConst (sr))
	312	{
	313	llgenindentmsgnoloc
	314	(message ("Context is literal, doesn't match %q", sRef_unparse (sr)));
	315	return;
	316	}
	317	break;
	318	case MTC_NULL:
	319	case MTC_REFERENCE:
	320	break;
	321	case MTC_CLAUSE:
	322	BADBRANCH;
	323	}
	324
	325	ct = sRef_getType (sr);
	326
	327	if (!mtContextNode_matchesType (context, ct))
	328	{
	329	llgenindentmsgnoloc
	330	(message ("Context type is %s, doesn't match type %s",
	331	ctype_unparse (context->type),
	332	ctype_unparse (ct)));
	333	}
	334	else
	335	{
	336	BADBRANCH;
	337	}
	338	}
28bf4b0b	339
	340
	341