]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
77d37419 | 3 | ** Copyright (C) 1994-2002 University of Virginia, |
616915dd | 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 |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
616915dd | 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 | ||
1b8ae690 | 34 | # include "splintMacros.nf" |
616915dd | 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" | |
616915dd | 45 | |
46 | void | |
47 | outputLCSFile (char *path, char *msg, char *specname) | |
48 | { | |
49 | static bool haserror = FALSE; | |
50 | char *sfile = mstring_concat (specname, ".lcs"); | |
51 | char *outfile = mstring_concat (path, sfile); | |
52 | char *s; | |
dfd82dce | 53 | FILE *outfptr = fileTable_openFile (context_fileTable (), cstring_fromChars (outfile), "w"); |
616915dd | 54 | sfree (sfile); |
55 | ||
56 | DPRINTF (("Output lcl file: %s / %s / %s", path, specname, outfile)); | |
57 | ||
58 | /* check write permission */ | |
59 | ||
dfd82dce | 60 | if (outfptr == NULL) /* Cannot open file */ |
61 | { | |
616915dd | 62 | if (!haserror) |
63 | { | |
64 | lclplainerror (message ("Cannot write to output file: %s", | |
65 | cstring_fromChars (outfile))); | |
66 | haserror = TRUE; | |
67 | } | |
68 | sfree (outfile); | |
69 | return; | |
70 | } | |
71 | ||
28bf4b0b | 72 | fprintf (outfptr, "%s", msg); |
616915dd | 73 | fprintf (outfptr, "%s\n", LCL_PARSE_VERSION); |
74 | ||
75 | /* output line %LCLimports foo bar ... */ | |
76 | fprintf (outfptr, "%%LCLimports "); | |
77 | ||
78 | lsymbolSet_elements (g_currentImports, sym) | |
79 | { | |
80 | s = lsymbol_toChars (sym); | |
81 | ||
82 | if (s != NULL && !mstring_equal (s, specname)) | |
83 | { | |
84 | fprintf (outfptr, "%s ", s); | |
85 | } | |
86 | } end_lsymbolSet_elements; | |
87 | ||
88 | fprintf (outfptr, "\n"); | |
89 | ||
90 | sort_dump (outfptr, TRUE); | |
91 | symtable_dump (g_symtab, outfptr, TRUE); | |
92 | ||
dfd82dce | 93 | check (fileTable_closeFile (context_fileTable (), outfptr)); |
616915dd | 94 | sfree (outfile); |
95 | } | |
96 | ||
97 | void | |
98 | importCTrait (void) | |
99 | { | |
28bf4b0b | 100 | cstring infile = cstring_undefined; |
101 | filestatus status = osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSYMSNAME), | |
102 | &infile); | |
616915dd | 103 | |
616915dd | 104 | switch (status) |
105 | { | |
106 | case OSD_FILEFOUND: | |
107 | /* | |
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 | |
111 | ** open the file. | |
112 | */ | |
113 | ||
28bf4b0b | 114 | (void) parseSignatures (cstring_fromCharsNew (CTRAITSYMSNAME)); |
115 | (void) parseSignatures (infile); | |
616915dd | 116 | break; |
117 | case OSD_FILENOTFOUND: | |
118 | /* try spec name */ | |
28bf4b0b | 119 | status = osd_findOnLarchPath (cstring_makeLiteralTemp (CTRAITSPECNAME), |
120 | &infile); | |
616915dd | 121 | |
122 | if (status == OSD_FILEFOUND) | |
123 | { | |
28bf4b0b | 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); | |
616915dd | 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))); | |
28bf4b0b | 137 | cstring_free (infile); |
138 | llexit (LLFAILURE); | |
616915dd | 139 | } |
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))); | |
28bf4b0b | 145 | cstring_free (infile); |
616915dd | 146 | break; |
147 | } | |
616915dd | 148 | } |
149 | ||
150 | /* | |
151 | ** processImport --- load imports from file | |
152 | ** | |
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" | |
161 | */ | |
162 | ||
163 | void | |
164 | processImport (lsymbol importSymbol, ltoken tok, impkind kind) | |
165 | { | |
166 | bool readableP, oldexporting; | |
28bf4b0b | 167 | bool compressedFormat = FALSE; |
168 | inputStream imported, imported2, lclsource; | |
169 | char *bufptr; | |
170 | char *tmpbufptr; | |
171 | char *cptr; | |
172 | cstring name; | |
616915dd | 173 | lsymbol sym; |
28bf4b0b | 174 | char importName[MAX_NAME_LENGTH + 1]; |
175 | cstring importFileName; | |
176 | cstring path = cstring_undefined; | |
177 | cstring fpath, fpath2; | |
178 | mapping map; | |
616915dd | 179 | filestatus ret; |
180 | ||
28bf4b0b | 181 | importFileName = lsymbol_toString (importSymbol); |
182 | name = cstring_concat (importFileName, cstring_makeLiteralTemp (IO_SUFFIX)); | |
616915dd | 183 | |
184 | /* | |
185 | ** find .lcs file | |
186 | */ | |
187 | ||
188 | switch (kind) | |
189 | { | |
190 | case IMPPLAIN: | |
7272a1c1 | 191 | path = message ("%s%c%s", cstring_fromChars (g_localSpecPath), PATH_SEPARATOR, |
28bf4b0b | 192 | context_getLarchPath ()); |
193 | ||
616915dd | 194 | break; |
195 | case IMPBRACKET: | |
28bf4b0b | 196 | path = cstring_copy (context_getLCLImportDir ()); |
616915dd | 197 | break; |
198 | case IMPQUOTE: | |
28bf4b0b | 199 | path = cstring_fromCharsNew (g_localSpecPath); |
616915dd | 200 | break; |
201 | default: | |
616915dd | 202 | llbuglit ("bad imports case\n"); |
203 | } | |
204 | ||
28bf4b0b | 205 | if ((ret = osd_getPath (path, name, &fpath)) != OSD_FILEFOUND) |
616915dd | 206 | { |
28bf4b0b | 207 | cstring fname2; |
616915dd | 208 | |
209 | if (ret == OSD_PATHTOOLONG) | |
210 | { | |
211 | llfatalerrorLoc (cstring_makeLiteral ("Path too long")); | |
212 | } | |
213 | ||
28bf4b0b | 214 | imported2 = inputStream_create (cstring_copy (importFileName), |
215 | LCL_EXTENSION, FALSE); | |
216 | fname2 = inputStream_fileName (imported2); | |
616915dd | 217 | |
218 | if (osd_getPath (path, fname2, &fpath2) == OSD_FILEFOUND) | |
219 | { | |
220 | llfatalerrorLoc | |
221 | (message ("Specs must be processed before it can be imported: %s", | |
28bf4b0b | 222 | fpath2)); |
616915dd | 223 | } |
224 | else | |
225 | { | |
226 | if (kind == IMPPLAIN || kind == IMPQUOTE) | |
28bf4b0b | 227 | { |
228 | llfatalerrorLoc (message ("Cannot find file to import: %s", name)); | |
229 | } | |
616915dd | 230 | else |
28bf4b0b | 231 | { |
232 | llfatalerrorLoc (message ("Cannot find standard import file: %s", name)); | |
233 | } | |
616915dd | 234 | } |
235 | } | |
236 | ||
237 | ||
28bf4b0b | 238 | imported = inputStream_create (fpath, cstring_makeLiteralTemp (IO_SUFFIX), FALSE); |
239 | ||
240 | readableP = inputStream_open (imported); | |
616915dd | 241 | |
242 | if (!readableP) | |
243 | { /* can't read ? */ | |
244 | llfatalerrorLoc (message ("Cannot open import file for reading: %s", | |
28bf4b0b | 245 | inputStream_fileName (imported))); |
616915dd | 246 | } |
247 | ||
28bf4b0b | 248 | bufptr = inputStream_nextLine (imported); |
616915dd | 249 | |
250 | if (bufptr == 0) | |
251 | { | |
252 | llerror (FLG_SYNTAX, message ("Import file is empty: %s", | |
28bf4b0b | 253 | inputStream_fileName (imported))); |
254 | cstring_free (name); | |
255 | (void) inputStream_close (imported); | |
256 | inputStream_free (imported); | |
616915dd | 257 | |
28bf4b0b | 258 | cstring_free (path); |
616915dd | 259 | return; |
260 | } | |
261 | ||
262 | /* was it processed successfully ? */ | |
263 | if (firstWord (bufptr, "%FAILED")) | |
264 | { | |
265 | llfatalerrorLoc | |
28bf4b0b | 266 | (message ("Imported file was not checked successfully: %s.", name)); |
616915dd | 267 | } |
268 | ||
28bf4b0b | 269 | /* |
270 | ** Is it generated by the right version of the checker? | |
271 | ** | |
272 | ** Uncompressed .lcs files start with %PASSED | |
273 | ** Compressed files start with %LCS | |
274 | */ | |
616915dd | 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 | { | |
28bf4b0b | 286 | /* |
287 | ** Only really old files start this way! | |
288 | */ | |
289 | ||
616915dd | 290 | cptr += 12; |
291 | if (*cptr != '2' && *cptr != '3') | |
292 | { | |
28bf4b0b | 293 | llfatalerrorLoc (message ("Imported file %s is obsolete: %s.", |
294 | inputStream_fileName (imported), | |
295 | cstring_fromChars (bufptr))); | |
616915dd | 296 | } |
297 | } | |
28bf4b0b | 298 | |
299 | compressedFormat = FALSE; | |
616915dd | 300 | } |
301 | else | |
302 | { | |
303 | if (!firstWord (bufptr, "%LCS")) | |
304 | { | |
28bf4b0b | 305 | llfatalerrorLoc (message ("Imported file %s is not in correct format: %s", |
306 | inputStream_fileName (imported), | |
616915dd | 307 | cstring_fromChars (bufptr))); |
308 | } | |
28bf4b0b | 309 | |
310 | compressedFormat = TRUE; | |
616915dd | 311 | } |
312 | ||
313 | /* push the imported LCL spec onto g_currentImports */ | |
314 | ||
315 | context_enterImport (); | |
316 | ||
28bf4b0b | 317 | bufptr = inputStream_nextLine (imported); |
616915dd | 318 | llassert (bufptr != NULL); |
319 | ||
320 | tmpbufptr = bufptr; | |
321 | ||
322 | /* expect %LCLimports foo bar ... */ | |
323 | if (firstWord (bufptr, "%LCLimports ")) | |
324 | { | |
325 | bufptr = bufptr + strlen ("%LCLimports "); | |
326 | while (sscanf (bufptr, "%s", importName) == 1) | |
327 | { | |
328 | bufptr = bufptr + strlen (importName) + 1; /* 1 for space */ | |
329 | sym = lsymbol_fromChars (importName); | |
330 | if (sym == importSymbol || | |
331 | lsymbolSet_member (g_currentImports, sym)) | |
332 | { | |
333 | /* ensure that the import list does not contain itself: an | |
334 | invariant useful for checking imports cycles. */ | |
335 | lclsource = LCLScanSource (); | |
336 | lclfatalerror (tok, | |
28bf4b0b | 337 | message ("Imports cycle: %s%s imports %s", |
338 | importFileName, | |
339 | LCL_EXTENSION, | |
616915dd | 340 | cstring_fromChars (importName))); |
341 | } | |
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); */ | |
345 | } | |
346 | } | |
347 | else | |
348 | { | |
349 | lclsource = LCLScanSource (); | |
350 | lclfatalerror (tok, message ("Unexpected line in imported file %s: %s", | |
28bf4b0b | 351 | name, |
616915dd | 352 | cstring_fromChars (bufptr))); |
353 | } | |
354 | ||
355 | /* read in the imported info */ | |
356 | oldexporting = sort_setExporting (TRUE); | |
357 | ||
358 | map = mapping_create (); | |
359 | ||
360 | /* tok for error line numbering */ | |
361 | ||
28bf4b0b | 362 | if (!compressedFormat) |
616915dd | 363 | { |
28bf4b0b | 364 | sort_import (imported, tok, map); |
616915dd | 365 | } |
28bf4b0b | 366 | |
616915dd | 367 | (void) sort_setExporting (oldexporting); |
28bf4b0b | 368 | |
616915dd | 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); */ | |
372 | ||
28bf4b0b | 373 | if (!compressedFormat) |
616915dd | 374 | { |
375 | symtable_import (imported, tok, map); | |
376 | } | |
377 | else | |
378 | { | |
379 | /* symtable_loadImport (imported, tok, map); */ | |
380 | } | |
381 | ||
28bf4b0b | 382 | check (inputStream_close (imported)); |
383 | inputStream_free (imported); | |
384 | ||
385 | mapping_free (map); | |
386 | cstring_free (name); | |
387 | cstring_free (path); | |
616915dd | 388 | |
389 | context_leaveImport (); | |
390 | } | |
391 | ||
392 | ||
393 |