Guide Contents 1. Overview 2. Operation 3. Abstract Types	4. Function Interfaces 5. Memory Management 6. Sharing 7. Value Constraints	8. Macros 9. Naming Conventions 10. Other Checks Contact: lclint@cs.virginia.edu
This guide is preserved to maintain old links, but has been replaced by the Splint Manual.

Appendix G Specifications

Another way of providing more information about programs is to use formal specifications. Although this document has largely ignored specifications, LCLint 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 LCLint checking. However, LCL specifications can provide more precise documentation on program interfaces than is possible with LCLint 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, Tan94] 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 LCLint (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.

The LCLint release package includes a grammar for LCL and examples of LCL specifications.

Specification Flags

These flags are relevant only when LCLint 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: -+++
impcheckedspecglobs
Implicit checked qualifier on global variables specified in an LCL file with no checking annotation.

m: ----
impcheckmodspecglobs
Implicit checkmod qualifier on global variables specified in an LCL file with no checking annotation.

m: ---+
impcheckedstrictspecglobs

Implicit checked qualifier on global variables specified in an LCL file with no checking annotation.

Implicit Annotations

plain: -
specglobimponly

Implicit only annotation on global variable declaration in an LCL file with no allocation annotation.

plain: -
specretimponly

Implicit only annotation on return value declaration in an LCL file with no allocation annotation.

plain: -
specstructimponly

Implicit only annotation on structure field declarations in an LCL file with no allocation annotation.

shortcut
specimponly

Sets specglobimponly, specretimponly and specstructimponly.

Macro Expansion

plain: +
specmacros

Macros defining specified identifiers are not expanded and are checked according to the specification.

Complete Programs and Specifications

m: -+++
specundef

Function, variable, iterator or constant specified but never defined.

plain: -
specundecl

Function, variable, iterator or constant specified but never declared.

plain: -
needspec

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.

shortcut
exportany

An error is reported for any identifier that is exported but not specified. (Sets all export flags below.)

m: ---+
exportconst

Constant exported but not specified.

m: ---+
exportvar

Variable exported but not specified.

m: ---+
exportfcn

Function exported but not specified.

m: ---+
exportiter

Iterator exported but not specified.

m: ---+
exportmacro

An expanded macro exported but not specified

m: ---+
exporttype

Type definition exported but not specified

Next: References
Contents

This guide is preserved to maintain old links, but has been replaced by the Splint Manual.
	Guide Contents 1. Overview 2. Operation 3. Abstract Types	4. Function Interfaces 5. Memory Management 6. Sharing 7. Value Constraints	8. Macros 9. Naming Conventions 10. Other Checks Contact: lclint@cs.virginia.edu