After empty(), also model size() to further improve existing checkers and enable more future checkers for iterators and containers.
Just out of curiosity: How do we handle containers that do not have a contiguous memory region? Balanced trees, bucketed hash-maps, etc.
How? I don't see how does it access the size.
What if we have both RetSize and CalcSize? Should we check their values for consistency? (And perhaps adding another sink node if we have inconsistency?)
Yes. The region just serves to identify the container. It is not necessarily the region where the data is stored.
As explained between the parenthesis, the actual size of the container is the difference between its begin() and its end(). If we have this difference, then we know the actual size. The other value we may have is the return value of the size() function. We either have one of them, both or none. If we have one, then we adjust the other. If we have both, then we check for consistency, and generated a sink if they are inconsistent. If we have none, then we do nothing.
This is handled in the if branch: having CalcSize means that we know the difference between the begin() and the end(), thus inconsistency between RetSize and CalcSize is the same as inconstistency between CalcEnd and EndSym. The comment above explains that if there is such inconsistency, then relateSymbols() returns a null pointer which we assign to State. At the end of this functions we generate a sink whenever State is a null pointer.