[splint.git] / src / imports.c

/*
** LCLint - 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://lclint.cs.virginia.edu
*/
/*
** imports.c
**
** module for importing LCL specs.
**
**  AUTHOR:
**	Yang Meng Tan,
**         Massachusetts Institute of Technology
*/

# include "lclintMacros.nf"
# include "llbasic.h" 
# include "osd.h"
# include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
# include "lclscan.h"
# include "checking.h"
# include "imports.h"
# include "lslparse.h"
# include "lh.h"
# include "llmain.h"
# include "portab.h"
# include "herald.h"

void
outputLCSFile (char *path, char *msg, char *specname)
{
  static bool haserror = FALSE;
  char *sfile = mstring_concat (specname, ".lcs");
  char *outfile = mstring_concat (path, sfile);
  char *s;
  FILE *outfptr = fopen (outfile, "w");
  sfree (sfile);

  DPRINTF (("Output lcl file: %s / %s / %s", path, specname, outfile));
  
  /* check write permission */
  
  if (outfptr == 0)
    {				/* fopen fails */
      if (!haserror)
	{
	  lclplainerror (message ("Cannot write to output file: %s", 
				  cstring_fromChars (outfile)));
	  haserror = TRUE;
	}
      sfree (outfile);
      return;
    }

  fprintf (outfptr, msg);
  fprintf (outfptr, "%s\n", LCL_PARSE_VERSION);
  
  /* output line %LCLimports foo bar ... */
  fprintf (outfptr, "%%LCLimports ");

  lsymbolSet_elements (g_currentImports, sym)
    {
      s = lsymbol_toChars (sym);

      if (s != NULL && !mstring_equal (s, specname))
	{
	  fprintf (outfptr, "%s ", s);
	}
    } end_lsymbolSet_elements;
  
  fprintf (outfptr, "\n");
  
  sort_dump (outfptr, TRUE);
  symtable_dump (g_symtab, outfptr, TRUE);

  check (fclose (outfptr) == 0);  
  sfree (outfile);  
}

void
importCTrait (void)
{
  char **infile = (char **) dmalloc (sizeof (*infile));
  filestatus status = osd_findOnLarchPath (CTRAITSYMSNAME, infile);

  
  switch (status)
    {
    case OSD_FILEFOUND:
      /*
      ** This line was missing before version 2.3f.  Bug fix by Mike Smith.
      **    This looks like a bug - infile is already fully qualified path  
      **    parseSignatures() adds another path to the front and fails to   
      **    open the file.                                                  
      */
	   
      (void) parseSignatures (cstring_fromChars (CTRAITSYMSNAME));
      (void) parseSignatures (cstring_fromChars (*infile));
      break;
    case OSD_FILENOTFOUND:
      /* try spec name */
      status = osd_findOnLarchPath (CTRAITSPECNAME, infile);

      if (status == OSD_FILEFOUND)
	{
	  callLSL (CTRAITSPECNAME,
		   cstring_toCharsSafe
		   (message ("includes %s (%s for String)",
			     cstring_fromChars (CTRAITFILENAMEN), 
			     cstring_fromChars (sort_getName (sort_cstring)))));
	  break;
	}
      else
	{
	  lldiagmsg 
	    (message ("Unable to find %s or %s.  Check LARCH_PATH environment variable.",
		      cstring_fromChars (CTRAITSYMSNAME), 
		      cstring_fromChars (CTRAITSPECNAME)));
	  llexit (LLFAILURE);
	}
    case OSD_PATHTOOLONG:
      lclbug (message ("importCTrait: the concatenated directory and file "
		       "name are too long: %s: "
		       "continuing without it", 
		       cstring_fromChars (CTRAITSPECNAME)));
      break;
    }

  sfree (*infile);
  sfree (infile);
}

/*
** processImport --- load imports from file
**
**    impkind: IMPPLAIN  file on SPEC_PATH
**                       # include "./file.h" if it exists,
**			 # include "<directory where spec was found>/file.h" if not.
**			   (warn if neither exists)
**            IMPBRACKET file in default LCL imports directory
**                       # include <file.h>
**            IMPQUOTE   file directly
**                       # include "file.h"
*/

