Placement

Attributes bind to the declarator they precede, so put them immediately before the name for parameters and variables:

struct buffer *WEAVEC_OWNED buffer_new(size_t n);           /* return value */
void buffer_free(struct buffer *WEAVEC_OWNED b);            /* consumes b   */
size_t buffer_len(const struct buffer *WEAVEC_BORROWED b);  /* borrows b    */
void buffer_push(struct buffer *WEAVEC_MUT b, int v);       /* mutably      */

int *WEAVEC_OWNED p = malloc(sizeof *p);

struct node *WEAVEC_BORROWED WEAVEC_NULLABLE find(int key); /* may return NULL */
int node_value(const struct node *WEAVEC_BORROWED WEAVEC_NONNULL n);

For functions, WEAVEC_UNSAFE goes before the declaration:

WEAVEC_UNSAFE void poke_hardware(volatile uint32_t *reg) { *reg = 1; }

For blocks, before the opening brace:

void f(int *p) {
  free(p);
  WEAVEC_UNSAFE {
    /* p is dangling here; we know the allocator keeps the page mapped. */
    log_address(p);
  }
}

An unsafe region is a boundary, not a hole: the checker still analyses what happens inside it (so a free inside the block is a free as far as the code after it is concerned, and the function’s summary is still inferred) and only stops reporting there. It is also the only place a WEAVEC_RAW pointer may be dereferenced, released or handed to an owning parameter, and the place to assert what a raw pointer really is:

struct node *WEAVEC_OWNED node_from_handle(uintptr_t h) {
  WEAVEC_UNSAFE { return (struct node *)h; }   /* asserts: this is owned */
}

void stash(struct node *WEAVEC_OWNED n) {
  WEAVEC_UNSAFE { registry[key] = (uintptr_t)n; } /* ownership leaves the model */
}

Outside an unsafe region the same statements are unsafe-operation errors, but the asserted kind still holds afterwards, so a single error replaces a cascade. See RFC 0004, Laundering.

Where raw pointers come from

• a cast from an integer ((struct node *)h, (void *)uintptr);
• a declaration annotated WEAVEC_RAW (parameters, variables, fields, results and function-pointer results);
• a load through a raw pointer (raw->next is raw too);
• the result of a callee whose body returns or stores a raw value, or whose declaration says WEAVEC_RAW;
• under --strict-externs, every pointer that passes through a call the checker cannot resolve (see annotation-required).

Copying, comparing and converting a raw pointer back to an integer are fine anywhere; passing it to a callee’s WEAVEC_RAW parameter is fine too. Only a dereference, a release, a move into an owning parameter, or a borrow by a callee that reads or writes through it is a raw operation.