[splint.git] / src / inputStream.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
*/
/*
** source.c
**
** Interface to source file abstraction
**
**	NOTE:	    This module is almost identical to the one for LCL.  The
**		    only difference is that a couple of source lines have been
**		    commented out.
**
**		    This module has too many dependencies to be in the common
**		    source area.  Any of the solutions that would allow this
**		    module to be common had its own set of compromises.  It
**		    seemed best and most straightforward to just keep separte
**		    copies for LSL and LCL.  We should examine this again if we
**		    ever reorganize the module structure.
**
**  AUTHORS:
**
**     Steve Garland,
**         Massachusetts Institute of Technology
**     Joe Wild, Technical Languages and Environments, DECspec project
*/

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

extern bool
inputStream_close (inputStream s)
{
  llassert (inputStream_isDefined (s));

  if (s->file != NULL)
    {
      check (fileTable_closeFile (context_fileTable (), s->file));
      s->file = NULL;
      return TRUE;
    }

  return FALSE;
}

extern void
inputStream_free (/*@null@*/ /*@only@*/ inputStream s)
{
  if (inputStream_isDefined (s))
    {
      cstring_free (s->name);
      cstring_free (s->stringSource);
      sfree (s);
    }
}

extern /*@only@*/ inputStream 
inputStream_create (cstring name, cstring suffix, bool echo)
{
  char *ps;
  inputStream s = (inputStream) dmalloc (sizeof (*s));

  s->name = name;
  s->file = NULL;

  /*@access cstring@*/
  llassert (cstring_isDefined (s->name));
  ps = strrchr (s->name, CONNECTCHAR);

  if (ps == NULL)
    {
      ps = s->name;
    }
  /*@noaccess cstring@*/

  if (strchr (ps, '.') == NULL)
    {
      s->name = cstring_concatFree1 (s->name, suffix);
    }

  s->name = fileLib_cleanName (s->name);

  s->lineNo = 0;
  s->charNo = 0;
  s->curLine = NULL;
  s->echo = echo;
  s->fromString = FALSE;
  s->stringSource = NULL;
  s->stringSourceTail = NULL;
  s->buffer[0] = '\0';

  return s;
}

extern /*@only@*/ inputStream 
inputStream_fromString (cstring name, cstring str)
{
  inputStream s = (inputStream) dmalloc (sizeof (*s));

  s->name = cstring_copy (name);
  s->stringSource = cstring_copy (str);
  s->stringSourceTail = s->stringSource;
  s->file = 0;
  s->echo = FALSE;
  s->fromString = TRUE;
  s->lineNo = 0;
  s->charNo = 0;
  s->curLine = NULL;
  s->buffer[0] = '\0';

  return s;
}

extern int inputStream_nextChar (inputStream s)
{
  int res;

  llassert (inputStream_isDefined (s));
  res = inputStream_peekChar (s);

  if (res != EOF) 
    {
      if (res == (int) '\n')
	{
	  s->curLine = NULL;
	  s->charNo = 0;
	  incLine ();
	}
      else
	{
	  s->charNo++;
	  incColumn ();
	}
    }

  DPRINTF (("Next char: %c [%d]", (char) res, res));
  return res;
}

extern int inputStream_peekNChar (inputStream s, int n)
     /* Doesn't work across lines! */
{
  llassert (inputStream_isDefined (s));
  llassert (s->curLine != NULL);
  llassert (s->charNo + n < strlen (s->curLine));
  return ((int) s->curLine [s->charNo + n]);
}

extern int inputStream_peekChar (inputStream s)
{  
  llassert (inputStream_isDefined (s));

  if (s->curLine == NULL)
    {
      char *cur;
      s->curLine = NULL;
      cur = inputStream_nextLine (s);
      s->curLine = cur; /* split this to avoid possible undefined behavior */
      s->charNo = 0;
    }

  if (s->curLine == NULL)  
    {
      return EOF;
    }
 
  llassert (s->charNo <= strlen (s->curLine));

  if (s->curLine[s->charNo] == '\0') 
    {
      return (int) '\n';
    }
 
  return ((int) s->curLine [s->charNo]);
} 