void
processImport (lsymbol importSymbol, ltoken tok, impkind kind)
{
  bool readableP, oldexporting;
  bool oldFormat = FALSE;
  tsource *imported, *imported2, *lclsource;
  char *bufptr, *tmpbufptr, *cptr;
  char *name;
  lsymbol sym;
  char importName[MAX_NAME_LENGTH + 1], *importFileName, *realfname;
  char *path;
  char *fpath, *fpath2;
  mapping *map;
  filestatus ret;

  importFileName = lsymbol_toCharsSafe (importSymbol);
  name = mstring_concat (importFileName, IO_SUFFIX);
  realfname = name;

  /*
  ** find .lcs file
  */
  
  switch (kind)
    {
    case IMPPLAIN:
      path = cstring_toCharsSafe 
	(message ("%s%c%s", cstring_fromChars (g_localSpecPath), SEPCHAR, context_getLarchPath ()));
      
      break;
    case IMPBRACKET:
      path = mstring_copy (cstring_toCharsSafe (context_getLCLImportDir ()));
      break;
    case IMPQUOTE:
      path = mstring_copy (g_localSpecPath);
      break;
    default:
      path = mstring_createEmpty (); /* suppress gcc error message */
      llbuglit ("bad imports case\n");
    }

  if ((ret = osd_getPath (path, realfname, &fpath)) != OSD_FILEFOUND)
    {
      char *fname2;
      
      if (ret == OSD_PATHTOOLONG)
	{
	  llfatalerrorLoc (cstring_makeLiteral ("Path too long"));
	}
      
      imported2 = tsource_create (importFileName, LCL_SUFFIX, FALSE);
      fname2 = tsource_fileName (imported2);
      
      

      if (osd_getPath (path, fname2, &fpath2) == OSD_FILEFOUND)
	{
	  llfatalerrorLoc
	    (message ("Specs must be processed before it can be imported: %s", 
		      cstring_fromChars (fpath2)));
	}
      else
	{
	  if (kind == IMPPLAIN || kind == IMPQUOTE)
	    llfatalerrorLoc (message ("Cannot find file to import: %s", 
				       cstring_fromChars (realfname)));
	  else
	    llfatalerrorLoc (message ("Cannot find standard import file: %s",
				       cstring_fromChars (realfname)));
	}
    }

  
  imported = tsource_create (fpath, IO_SUFFIX, FALSE);
  
  
  readableP = tsource_open (imported);
    
  if (!readableP)
    {			/* can't read ? */
      llfatalerrorLoc (message ("Cannot open import file for reading: %s",
				 cstring_fromChars (tsource_fileName (imported))));
    }

  bufptr = tsource_nextLine (imported);

  if (bufptr == 0)
    {
      llerror (FLG_SYNTAX, message ("Import file is empty: %s", 
				    cstring_fromChars (tsource_fileName (imported))));
      sfree (name);
      (void) tsource_close (imported);
      tsource_free (imported);

      sfree (path);
      return;
    }

  /* was it processed successfully ? */
  if (firstWord (bufptr, "%FAILED"))
    {
      llfatalerrorLoc
	(message ("Imported file was not checked successfully: %s.", 
		  cstring_fromChars (name)));
    }
  
  /** is it generated by the right version of the checker? 
   **
   ** old .lcs files start with %PASSED
   ** new (compressed) files start with %LCS 
   */
  
  if (firstWord (bufptr, "%PASSED"))
    {
      /* %PASSED Output from LCP Version 2.* and 3.* */
      /*                     1234567890123*/
      /*                                 +*/

      cptr = strstr (bufptr, "LCP Version");
      
      if (cptr != NULL)
	{
	  cptr += 12;
	  if (*cptr != '2' && *cptr != '3')
	    {
	      llfatalerrorLoc (message ("Imported file is obsolete: %s.",
					 cstring_fromChars (bufptr)));
	    }
	}
      oldFormat = TRUE;
    }
  else 
    {
      if (!firstWord (bufptr, "%LCS"))
	{
	  llfatalerrorLoc (message ("Imported file is not in correct format: %s.",
				    cstring_fromChars (bufptr)));
	}
    }
  
  /* push the imported LCL spec onto g_currentImports */

  context_enterImport ();
  
  bufptr = tsource_nextLine (imported);
  llassert (bufptr != NULL);

  tmpbufptr = bufptr;

    /* expect %LCLimports foo bar ... */
  if (firstWord (bufptr, "%LCLimports "))
    {
      bufptr = bufptr + strlen ("%LCLimports ");
      while (sscanf (bufptr, "%s", importName) == 1)
	{
	  bufptr = bufptr + strlen (importName) + 1;	/* 1 for space */
	  sym = lsymbol_fromChars (importName);
	  if (sym == importSymbol || 
	      lsymbolSet_member (g_currentImports, sym))
	    {
	      /* ensure that the import list does not contain itself: an
		 invariant useful for checking imports cycles. */
	      lclsource = LCLScanSource ();
	      lclfatalerror (tok, 
			     message ("Imports cycle: %s.lcl imports %s",
				      cstring_fromChars (importFileName),
				      cstring_fromChars (importName)));
	    }	  
	  /* push them onto g_currentImports */
	  /* evs - 94 Apr 3:  I don't think it should do this! */
	  /* (void) lsymbolSet_insert (g_currentImports, sym); */
	}
    }
  else
    {
      lclsource = LCLScanSource ();
      lclfatalerror (tok, message ("Unexpected line in imported file %s: %s", 
				   cstring_fromChars (name), 
				   cstring_fromChars (bufptr)));
    }
	  
  /* read in the imported info */
  oldexporting = sort_setExporting (TRUE);

  map = mapping_create ();

  /* tok for error line numbering */

  if (oldFormat)
    {
            sort_import (imported, tok, map);	
    }

  (void) sort_setExporting (oldexporting);

  /* sort_import updates a mapping of old anonymous sorts to new
     anonymous sort that is needed in symtable_import */
  /* mapping_print (map); */
  
  if (oldFormat)
    {
      symtable_import (imported, tok, map);
    }
  else
    {
      /* symtable_loadImport (imported, tok, map); */
    }
  
  check (tsource_close (imported));
  tsource_free (imported);

  sfree (map);
  sfree (name);
  sfree (path);

  context_leaveImport ();  
}
Commit	Line	Data
616915dd	1	/*
	2	** LCLint - annotation-assisted static program checker
	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
	22	** For more information: http://lclint.cs.virginia.edu
	23	*/
	24	/*
	25	** imports.c
	26	**
	27	** module for importing LCL specs.
	28	**
	29	** AUTHOR:
	30	** Yang Meng Tan,
	31	** Massachusetts Institute of Technology
	32	*/
	33
	34	# include "lclintMacros.nf"
	35	# include "llbasic.h"
	36	# include "osd.h"
	37	# include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
	38	# include "lclscan.h"
	39	# include "checking.h"
	40	# include "imports.h"
	41	# include "lslparse.h"
	42	# include "lh.h"
	43	# include "llmain.h"
	44	# include "portab.h"
	45	# include "herald.h"
	46
	47	void
	48	outputLCSFile (char path, char msg, char *specname)
	49	{
	50	static bool haserror = FALSE;
	51	char *sfile = mstring_concat (specname, ".lcs");
	52	char *outfile = mstring_concat (path, sfile);
	53	char *s;
	54	FILE *outfptr = fopen (outfile, "w");
	55	sfree (sfile);
	56
	57	DPRINTF (("Output lcl file: %s / %s / %s", path, specname, outfile));
	58
	59	/* check write permission */
	60
	61	if (outfptr == 0)
	62	{ /* fopen fails */
	63	if (!haserror)
	64	{
65	lclplainerror (message ("Cannot write to output file: %s",
66	cstring_fromChars (outfile)));
67	haserror = TRUE;
68	}
69	sfree (outfile);
70	return;
71	}
72
73	fprintf (outfptr, msg);
74	fprintf (outfptr, "%s\n", LCL_PARSE_VERSION);
75
76	/* output line %LCLimports foo bar ... */
77	fprintf (outfptr, "%%LCLimports ");
78
79	lsymbolSet_elements (g_currentImports, sym)
80	{
81	s = lsymbol_toChars (sym);
82
83	if (s != NULL && !mstring_equal (s, specname))
84	{
85	fprintf (outfptr, "%s ", s);
86	}
87	} end_lsymbolSet_elements;
88
89	fprintf (outfptr, "\n");
90
91	sort_dump (outfptr, TRUE);
92	symtable_dump (g_symtab, outfptr, TRUE);
93
94	check (fclose (outfptr) == 0);
95	sfree (outfile);
96	}
97
98	void
99	importCTrait (void)
100	{
101	char infile = (char ) dmalloc (sizeof (*infile));
102	filestatus status = osd_findOnLarchPath (CTRAITSYMSNAME, infile);
103
104
105	switch (status)
106	{
107	case OSD_FILEFOUND:
108	/*
109	** This line was missing before version 2.3f. Bug fix by Mike Smith.
110	** This looks like a bug - infile is already fully qualified path
111	** parseSignatures() adds another path to the front and fails to
112	** open the file.
113	*/
114
115	(void) parseSignatures (cstring_fromChars (CTRAITSYMSNAME));
116	(void) parseSignatures (cstring_fromChars (*infile));
117	break;
118	case OSD_FILENOTFOUND:
119	/* try spec name */
120	status = osd_findOnLarchPath (CTRAITSPECNAME, infile);
121
122	if (status == OSD_FILEFOUND)
123	{
124	callLSL (CTRAITSPECNAME,
125	cstring_toCharsSafe
126	(message ("includes %s (%s for String)",
127	cstring_fromChars (CTRAITFILENAMEN),
128	cstring_fromChars (sort_getName (sort_cstring)))));
129	break;
130	}
131	else
132	{
133	lldiagmsg
134	(message ("Unable to find %s or %s. Check LARCH_PATH environment variable.",
135	cstring_fromChars (CTRAITSYMSNAME),
136	cstring_fromChars (CTRAITSPECNAME)));
137	llexit (LLFAILURE);
138	}
139	case OSD_PATHTOOLONG:
140	lclbug (message ("importCTrait: the concatenated directory and file "
141	"name are too long: %s: "
142	"continuing without it",
143	cstring_fromChars (CTRAITSPECNAME)));
144	break;
145	}
146
147	sfree (*infile);
148	sfree (infile);
149	}
150
151	/*
152	** processImport --- load imports from file
153	**
154	** impkind: IMPPLAIN file on SPEC_PATH
155	** # include "./file.h" if it exists,
156	** # include "<directory where spec was found>/file.h" if not.
157	** (warn if neither exists)
158	** IMPBRACKET file in default LCL imports directory
159	** # include <file.h>
160	** IMPQUOTE file directly
161	** # include "file.h"
162	*/
163
164	void
165	processImport (lsymbol importSymbol, ltoken tok, impkind kind)
166	{
167	bool readableP, oldexporting;
168	bool oldFormat = FALSE;
169	tsource imported, imported2, *lclsource;
170	char bufptr, tmpbufptr, *cptr;
171	char *name;
172	lsymbol sym;
173	char importName[MAX_NAME_LENGTH + 1], importFileName, realfname;
174	char *path;
175	char fpath, fpath2;
176	mapping *map;
177	filestatus ret;
178
179	importFileName = lsymbol_toCharsSafe (importSymbol);
180	name = mstring_concat (importFileName, IO_SUFFIX);
181	realfname = name;
182
183	/*
184	** find .lcs file
185	*/
186
187	switch (kind)
188	{
189	case IMPPLAIN:
190	path = cstring_toCharsSafe
191	(message ("%s%c%s", cstring_fromChars (g_localSpecPath), SEPCHAR, context_getLarchPath ()));
192
193	break;
194	case IMPBRACKET:
195	path = mstring_copy (cstring_toCharsSafe (context_getLCLImportDir ()));
196	break;
197	case IMPQUOTE:
198	path = mstring_copy (g_localSpecPath);
199	break;
200	default:
201	path = mstring_createEmpty (); /* suppress gcc error message */
202	llbuglit ("bad imports case\n");
203	}
204
205	if ((ret = osd_getPath (path, realfname, &fpath)) != OSD_FILEFOUND)
206	{
207	char *fname2;
208
209	if (ret == OSD_PATHTOOLONG)
210	{
211	llfatalerrorLoc (cstring_makeLiteral ("Path too long"));
212	}
213
214	imported2 = tsource_create (importFileName, LCL_SUFFIX, FALSE);
215	fname2 = tsource_fileName (imported2);
216
217
218
219	if (osd_getPath (path, fname2, &fpath2) == OSD_FILEFOUND)
220	{
221	llfatalerrorLoc
222	(message ("Specs must be processed before it can be imported: %s",
223	cstring_fromChars (fpath2)));
224	}
225	else
226	{
227	if (kind == IMPPLAIN \|\| kind == IMPQUOTE)
228	llfatalerrorLoc (message ("Cannot find file to import: %s",
229	cstring_fromChars (realfname)));
230	else
231	llfatalerrorLoc (message ("Cannot find standard import file: %s",
232	cstring_fromChars (realfname)));
233	}
234	}
235
236
237	imported = tsource_create (fpath, IO_SUFFIX, FALSE);
238
239
240	readableP = tsource_open (imported);
241
242	if (!readableP)
243	{ /* can't read ? */
244	llfatalerrorLoc (message ("Cannot open import file for reading: %s",
245	cstring_fromChars (tsource_fileName (imported))));
246	}
247
248	bufptr = tsource_nextLine (imported);
249
250	if (bufptr == 0)
251	{
252	llerror (FLG_SYNTAX, message ("Import file is empty: %s",
253	cstring_fromChars (tsource_fileName (imported))));
254	sfree (name);
255	(void) tsource_close (imported);
256	tsource_free (imported);
257
258	sfree (path);
259	return;
260	}
261
262	/* was it processed successfully ? */
263	if (firstWord (bufptr, "%FAILED"))
264	{
265	llfatalerrorLoc
266	(message ("Imported file was not checked successfully: %s.",
267	cstring_fromChars (name)));
268	}
269
270	/** is it generated by the right version of the checker?
271	**
272	** old .lcs files start with %PASSED
273	** new (compressed) files start with %LCS
274	*/
275
276	if (firstWord (bufptr, "%PASSED"))
277	{
278	/* %PASSED Output from LCP Version 2.* and 3.* */
279	/* 1234567890123*/
280	/* +*/
281
282	cptr = strstr (bufptr, "LCP Version");
283
284	if (cptr != NULL)
285	{
286	cptr += 12;
287	if (cptr != '2' && cptr != '3')
288	{
289	llfatalerrorLoc (message ("Imported file is obsolete: %s.",
290	cstring_fromChars (bufptr)));
291	}
292	}
293	oldFormat = TRUE;
294	}
295	else
296	{
297	if (!firstWord (bufptr, "%LCS"))
298	{
299	llfatalerrorLoc (message ("Imported file is not in correct format: %s.",
300	cstring_fromChars (bufptr)));
301	}
302	}
303
304	/* push the imported LCL spec onto g_currentImports */
305
306	context_enterImport ();
307
308	bufptr = tsource_nextLine (imported);
309	llassert (bufptr != NULL);
310
311	tmpbufptr = bufptr;
312
313	/* expect %LCLimports foo bar ... */
314	if (firstWord (bufptr, "%LCLimports "))
315	{
316	bufptr = bufptr + strlen ("%LCLimports ");
317	while (sscanf (bufptr, "%s", importName) == 1)
318	{
319	bufptr = bufptr + strlen (importName) + 1; /* 1 for space */
320	sym = lsymbol_fromChars (importName);
321	if (sym == importSymbol \|\|
322	lsymbolSet_member (g_currentImports, sym))
323	{
324	/* ensure that the import list does not contain itself: an
325	invariant useful for checking imports cycles. */
326	lclsource = LCLScanSource ();
327	lclfatalerror (tok,
328	message ("Imports cycle: %s.lcl imports %s",
329	cstring_fromChars (importFileName),
330	cstring_fromChars (importName)));
331	}
332	/* push them onto g_currentImports */
333	/* evs - 94 Apr 3: I don't think it should do this! */
334	/* (void) lsymbolSet_insert (g_currentImports, sym); */
335	}
336	}
337	else
338	{
339	lclsource = LCLScanSource ();
340	lclfatalerror (tok, message ("Unexpected line in imported file %s: %s",
341	cstring_fromChars (name),
342	cstring_fromChars (bufptr)));
343	}
344
345	/* read in the imported info */
346	oldexporting = sort_setExporting (TRUE);
347
348	map = mapping_create ();
349
350	/* tok for error line numbering */
351
352	if (oldFormat)
353	{
354	sort_import (imported, tok, map);
355	}
356
357	(void) sort_setExporting (oldexporting);
358
359	/* sort_import updates a mapping of old anonymous sorts to new
360	anonymous sort that is needed in symtable_import */
361	/* mapping_print (map); */
362
363	if (oldFormat)
364	{
365	symtable_import (imported, tok, map);
366	}
367	else
368	{
369	/* symtable_loadImport (imported, tok, map); */
370	}
371
372	check (tsource_close (imported));
373	tsource_free (imported);
374
375	sfree (map);
376	sfree (name);
377	sfree (path);
378
379	context_leaveImport ();
380	}
381
382
383