Module Log_With_Focusing.QuerySource

Reachable means that the set of memory states is not empty.

• If we return Top (i.e. {True,False}), then the memory may be reachable;
• If we return True, then the memory is reachable;
• If we return False or Bottom, the memory is not reachable.