Module MakeImplCommon::Cached

Provides predicates for calculating flow-through summaries.

If needed, call this predicate from DataFlowImplSpecific.qll in order to force a stage-dependency on the DataFlowImplCommon.qll stage and thereby collapsing the two stages.

Holds if data can flow in one local step from node1 to node2.

Holds if the set of viable implementations that can be called by call might be improved by knowing the call context.

Holds if data can flow from node1 to node2 via a direct assignment to c.

Gets a viable target for the lambda call call.

Gets a viable dispatch target of call in the context ctx. This is restricted to those calls for which a context might make a difference.

Holds if arg is a possible argument to p in call, taking virtual dispatch into account.

Holds if a value at return position pos can be returned to out via call, taking virtual dispatch into account.

A set of nodes that is unreachable in some call context.

A cached version of the CallContextSensitivity module. Only used in pruning stages 1+2 and flow exploration; all subsequent pruning stages use a pruned version, based on the relevant call edges from the previous stage.

An option type. This is either a singleton None or a Some wrapping the given type.