extern /*@dependent@*/ /*@null@*/ 
char *inputStream_nextLine (inputStream s)
{
  char *currentLine;
  size_t len;

  llassert (inputStream_isDefined (s));
  llassert (s->curLine == NULL);
  s->charNo = 0;

  if (s->fromString)
    {
      if (cstring_isEmpty (s->stringSourceTail))
	{
	  currentLine = 0;
	}
      else
	{
	  /*@access cstring@*/
	  char *c = strchr (s->stringSourceTail, '\n');
	  
	  /* in case line is terminated not by newline */ 
	  if (c == 0)
	    {
	      c = strchr (s->stringSourceTail, '\0');
	    }

	  len = size_fromInt (c - s->stringSourceTail + 1);

	  if (len > size_fromInt (STUBMAXRECORDSIZE - 2))
	    {
	      len = size_fromInt (STUBMAXRECORDSIZE - 2);
	    }

	  currentLine = &(s->buffer)[0];
	  strncpy (currentLine, s->stringSourceTail, len);
	  currentLine[len] = '\0';
	  s->stringSourceTail += len;
	  /*@noaccess cstring@*/
	}
      
    }
  else
    {
      llassert (s->file != NULL);
      currentLine = fgets (&(s->buffer)[0], STUBMAXRECORDSIZE, s->file);
    }
  if (currentLine == 0)
    {
      strcpy (s->buffer, "*** End of File ***");
    }
  else
    {
      s->lineNo++;
      len = strlen (currentLine) - 1;
      if (s->buffer[len] == '\n')
	{
	  s->buffer[len] = '\0';
	}
      else 
	{
	  if (len >= size_fromInt (STUBMAXRECORDSIZE - 2))
	    {
	      lldiagmsg (message ("Input line too long: %s",
				  cstring_fromChars (currentLine)));
	    }
	}
    }

  /* if (s->echo) slo_echoLine (currentLine);		only needed in LCL */
  return currentLine;
}

extern bool
inputStream_open (inputStream s)
{
  llassert (inputStream_isDefined (s));
  if (s->fromString)
    {
      /* not an error: tail is dependent */
      s->stringSourceTail = s->stringSource; 
      return TRUE;
    }

  DPRINTF (("Opening: %s", s->name));
  s->file = fileTable_openReadFile (context_fileTable (), s->name);
  return (s->file != 0 || s->fromString);
}

/*
** requires
**  path != NULL \and
**  s != NULL \and
**  *s.name == filename (*s.name) || filetype (*s.name)
**      *s.name consists of a file name and type only ("<filename>.<type>)
**	No path name is included
**
** ensures
**  if filefound (*path, *s) then
**	result = true \and *s.name = filespec_where_file_found (*path, *s)
**  else
**	result = false
*/

extern bool inputStream_getPath (cstring path, inputStream s)
{
  cstring returnPath;
  filestatus status;		/* return status of osd_getEnvPath.*/
  bool rVal;			/* return value of this procedure. */
  
  llassert (cstring_isDefined (path));
  llassert (inputStream_isDefined (s));
  llassert (cstring_isDefined (s->name));

  status = osd_getPath (path, s->name, &returnPath);

  if (status == OSD_FILEFOUND)
    {				/* Should be majority of cases. */
      rVal = TRUE;
      
      cstring_free (s->name);
      s->name = fileLib_cleanName (returnPath);
    }
  else if (status == OSD_FILENOTFOUND)
    {
      rVal = FALSE;
    }
  else if (status == OSD_PATHTOOLONG)
    {
      rVal = FALSE;
     /* Directory and filename are too long.  Report error. */
     llbuglit ("soure_getPath: Filename plus directory from search path too long");
 }
  else
    {
      rVal = FALSE;
      llbuglit ("inputStream_getPath: invalid return status");
    }

  return rVal;
}

