Consider the program
i = 0; while (i < 10) { if (i > 1) i = i + 3; else i = i + 2; }
A possible corresponding control-flow graph is:
Suppose that
Compute the set of states at each vertex in CFG
For each program point we associate a set of states , , …, .
One way to describe the set of state: for each initial state, run the CFG with this state and insert the modified states at appropriate points.
If is the label on the edge of the graph, let denote the relation between initial and final state that describes the meaning of statement. For example,
We will write for the image of set under relation . For example,
Note that that if [p] is a condition (as generated by 'if' and 'while') then
If an edge has no label, we denote it skip. So, .
Now, we can describe the meaning of our program using recursive equations:
Note that the solution we computed satisfies the recursive equations. In fact, our solution is the unique least solution of these equations.
The problem with these exact equations is that they are as difficult to compute as running the program on all possible input states. Instead, when we do data-flow analysis, as with type systems, we will consider approximate descriptions of these sets of states.