Appendix C                    Annotations

Suppressing Warnings

Several annotations are provided for suppressing messages.  In general, it is usually better to use specific flags to suppress a particular error permanently, but the general error suppression flags may be more convenient for quickly suppressing messages for code that will be corrected or documented later.

ignore

end

No errors will be reported in code regions between /*@ignore@*/ and /*@end@*/.  These comments can be used to easily suppress an unlimited number of messages, but are dangerous since if real errors are introduced in the ignoreend region they will not be reported. The ignore and end comments must be matched — a warning is printed if the file ends in an ignore region or if ignore is used inside ignore region.

i

No errors will be reported from an /*@i@*/ comment to the end of the line.

i<n>

No errors will be reported from an /*@i<n>@*/ (e.g., /*@i3@*/) comment to the end of the line.  If there are not exactly n errors suppressed from the comment point to the end of the line, Splint will report an error.  This is more robust than i or ignore since a message is generated if the expected number errors is not present.  Since errors are not necessarily detected until after this file is processed (for example, and unused variable error), suppress count errors are reported after all files have been processed.  The ‑supcounts flag may be used to suppress these errors.  This is useful when a system if being rechecked with different flag settings.

t

t<n>

Like i and i<n>, except controlled by +tmpcomments flag.  These can be used to temporarily suppress certain errors.  Then, -tmpcomments can be set to find them again.

Syntactic Annotations

The grammar below is the C syntax from [K&R,A13] modified to show the syntax of syntactic comments.  Only productions effected by Splint annotations are shown.  In the annotations, the @ represents the comment marker char, set by -commentchar (default is @).

Functions

direct-declarator Þ

   direct-declarator (parameter-type-listopt ) stateClause*opt globalsopt modifiesopt

|  direct-declarator (identifier-listopt ) stateClause*opt globalsopt modifiesopt

 

stateClause Þ /*@ ( uses | sets | defines | allocates | releases) reference,+ ;opt @*/

               | /*@ ( ensures | requires ) stateTag reference,+ ;opt @*/                    (Section 7.4)

 

stateTag Þ only | shared | owned | dependent | observer | exposed | isnull | notnull

     | identifier                           (Annotation defined by metastate definition, Section 10)

           

globals Þ /*@globals globitem,+ ;opt @*/ | /*@globalsdeclaration-listopt  ;opt @*/ 

globitem Þ [ ( undef | killed )* ]    identifier |  internalState fileSystem

 

modifies Þ /*@modifies (nothing | (expression | internalState | fileSystem)+ ;opt) @*/        

     | /*@*/                   (Abbreviation for no globals and modifies nothing.)

Iterators (Section 11.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-listopt ) iterGlobalsopt iterModifiesopt @*/

 

iter-globals Þ globals declaration-listopt ;opt

iter-modifies Þ modifies  moditem,+;opt|  modifies nothing;opt

Constants (Section 11.1)

external-declaration Þ /*@constant declaration  ;opt @*/

Alternate Types (Section 4.4)

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 comments would be used since they are within a comment.

Type Definitions (Section 4.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 abstraction (representation is hidden from clients.)

concrete

Type is concrete (representation is visible to clients.)

immutable

Instances of the type cannot change value.

mutable

Instances of the type can change value.

refcounted

Reference counted (Section 5.4).

Type Access

Control comments may also be used to override type access settings.

 

/*@access <type>,+@*/ 

Allows the following code to access the representation of <type>.  Type access applies from the point of the comment to the end of the file or the next access control comment for this type.

/*@noaccess <type>,+@*/

Restricts access to the representation of <type>.  The type in a noaccess comment must have been declared as an abstract type. 

Global Variables  (Section 7.2 )

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 3 )

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

An 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 )

Definition State (Section 3 )

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.2.2)

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 2 )

null

Possibly null pointer.

notnull  

Non-null pointer.

relnull

Relax null checking.  No errors when NULLis assigned to it, or when it is used as a non-null pointer.

