Instantiation of the DF Architecture
Control Flow Graph
- control graph is extracted from class definition
Lattice formalizing the class of “facts” computed by the analysis
- type information for each stack element and local variable
- signature and subtype assertions
Transfer functions mapping lattice values to lattice values describing the semantics of the program constructs w.r.t. the abstract domain
- Captures the type transformation of each instruction. Depends on the instruction’s op code and optionally its operand.
Initial map of a lattice values to control flow nodes
- reflects method initialization
- method is initiated with the stack empty
- and actual parameters in local variables
- threaded global typing context, augmented with class’ symbol table entries