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: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
27 ** Module for calling LSL checker.
31 ** Massachusetts Institute of Technology
34 # include "splintMacros.nf"
37 # include "signature.h"
38 # include "signature2.h"
40 # include "scanline.h"
41 # include "syntable.h"
42 # include "tokentable.h"
44 # include "lslparse.h"
49 /*@dependent@*/ /*@null@*/ lslOp g_importedlslOp = NULL;
50 bool g_lslParsingTraits = FALSE;
52 static void invokeLSL (cstring p_infile, cstring p_outfile, bool p_deletep);
55 parseSignatures (cstring infile)
57 inputStream sourceFile;
58 ltoken *id = (ltoken *) dmalloc (sizeof (*id));
62 *id = LSLInsertToken (LST_SIMPLEID, lsymbol_fromString (infile), 0, FALSE);
63 ltoken_setFileName (*id, infile);
64 ltoken_setLine (*id, 0);
65 ltoken_setCol (*id, 0);
67 sourceFile = inputStream_create (infile, cstring_undefined, FALSE);
69 if (!inputStream_getPath (context_getLarchPath (), sourceFile))
72 (message ("LSL signature parsing: can't find file %s containing trait",
73 inputStream_fileName (sourceFile)));
77 inputStream_free (sourceFile);
81 if (!inputStream_open (sourceFile))
84 (cstring_makeLiteral ("LSL parsing: can't open file containing trait"));
87 inputStream_free (sourceFile);
93 g_lslParsingTraits = TRUE;
94 LSLScanReset (sourceFile);
95 LSLReportEolTokens (FALSE);
99 /* symtable_dump (symtab, stdout, TRUE); */
100 g_lslParsingTraits = FALSE;
102 (void) inputStream_close (sourceFile);
103 inputStream_free (sourceFile);
112 parseOpLine (cstring fname, cstring line)
114 inputStream sourceFile;
117 sourceFile = inputStream_fromString (fname, line);
119 if (check (inputStream_open (sourceFile)))
121 LSLScanReset (sourceFile);
122 LSLReportEolTokens (FALSE); /* 0 by default, lslParsingTraits = 0; */
125 ** lsl parsing and importing .lcs files are expected to be mutually
128 ** lslparse sets importedlslOp
131 status = (lslparse () != 0);
135 lclplainfatalerror (message ("Error in parsing line: %s", line));
138 (void) inputStream_close (sourceFile);
141 inputStream_free (sourceFile);
143 llassert (g_importedlslOp != NULL);
144 return (lslOp_copy (g_importedlslOp));
148 processTraitSortId (lsymbol sortid)
150 lsymbol out = lsymbol_sortFromType (g_symtab, sortid);
152 { /* may be a new sort */
153 (void) sort_fromLsymbol (sortid);
158 /* formerly from check.c module */
160 static /*@only@*/ cstring
161 printTypeName2 (typeNameNode n)
163 cstring s = cstring_undefined;
168 if (n != (typeNameNode) 0)
172 /* does not process opForm renaming, pass on to LSL
173 and hope that it works for now. */
174 typeNamePack p = n->typename;
176 llassert (p != NULL);
178 /* get the LCL type, assume LCL type has already been mentioned. */
179 lclSort = lclTypeSpecNode2sort (p->type);
180 lclSort = sort_getUnderlying (lclSort);
181 /* lclsource = LCLSLScanSource (); */
182 if (!sort_isValidSort (lclSort))
184 err = lclTypeSpecNode_errorToken (p->type);
185 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (err)); */
186 lclerror (err, message ("Unrecognized type in uses: %q",
187 typeNameNode_unparse (n)));
192 ** Below is necessary because this is one place where an LCL mutable
193 ** type name is mapped directly into its value sort, not obj sort.
194 ** Allows us to support only one qualifying "obj", rather
195 ** than "val" as well.
198 lclSort = typeExpr2ptrSort (lclSort, p->abst);
199 lclSort = sort_makeVal (lclSort);
202 ** Check that lclSort is not a HOFSort ...
203 ** Propagation of HOFSort should stop here.
206 if (sort_isHOFSortKind (lclSort))
208 err = lclTypeSpecNode_errorToken (p->type);
213 ("LCL uses cannot handle higher-order types"));
216 lclSort = sort_makeObj (lclSort);
219 lclSort = sort_makeVal (lclSort);
222 sn = sort_lookup (lclSort);
223 s = cstring_copy (cstring_fromChars (lsymbol_toChars (sn->name)));
224 /* s = string_paste (s, AbstDeclaratorNode_unparse (p->abst)); */
229 /* s = OpFormNode_unparse (n->opform); */
234 cstring_makeLiteral ("Attempt to rename operator with uses: "
235 "use LSL includes renaming facility"));
246 static /*@only@*/ cstring
247 replaceNode_unparseAlt (replaceNode x)
249 cstring s = cstring_undefined;
251 if (x != (replaceNode) 0)
253 s = printTypeName2 (x->typename);
254 s = cstring_concatChars (s, " for ");
258 s = cstring_concatFree1 (s, ltoken_unparse (x->content.ctype));
262 s = cstring_concatFree (s, nameNode_unparse (x->content.renamesortname.name));
263 s = cstring_concatFree (s,
264 sigNode_unparse (x->content.renamesortname.signature));
271 static /*@only@*/ cstring
272 replaceNodeList_unparseAlt (replaceNodeList x)
274 cstring s = cstring_undefined;
277 replaceNodeList_elements (x, i)
281 s = replaceNode_unparseAlt (i);
286 s = message ("%q, %q", s, replaceNode_unparseAlt (i));
288 } end_replaceNodeList_elements;
293 static /*@only@*/ cstring
294 printNameList2 (typeNameNodeList x)
296 /* printing a list of typeNameNode's, not nameNode's */
298 cstring s = cstring_undefined;
300 typeNameNodeList_elements (x, i)
304 s = printTypeName2 (i);
309 s = message ("%q, %q", s, printTypeName2 (i));
311 } end_typeNameNodeList_elements;
316 static /*@only@*/ cstring
317 printRenamingNode2 (renamingNode x)
319 cstring s = cstring_undefined;
321 if (x != (renamingNode) 0)
325 replaceNodeList r = x->content.replace;
326 s = replaceNodeList_unparseAlt (r);
330 nameAndReplaceNode n = x->content.name;
331 bool printComma = TRUE;
332 if (typeNameNodeList_size (n->namelist) == 0)
336 s = printNameList2 (n->namelist);
338 if (replaceNodeList_isDefined (n->replacelist) &&
339 replaceNodeList_size (n->replacelist) != 0)
341 s = cstring_appendChar (s, ',');
342 s = cstring_appendChar (s, ' ');
344 s = cstring_concatFree (s, replaceNodeList_unparseAlt (n->replacelist));
350 static /*@only@*/ cstring
351 printTraitRefList2 (traitRefNodeList x) /*@*/
353 cstring s = cstring_undefined;
355 traitRefNodeList_elements (x, i)
357 s = message ("%qincludes (%q)", s, printRawLeaves2 (i->traitid));
361 s = message ("%q(%q)", s, printRenamingNode2 (i->rename));
364 s = message ("%q\n", s);
365 } end_traitRefNodeList_elements;
371 callLSL (/*@unused@*/ cstring specfile, /*@only@*/ cstring text)
373 /* specfile is the name of the LCL file that contains "uses"
374 Create an intermediate file named
375 specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_IN_SUFFIX>.
376 put text in the file, run lsl on it and direct
377 output to specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_OUT_SUFFIX>.
378 specfile can be a full pathname.
379 Note: LSL does not support traitnames that are pathnames, only
389 infile = fileTable_fileName (fileTable_addltemp (context_fileTable ()));
390 inptr = fileTable_openFile (context_fileTable (), infile, "w");
395 llfatalerror (message ("Unable to write intermediate file: %s",
399 nopath = fileLib_removePath (infile);
400 noext = fileLib_removeAnyExtension (nopath);
402 fprintf (inptr, "%s : trait\n", cstring_toCharsSafe (noext));
404 cstring_free (noext);
405 cstring_free (nopath);
407 fprintf (inptr, "%s", cstring_toCharsSafe (text));
408 check (fileTable_closeFile (context_fileTable (), inptr));
410 /* the default is to delete the input file */
412 outfile = fileTable_fileName (fileTable_addltemp (context_fileTable ()));
413 invokeLSL (infile, outfile, context_getFlag (FLG_KEEP));
417 static void invokeLSL (cstring infile, cstring outfile, bool deletep)
419 /* run lsl on infile and leave result in outfile */
424 cstring returnPath = cstring_undefined;
427 ** Ensures that outfile can be written into, should find a better
431 outptr = fileTable_openFile (context_fileTable (), outfile, "w");
436 llfatalerror (message ("Unable to write intermediate file: %s",
440 check (fileTable_closeFile (context_fileTable (), outptr));
442 /* set call to the right command */
443 status = osd_getExePath (cstring_makeLiteralTemp ("PATH"),
444 cstring_makeLiteralTemp ("lsl"),
448 if (status == OSD_FILEFOUND)
450 call = message ("%s -syms %s > %s", returnPath, infile, outfile);
452 /* before calling, make sure old file is removed */
453 (void) osd_unlink (outfile);
455 callstatus = osd_system (call);
459 if (callstatus != CALL_SUCCESS)
462 ** lsl errors: call lsl again without -syms, sending output to stdout
464 cstring syscal = message ("%s %s", returnPath, infile);
465 (void) osd_system (syscal);
466 cstring_free (syscal);
468 llfatalerror (cstring_makeLiteral ("LSL trait used contains errors."));
472 /* Now parse the LSL output and store info in symbol table */
473 callstatus = parseSignatures (cstring_copy (outfile));
478 if (!context_getFlag (FLG_KEEP))
480 /* delete temporary files */
483 (void) osd_unlink (infile);
486 (void) osd_unlink (outfile);
491 else if (status == OSD_FILENOTFOUND)
494 (cstring_makeLiteral ("Cannot find LSL checker: check your command search path."));
496 else /* must be (status == OSD_PATHTOOLONG) */
498 lclfatalbug ("invokeLSL: lsl plus directory from search path is too long");
502 /* callLSL ("MySet", "includes Set (CC for C, EE for E)"); */
505 readlsignatures (interfaceNode n)
507 /* assume n->kind = usesKIND */
508 callLSL (g_currentSpec, printTraitRefList2 (n->content.uses));