|
Splint - Secure Programming Lint |
info@splint.org |
| Manual Contents - Other Formats | Section: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 A B C D E Sponsors - Credits |
Another way of providing more information about programs is to use formal specifications. Although this document has largely ignored specifications, Splint was originally designed to use the information in LCL specifications instead of source-code annotations. This document focuses on annotations since it takes less effort to add annotations to source code than to maintain an additional specification file. Annotations can express everything that can be expressed in LCL specifications that is relevant to Splint checking. However, LCL specifications can provide more precise documentation on program interfaces than is possible with Splint annotations. This appendix (extracted from [Evans94]) is a very brief introduction to LCL Specifications. For more information, consult [GH93].
The Larch family of languages is a two-tiered approach to formal specification. A specification is built using two languages — the Larch Shared Language (LSL), which is independent of the implementation language, and a Larch Interface Language designed for the specific implementation language. An LSL specification defines sorts, analogous to abstract types in a programming language, and operators, analogous to procedures. It expresses the underlying semantics of an abstraction.
The interface language specifies an interface to an abstraction in a particular programming language. It captures the details of the interface needed by a client using the abstraction and places constraints on both correct implementations and uses of the module. The semantics of the interface are described using primitives and sorts and operators defined in LSL specifications. Interface languages have been designed for several programming languages.
LCL [GH93, Tan95] is a Larch interface language for Standard C. LCL uses a C-like syntax. Traditionally, a C module M consists of a source file, M .c, and a header file, M .h. The header file contains prototype declarations for functions, variables and constants exported by M, as well as those macro definitions that implement exported functions or constants, and definitions of exported types. When using LCL, a module includes two additional files — M .lcl, a formal specification of M, and M.lh, which is derived by Splint (if the lh flag is on) from M .lcl. Clients use M .lcl for documentation, and should not need to look at any implementation file. The derived file, M .lh, contains include directives (if M depends on other specified modules), prototypes of functions and declarations of variables as specified in M .lcl. The file M .h should include M .lh and retain the implementation aspects of the old M .h, but is no longer used for client documentation.
These flags are relevant only when Splint is used with LCL specifications.
Global Flags
lcs
Generate .lcs files containing symbolic state of .lcl files (used for imports). By default .lcs files are generated for each .lcl file processed. Use -lcs to prevent generation of .lcs files.
lh
Generate .lh files. By default, -lh is set and no .lh files are generated. Use +lh to enable .lh file generation.
i <file>
Set LCL initialization file to <file>. The LCL initialization file is read if any .lcl files are listed on the command line. The default file is lclinit.lci, found on the LARCH_PATH.
lclexpect <number>
Exactly <number> specification errors are expected. Specification errors are errors detected when checking the specifications. They do not depend on the source code.
Implicit Globals Checking Qualifiers
m:-++-
imp-checked-spec-globs
Implicit checked qualifier on global variables specified in an LCL file with no checking annotation.
m:----
imp-checkmod-spec-globs
m:---+
Implicit checkmod qualifier on global variables specified in an LCL file with no checking annotation.
imp-checkedstrict-spec-globs
Implicit checked qualifier on global variables specified in an LCL file with no checking annotation.
P: -
Implicit Annotations
spec-glob-imp-only
Implicit only annotation on global variable declaration in an LCL file with no allocation annotation.
P: -
spec-ret-imp-only
Implicit only annotation on return value declaration in an LCL file with no allocation annotation.
P: -
spec-struct-imp-only
Implicit only annotation on structure field declarations in an LCL file with no allocation annotation.
shortcut
spec-imp-only
Sets spec-glob-imp-only, spec-ret-imp-only and spec-struct-imp-only.
Macro Expansion
P: +
spec-macros
Macros defining specified identifiers are not expanded and are checked according to the specification.
m:-+++
Complete Programs and Specifications
spec-undef
Function, variable, iterator or constant specified but never defined.
P: -
spec-undecl
Function, variable, iterator or constant specified but never declared.
P: -
need-spec
shortcut
There is information in the specification that is not duplicated in syntactic comments. Normally, this is not an error, but it may be useful to detect it to make sure checking incomplete systems without the specifications will still use this information.
export-any
m:---+
An error is reported for any identifier that is exported but not specified. (Sets all export flags below.)
export-const
Constant exported but not specified.
m:---+
export-var
Variable exported but not specified.
m:---+
export-fcn
Function exported but not specified.
m:---+
export-iter
Iterator exported but not specified.
m:---+
export-macro
An expanded macro exported but not specified
m:---+
export-type
Type definition exported but not specified
Next: Appendix E. Annotated Bibliography
Return to Contents