[splint.git] / src / source.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2000 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
*/
/*
** 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 "lclintMacros.nf"
# include "llbasic.h"
# include "osd.h"
# include "portab.h"

extern bool
inputStream_close (inputStream s)
{
  if (s->file != NULL)
    {
      check (fileTable_closeFile (context_fileTable (),s->file) == 0);
      s->file = NULL;
      return TRUE;
    }

  return FALSE;
}

extern void
inputStream_free (/*@null@*/ /*@only@*/ inputStream s)
{
  if (s != NULL)
    {
      sfree (s->name);
      sfree (s->stringSource);
      sfree (s->curLine);
      sfree (s);
    }
}

extern /*@only@*/ inputStream 
  inputStream_create (char *name, char *suffix, bool echo)
{
  char *ps;
  inputStream s = (inputStream) dmalloc (sizeof (*s));
  
  s->name = (char *) dmalloc (strlen (name) + strlen (suffix) + 1);
  s->file = 0;
  strcpy (s->name, name);

  ps = strrchr (s->name, CONNECTCHAR);

  if (ps == (char *) 0)
    {
      ps = s->name;
    }

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

  s->lineNo = 0;
  s->charNo = 0;
  s->curLine = NULL;
  s->echo = echo;
  s->fromString = FALSE;
  s->stringSource = NULL;
  s->stringSourceTail = NULL;
  
  return s;
}

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

  s->name = mstring_copy (name);
  s->stringSource = mstring_copy (str);
  s->stringSourceTail = s->stringSource;
  s->file = 0;
  s->echo = FALSE;
  s->fromString = TRUE;
  s->lineNo = 0;
  s->charNo = 0;
  s->curLine = NULL;

  return s;
}

