2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: splint@cs.virginia.edu
21 ** To report a bug: splint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
27 ** module for importing LCL specs.
31 ** Massachusetts Institute of Technology
34 # include "splintMacros.nf"
37 # include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
39 # include "checking.h"
41 # include "lslparse.h"
47 outputLCSFile (char *path, char *msg, char *specname)
49 static bool haserror = FALSE;
50 char *sfile = mstring_concat (specname, ".lcs");
51 char *outfile = mstring_concat (path, sfile);
53 FILE *outfptr = fileTable_openFile (context_fileTable (), cstring_fromChars (outfile), "w");
56 DPRINTF (("Output lcl file: %s / %s / %s", path, specname, outfile));
58 /* check write permission */
60 if (outfptr == NULL) /* Cannot open file */
64 lclplainerror (message ("Cannot write to output file: %s",
65 cstring_fromChars (outfile)));
72 fprintf (outfptr, "%s", msg);
73 fprintf (outfptr, "%s\n", LCL_PARSE_VERSION);
75 /* output line %LCLimports foo bar ... */
76 fprintf (outfptr, "%%LCLimports ");
78 lsymbolSet_elements (g_currentImports, sym)
80 s = lsymbol_toChars (sym);
82 if (s != NULL && !mstring_equal (s, specname))
84 fprintf (outfptr, "%s ", s);
86 } end_lsymbolSet_elements;
88 fprintf (outfptr, "\n");
90 sort_dump (outfptr, TRUE);
91 symtable_dump (g_symtab, outfptr, TRUE);
93 check (fileTable_closeFile (context_fileTable (), outfptr));
100 cstring infile = cstring_undefined;
101 filestatus status = osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSYMSNAME),
108 ** This line was missing before version 2.3f. Bug fix by Mike Smith.
109 ** This looks like a bug - infile is already fully qualified path
110 ** parseSignatures() adds another path to the front and fails to
114 (void) parseSignatures (cstring_fromCharsNew (CTRAITSYMSNAME));
115 (void) parseSignatures (infile);
117 case OSD_FILENOTFOUND:
119 status = osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSPECNAME),
122 if (status == OSD_FILEFOUND)
124 callLSL (cstring_makeLiteralTemp (CTRAITSPECNAME),
125 message ("includes %s (%s for String)",
126 cstring_fromChars (CTRAITFILENAMEN),
127 cstring_fromChars (sort_getName (sort_cstring))));
128 cstring_free (infile);
134 (message ("Unable to find %s or %s. Check LARCH_PATH environment variable.",
135 cstring_fromChars (CTRAITSYMSNAME),
136 cstring_fromChars (CTRAITSPECNAME)));
137 cstring_free (infile);
140 case OSD_PATHTOOLONG:
141 lclbug (message ("importCTrait: the concatenated directory and file "
142 "name are too long: %s: "
143 "continuing without it",
144 cstring_fromChars (CTRAITSPECNAME)));
145 cstring_free (infile);
151 ** processImport --- load imports from file
153 ** impkind: IMPPLAIN file on SPEC_PATH
154 ** # include "./file.h" if it exists,
155 ** # include "<directory where spec was found>/file.h" if not.
156 ** (warn if neither exists)
157 ** IMPBRACKET file in default LCL imports directory
158 ** # include <file.h>
159 ** IMPQUOTE file directly
160 ** # include "file.h"
164 processImport (lsymbol importSymbol, ltoken tok, impkind kind)
166 bool readableP, oldexporting;
167 bool compressedFormat = FALSE;
168 inputStream imported, imported2, lclsource;
174 char importName[MAX_NAME_LENGTH + 1];
175 cstring importFileName;
176 cstring path = cstring_undefined;
177 cstring fpath, fpath2;
181 importFileName = lsymbol_toString (importSymbol);
182 name = cstring_concat (importFileName, cstring_makeLiteralTemp (IO_SUFFIX));
191 path = message ("%s%c%s", cstring_fromChars (g_localSpecPath), PATH_SEPARATOR,
192 context_getLarchPath ());
196 path = cstring_copy (context_getLCLImportDir ());
199 path = cstring_fromCharsNew (g_localSpecPath);
202 llbuglit ("bad imports case\n");
205 if ((ret = osd_getPath (path, name, &fpath)) != OSD_FILEFOUND)
209 if (ret == OSD_PATHTOOLONG)
211 llfatalerrorLoc (cstring_makeLiteral ("Path too long"));
214 imported2 = inputStream_create (cstring_copy (importFileName),
215 LCL_EXTENSION, FALSE);
216 fname2 = inputStream_fileName (imported2);
218 if (osd_getPath (path, fname2, &fpath2) == OSD_FILEFOUND)
221 (message ("Specs must be processed before it can be imported: %s",
226 if (kind == IMPPLAIN || kind == IMPQUOTE)
228 llfatalerrorLoc (message ("Cannot find file to import: %s", name));
232 llfatalerrorLoc (message ("Cannot find standard import file: %s", name));
238 imported = inputStream_create (fpath, cstring_makeLiteralTemp (IO_SUFFIX), FALSE);
240 readableP = inputStream_open (imported);
244 llfatalerrorLoc (message ("Cannot open import file for reading: %s",
245 inputStream_fileName (imported)));
248 bufptr = inputStream_nextLine (imported);
252 llerror (FLG_SYNTAX, message ("Import file is empty: %s",
253 inputStream_fileName (imported)));
255 (void) inputStream_close (imported);
256 inputStream_free (imported);
262 /* was it processed successfully ? */
263 if (firstWord (bufptr, "%FAILED"))
266 (message ("Imported file was not checked successfully: %s.", name));
270 ** Is it generated by the right version of the checker?
272 ** Uncompressed .lcs files start with %PASSED
273 ** Compressed files start with %LCS
276 if (firstWord (bufptr, "%PASSED"))
278 /* %PASSED Output from LCP Version 2.* and 3.* */
282 cptr = strstr (bufptr, "LCP Version");
287 ** Only really old files start this way!
291 if (*cptr != '2' && *cptr != '3')
293 llfatalerrorLoc (message ("Imported file %s is obsolete: %s.",
294 inputStream_fileName (imported),
295 cstring_fromChars (bufptr)));
299 compressedFormat = FALSE;
303 if (!firstWord (bufptr, "%LCS"))
305 llfatalerrorLoc (message ("Imported file %s is not in correct format: %s",
306 inputStream_fileName (imported),
307 cstring_fromChars (bufptr)));
310 compressedFormat = TRUE;
313 /* push the imported LCL spec onto g_currentImports */
315 context_enterImport ();
317 bufptr = inputStream_nextLine (imported);
318 llassert (bufptr != NULL);
322 /* expect %LCLimports foo bar ... */
323 if (firstWord (bufptr, "%LCLimports "))
325 bufptr = bufptr + strlen ("%LCLimports ");
326 while (sscanf (bufptr, "%s", importName) == 1)
328 bufptr = bufptr + strlen (importName) + 1; /* 1 for space */
329 sym = lsymbol_fromChars (importName);
330 if (sym == importSymbol ||
331 lsymbolSet_member (g_currentImports, sym))
333 /* ensure that the import list does not contain itself: an
334 invariant useful for checking imports cycles. */
335 lclsource = LCLScanSource ();
337 message ("Imports cycle: %s%s imports %s",
340 cstring_fromChars (importName)));
342 /* push them onto g_currentImports */
343 /* evs - 94 Apr 3: I don't think it should do this! */
344 /* (void) lsymbolSet_insert (g_currentImports, sym); */
349 lclsource = LCLScanSource ();
350 lclfatalerror (tok, message ("Unexpected line in imported file %s: %s",
352 cstring_fromChars (bufptr)));
355 /* read in the imported info */
356 oldexporting = sort_setExporting (TRUE);
358 map = mapping_create ();
360 /* tok for error line numbering */
362 if (!compressedFormat)
364 sort_import (imported, tok, map);
367 (void) sort_setExporting (oldexporting);
369 /* sort_import updates a mapping of old anonymous sorts to new
370 anonymous sort that is needed in symtable_import */
371 /* mapping_print (map); */
373 if (!compressedFormat)
375 symtable_import (imported, tok, map);
379 /* symtable_loadImport (imported, tok, map); */
382 check (inputStream_close (imported));
383 inputStream_free (imported);
389 context_leaveImport ();