JSpecify and restrictive annotations

According to the JSpecify spec, a @Nullable annotation should be acknowledged even if it appears in unannotated (unmarked) code. See the spec and also https://github.com/jspecify/jspecify/issues/235. This treatment corresponds roughly to NullAway's AcknowledgeRestrictiveAnnotations setting, which is off by default. If we want to be compatible with the JSpecify spec on this point out of the box, we need to default AcknowledgeRestrictiveAnnotations to true. But, this could lead to many unexpected (and possible undesirable?) new warnings after a NullAway upgrade. Alternately, we could add a new flag (sigh) like JSpecifyStrict, and then have JSpecifyStrict imply AcknowledgeRestrictiveAnnotations. We might need a new JSpecify-related flag anyway for handling of other features (like arrays).

@lazaroclapp thoughts?

(Side note: I think the current docs for AcknowledgeRestrictiveAnnotations are a bit wrong, in that AcknowledgeRestrictiveAnnotations impacts treatment of any unannotated code, whether present as bytecode or source.)

Start by comparing the JSpecify specification and issue #235 with NullAway's AcknowledgeRestrictiveAnnotations setting and its current documentation. Resolve whether compatibility requires changing the default or adding a JSpecifyStrict flag, including how future JSpecify features such as arrays fit; done means the behavior choice and documentation are consistent.