extern int inputStream_nextChar (inputStream s)
{
  int res = inputStream_peekChar (s);

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

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

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

extern int inputStream_peekChar (inputStream s)
{  
  if (s->curLine == NULL)
    {
      s->curLine = NULL;
      s->curLine = inputStream_nextLine (s);
      s->charNo = 0;
    }

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

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

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

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

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

	  len = c - s->stringSourceTail + 1;

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

	  currentLine = &(s->buffer)[0];
	  strncpy (currentLine, s->stringSourceTail, size_fromInt (len));
	  currentLine[len] = '\0';
	  s->stringSourceTail += len;
	}
      
    }
  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 >= 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)
{
  if (s->fromString)
    {
      /* not an error: tail is dependent */
      s->stringSourceTail = s->stringSource; 
      return TRUE;
    }

  DPRINTF (("Open: %s", s->name));
  s->file = fileTable_openFile (context_fileTable (), s->name, "r");
  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 (char *path, inputStream s)
{
  char *returnPath;
  filestatus status;		/* return status of osd_getEnvPath.*/
  bool rVal;			/* return value of this procedure. */

 /* Check if requires met. */
  if (path == NULL || s == NULL || s->name == NULL)
    {
      llbugexitlit ("inputStream_getPath: invalid parameter");
    }

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

  if (status == OSD_FILEFOUND)
    {				/* Should be majority of cases. */
      rVal = TRUE;
      
      sfree (s->name);
      s->name = 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;
}

# ifndef NOLCL
char *specFullName (char *specfile, /*@out@*/ char **inpath)
{
  /* extract the path and the specname associated with the given file */
  char *specname = (char *) dmalloc (sizeof (*specname) 
				     * (strlen (specfile) + 9));
  char *ospecname = specname;
  char *path = (char *) dmalloc (sizeof (*path) * (strlen (specfile)));
  size_t size;
  long int i, j;
  
  /* initialized path to empty string or may have accidental garbage */
  *path = '\0';

  /*@-mayaliasunique@*/ 
  strcpy (specname, specfile);
  /*@=mayaliasunique@*/ 

  /* trim off pathnames in specfile */
  size = strlen (specname);

  for (i = size_toInt (size) - 1; i >= 0; i--)
    {
      if (specname[i] == CONNECTCHAR)
	{
	  /* strcpy (specname, (char *)specname+i+1); */
	  for (j = 0; j <= i; j++)	/* include '/'  */
	    {
	      path[j] = specname[j];
	    }

	  path[i + 1] = '\0';
	  specname += i + 1;
	  break;
	}
    }

  /* 
  ** also remove .lcl file extension, assume it's the last extension
  ** of the file name 
  */

  size = strlen (specname);

  for (i = size_toInt (size) - 1; i >= 0; i--)
    {
      if (specname[i] == '.')
	{
	  specname[i] = '\0';
	  break;
	}
    }
  
  *inpath = path;

  /*
  ** If specname no longer points to the original char,
  ** we need to allocate a new pointer and copy the string.
  */

  if (specname != ospecname) {
    char *rspecname = (char *) dmalloc (sizeof (*rspecname) * (strlen (specname) + 1));
    strcpy (rspecname, specname); /* evs 2000-05-16: Bug: was ospecname! */
    sfree (ospecname);
    return rspecname;
  } 

  return specname;
}
# endif
Commit	Line	Data
616915dd	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
616915dd	3	** Copyright (C) 1994-2000 University of Virginia,
	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
616915dd	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
	47	# include "lclintMacros.nf"
	48	# include "llbasic.h"
	49	# include "osd.h"
	50	# include "portab.h"
	51
	52	extern bool
2c88d156	53	inputStream_close (inputStream s)
616915dd	54	{
	55	if (s->file != NULL)
	56	{
dfd82dce	57	check (fileTable_closeFile (context_fileTable (),s->file) == 0);
616915dd	58	s->file = NULL;
	59	return TRUE;
	60	}
	61
	62	return FALSE;
	63	}
	64
	65	extern void
2c88d156	66	inputStream_free (/@null@/ /@only@/ inputStream s)
616915dd	67	{
	68	if (s != NULL)
	69	{
	70	sfree (s->name);
	71	sfree (s->stringSource);
2c88d156	72	sfree (s->curLine);
616915dd	73	sfree (s);
	74	}
	75	}
	76
2c88d156	77	extern /@only@/ inputStream
2c88d156	78	inputStream_create (char name, char suffix, bool echo)
616915dd	79	{
616915dd	80	char *ps;
2c88d156	81	inputStream s = (inputStream) dmalloc (sizeof (*s));
616915dd	82
	83	s->name = (char *) dmalloc (strlen (name) + strlen (suffix) + 1);
	84	s->file = 0;
	85	strcpy (s->name, name);
	86
	87	ps = strrchr (s->name, CONNECTCHAR);
	88
	89	if (ps == (char *) 0)
	90	{
	91	ps = s->name;
	92	}
	93
	94	if (strchr (ps, '.') == NULL)
	95	{
	96	strcat (s->name, suffix);
	97	}
	98
616915dd	99	s->lineNo = 0;
2c88d156	100	s->charNo = 0;
2c88d156	101	s->curLine = NULL;
616915dd	102	s->echo = echo;
	103	s->fromString = FALSE;
	104	s->stringSource = NULL;
	105	s->stringSourceTail = NULL;
	106
616915dd	107	return s;
	108	}
	109
2c88d156	110	extern /@only@/ inputStream
2c88d156	111	inputStream_fromString (char name, char str)
616915dd	112	{
2c88d156	113	inputStream s = (inputStream) dmalloc (sizeof (*s));
616915dd	114
	115	s->name = mstring_copy (name);
	116	s->stringSource = mstring_copy (str);
	117	s->stringSourceTail = s->stringSource;
	118	s->file = 0;
	119	s->echo = FALSE;
	120	s->fromString = TRUE;
	121	s->lineNo = 0;
2c88d156	122	s->charNo = 0;
	123	s->curLine = NULL;
	124
	125	return s;
	126	}
	127
	128	extern int inputStream_nextChar (inputStream s)
	129	{
	130	int res = inputStream_peekChar (s);
	131
	132	if (res != EOF)
	133	{
	134	if (res == '\n')
	135	{
	136	s->curLine = NULL;
	137	s->charNo = 0;
	138	}
	139	else
	140	{
	141	s->charNo++;
	142	}
	143	}
	144
990ec868	145	DPRINTF (("Next char: %c [%d]", res, res));
2c88d156	146	return res;
2c88d156	147	}
616915dd	148
2c88d156	149	extern int inputStream_peekNChar (inputStream s, int n)
	150	/* Doesn't work across lines! */
	151	{
	152	llassert (s->curLine != NULL);
	153	llassert (s->charNo + n < strlen (s->curLine));
	154	return ((int) s->curLine [s->charNo + n]);
616915dd	155	}
616915dd	156
2c88d156	157	extern int inputStream_peekChar (inputStream s)
	158	{
	159	if (s->curLine == NULL)
	160	{
	161	s->curLine = NULL;
	162	s->curLine = inputStream_nextLine (s);
	163	s->charNo = 0;
	164	}
	165
	166	if (s->curLine == NULL)
	167	{
	168	return EOF;
	169	}
	170
	171	llassert (s->charNo <= strlen (s->curLine));
	172
	173	if (s->curLine[s->charNo] == '\0')
	174	{
	175	return '\n';
	176	}
	177
	178	return ((int) s->curLine [s->charNo]);
	179	}
	180
616915dd	181	extern /@dependent@/ /@null@/
2c88d156	182	char *inputStream_nextLine (inputStream s)
616915dd	183	{
	184	char *currentLine;
	185	int len;
	186
2c88d156	187	llassert (s->curLine == NULL);
	188	s->charNo = 0;
	189
616915dd	190	if (s->fromString)
	191	{
	192	if (s->stringSourceTail == NULL \|\| (strlen (s->stringSourceTail) == 0))
	193	{
	194	currentLine = 0;
	195	}
	196	else
	197	{
	198	char *c = strchr (s->stringSourceTail, '\n');
	199
	200
	201	/* in case line is terminated not by newline */
	202	if (c == 0)
	203	{
	204	c = strchr (s->stringSourceTail, '\0');
	205	}
	206
	207	len = c - s->stringSourceTail + 1;
	208
	209	if (len > STUBMAXRECORDSIZE - 2)
	210	{
	211	len = (STUBMAXRECORDSIZE - 2);
	212	}
	213
	214	currentLine = &(s->buffer)[0];
	215	strncpy (currentLine, s->stringSourceTail, size_fromInt (len));
	216	currentLine[len] = '\0';
	217	s->stringSourceTail += len;
	218	}
	219
	220	}
	221	else
	222	{
	223	llassert (s->file != NULL);
	224	currentLine = fgets (&(s->buffer)[0], STUBMAXRECORDSIZE, s->file);
	225	}
	226	if (currentLine == 0)
	227	{
	228	strcpy (s->buffer, "* End of File *");
	229	}
	230	else
	231	{
	232	s->lineNo++;
	233	len = strlen (currentLine) - 1;
	234	if (s->buffer[len] == '\n')
	235	{
	236	s->buffer[len] = '\0';
	237	}
	238	else
	239	{
	240	if (len >= STUBMAXRECORDSIZE - 2)
	241	{
	242	lldiagmsg (message ("Input line too long: %s",
	243	cstring_fromChars (currentLine)));
	244	}
	245	}
	246	}
2c88d156	247
616915dd	248	/* if (s->echo) slo_echoLine (currentLine); only needed in LCL */
2c88d156	249	return currentLine;
616915dd	250	}
	251
	252	extern bool
2c88d156	253	inputStream_open (inputStream s)
616915dd	254	{
	255	if (s->fromString)
	256	{
	257	/* not an error: tail is dependent */
	258	s->stringSourceTail = s->stringSource;
	259	return TRUE;
	260	}
	261
	262	DPRINTF (("Open: %s", s->name));
dfd82dce	263	s->file = fileTable_openFile (context_fileTable (), s->name, "r");
616915dd	264	return (s->file != 0 \|\| s->fromString);
	265	}
	266
	267	/*
	268	** requires
	269	** path != NULL \and
	270	** s != NULL \and
	271	** s.name == filename (s.name) \|\| filetype (*s.name)
	272	** *s.name consists of a file name and type only ("<filename>.<type>)
	273	** No path name is included
	274	**
	275	** ensures
	276	** if filefound (path, s) then
	277	** result = true \and s.name = filespec_where_file_found (path, *s)
	278	** else
	279	** result = false
	280	*/
	281
2c88d156	282	extern bool inputStream_getPath (char *path, inputStream s)
616915dd	283	{
	284	char *returnPath;
	285	filestatus status; /* return status of osd_getEnvPath.*/
	286	bool rVal; /* return value of this procedure. */
	287
	288	/* Check if requires met. */
	289	if (path == NULL \|\| s == NULL \|\| s->name == NULL)
	290	{
2c88d156	291	llbugexitlit ("inputStream_getPath: invalid parameter");
616915dd	292	}
	293
	294	status = osd_getPath (path, s->name, &returnPath);
	295
	296	if (status == OSD_FILEFOUND)
	297	{ /* Should be majority of cases. */
	298	rVal = TRUE;
	299
	300	sfree (s->name);
	301	s->name = returnPath;
	302	}
	303	else if (status == OSD_FILENOTFOUND)
	304	{
	305	rVal = FALSE;
	306	}
	307	else if (status == OSD_PATHTOOLONG)
	308	{
	309	rVal = FALSE;
	310	/* Directory and filename are too long. Report error. */
	311	llbuglit ("soure_getPath: Filename plus directory from search path too long");
	312	}
	313	else
	314	{
	315	rVal = FALSE;
2c88d156	316	llbuglit ("inputStream_getPath: invalid return status");
616915dd	317	}
	318	return rVal;
	319	}
	320
	321	# ifndef NOLCL
	322	char specFullName (char specfile, /@out@/ char **inpath)
	323	{
	324	/* extract the path and the specname associated with the given file */
	325	char specname = (char ) dmalloc (sizeof (*specname)
	326	* (strlen (specfile) + 9));
	327	char *ospecname = specname;
	328	char path = (char ) dmalloc (sizeof (path) (strlen (specfile)));
	329	size_t size;
	330	long int i, j;
	331
	332	/* initialized path to empty string or may have accidental garbage */
	333	*path = '\0';
	334
	335	/@-mayaliasunique@/
	336	strcpy (specname, specfile);
	337	/@=mayaliasunique@/
	338
	339	/* trim off pathnames in specfile */
	340	size = strlen (specname);
	341
	342	for (i = size_toInt (size) - 1; i >= 0; i--)
	343	{
	344	if (specname[i] == CONNECTCHAR)
	345	{
	346	/* strcpy (specname, (char )specname+i+1); /
	347	for (j = 0; j <= i; j++) /* include '/' */
	348	{
	349	path[j] = specname[j];
	350	}
	351
	352	path[i + 1] = '\0';
	353	specname += i + 1;
	354	break;
	355	}
	356	}
	357
	358	/*
	359	** also remove .lcl file extension, assume it's the last extension
	360	** of the file name
	361	*/
	362
	363	size = strlen (specname);
	364
	365	for (i = size_toInt (size) - 1; i >= 0; i--)
	366	{
	367	if (specname[i] == '.')
	368	{
	369	specname[i] = '\0';
	370	break;
	371	}
	372	}
	373
	374	*inpath = path;
	375
	376	/*
	377	** If specname no longer points to the original char,
	378	** we need to allocate a new pointer and copy the string.
	379	*/
	380
381	if (specname != ospecname) {
382	char rspecname = (char ) dmalloc (sizeof (rspecname) (strlen (specname) + 1));
383	strcpy (rspecname, specname); /* evs 2000-05-16: Bug: was ospecname! */
384	sfree (ospecname);
385	return rspecname;
386	}
387
388	return specname;
389	}
390	# endif
391