Module non_null 

Non-null pointer checks. Non-null contract checker.

This module verifies NonNull obligations against the graph’s operational trace state for the object reached by a pointer or reference.