Predicate functionEnsuresInputIsConstant

Holds if whenever outp of function f satisfies p, the input inp of f matched a constant in a case clause of a switch statement.

We check this by looking for guards on inp that collectively dominate all the return statements in f that can return true. This means that if f returns true, one of the guards must have been satisfied. (Similar reasoning is applied for statements returning false, nil or a non-nil value.)