In unreachable code, the state for every trackable variable should be "not null".

There are a few reasons for this:

1. From a formal, flow-analysis theoretical point of view, this is one end of the lattice and is therefore the default value of the state that is refined as flow analysis proceeds.
2. From a practical point of view, this prevents producing (most) warnings in unreachable code (even if those warnings would later be suppressed).
3. The flow analysis base classes expect the state to implement bool AbstractState.Reachable { get; }

There are a couple of approaches for doing this. The simplest is to have a bit in the state that tracks whether the state is reachable or not (just like control flow analysis and data flow analysis). When such a state is asked for the nullable state of some variable, it always answers "not null".

Another approach, which may be worth doing in addition, would be to

1. Suppress all warnings when the state is unreachable.
2. When merging two states, if one of them is reachable then the result state is the other one.