Expand description
Control flow analysis for the session type CFG.
Structs§
- Dnf
- A disjunction of conjunctions of constraints: true if any of the clauses contain constraints all of which are true.
- Flow
Analysis - The output of a flow analysis is two sets: the “passable” set, indicating which nodes have a
possible path “through” them to their continuation - and the “haltable” set, indicating which
nodes can possibly be run all the way to
Done. - Implication
- An implication in normal form: a set of preconditions which prove a consequence.
- Solver
- The current state of the flow analysis solver.
Enums§
- Constraint
- Flow analysis works by using a constraint solver: we try to solve for whether every node in the graph is “passable”, and in the process of doing so, we also solve “haltable” and “breaks from within some node or its children to some given parent loop node” constraints.
- Validity
- A result from breaking apart a DNF and attempting to determine whether it holds.
Functions§
- analyze
- Analyze a CFG for passability of every contained node.
Type Aliases§
- Conjunction
- A conjunction of constraints: true if all are true.