/*:open:*/ FILE *inputStream_getFile (inputStream s)
{
  llassert (inputStream_isDefined (s));
  llassert (s->file != NULL);
  return s->file;
}

cstring inputStream_fileName (inputStream s)
{
  llassert (inputStream_isDefined (s));
  return s->name;
}

bool inputStream_isOpen (inputStream s)
{
  return (inputStream_isDefined (s) && (s->file != 0 || s->fromString));
}

int inputStream_thisLineNumber (inputStream s)
{
  llassert (inputStream_isDefined (s));
  return s->lineNo;
}
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	** source.c
	26	**
	27	** Interface to source file abstraction
	28	**
	29	** NOTE: This module is almost identical to the one for LCL. The
	30	** only difference is that a couple of source lines have been
	31	** commented out.
	32	**
	33	** This module has too many dependencies to be in the common
	34	** source area. Any of the solutions that would allow this
	35	** module to be common had its own set of compromises. It
	36	** seemed best and most straightforward to just keep separte
	37	** copies for LSL and LCL. We should examine this again if we
	38	** ever reorganize the module structure.
	39	**
	40	** AUTHORS:
	41	**
	42	** Steve Garland,
	43	** Massachusetts Institute of Technology
	44	** Joe Wild, Technical Languages and Environments, DECspec project
	45	*/
	46
1b8ae690	47	# include "splintMacros.nf"
b73d1009	48	# include "basic.h"
28bf4b0b	49	# include "osd.h"
	50	# include "portab.h"
	51
	52	extern bool
	53	inputStream_close (inputStream s)
	54	{
	55	llassert (inputStream_isDefined (s));
	56
	57	if (s->file != NULL)
	58	{
dfd82dce	59	check (fileTable_closeFile (context_fileTable (), s->file));
28bf4b0b	60	s->file = NULL;
	61	return TRUE;
	62	}
	63
	64	return FALSE;
	65	}
	66
	67	extern void
	68	inputStream_free (/@null@/ /@only@/ inputStream s)
	69	{
	70	if (inputStream_isDefined (s))
	71	{
	72	cstring_free (s->name);
	73	cstring_free (s->stringSource);
	74	sfree (s);
	75	}
	76	}
	77
	78	extern /@only@/ inputStream
