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 calling LSL checker.
31 ** Massachusetts Institute of Technology
34 # include "splintMacros.nf"
38 # include "lslgrammar.h"
40 # include "lslscanline.h"
41 # include "lsltokentable.h"
42 # include "lslparse.h"
46 /*@dependent@*/ /*@null@*/ lslOp g_importedlslOp
= NULL
;
47 bool g_lslParsingTraits
= FALSE
;
49 static void invokeLSL (cstring p_infile
, cstring p_outfile
, bool p_deletep
);
52 parseSignatures (cstring infile
)
54 inputStream sourceFile
;
55 ltoken
*id
= (ltoken
*) dmalloc (sizeof (*id
));
59 *id
= LSLInsertToken (LST_SIMPLEID
, lsymbol_fromString (infile
), 0, FALSE
);
60 ltoken_setFileName (*id
, infile
);
61 ltoken_setLine (*id
, 0);
62 ltoken_setCol (*id
, 0);
64 sourceFile
= inputStream_create (infile
, cstring_undefined
, FALSE
);
66 if (!inputStream_getPath (context_getLarchPath (), sourceFile
))
69 (message ("LSL signature parsing: can't find file %s containing trait",
70 inputStream_fileName (sourceFile
)));
74 inputStream_free (sourceFile
);
78 if (!inputStream_open (sourceFile
))
81 (cstring_makeLiteral ("LSL parsing: can't open file containing trait"));
84 inputStream_free (sourceFile
);
90 g_lslParsingTraits
= TRUE
;
91 LSLScanReset (sourceFile
);
92 LSLReportEolTokens (FALSE
);
96 /* symtable_dump (symtab, stdout, TRUE); */
97 g_lslParsingTraits
= FALSE
;
99 (void) inputStream_close (sourceFile
);
100 inputStream_free (sourceFile
);
109 parseOpLine (cstring fname
, cstring line
)
111 inputStream sourceFile
;
114 sourceFile
= inputStream_fromString (fname
, line
);
116 if (check (inputStream_open (sourceFile
)))
118 LSLScanReset (sourceFile
);
119 LSLReportEolTokens (FALSE
); /* 0 by default, lslParsingTraits = 0; */
122 ** lsl parsing and importing .lcs files are expected to be mutually
125 ** lslparse sets importedlslOp
128 status
= (lslparse () != 0);
132 lclplainfatalerror (message ("Error in parsing line: %s", line
));
135 (void) inputStream_close (sourceFile
);
138 inputStream_free (sourceFile
);
140 llassert (g_importedlslOp
!= NULL
);
141 return (lslOp_copy (g_importedlslOp
));
145 processTraitSortId (lsymbol sortid
)
147 lsymbol out
= lsymbol_sortFromType (g_symtab
, sortid
);
149 { /* may be a new sort */
150 (void) sort_fromLsymbol (sortid
);
155 /* formerly from check.c module */
157 static /*@only@*/ cstring
158 printTypeName2 (typeNameNode n
)
160 cstring s
= cstring_undefined
;
165 if (n
!= (typeNameNode
) 0)
169 /* does not process opForm renaming, pass on to LSL
170 and hope that it works for now. */
171 typeNamePack p
= n
->typename
;
173 llassert (p
!= NULL
);
175 /* get the LCL type, assume LCL type has already been mentioned. */
176 lclSort
= lclTypeSpecNode2sort (p
->type
);
177 lclSort
= sort_getUnderlying (lclSort
);
178 /* lclsource = LCLSLScanSource (); */
179 if (!sort_isValidSort (lclSort
))
181 err
= lclTypeSpecNode_errorToken (p
->type
);
182 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (err)); */
183 lclerror (err
, message ("Unrecognized type in uses: %q",
184 typeNameNode_unparse (n
)));
189 ** Below is necessary because this is one place where an LCL mutable
190 ** type name is mapped directly into its value sort, not obj sort.
191 ** Allows us to support only one qualifying "obj", rather
192 ** than "val" as well.
195 lclSort
= typeExpr2ptrSort (lclSort
, p
->abst
);
196 lclSort
= sort_makeVal (lclSort
);
199 ** Check that lclSort is not a HOFSort ...
200 ** Propagation of HOFSort should stop here.
203 if (sort_isHOFSortKind (lclSort
))
205 err
= lclTypeSpecNode_errorToken (p
->type
);
210 ("LCL uses cannot handle higher-order types"));
213 lclSort
= sort_makeObj (lclSort
);
216 lclSort = sort_makeVal (lclSort);
219 sn
= sort_lookup (lclSort
);
220 s
= cstring_copy (cstring_fromChars (lsymbol_toChars (sn
->name
)));
221 /* s = string_paste (s, AbstDeclaratorNode_unparse (p->abst)); */
226 /* s = OpFormNode_unparse (n->opform); */
231 cstring_makeLiteral ("Attempt to rename operator with uses: "
232 "use LSL includes renaming facility"));
243 static /*@only@*/ cstring
244 replaceNode_unparseAlt (replaceNode x
)
246 cstring s
= cstring_undefined
;
248 if (x
!= (replaceNode
) 0)
250 s
= printTypeName2 (x
->typename
);
251 s
= cstring_concatChars (s
, " for ");
255 s
= cstring_concatFree1 (s
, ltoken_unparse (x
->content
.ctype
));
259 s
= cstring_concatFree (s
, nameNode_unparse (x
->content
.renamesortname
.name
));
260 s
= cstring_concatFree (s
,
261 sigNode_unparse (x
->content
.renamesortname
.signature
));
268 static /*@only@*/ cstring
269 replaceNodeList_unparseAlt (replaceNodeList x
)
271 cstring s
= cstring_undefined
;
274 replaceNodeList_elements (x
, i
)
278 s
= replaceNode_unparseAlt (i
);
283 s
= message ("%q, %q", s
, replaceNode_unparseAlt (i
));
285 } end_replaceNodeList_elements
;
290 static /*@only@*/ cstring
291 printNameList2 (typeNameNodeList x
)
293 /* printing a list of typeNameNode's, not nameNode's */
295 cstring s
= cstring_undefined
;
297 typeNameNodeList_elements (x
, i
)
301 s
= printTypeName2 (i
);
306 s
= message ("%q, %q", s
, printTypeName2 (i
));
308 } end_typeNameNodeList_elements
;
313 static /*@only@*/ cstring
314 printRenamingNode2 (renamingNode x
)
316 cstring s
= cstring_undefined
;
318 if (x
!= (renamingNode
) 0)
322 replaceNodeList r
= x
->content
.replace
;
323 s
= replaceNodeList_unparseAlt (r
);
327 nameAndReplaceNode n
= x
->content
.name
;
328 bool printComma
= TRUE
;
329 if (typeNameNodeList_size (n
->namelist
) == 0)
333 s
= printNameList2 (n
->namelist
);
335 if (replaceNodeList_isDefined (n
->replacelist
) &&
336 replaceNodeList_size (n
->replacelist
) != 0)
338 s
= cstring_appendChar (s
, ',');
339 s
= cstring_appendChar (s
, ' ');
341 s
= cstring_concatFree (s
, replaceNodeList_unparseAlt (n
->replacelist
));
347 static /*@only@*/ cstring
348 printTraitRefList2 (traitRefNodeList x
) /*@*/
350 cstring s
= cstring_undefined
;
352 traitRefNodeList_elements (x
, i
)
354 s
= message ("%qincludes (%q)", s
, printRawLeaves2 (i
->traitid
));
358 s
= message ("%q(%q)", s
, printRenamingNode2 (i
->rename
));
361 s
= message ("%q\n", s
);
362 } end_traitRefNodeList_elements
;
368 callLSL (/*@unused@*/ cstring specfile
, /*@only@*/ cstring text
)
370 /* specfile is the name of the LCL file that contains "uses"
371 Create an intermediate file named
372 specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_IN_SUFFIX>.
373 put text in the file, run lsl on it and direct
374 output to specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_OUT_SUFFIX>.
375 specfile can be a full pathname.
376 Note: LSL does not support traitnames that are pathnames, only
386 infile
= fileTable_fileName (fileTable_addTempFile (context_fileTable (), FILE_LSLTEMP
, fileId_invalid
));
387 inptr
= fileTable_createTempFile (context_fileTable (), infile
, FALSE
);
392 llfatalerror (message ("Unable to write intermediate file: %s",
396 nopath
= fileLib_removePath (infile
);
397 noext
= fileLib_removeAnyExtension (nopath
);
399 fprintf (inptr
, "%s : trait\n", cstring_toCharsSafe (noext
));
401 cstring_free (noext
);
402 cstring_free (nopath
);
404 fprintf (inptr
, "%s", cstring_toCharsSafe (text
));
405 check (fileTable_closeFile (context_fileTable (), inptr
));
407 /* the default is to delete the input file */
409 outfile
= fileTable_fileName (fileTable_addTempFile (context_fileTable (), FILE_LSLTEMP
, fileId_invalid
));
410 invokeLSL (infile
, outfile
, context_getFlag (FLG_KEEP
));
414 static void invokeLSL (cstring infile
, cstring outfile
, bool deletep
)
416 /* run lsl on infile and leave result in outfile */
421 cstring returnPath
= cstring_undefined
;
424 ** Ensures that outfile can be written into, should find a better
428 outptr
= fileTable_createTempFile (context_fileTable (), outfile
, FALSE
);
433 llfatalerror (message ("Unable to write intermediate file: %s",
437 check (fileTable_closeFile (context_fileTable (), outptr
));
439 /* set call to the right command */
440 status
= osd_getExePath (cstring_makeLiteralTemp (getenv ("PATH")),
441 cstring_makeLiteralTemp ("lsl"),
445 if (status
== OSD_FILEFOUND
)
447 call
= message ("%s -syms %s > %s", returnPath
, infile
, outfile
);
449 /* before calling, make sure old file is removed */
450 (void) osd_unlink (outfile
);
452 callstatus
= osd_system (call
);
456 if (callstatus
!= CALL_SUCCESS
)
459 ** lsl errors: call lsl again without -syms, sending output to stdout
461 cstring syscal
= message ("%s %s", returnPath
, infile
);
462 (void) osd_system (syscal
);
463 cstring_free (syscal
);
465 llfatalerror (cstring_makeLiteral ("LSL trait used contains errors."));
469 /* Now parse the LSL output and store info in symbol table */
470 callstatus
= parseSignatures (cstring_copy (outfile
));
475 if (!context_getFlag (FLG_KEEP
))
477 /* delete temporary files */
480 (void) osd_unlink (infile
);
483 (void) osd_unlink (outfile
);
488 else if (status
== OSD_FILENOTFOUND
)
491 (cstring_makeLiteral ("Cannot find LSL checker: check your command search path."));
493 else /* must be (status == OSD_PATHTOOLONG) */
495 lclfatalbug ("invokeLSL: lsl plus directory from search path is too long");
499 /* callLSL ("MySet", "includes Set (CC for C, EE for E)"); */
502 readlsignatures (interfaceNode n
)
504 /* assume n->kind = usesKIND */
505 callLSL (g_currentSpec
, printTraitRefList2 (n
->content
.uses
));