Path-Aware Static Program Analyses for Specification Mining* - Mining Software Specifications: Methodologies and Applications - page 331

Parameter: If variables are supplied as arguments to the same param-
eter for a given procedure at different call-sites, their attributes can be
matched. Note, however, that while using positional parameter informa-
tion for the purposes of matching may be a useful heuristic, other vari-
ables that are not used as parameters, but nevertheless are significant
as preconditions, need to be detected as well (e.g., matching attribute
sets associated with ` in Figure 9.8).

Result: Variables that are assigned the return values of the same func-
tion can have their attribute sets matched.

Points-to set: If more attribute sets are present and are unmatched,
then pointer analysis is applied to group them.

By using these heuristics, we are able to prune down the number of possible
matchings significantly. Available algorithms easily scale to the sizes of the
pruned location sets.

9.2.6 Implementation

Source

CFG Generator Pointer Analysis

Annotated, acyclic control flow graphs

Intraprocedural analysis

Fixed−Point
Iteration

Interprocedural Analysis

Predicates User−defined

Confidence

Frequent
Itemset Miner

Sequence
Miner

Preconditions

FIGURE 9.9: Software architecture.

Our implementation (see Figure 9.9) takes as input the program source
and a user-defined confidence level for determining when a property should
form part of a precondition. We first generate the control-flow graph for each
procedure using an ecient program analysis tool [6]. The direction of all
edges in the control flow graph are reversed, since we are interested in con-
structing preconditions. Furthermore, all back edges in the control flow graph