6              Sharing

Errors involving unexpected sharing of storage can cause serious problems.  Undocumented sharing may lead to unpredictable modifications, and some library calls (e.g., strcpy) have undefined behavior if parameters share storage.  Another class of sharing errors occurs when clients of an abstract type may obtain a reference to mutable storage that is part of the abstract representation.  This exposes the representation of the abstract type, since clients may modify an instance of the abstract type indirectly through this shared storage.

6.1            Aliasing

Splint detects errors involving dangerous aliasing of parameters.  Some of these errors are already detected through the standard memory annotations (e.g., only parameters may not be aliases.)   Two additional annotations are provided for constraining aliasing of parameters and return values.

6.1.1        Unique Parameters

The unique annotation denotes a parameter that may not be aliased by any other storage reachable from the function implementation — that is, any storage reachable through the other parameters or global variables used by the function.  The unique annotation places similar constraints on function parameters as the only annotation, but it does not transfer the obligation to release storage.  Splint will report an error if a unique parameter may be aliased by another parameter or global variable.


Splint reports an error if a function returns a reference to storage reachable from one of its parameters (if retalias is on) since this may introduce unexpected aliases in the body of the calling function when the result is assigned.


Figure 10 illustrated sharing checks.  An error is reported since the first parameter to the library function strcpy is declared with unique.  If a unique qualifier were added to the parameter declaration for s or t, no error would be reported. 


Running Splint

# include <string.h>



capitalize (/*@out@*/ char *s,

            char *t)


 7  strcpy (s, t);

   *s = toupper (*s);


> splint unique.c


unique.c: (in function capitalize)

unique.c:7: Parameter 1 (s) to function strcpy is

    declared unique but may be aliased externally by

    parameter 2 (t)


Figure 10.  Unique parameters

6.1.2        Returned Parameters

The returned annotation denotes a parameter that may be aliased by the return value.  Splint checks the call assuming the result may be an alias to the returned parameter.


Consider the following code excerpt:


extern intSet intSet_insert (/*@returned@*/ intSet s, int x);


intSet intSet_singleton (int x)


7  return (intSet_insert (intSet_new (), x));



Without the returned qualifier on the parameter to intSet_insert, a memory leak error would be reported for line 7, since the only storage returned by intSet_new is not released.  Because of the returned qualifier, Splint assumes the result of intSet_insert is the same storage as its first parameter, in this case the storage returned by intSet_new.  No error is reported, since the only storage is then transferred through the return value (which has an implicit only annotation, see Section 5.3).

6.2            Exposure

Splint detects places where the representation of an abstract type is exposed.  This occurs if a client has a pointer to storage that is part of the representation of an instance of the abstract type.  The client can then modify or examine the storage this points to, and manipulate the value of the abstract type instance without using its operations.


There are three ways a representation may be exposed:

1.       Returning (or assigning to a global variable) an object that includes a pointer to a mutable component of an abstract type representation.  (Controlled by ret-expose).

2.       Assigning a mutable component of an abstract object to storage reachable from an actual parameter or a global variable that may be used after the call.   This means the client may manipulate the abstract object using the actual parameter after the call.  Note that if the corresponding formal parameter is declared only, the caller may not use the actual parameter after the call so the representation is not exposed.  (Controlled by assign-expose).

3.       Casting mutable storage to or from an abstract type.  (Controlled by cast-expose).

Annotations may be used to allow exposed storage to be returned safely by restricting how the caller may use the returned storage.

6.2.1        Read-Only Storage

It is often useful for a function to return a pointer to internal storage (or an instance of a mutable abstract type) that is intended only as an observer.  The caller may use the result, but should not modify the storage it points to.  For example, consider a naïve implementation of the employee_getName operation for the abstract employee type:

   typedef /*@abstract@*/ struct {

      char *name;

      int id;

   } *employee;


   char *employee_getName (employee e) { return e->name; }

Splint produces a message to indicate that the return value exposes the representation.  One solution would be to return a fresh copy of e->name.  This is expensive, though, especially if we expect employee_getName is used mainly just to get a string for searching or printing.  Instead, we could change the declaration of employee_getName to:

extern /*@observer@*/ char *employee_getName (employee e);

Now, the original implementation is correct.  The declaration indicates that the caller may not modify the result, so it is acceptable to return shared storage.  (The program must also not use the returned observer storage after any other calls to the abstract type module using the same parameter.  Splint does not attempt to check this, and in practice it is rarely a problem.)  Splint checks that the caller does not modify the return value.  An error is reported if observer storage is modified directly, passed as a function parameter that may be modified, assigned to a global variable or reference derivable from a global variable that is not declared with an observer annotation , or returned as a function result or a reference derivable from the function result that is not annotation with an observer annotation.

String Literals

A program that attempts to modify a string literal has undefined behavior [ISO, 6.4.5]. This is not enforced by most C compilers, and can lead to particularly pernicious bugs that only appear when optimizations are turned on and the compiler attempts to minimize storage for string literals.  Splint can be used to check that string literals are not modified, by treating them as -observer storage.  If +read-only-strings is set (default in standard mode), Splint will report an error if a string literal is modified.

6.2.2        Exposed Storage

Sometimes it is necessary to expose the representation of an abstract type.  This may be evidence of a design flaw, but in some cases is justified for efficiency reasons.  The exposed annotation denotes storage that is exposed.  It may be used on a return value for results that reference storage internal to an abstract representation, on a parameter value to indicate a parameter that may be assigned directly to part of an abstract representation (note that if the parameter is annotated with only, it is not an error to assign it to part of an abstract representation, since the caller may not use the storage after the call returns), or on a field of an abstract representation to indicate that external references to the storage may exist.  An error is reported if exposed storage is released, but unlike an observer, no error is reported if it is modified.  Figure 11 shows examples of exposure problems detected by Splint.



Running Splint

# include "employee.h"


char *

employee_getName (employee e)


6  return e->name;



/*@observer@*/ char *

employee_obsName (employee e)

{ return e->name; }


/*@exposed@*/ char *

employee_exposeName (employee e)

{ return e->name; }



employee_capName (employee e)


  char *name;


  name = employee_obsName (e);

23 *name = toupper (*name);


> splint exposure.c +checks


exposure.c:6: Function returns reference to

                 parameter e: e->name

exposure.c:6: Return value exposes rep of

                 employee: e->name

exposure.c:6: Released storage e->name reachable

                 from parameter at return point

   exposure.c:6: Storage e->name is released

exposure.c:23: Suspect modification of observer

                  name: *name = toupper(*name)


Three messages are reported for line 6 where a mutable field of an abstract type is returned with no sharing qualifier (without +checksonly the third one would be reported.)  The error for line 23 reports a modification of an observer.  If the call in line 22 were changed to call employee_exposeName , no error would be reported.

Figure 11.  Exposure

Next: 7. Function Interfaces
Return to Contents