While the static analyzer is doing a great job modeling functions most of the time, sometimes we have global dynamic invariants that might be infeasible to reason about statically (or in some cases just to complex to worth to implement it).
It would be great to have a way to tell the checkers that certain functions are not worth modeling. In case of fuchsia.HandleCheck, we could achieve the same by simply removing all the annotations. This is not always desired though. The annotations are useful on their own, they document the ownership semantics of the handles. So instead of removing the annotations for these functions, we think it might be better to introduce yet another annotation for this use case.
What do you think? Is this reasonable or do you have any alternative ideas?
For the curious the syscall I have problem with in Fuchsia is the zx_channel_read: https://fuchsia.dev/fuchsia-src/reference/syscalls/channel_read.md
The problem is mainly with the handles parameter. We might not receive handles at all. And we might know that in advance that we will not receive handles, so we do not need to check the actual_handles. So assuming handles contains open handles will end up producing spurious handle leak errors.