2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 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: info@splint.org
21 ** To report a bug: splint-bug@splint.org
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"
46 outputLCSFile (char *path
, char *msg
, char *specname
)
48 static bool haserror
= FALSE
;
49 char *sfile
= mstring_concat (specname
, ".lcs");
50 char *outfile
= mstring_concat (path
, sfile
);
52 FILE *outfptr
= fileTable_openWriteFile (context_fileTable (), cstring_fromChars (outfile
));
55 DPRINTF (("Output lcl file: %s / %s / %s", path
, specname
, outfile
));
57 /* check write permission */
59 if (outfptr
== NULL
) /* Cannot open file */
63 lclplainerror (message ("Cannot write to output file: %s",
64 cstring_fromChars (outfile
)));
71 fprintf (outfptr
, "%s", msg
);
72 fprintf (outfptr
, "%s\n", LCL_PARSE_VERSION
);
74 /* output line %LCLimports foo bar ... */
75 fprintf (outfptr
, "%%LCLimports ");
77 lsymbolSet_elements (g_currentImports
, sym
)
79 s
= lsymbol_toChars (sym
);
81 if (s
!= NULL
&& !mstring_equal (s
, specname
))
83 fprintf (outfptr
, "%s ", s
);
85 } end_lsymbolSet_elements
;
87 fprintf (outfptr
, "\n");
89 sort_dump (outfptr
, TRUE
);
90 symtable_dump (g_symtab
, outfptr
, TRUE
);
92 check (fileTable_closeFile (context_fileTable (), outfptr
));
99 cstring infile
= cstring_undefined
;
100 filestatus status
= osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSYMSNAME
),
107 ** This line was missing before version 2.3f. Bug fix by Mike Smith.
108 ** This looks like a bug - infile is already fully qualified path
109 ** parseSignatures() adds another path to the front and fails to
113 (void) parseSignatures (cstring_fromCharsNew (CTRAITSYMSNAME
));
114 (void) parseSignatures (infile
);
116 case OSD_FILENOTFOUND
:
118 status
= osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSPECNAME
),
121 if (status
== OSD_FILEFOUND
)
123 callLSL (cstring_makeLiteralTemp (CTRAITSPECNAME
),
124 message ("includes %s (%s for String)",
125 cstring_fromChars (CTRAITFILENAMEN
),
126 cstring_fromChars (sort_getName (g_sortCstring
))));
127 cstring_free (infile
);
133 (message ("Unable to find %s or %s. Check LARCH_PATH environment variable.",
134 cstring_fromChars (CTRAITSYMSNAME
),
135 cstring_fromChars (CTRAITSPECNAME
)));
136 cstring_free (infile
);
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 cstring_free (infile
);
150 ** processImport --- load imports from file
152 ** impkind: IMPPLAIN file on SPEC_PATH
153 ** # include "./file.h" if it exists,
154 ** # include "<directory where spec was found>/file.h" if not.
155 ** (warn if neither exists)
156 ** IMPBRACKET file in default LCL imports directory
157 ** # include <file.h>
158 ** IMPQUOTE file directly
159 ** # include "file.h"
163 processImport (lsymbol importSymbol
, ltoken tok
, impkind kind
)
165 bool readableP
, oldexporting
;
166 bool compressedFormat
= FALSE
;
167 inputStream imported
, imported2
, lclsource
;
173 char importName
[MAX_NAME_LENGTH
+ 1];
174 cstring importFileName
;
175 cstring path
= cstring_undefined
;
176 cstring fpath
, fpath2
;
180 importFileName
= lsymbol_toString (importSymbol
);
181 name
= cstring_concat (importFileName
, cstring_makeLiteralTemp (IO_SUFFIX
));
190 path
= message ("%s%c%s", cstring_fromChars (g_localSpecPath
), PATH_SEPARATOR
,
191 context_getLarchPath ());
195 path
= cstring_copy (context_getLCLImportDir ());
198 path
= cstring_fromCharsNew (g_localSpecPath
);
201 llbuglit ("bad imports case\n");
204 if ((ret
= osd_getPath (path
, name
, &fpath
)) != OSD_FILEFOUND
)
208 if (ret
== OSD_PATHTOOLONG
)
210 llfatalerrorLoc (cstring_makeLiteral ("Path too long"));
213 imported2
= inputStream_create (cstring_copy (importFileName
),
214 LCL_EXTENSION
, FALSE
);
215 fname2
= inputStream_fileName (imported2
);
217 if (osd_getPath (path
, fname2
, &fpath2
) == OSD_FILEFOUND
)
220 (message ("Specs must be processed before it can be imported: %s",
225 if (kind
== IMPPLAIN
|| kind
== IMPQUOTE
)
227 llfatalerrorLoc (message ("Cannot find file to import: %s", name
));
231 llfatalerrorLoc (message ("Cannot find standard import file: %s", name
));
237 imported
= inputStream_create (fpath
, cstring_makeLiteralTemp (IO_SUFFIX
), FALSE
);
239 readableP
= inputStream_open (imported
);
243 llfatalerrorLoc (message ("Cannot open import file for reading: %s",
244 inputStream_fileName (imported
)));
247 bufptr
= inputStream_nextLine (imported
);
251 llerror (FLG_SYNTAX
, message ("Import file is empty: %s",
252 inputStream_fileName (imported
)));
254 (void) inputStream_close (imported
);
255 inputStream_free (imported
);
261 /* was it processed successfully ? */
262 if (firstWord (bufptr
, "%FAILED"))
265 (message ("Imported file was not checked successfully: %s.", name
));
269 ** Is it generated by the right version of the checker?
271 ** Uncompressed .lcs files start with %PASSED
272 ** Compressed files start with %LCS
275 if (firstWord (bufptr
, "%PASSED"))
277 /* %PASSED Output from LCP Version 2.* and 3.* */
281 cptr
= strstr (bufptr
, "LCP Version");
286 ** Only really old files start this way!
290 if (*cptr
!= '2' && *cptr
!= '3')
292 llfatalerrorLoc (message ("Imported file %s is obsolete: %s.",
293 inputStream_fileName (imported
),
294 cstring_fromChars (bufptr
)));
298 compressedFormat
= FALSE
;
302 if (!firstWord (bufptr
, "%LCS"))
304 llfatalerrorLoc (message ("Imported file %s is not in correct format: %s",
305 inputStream_fileName (imported
),
306 cstring_fromChars (bufptr
)));
309 compressedFormat
= TRUE
;
312 /* push the imported LCL spec onto g_currentImports */
314 context_enterImport ();
316 bufptr
= inputStream_nextLine (imported
);
317 llassert (bufptr
!= NULL
);
321 /* expect %LCLimports foo bar ... */
322 if (firstWord (bufptr
, "%LCLimports "))
324 bufptr
= bufptr
+ strlen ("%LCLimports ");
325 while (sscanf (bufptr
, "%s", importName
) == 1)
327 bufptr
= bufptr
+ strlen (importName
) + 1; /* 1 for space */
328 sym
= lsymbol_fromChars (importName
);
329 if (sym
== importSymbol
||
330 lsymbolSet_member (g_currentImports
, sym
))
332 /* ensure that the import list does not contain itself: an
333 invariant useful for checking imports cycles. */
334 lclsource
= LCLScanSource ();
336 message ("Imports cycle: %s%s imports %s",
339 cstring_fromChars (importName
)));
341 /* push them onto g_currentImports */
342 /* evs - 94 Apr 3: I don't think it should do this! */
343 /* (void) lsymbolSet_insert (g_currentImports, sym); */
348 lclsource
= LCLScanSource ();
349 lclfatalerror (tok
, message ("Unexpected line in imported file %s: %s",
351 cstring_fromChars (bufptr
)));
354 /* read in the imported info */
355 oldexporting
= sort_setExporting (TRUE
);
357 map
= mapping_create ();
359 /* tok for error line numbering */
361 if (!compressedFormat
)
363 sort_import (imported
, tok
, map
);
366 (void) sort_setExporting (oldexporting
);
368 /* sort_import updates a mapping of old anonymous sorts to new
369 anonymous sort that is needed in symtable_import */
370 /* mapping_print (map); */
372 if (!compressedFormat
)
374 symtable_import (imported
, tok
, map
);
378 /* symtable_loadImport (imported, tok, map); */
381 check (inputStream_close (imported
));
382 inputStream_free (imported
);
388 context_leaveImport ();