Download Paper - STS

2 Introduction to Data Flow Analyses
2.2 Forward Data Flow Analysis
Picking up the example from the introduction, let us say we are interested in a data flow
analysis that tells us that after a certain statement, a variable cannot be zero for the
program to run error-free. For that analysis, we need to track variables that cannot be
zero after a statement.
To track the variable, we add it to our flow data, which is a set containing all the
variables that cannot be zero. These flow data are attached to the edges. The flow
data are calculated in each block and the result of that calculation is passed on using
the outgoing edges. To calculate the flow data, we need to check if Frama-C threw a
division-by-zero warning. In case there is a warning, we need to add the corresponding
variable to the flow data.
However, we also have to remove variables from the flow data. We want to know
if a variable cannot be zero. In case a variable is reassigned, we remove that variable
from the flow data if it was in the flow data. After a reassignment, the variable is again
allowed to be zero and we remove that variable. The variable is allowed to be zero until
we see a division-by-zero warning with that variable again. We go through the CFG from
the entry block to the possible exit blocks of the function. Such a data flow analysis is
called forward data flow analysis.
h = 1/x 1
{x 6= 0}
h = 1/x 2
{x 6= 0}
x=y
3
h = 1/x 4
{x 6= 0}
Figure 2.2: CFG with Warnings
For our analysis, we do not only need the CFG of the program but also the statements
that threw a division-by-zero warning and the affected variable. Figure 2.2 displays the
combination of the CFG and the attachment of warnings to statements. In the figure, we
have the CFG and on the right side of the blocks, coloured in orange, the division-by-zero
warnings of Frama-C that correspond to that block.
6