This patch clarifies the semantics of nocapture attribute.
A 'Pointer Capture' subsection is added to describe the semantics of pointer capture first.
For the nocapture example with two same pointer arguments, it is consistent with the semantics that Alive2 used to run lit tests.
I suggest tweaking this wording slightly. Specifically:
"This attribute applies only to the particular copy of the pointer passed in this argument. A caller could pass two copies of the same pointer with one being annotated nocapture and the other not, and the callee could validly capture through the non annotated parameter.
(Great example btw.)