REFERENCE
Annotations
WeaveC annotations live in the weavec.h header, which weavec puts on the
system include path automatically (#include <weavec.h>). Every macro expands
to __attribute__((annotate("weavec.<name>"))) under Clang and to nothing
under compilers without the annotate attribute, so annotated code stays
portable C.
| Macro | Applies to | Meaning |
|---|---|---|
WEAVEC_OWNED |
pointer parameters, returns, variables, fields | The pointer uniquely owns its referent and must release it exactly once. On a struct field: the field owns its referent whenever the struct is live, so freeing the struct without releasing, moving or nulling the field first is a leak (RFC 0007). |
WEAVEC_BORROWED |
pointer parameters, returns, variables, fields | Shared, read-only borrow. The referent outlives the borrow. |
WEAVEC_MUT |
pointer parameters, returns, variables, fields | Exclusive, mutable borrow. |
WEAVEC_RAW |
pointer parameters, returns, variables, fields, function-pointer types | No guarantee at all: the checker tracks the pointer but any dereference, release or transfer of ownership must happen inside a WEAVEC_UNSAFE region. |
WEAVEC_UNSAFE |
function declarations, compound statements | An unsafe region: raw operations are permitted and nothing inside is reported, but ownership still flows through it and out of it. |
WEAVEC_NULLABLE |
pointer parameters, returns, variables, fields | The pointer may be null (RFC 0008). On a parameter: the body must test it before dereferencing it, and callers may pass null. On a return type: callers must test the result. On a variable or field: every load is treated as maybe-null until it is tested. Says nothing about ownership; combine with WEAVEC_OWNED/WEAVEC_BORROWED/WEAVEC_MUT as needed. |
WEAVEC_NONNULL |
pointer parameters, returns, variables, fields | The pointer is never null (RFC 0008). On a parameter: callers must pass a pointer the checker knows is non-null, even if the body never dereferences it. On a return type: callers need not test the result. On a variable or field: it is never reported as null. Says nothing about ownership. |
WEAVEC_RETAINS |
pointer parameters | The callee takes a reference on the argument’s object (RFC 0010): the caller’s pointer gains a share, which the next copy of it carries away. On a declaration with no body whose result has the parameter’s type and no ownership annotation, the result is a copy of the argument (the shape of g_object_ref). |
WEAVEC_RELEASES |
pointer parameters | The callee releases one reference (RFC 0010): the argument’s name is dead afterwards; other shares of the object are untouched. |
WEAVEC_REFCOUNT |
integer fields | The field is a reference count (RFC 0010): a share taken through it and never released is a leak even when no function in the program releases through it. Inference recognises the field by its increments and decrements regardless. |
WEAVEC_OWNED_BY(f) |
pointer parameters and returns, next to WEAVEC_OWNED |
The release family is f (RFC 0010): struct handle *handle_open(void) WEAVEC_OWNED WEAVEC_OWNED_BY(handle_close); makes free(handle_open()) a mismatched-release. Without WEAVEC_OWNED it is an invalid-annotation. |
WEAVEC_SIZED_BY(n) |
pointer parameters, pointer fields | On a parameter: the caller passes at least n elements behind the pointer (bytes for void *), n being another parameter of the same function by name (RFC 0011): void fill(char *WEAVEC_SIZED_BY(len) buf, size_t len);. Inside the body the parameter has that extent, so buf[len] is out-of-bounds; at every call the argument must have at least that many, so fill(small, 8) on char small[4] is out-of-bounds. On a field: the object holds at least n elements behind the pointer, n being another integer field of the same struct by name (RFC 0012): struct buf { char *WEAVEC_SIZED_BY(cap) data; size_t cap; };. Every function that loads the field sees that extent (b->data[b->cap] is out-of-bounds, for (i = 0; i <= b->cap; i++) b->data[i] may be), and a store into the field of an object the count says is too small is an annotation-mismatch (b->data = malloc(4); b->cap = 8;, in either order). Says nothing about ownership or nullness; combine with the others as needed. On a non-pointer, or naming a parameter or field that does not exist or is not an integer: invalid-annotation. |
WEAVEC_ASSUME(expr) |
statements | expr holds from here on, as if the code below were inside if (expr) (RFC 0012): WEAVEC_ASSUME(b->len < b->cap); lets the checker prove d[b->len] in bounds on malloc(b->cap), WEAVEC_ASSUME(p != NULL) removes a null-dereference. Trusted like every annotation: an assumption the checker’s facts contradict ends the path (nothing below it is analysed), and a false one hides reports. expr must be side-effect free; it is evaluated under WeaveC and is an unevaluated operand (sizeof) under every other compiler. |
WEAVEC_ENABLED |
(macro, not an attribute) | 1 when the TU is being processed by weavec, else 0. |
Annotations on a function-pointer type describe whatever is called through it (RFC 0004):
typedef void (*dtor_t)(struct node *WEAVEC_OWNED); /* every call consumes */typedef WEAVEC_OWNED struct node *(*maker_t)(void); /* every call allocates */struct ops { void (*drop)(struct node *WEAVEC_OWNED); /* fields too */ void *(*WEAVEC_OWNED alloc)(size_t); /* result of alloc */};An annotation on the declarator of a function pointer (the typedef name, the field or the parameter) describes the result of calls through it; the annotations inside its parameter list describe the arguments.
Without a type contract, calls use the actual function-pointer values that reach them (RFC 0014). A helper can be checked with distinct callback bindings; a same-type function elsewhere in the program does not provide an unknown callback’s behavior. Global target values include possible writes from analyzed functions, while a known store at a call updates that caller’s state. Unknown alternatives remain boundaries.