6fcd0b1e	79	inputStream_create (cstring name, cstring suffix, bool echo)
28bf4b0b	80	{
	81	char *ps;
	82	inputStream s = (inputStream) dmalloc (sizeof (*s));
6fcd0b1e	83
28bf4b0b	84	s->name = name;
	85	s->file = NULL;
	86
	87	/@access cstring@/
	88	llassert (cstring_isDefined (s->name));
28bf4b0b	89	ps = strrchr (s->name, CONNECTCHAR);
	90
	91	if (ps == NULL)
	92	{
	93	ps = s->name;
	94	}
	95	/@noaccess cstring@/
	96
	97	if (strchr (ps, '.') == NULL)
	98	{
	99	s->name = cstring_concatFree1 (s->name, suffix);
	100	}
	101
	102	s->name = fileLib_cleanName (s->name);
	103
	104	s->lineNo = 0;
	105	s->charNo = 0;
	106	s->curLine = NULL;
	107	s->echo = echo;
	108	s->fromString = FALSE;
	109	s->stringSource = NULL;
	110	s->stringSourceTail = NULL;
6fcd0b1e	111	s->buffer[0] = '\0';
6fcd0b1e	112
b73d1009	113	return s;
28bf4b0b	114	}
	115
	116	extern /@only@/ inputStream
	117	inputStream_fromString (cstring name, cstring str)
	118	{
	119	inputStream s = (inputStream) dmalloc (sizeof (*s));
	120
	121	s->name = cstring_copy (name);
	122	s->stringSource = cstring_copy (str);
	123	s->stringSourceTail = s->stringSource;
	124	s->file = 0;
	125	s->echo = FALSE;
	126	s->fromString = TRUE;
	127	s->lineNo = 0;
	128	s->charNo = 0;
	129	s->curLine = NULL;
3120b462	130	s->buffer[0] = '\0';
28bf4b0b	131
	132	return s;
	133	}
	134
	135	extern int inputStream_nextChar (inputStream s)
	136	{
	137	int res;
	138
	139	llassert (inputStream_isDefined (s));
	140	res = inputStream_peekChar (s);
	141
	142	if (res != EOF)
	143	{
	144	if (res == (int) '\n')
	145	{
	146	s->curLine = NULL;
	147	s->charNo = 0;
	148	incLine ();
	149	}
	150	else
	151	{
	152	s->charNo++;
	153	incColumn ();
	154	}
	155	}
	156
	157	DPRINTF (("Next char: %c [%d]", (char) res, res));
	158	return res;
	159	}
	160
	161	extern int inputStream_peekNChar (inputStream s, int n)
	162	/* Doesn't work across lines! */
	163	{
abd7f895	164	llassert (inputStream_isDefined (s));
28bf4b0b	165	llassert (s->curLine != NULL);
	166	llassert (s->charNo + n < strlen (s->curLine));
	167	return ((int) s->curLine [s->charNo + n]);
	168	}
	169
	170	extern int inputStream_peekChar (inputStream s)
	171	{
abd7f895	172	llassert (inputStream_isDefined (s));
abd7f895	173
28bf4b0b	174	if (s->curLine == NULL)
	175	{
	176	char *cur;
	177	s->curLine = NULL;
	178	cur = inputStream_nextLine (s);
	179	s->curLine = cur; /* split this to avoid possible undefined behavior */
	180	s->charNo = 0;
	181	}
	182
	183	if (s->curLine == NULL)
	184	{
	185	return EOF;
	186	}
	187
	188	llassert (s->charNo <= strlen (s->curLine));
	189
	190	if (s->curLine[s->charNo] == '\0')
	191	{
	192	return (int) '\n';
	193	}
	194
	195	return ((int) s->curLine [s->charNo]);
	196	}
	197
	198	extern /@dependent@/ /@null@/
	199	char *inputStream_nextLine (inputStream s)
	200	{
	201	char *currentLine;
e5081f8c	202	size_t len;
28bf4b0b	203
abd7f895	204	llassert (inputStream_isDefined (s));
28bf4b0b	205	llassert (s->curLine == NULL);
	206	s->charNo = 0;
	207
	208	if (s->fromString)
	209	{
	210	if (cstring_isEmpty (s->stringSourceTail))
	211	{
	212	currentLine = 0;
	213	}
	214	else
	215	{
	216	/@access cstring@/
	217	char *c = strchr (s->stringSourceTail, '\n');
	218
	219	/* in case line is terminated not by newline */
	220	if (c == 0)
	221	{
	222	c = strchr (s->stringSourceTail, '\0');
	223	}
	224
e5081f8c	225	len = size_fromInt (c - s->stringSourceTail + 1);
28bf4b0b	226
e5081f8c	227	if (len > size_fromInt (STUBMAXRECORDSIZE - 2))
28bf4b0b	228	{
e5081f8c	229	len = size_fromInt (STUBMAXRECORDSIZE - 2);
28bf4b0b	230	}
	231
	232	currentLine = &(s->buffer)[0];
e5081f8c	233	strncpy (currentLine, s->stringSourceTail, len);
28bf4b0b	234	currentLine[len] = '\0';
	235	s->stringSourceTail += len;
	236	/@noaccess cstring@/
	237	}
	238
	239	}
	240	else
	241	{
	242	llassert (s->file != NULL);
	243	currentLine = fgets (&(s->buffer)[0], STUBMAXRECORDSIZE, s->file);
	244	}
	245	if (currentLine == 0)
	246	{
	247	strcpy (s->buffer, "* End of File *");
	248	}
	249	else
	250	{
	251	s->lineNo++;
	252	len = strlen (currentLine) - 1;
	253	if (s->buffer[len] == '\n')
	254	{
	255	s->buffer[len] = '\0';
	256	}
	257	else
	258	{
e5081f8c	259	if (len >= size_fromInt (STUBMAXRECORDSIZE - 2))
28bf4b0b	260	{
	261	lldiagmsg (message ("Input line too long: %s",
	262	cstring_fromChars (currentLine)));
	263	}
	264	}
	265	}
	266
	267	/* if (s->echo) slo_echoLine (currentLine); only needed in LCL */
	268	return currentLine;
	269	}
	270
	271	extern bool
	272	inputStream_open (inputStream s)
	273	{
abd7f895	274	llassert (inputStream_isDefined (s));
28bf4b0b	275	if (s->fromString)
	276	{
	277	/* not an error: tail is dependent */
	278	s->stringSourceTail = s->stringSource;
	279	return TRUE;
	280	}
	281
d5047b91	282	DPRINTF (("Opening: %s", s->name));
d5047b91	283	s->file = fileTable_openReadFile (context_fileTable (), s->name);
28bf4b0b	284	return (s->file != 0 \|\| s->fromString);
	285	}
	286
	287	/*
	288	** requires
	289	** path != NULL \and
	290	** s != NULL \and
	291	** s.name == filename (s.name) \|\| filetype (*s.name)
	292	** *s.name consists of a file name and type only ("<filename>.<type>)
	293	** No path name is included
	294	**
	295	** ensures
	296	** if filefound (path, s) then
	297	** result = true \and s.name = filespec_where_file_found (path, *s)
	298	** else
	299	** result = false
	300	*/
	301
	302	extern bool inputStream_getPath (cstring path, inputStream s)
	303	{
	304	cstring returnPath;
	305	filestatus status; /* return status of osd_getEnvPath.*/
	306	bool rVal; /* return value of this procedure. */
	307
	308	llassert (cstring_isDefined (path));
	309	llassert (inputStream_isDefined (s));
	310	llassert (cstring_isDefined (s->name));
	311
	312	status = osd_getPath (path, s->name, &returnPath);
	313
	314	if (status == OSD_FILEFOUND)
	315	{ /* Should be majority of cases. */
	316	rVal = TRUE;
	317
	318	cstring_free (s->name);
	319	s->name = fileLib_cleanName (returnPath);
	320	}
	321	else if (status == OSD_FILENOTFOUND)
	322	{
	323	rVal = FALSE;
	324	}
	325	else if (status == OSD_PATHTOOLONG)
	326	{
	327	rVal = FALSE;
	328	/* Directory and filename are too long. Report error. */
	329	llbuglit ("soure_getPath: Filename plus directory from search path too long");
	330	}
	331	else
	332	{
	333	rVal = FALSE;
	334	llbuglit ("inputStream_getPath: invalid return status");
	335	}
	336
	337	return rVal;
	338	}
	339
15b3d2b2	340	/:open:/ FILE *inputStream_getFile (inputStream s)
28bf4b0b	341	{
28bf4b0b	342	llassert (inputStream_isDefined (s));
abd7f895	343	llassert (s->file != NULL);
28bf4b0b	344	return s->file;
	345	}
	346
	347	cstring inputStream_fileName (inputStream s)
	348	{
	349	llassert (inputStream_isDefined (s));
	350	return s->name;
	351	}
	352
	353	bool inputStream_isOpen (inputStream s)
	354	{
	355	return (inputStream_isDefined (s) && (s->file != 0 \|\| s->fromString));
	356	}
	357
	358	int inputStream_thisLineNumber (inputStream s)
	359	{
	360	llassert (inputStream_isDefined (s));
	361	return s->lineNo;
	362	}
	363
	364
	365
	366