Static API Specification Mining: Exploiting Source Code Model Checking - Mining Software Specifications: Methodologies and Applications - page 140

however, does not show normal paths or traces for simplicity). Our adaptation
generates multiple-API specifications by applying sequence mining on normal
traces.
Verification. Our static verifier uses the mined specifications (error-
check and multiple-API specifications) to detect violations (error-check and
multiple-API violations) in the source code. Next, we present the various com-
ponents of our adaptation in detail.

5.3.2 Adaptation { The Details
The algorithm presented in Figure 5.19 shows the details of our adap-
tations. There are 3 stages and 10 steps (numbered 1-10) in our algorithm.
Section 5.3.2.1 describes the error/normal trace generation stage (Steps 1-6).
Section 5.3.2.2 (Steps 7-8) explains the steps involved in mining API error-
handling specifications from the static traces. Finally, Section 5.3.2.3 describes
the verification stage for detecting API error-handling violations from the
mined specifications (Steps 9-10).

5.3.2.1 Error/Normal Trace Generation

In this section, we explain how we adapt the trace generation technique
for generating API error and normal traces from source code. As shown in
Figure 5.19, the error/normal trace generation stage has six steps: generate
error traces (Step 1), process error traces (Steps 2-4), identify critical APIs
and probable clean up APIs from error traces (Step 5), and finally, generate
normal traces (Step 6). The various steps are explained next.
Step 1 - Generate error traces. An error trace starts from the begin-
ning of the main procedure and ends in some API error-block with an exit
call (causing the program to exit) or a return call (causing the enclosing pro-
cedure to return). The trigger FSM, sayF(Step 1, Figure 5.19), is used by
our trace generator (procedure TG in the figure) to generate error traces from
the program source code (P). The procedure TG represents our trace genera-
tion technique, which adapts the push-down model checking (PDMC) process.
Transitions retValChk and errnoChk in the triggerF(from State 2 to State 3 )
identify the return-value check and error-flag check, respectively, for the API.
Transitions from State 3 to the final state (State end ) in the triggerFcapture
code blocks following the retValChk or errnoChk in which the program exits
or the enclosing procedure returns. The procedure TG generates all traces in P
that satisfy the triggerF. However, the procedure getShortest (Step 1, Fig-
ure 5.19) returns only the shortest trace from the set of all traces generated
by TG . As we are interested only in the API-error check and the set of prob-
able clean up APIs (PC) in the API error-block for a given API from error
traces, the program statements prior to the API invocation are not needed.
Hence, it suces to generate the shortest path for each API invocation with
a following retValChk or errnoChk . In case there are multiple retValChk or