analyzer: check borrow returns of forward-called functions at the unit's end; borrows clause for prototypes, definitions, externs and function types, checked against the body

1 files changed, 6 insertions, 0 deletions

diff --git a/docs/SPEC.md b/docs/SPEC.md
index 923e24b..b2aa5ea 100644
--- a/docs/SPEC.md
+++ b/docs/SPEC.md
@@ -890,6 +890,10 @@ placing `rt.free(b)` after the use is accepted (the alias's last use precedes th
 
 6.6.4 a checked function cannot return an alias of a local owner (error: a borrow of a local owner cannot escape through return; return the owner). it can return an alias of a parameter (the caller owns it), but not as an owned result of `.u` (error: a borrowed parameter cannot be returned as an owned result; a borrowed projection cannot be returned as an owned result).
 
+6.6.5 a function called before its body is checked the same way once the body has been read: the use of the result after the owner ended is remembered at the call, and reported at the end of the unit if the body returns a borrow of that argument (`...; skip, defined after this call, returns a borrow of its argument`). only a result bound directly to a local (`let r = skip(t);`) is followed; the check never fires for a body that does not return a borrow.
+
+6.6.6 `borrows s` after the parameter list of a prototype, a definition, an `extern` or a function type says the result is a borrow of parameter `s` and of no other parameter. a parameter is named, or given by its position from 0 where it has no name (`extern char* strchr(char*, int) borrows 0;`, `char*(char*) borrows 0 f = skip;`); a declaration may list several (`borrows a, b`), a function type one. the clause is part of the signature: a definition after a prototype keeps the prototype's clause, and a definition whose body returns a borrow of a parameter the clause does not name is an error (`first: returns a borrow of b, but its borrows clause doesn't name it`). without a clause, a bodyless callee is assumed to return a borrow of every argument, so arguments with different owners leave the result untracked; with one, only the named argument's owner is tied to the result.
+
 ### 6.7 recasts
 
 `u*x`, `d*x`, `m*x` (no space between tag and `*`).
@@ -949,6 +953,8 @@ rt.outbuf = saved;
 each fixture in `tests/errors/` starts with `// expect: MESSAGE`; the messages that the analyzer produces are (X is a variable name):
 
 - X: used after it was given away; X borrows Y, and Y was HOW on line N (Y declared on line M), or, for the owner itself, X was HOW on line N (declared on line M). HOW is one of: freed, freed by reassigning it, given to F's .d parameter, moved into Z, stored into Z, pushed into an array, stored in a global or untracked memory, returned, or transferred when the analyzer has no more specific cause
+- F: returns a borrow of P, but its borrows clause doesn't name it
+- borrows names a parameter, by name or by its position from 0
 - X: owned object is never used
 - X: still owns an object; overwriting it would leak it
 - X: is an owned object and can't be copied into another variable