Libraries can be used to record interface information. A library containing information about the standard C Library is used to enable checking of library calls. Program libraries can be created to enable fast checking of single modules in a large program.
In order to check calls to library functions, Splint uses an annotated standard library. This contains more information about function interfaces then is available in the system header files since it uses annotations. Further, it contains only those functions documented in the ISO C99 standard. Many systems include extra functions in their system libraries; programs that use these functions cannot be compiled on other systems that do not provide them. Certain types defined by the library are treated as abstract types (e.g., a program should not rely on how the FILE type is implemented). When checking source code, Splint does include system headers corresponding to files in the library, but instead uses the library description of the standard library.
The Splint distribution includes several different standard libraries: the ANSI standard library, the POSIX standard library[19], and a UNIX library based on the Open Group’s Single Unix Specification. Each library comes in two versions: the standard version and the strict version.
The default behavior of Splint is to use the ISO standard library (loaded from standard.lcd). This library is based on the standard library described in the ISO C99 standard.
The POSIX library is selected by the +posixlib flag. The POSIX library is based on the IEEE Std 1003.1-1990.
The UNIX library is selected by the +unixlib flag. This library is based on the Open Group’s Single Unix Specification, Version 2. In the UNIX library, free is declared with a non-null parameter. ISO specifies that free should handle the argument NULL, but several UNIX platforms crash if NULL is passed to free.
Stricter versions of the libraries are used is the -ansi-strict, posix-strict-lib or unix-strict-lib flag is used. These libraries use a stricter interpretation of the library. They will detect more errors in some programs, but may to produce many spurious errors for typical code.
The differences between the standard libraries and the strict libraries are:
· The standard libraries declare the printing functions (fprintf, printf, and sprintf) that may return error codes to return int or void. This prevents typical programs from leading to deluge of ignored return value errors, but may mean some relevant errors are not detected. In the strict library, they are declared to return int, so ignored return value errors will be reported (depending on other flag settings). Programs should check that this return value is non-negative.
· The standard libraries declare some parameters and return values to be alternate types (int or bool, or int or char). The ISO C99 standard specifies these types as int to be compatible with older versions of the library, but logically they make more sense as bool or char. In the strict library, the stronger type is used. The parameter to assert is int or bool in the standard library, and bool in the strict library. The parameter to the character functions isalnum, isalpha, iscntrl, isdigit, isgraph, islower, isprint, ispunct, isspace, isupper, isxdigit, tolower and toupper is char or unsigned char or int in the standard library and char in the strict library. The type of the return value of the character classification functions (all of the previous character functions except tolower and toupper) is bool or int in the standard library and bool in the strict library. The type of the first parameter to ungetc is char or int in the standard library and char in the strict library (EOF should not be passed to ungetc). The second parameter to strchr and strrchr is char or int in the standard library and char in the strict library.
· The global variables stdin, stdout and stderr are declared as unchecked variables (see Section 7.2) in the standard libraries. In the strict libraries, they arechecked.
· The global variable errno is declared unchecked in the standard libraries, but declared checkedstrict in the strict libraries.
If no library flag is used, Splint will load the standard library, standard.lcd. If +nolib is set, no library is loaded. The library source files can easily be modified, and new libraries created to better suit a particular application.
To enable running Splint on large systems, mechanisms are provided for creating libraries containing necessary information. This means source files can be checked independently, after a library has been created. The command line option -dump library stores information in the file library (the default extension .lcd is added). Then, -load library loads the library. The library contains interface information from the files checked when the library was created.
The standard libraries are generated from header files included in the Splint distribution. Some libraries are generated from more than one header file. Since the POSIX library subsumes the standard library, the headers for the standard and POSIX libraries are combined to produce the POSIX library. Similarly, the UNIX library is composed of the standard, POSIX and UNIX headers. The header files include some sections that are conditionally selected by defining STRICT. The commands to generate the standard libraries are:
splint -nolib ansi.h -dump ansi
splint -nolib -DSTRICT ansi.h -dump ansistrict
splint -nolib ansi.h posix.h -dump posix
splint -nolib -DSTRICT ansi.h posix.h -dump posixstrict
splint -nolib ansi.h posix.h unix.h -dump unix
splint -nolib -DSTRICT ansi.h posix.h unix.h -dump unixstrict
The standard behavior of Splint on encountering
#include <X.h>
is to search for a file named X .h on the include search path (set using –I) and then the system base include path (read from the include environment variable if set or using a default value, usually /usr/include). If X .h is the name of a header file in a loaded standard library and X .h is found in a directory that is a system directory (as set by the -sysdirs flag; the default is /usr/include), X .h will not be included if +skip-iso-headers or +skip-posix-headers (depending on whether X .h is an ISO or POSIX header file) is on (both are on by default). To force all headers to be included normally, use ‑skip-iso-headers.
Sometimes headers in system directories contain non-standard syntax that Splint is unable to parse. The +skip-sys-headers flag may be used to prevent any include file in a system directory from being included.
Splint is fast enough that it can be run on medium-size (10,000 line) programs without performance concerns. Libraries can be used to enable efficient checking of small modules in large programs. To further improve performance, header file inclusion can be optimized.
When processing a complete system in which many files include the same headers, a large fraction of processing time is wasted re-reading header files unnecessarily. If you are checking a 100-file program, and every file includes utils.h, Splint will have to process utils.h 100 times (as would most C compilers). If the +single-include flag is used, each header file is processed only once. Single header file processing produces a significant efficiency improvement when checking large programs split into many files, but is only safe if the same header file included in different contexts always has the same meaning (i.e., it does not depend on preprocessor variable defined differently at different inclusion sites).
When processing a single file in a large system, a large fraction of the time is spent processing included header files. This can be avoided if the information in the header files is stored in a library instead. If +never-include is set, inclusion of files ending in .h is prevented. Files with different suffixes are included normally. To do this the header files must not include any expanded macros. That is, the header file must be processed with +all-macros, and there must be no /*@notfunction@*/ control comments in the header. Then, the +never-include flag may be used to prevent inclusion of header files. Alternately, non-function macros can be moved to a different file with a name that does not end in .h. Remember, that this file must be included directly from the .c file, since if it is included from an .h file indirectly, that .h file is ignored so the other file is never included.
These options can be used for significant performance improvements on large systems. The performance depends on how the code is structured, but checking a single module in a large program is several times faster if libraries and +noinclude are used.
Splint defines the preprocessor constant S_SPLINT_S when preprocessing source files. If you want to include code that is processed only when Splint is used, surround the code with
# ifdef S_SPLINT_S
…
# endif
Next: Appendix A. Availability
Return to Contents