|
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 |
4 Types
Strong type checking often reveals programming errors. Splint can check primitive C types more strictly and flexibly than typical compilers (4.1) and provides support a Boolean type (4.2). In addition, users can define abstract types that provide information hiding (0).
4.1 Built in C Types
Two types have compatible type if their types are the same.
ANSI C, 3.1.2.6.
Splint supports stricter checking of built in C types. The char and enum types can be checked as distinct types, and the different numeric types can be type-checked strictly.
4.1.1 Characters
The primitive char type can be type-checked as a distinct type. If char is used as a distinct type, common errors involving assigning ints to chars are detected.
The +charint flag can be used for checking legacy programs where char and int are used interchangeably. If charint is on, char types indistinguishable from ints. To keep char and int as distinct types, but allow chars to be used to index arrays, use +charindex.
4.1.2 Enumerators
Standard C treats user-declared enum types just like integers. An arbitrary integral value may be assigned to an enum type, whether or not it was listed as an enumerator member. Splint checks each user-defined enum type as distinct type. An error is reported if a value that is not an enumerator member is assigned to the enum type, or if an enum type is used as an operand to an arithmetic operator. If the enumint flag is on, enum and int types may be used interchangeably. Like charindex, if the enumindex flag is on, enum types may be used to index arrays.
4.1.3 Numeric Types
Splint reports where numeric types are used in dangerous or inconsistent ways. With the strictest checking, Splint will report an error anytime numeric types do not match exactly. If the relax-quals flag is on, only those inconsistencies that may corrupt values are reported. For example, if an int is assigned to a variable of type long (or passed as a long formal parameter), Splint will not report an error if relax-quals is on since a long must have at least enough bits to store an int without data loss. On the other hand, an error would be reported if the long were assigned to an int, since the int type may not have enough bits to store the long value.
Similarly, if a signed value is assigned to an unsigned, Splint will report an error since an unsigned type cannot represent all signed values correctly. If the +ignore-signs flag is on, checking is relaxed to ignore all sign qualifiers in type comparisons (this is not recommended, since it will suppress reporting of real bugs, but may be necessary for quickly checking certain legacy code).
4.1.4 Arbitrary Integral Types
Some types are declared to be integral types, but the concrete type may be implementation dependent. For example, the standard library declares the types size_t, ptr_diff and wchar_t, but does not constrain their types other than limiting them to integral types. Programs may rely on them being integral types (e.g., can use + operator on two size_t operands), but should not rely on a particular representation (e.g., long unsigned).
Splint supports three different kinds of arbitrary integral types:
/*@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.
Splint reports an error if the code depends on the actual representation of a type declared as an arbitrary integral. The match-any-integral flag relaxes checking and allows an arbitrary integral type is allowed to match any integral type.
Other flags set the arbitrary integral types to a concrete type. These should only be used if portability to platforms that may use different representations is not important. The long-integral and long-unsigned-integral flags set the type corresponding to /*@integraltype@*/ to be unsigned long and long respectively. The long-unsigned-unsigned-integral flag sets the type corresponding to /*@unsignedintegraltype@*/ to be unsigned long. The long-signed-integral flag sets the type corresponding to /*@signedintegraltype@*/ to be long.
4.2 Boolean Types
Pre-ISO99 C had no Boolean representation – the result of a comparison operator was an integer, and no type checking is done for test expressions. C99 introduced a Boolean type (_Bool and bool, true and false macros in stdbool.h), but did not strengthen the type checking. Splint supports a Boolean type that can be checked distinctly from integral types. Many common errors can be detected by introducing a distinct Boolean type and stronger type checking.
Splint checks that the test expression in an if, while, or for statement or an operand of a &&, || or !operator is a Boolean. If the type of a test expression is not a Boolean, Splint will produce a warning depending on the type of the test expression and flag settings. If the test expression has pointer type, the warning is inhibited by –predboolptr (this can be used to prevent messages for the idiom of testing if a pointer is not null without a comparison). If it is type int, the warnings is inhibited by -pred-bool-int. For all other types, Splint warns unless -pred-bool-others is set. Relations, comparisons and certain standard library functions are declared to return Booleans.
Since using = instead of == is such a common bug, reporting of test expressions that are assignments is controlled by the separate pred-assign flag. The message can be suppressed by adding extra parentheses around the test expression.
Use the –booltype <name> flag to select the type name is used to represent Boolean values. There is no default Boolean type, although bool is used by convention. The names TRUE and FALSE are assumed to represent true and false Boolean values. To change the names of true and false, use -booltrue and -boolfalse. (The Splint distribution includes an implementation of bool, in lib/bool.h. However, it isn’t necessary to use this implementation to get the benefits of Boolean checking.)
Figure 4 illustrates some of the Boolean checking done by Splint.
bool.c
Running Splint
# include "bool.h"
int f (int i, char *s,
bool b1, bool b2)
{
6 if (i = 3)
7 return b1;
8 if (!i || s)
9 return i;
10 if (s)
11 return 7;
12 if (b1 == b2)
13 return 3;
14 return 2;
}
> splint bool.c +predboolptr –booltype bool
bool.c:6: Test expression for if is assignment expression: i = 3
bool.c:6: Test expression for if not bool, type int: i = 3
bool.c:7: Return value type bool does not match declared type int: b1
bool.c:8: Operand of ! is non-boolean (int): !i
bool.c:8: Right operand of || is non-boolean (char *): !i || s
bool.c:10: Test expression for if not bool, type char *: s
bool.c:12: Use of == with bool variables (risks inconsistency because
of multiple true values): b1 == b2
Finished checking --- 7 code warnings found
Figure 4. Boolean Checking
4.3 Abstract Types
Information hiding is a technique for handling complexity. By hiding implementation details, programs can be understood and developed in distinct modules and the effects of a change can be localized. One technique for information hiding is data abstraction. An abstract type is used to represent some natural program abstraction. It provides functions for manipulating instances of the type. The module that implements these functions is called the implementation module. We call the functions that are part of the implementation of an abstract type the operations of the type. Other modules that use the abstract type are called clients.
Clients may use the type name and operations, but should not manipulate or rely on the actual representation of the type. Only the implementation module may manipulate the representation of an abstract type. This hides information, since implementers and maintainers of client modules should not need to know anything about how the abstract type is implemented. It provides modularity, since the representation of an abstract type can be changed without having to change any client code.
Splint supports abstract types by detecting places where client code depends on the concrete representation of an abstract type. Some examples of abstraction violations detected by Splint are shown in Figure 5.
To declare an abstract type, the abstract annotation is added to a typedef. For example (in mstring.h),
typedef /*@abstract@*/ char *mstring;
declares mstring as an abstract type. It is implemented using a char *, but clients of the type should not depend on or need to be aware of this. If it later becomes apparent that a better representation such as a string table should be used, we should be able to change the implementation of mstring without having to change or inspect any client code.
In a client module, abstract types are checked by name, not structure. Splint reports an error if an instance of mstring is passed as a char * (for instance, as an argument to strlen), since the correctness of this call depends on the representation of the abstract type. Splint also reports errors if any C operator except assignment (=) or sizeof is used on an abstract type. The assignment operator is allowed since its semantics do not depend on the representation of the type (for abstract types whose instances can change value, a client does need to know if assignment has copy or sharing semantics as discussed in Section 4.3.2). The use of sizeof is also permitted, since this is the only way for clients to allocate pointers to the abstract type. Type casting objects to or from abstract types in a client module is an abstraction violation and will generate a warning message.
Normally, Splint will assume a type definition is not abstract unless the /*@abstract@*/ qualifier is used. If instead you want all user-defined types to be abstract types unless they are marked as concrete, the +imp-abstract flag can be used. This adds an implicit abstract annotation to any typedef that is not marked with /*@concrete@*/.
palindrome.c
Running Splint
# include "bool.h"
# include "mstring.h"
bool isPalindrome (mstring s)
{
6 char *current = (char *) s;
7 int i, len = (int) strlen (s);
for (i = 0; i <= (len+1) / 2; i++)
{
11 if (current[i] != s[len-i-1])
return FALSE;
}
return TRUE;
}
bool callPal (void)
{
19 return (isPalindrome ("bob"));
}
> splint palindrome.c
palindrome.c:6: Cast from underlying
abstract type mstring: (char *)s
palindrome.c:7: Function strlen expects arg
1 to be char * gets mstring: s
palindrome.c:11: Array fetch from non-array
(mstring): s[len - i - 1]
palindrome.c:19: Function isPalindrome
expects arg 1 to be mstring gets char *:
"bob"
Finished checking --- 4 code warnings
Figure 5. Information Hiding Violations
Traditionally, programming books wax mathematical when they arrive at the topic of abstract data types…
Such books make it seem as if you’d never actually use an abstract data type except as a sleep aid.Steve McConnell
4.3.1 Controlling Access
Where code may manipulate the representation of an abstract type, we say the code has access to that type. If code has access to an abstract type, the representation of the type and the abstract type are indistinguishable. Usually, a single program module that is the only code that has access to the type representation implements an abstract type. Sometimes, more complicated access control is desired if the implementation of an abstract type is split across program files, or particular client code needs to access the representation.
There are a several ways of selecting what code has access the representation of an abstract type:
· Modules. An abstract type defined in M .h is accessible in M.c. Controlled by the accessmodule flag. This means when accessmodule is on, as it is by default, the module access rule is in effect. If accessmodule is off (when -access-module is used), the module access rule is not in effect and an abstract type defined in M.h is not necessarily accessible in M .c.
· File names. An abstract type named type is accessible in files named type.<extension>. For example, the representation of mstring is accessible in mstring.h and mstring.c. Controlled by the access-file flag.
· Function names. An abstract type named type may be accessible in a function named type_name or typeName. For example, mstring_length and mstringLength would have access to the mstring abstract type. Controlled by accessfunction and the naming convention (see Section 12).
· Access control comments. The syntax /*@access type,+@*/[2] allows the following code to access the representation of type. Similarly, /*@noaccess type,+@*/ restricts access to the representation of type. The type in a noaccess comment must have been declared as an abstract type.
4.3.2 Mutability
We can view types as being mutable or immutable. A type is mutable if passing it as a parameter to a function call can change the value of an instance of the type. For example, the primitive type int is immutable. If i is a local variable of type int and no variables point to the location where i is stored, the value of i must be the same before and after the call f (i). Structure and union types are also immutable, since they are copied when they are passed as arguments. On the other hand, pointer types are mutable. If x is a local variable of type int *, the value of *x (and hence, the value of the object x) can be changed by the function call g(x).
The mutability of a concrete type is determined by its type definition. For abstract types, mutability does not depend on the type representation but on what operations the type provides. If an abstract type has operations that may change the value of instances of the type, the type is mutable. If not, it is immutable. The value of an instance of an immutable type never changes. Since object sharing is noticeable only for mutable types, they are checked differently from immutable types.
The /*@mutable@*/ and /*@immutable@*/ annotations are used to declare an abstract type as mutable or immutable. (If neither is used, the abstract type is assumed to be mutable.) For example,
typedef /*@abstract@*/ /*@mutable@*/ char *mstring;
typedef /*@abstract@*/ /*@immutable@*/ int weekDay;
declares mstring as a mutable abstract type and weekDay as an immutable abstract type.
Clients of a mutable abstract type need to know the semantics of assignment. After the assignment expression s = t, do s and t refer to the same object (that is, will changes to the value of s also change the value of t).
Splint prescribes that all abstract types have sharing semantics, so s and t would indeed be the same object. Splint will produce a warning if a mutable type is implemented with a representation (e.g., a struct) that does not provide sharing semantics (controlled by mutrep flag).
The mutability of an abstract type is not necessarily the same as the mutability of its representation. We could use the immutable concrete type int to represent mutable strings using an index into a string table, or declare mstring as immutable as long as no operations are provided that modify the value of an mstring.
4.3.3 Semi-Abstract Types
Sometimes it is useful to have a type that is abstract in some ways, but can be used with the standard numerical operators. Splint supports numabstract types for this purpose. The /*@numabstract@*/ annotation denotes a numabstract type. Splint will report warnings when numabstract types are used inconsistently, but allow binary numeric operators to operate on two values of the same numabstract type. Several flags control the strictness of type checking for numabstract types: numabstract, numabstractcast, numabstractlit, numabstractindex, and numabstractprint .
4.4 Polymorphism
In C, all declarators must be declared to have exactly one type. This makes it impossible to write functions that operate on more than one type of parameter – for example, we cannot use the same square function for ints and floats. Because of the stricter type checking made possible by Splint, it is often useful to declare a parameter that has more than one possible type.
Splint provides alternate types to indicate that a declaration may be one of several possible types. The /*@alt type,+@*/ annotation creates a union type. For example, int /*@alt char, unsigned char@*/ c declares c such that either an int, char or unsigned char value may be assigned to it without warning.
One use of alternate types is to specify the type of a macro that operates on multiple types of operands (see Section 11.2.1). Alternate types are also useful for declaring functions for which the return value may be safely ignored (see Section 8.4.2). A function can be declared to return t /*@alt void@*/ to indicate that it returns a value of type t, but there should be not warning if that value is ignored.
Next: 5. Memory Management
Return to Contents