Module Guards::Internal

INTERNAL: Do not use.

Imports

Predicates

asserts

Holds if assertion a directly asserts that expression e evaluates to value v.

getNullEquivParent

Gets the parent expression of e which is null only if e is null, if any. For example, result = x?.y and e = x, or result = x + 1 and e = x.

impliesSteps

Holds if the assumption that g1 has abstract value v1 implies that g2 has abstract value v2, using zero or more steps of reasoning. That is, the evaluation of g2 to v2 dominates the evaluation of g1 to v1.

nonNullValue

Holds if expression e is a non-null value.

Classes

Guard

An expression whose value may control the execution of another element.

Datatypes

Modules