Common Splint Annotations

This is a list of common Splint annotations, their meanings and common usages.

dependent

Marks that a pointer is a reference to externally owned memory.

Example: Wrapper for fopen

/*@dependent@*/ FILE *safe_fopen(const char *path, const char *mode);

Marks that a function will not return to this point after the function has been called.

Example: For usage function that exits after printing usage text

/*@noreturn@*/ void usage(void);

Marks that a function may either return a null pointer or take a null pointer as one of its arguments.

Example: Function that may return NULL

/*@null@*/ char *hash_table_lookup(Hash_Table *ht, char *key);

Example: Function that may be passed NULL as one of its arguments

Node *create_node(int value, /*@null@*/Node *nextnode);

Marks that memory reachable from reference need not be defined. ie. Something else will set legal values to the memory before it is used.

Example: Wrapper script for malloc

/*@out@*/void *safe_malloc(size_t size);

Marks that a parameter will be used as the return value.

Example: string will be returned in the return value

char *chomp(/*@returned@*/char *string);