LCLint User's Guide - Appendix D: Annotations

	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 D Annotations
The grammar below is the C syntax from [K&R,A13] modified to show the syntax of syntactic comments. Only productions effected by LCLint annotations are shown. In the annotations, the @ represents the comment marker char, set by -commentchar (default is @).
Functions
direct-declarator:
	  direct-declarator (parameter-type-list_opt) globals_opt modifies_opt
	| direct-declarator (identifier-list_opt) globals_opt modifies_opt
globals: (Section 4.2)
	  /*@globals globitem,+ ;_opt @*/
	| /*@globals declaration-list_opt ;_opt @*/
globitem:
	   globannot* identifier
        |  internalState
	|  systemState
globannot: undef | killed

modifies: (Section 4.1)
           /*@modifies moditem,+;_opt @*/	
         | /*@modifies nothing ;_opt @*/
         | /*@*/  (Abbreviation for no globals and modifies nothing.)
moditem:
	   expression	
         | internalState
         | systemState
Iterators (Section 8.4)
The globals and modifies clauses for an iterator are the same as those for a function, except they are not enclosed by a comment, since the iterator is already a comment.
direct-declarator:
       /*@iter identifier (parameter-type-list_opt) globals_opt
modifies_opt @*/
Constants (Section 8.1)
external-declaration:
       /*@constant declaration ;_opt @*/
Alternate Types (Section 8.2.2)
Alternate types may be used in the type specification of parameters and return values.
extended-type:
        type-specifier alt-type_opt
alt-type:
        /*@alt basic-type,+ @*/
Declarator Annotations
General annotations appear after storage-class-specifiers and before type-specifiers. Multiple annotations may be used in any order. Here, annotations are without the surrounding comment. In a declaration, the annotation would be surrounded by /*@ and @*/. In a globals or modifies clause or iterator or constant declaration, no surrounding comment would be used since they are within a comment.
Type Definitions (Section 3)
A type definition may use any either abstract or concrete, either mutable or immutable, and refcounted. Only a pointer to a struct may be declared with refcounted. Mutability annotations may not be used with concrete types since concrete types inherit their mutability from the actual type.
abstract
Type is abstract (representation is hidden from clients).
concrete
Type is concrete (representation is visible to clients).
immutable
Instances of the type cannot change value. (Section 3.2)
mutable
Instances of the type can change value. (Section 3.2)
refcounted
Reference counted type. (Section 5.4)
Global Variables (Section 4.2.1)
One check annotation may be used on a global or file-static variable declaration.
unchecked
Weakest checking for global use.
checkmod
Check modification by not use of global.
checked
Check use and modification of global.
checkedstrict
Check use of global, even in functions with no global list.
Memory Management (Section 5)
dependent
A reference to externally-owned storage. (Section 5.2.2)
keep
A parameter that is kept by the called function. The caller may use the storage after the call, but the called function is responsible for making sure it is deallocated. (Section 5.2.4)
killref
A refcounted parameter. This reference is killed by the call. (Section 5.4)
only
A unshared reference. Associated memory must be released before reference is lost. (Section 5.2)
owned
Storage may be shared by dependent references, but associated memory must be released before this reference is lost. (Section 5.2.2)
shared
Shared reference that is never deallocated. (Section 5.2.5)
temp
A temporary parameter. May not be released, and new aliases to it may not be created. (Section 5.2.2)
Aliasing (Section 6)
Both alias annotations may be used on a parameter declaration.
unique
Parameter that may not be aliased by any other reference visible to the function. (Section 6.1.1)
returned
Parameter that may be aliased by the return value. (Section 6.1.2)
Exposure (Section 6.2)
observer
Reference that cannot be modified. (Section 6.2.1)
exposed
Exposed reference to storage in another object. (Section 6.2.1)
Definition State (Section 7.1)
out
Storage reachable from reference need not be defined.
in
All storage reachable from reference must be defined.
partial
Partially defined. A structure may have undefined fields. No errors reported when fields are used.
reldef
Relax definition checking. No errors when reference is not defined, or when it is used.
Global State (Section 7.1.4)
These annotations may only be used in globals lists. Both annotations may be used for the same variable, to mean the variable is undefined before and after the call.

undef
Variable is undefined before the call.
killed
Variable is undefined after the call.
Null State (Section 7.2)
null
Possibly null pointer.
notnull
Non-null pointer.
relnull
Relax null checking. No errors when NULL is assigned to it, or when it is used as a non-null pointer.
Null Predicates (Section 7.2.1)
A null predicate annotation may be used of the return value of a function returning a boolean type, taking a possibly-null pointer for its first argument.
truenull
If result is TRUE, first parameter is NULL.
falsenull
If result is TRUE, first parameter is not NULL.
Execution (Section 7.3)
The exits, mayexit and neverexits annotations may be used on any function. The trueexit and falseexit annotations may only be used on functions whose first argument is a boolean.
exits
Function never returns.
mayexit
Function may or may not return.
trueexit
Function does not return if first parameter is TRUE.
falseexit
Function does not return if first parameter if FALSE.
neverexit
Function always returns.
Side-Effects (Section 8.2.1)
sef
Corresponding actual parameter has no side effects.
Declaration
These annotations can be used on a declaration to control unused or undefined error reporting.
unused
Identifier need not be used (no unused errors reported.) (Section 10.4)
external
Identifier is defined externally (no undefined error reported.) (Section 10.5)
Case
fallthrough
Fall-through case. No message is reported if the previous case may fall-through into the one immediately after the fallthrough.
Break (Section 10.2.3)
These annotations are used before a break or continue statement.
innerbreak
Break is breaking an inner loop or switch.
loopbreak
Break is breaking a loop.
switchbreak
Break is breaking a switch.
innercontinue
Continue is continuing an inner loop.
Unreachable Code
This annotation is used before a statement to prevent unreachable code errors.
notreached
Statement may be unreachable.
Special Functions (Apppendix E)
These annotations are used immediately before a function declaration.
printflike
Check variable arguments like printf library function.
scanflike
Check variable arguments like scanf library function.
Next: Appendix E. Control Comments
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