Null Predicates (Section 2.1.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.

nullwhentrue

If result is true, first parameter is NULL.

falsewhennull

If result is TRUE, first parameter is not NULL.

Execution  (Section 8.1 )

The noreturn, maynotreturn and alwaysreturn annotations may be used on any function.  The noreturnwhentrue and noreturnwhenfalse annotations may only be used on functions whose first argument is a Boolean.  

noreturn                       

Function never returns.

maynotreturn

Function may or may not return.

noreturnwhentrue

Function does not return if first parameter is TRUE.

noreturnwhenfalse

Function does not return if first parameter if FALSE.

alwaysreturn

Function always returns.

Side Effects (Section 11.2.1)

sef

Corresponding actual parameter has no side effects.

Declarations

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 13.1 )

external

Identifier is defined externally (no undefined error reported.) (Section 13.2 )

Switch Statements

fallthrough

Fall through case.  No message is reported if the previous case may fall through into the one immediately after the fallthrough.

Break and Continue Statements (Section 8.3.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.

Format String Arguments 

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.

Use Warnings

These annotations are used immediately before a function, variable or type declaration.

warn <flag-specifier> <message>

Issue a warning (controlled by flag-specifier) where this declarator is used.

Macro Expansion

/*@notfunction@*/

The next macro definition is not intended to be a function, and should be expanded in line instead of checked as a macro function definition.

Arbitrary Integral Types

These annotations are used to represent arbitrary integral types.  Syntactically, they replace the implicit int type.

 

/*@integraltype@*/

An arbitrary integral type.  The actual type may be any one of short, int, long, unsigned short, unsigned, or unsigned long.

/*@unsignedintegraltype@*/

An arbitrary unsigned integral type.  The actual type may be any one of unsigned short, unsigned, or unsigned long.

/*@signedintegraltype@*/

An arbitrary signed integral type.  The actual type may be any one of short, int, or long.

Traditional Lint Comments

Some of the control comments supported by most standard UNIX lints are supported by Splint so legacy systems can be checked more easily.  These comments are not lexically consistent with Splint comments, and their meanings are less precise (and may vary between different lint programs), so we recommend that Splint comments are used instead except for checking legacy systems already containing standard lint comments.

 

These standard lint comments supported by Splint:

/*FALLTHROUGH*/ (alternate misspelling, /*FALLTHRU*/)

Prevents errors for fall through cases.  Same meaning as /*@fallthrough@*/.

/*NOTREACHED*/

Prevents errors about unreachable code (until the end of the function).  Same meaning as /*@notreached@*/.  

/*PRINTFLIKE*/

Arguments similar to the printf library function (there didn’t seem to be much of a consensus among standard lints as to exactly what this means).  Splint supports:

/*@printflike@*/

Function takes zero or more arguments of any type, an unmodified char * format string argument and zero of more arguments of type and number dictated by the format string.  Format codes are interpreted identically to the printf standard library function.  May return a result of any type.  (Splint interprets /*PRINTFLIKE*/ as /*@printflike@*/.)

/*@scanflike@*/

Like printflike, except format codes are interpreted as in the scanf library function.

 

/*ARGSUSED*/

Turns off unused parameter messages for this function.  The control comment, /*@‑paramuse @*/ can be used to the same effect, or /*@unused@*/ can be used in individual parameter declarations.

 

Splint will ignore standard lint comments if -lint-comments is used.  If +warn-lint-comments is used, Splint generates a message for standard lint comments and suggest replacements.

Metastate Definitions

The grammar for .mts files is shown below.

 

metastate    Þ [ global ] attribute identifier clause* end

clause        Þ contextClause | valuesClause | defaultClause | defaultsClause

      | annotationsClause | mergeClause | transfersClause | loserefClause

| preconditionsClause | postconditionsClause

contextClauseÞ context contextSelector

contextSelector Þ ( parameter | reference | result | clause | literal | null ) [ type ]

valuesClauseÞ oneof valueChoice,*

 

defaultClause Þ default valueChoide

defaultsClauseÞ defaults ( contextSelector ==> valueChoice )*

 

annotationsClauseÞ annotations  ( identifier [ contextSelector ] ==> valueChoice )*

 

mergeClauseÞ merge ( mergeItem + mergeItem ==> transferAction )*

mergeItemÞ valueChoice | *

 

transfersClauseÞ transfers ( valueChoice as valueChoice==> transferAction )*

loserefClauseÞ losereference ( valueChoice ==> errorAction )*

 

transferActionÞ valueChoice | errorAction

errorActionÞ error [ stringLiteral ]

 

valueChoiceÞ identifier               

Next: Appendix D. Specifications
Return to Contents