Information Technology Reference
In-Depth Information
N
Example
Key part of
Native
Early
Late
the precond.
Time
Paths
Time
Paths
Time Paths Precond. calls
1
Merge
∀i, t
i
≤ t
i
+1
3m32s 8718
117m43s 73644 4m8s 8142
31415
2 TriangMatrix
∀i ≥ j, M
ij
=0
—
38.6s
4893
27.5s 4093
557
3 PermutOrder
∀
i
=
j, p
i
=
p
j
17.9s
5153
23s
5179
23.2s 6071
2273
4 PermutOrder
∀i, ∃j, p
j
=
i
—
2m12s
14491
25s
6027
2266
Fig. 3.
Late precondition compared to native and early precondition treatment in P
AT H
C
RAWLER
precondition format of P
AT H
C
RAWLER
). The difficulty of treating any C function
p
is
that
p
can have several paths that may lead to an accepting
return
statement since a
C precondition may encode a complex logic formula with disjunctions. How to cover,
without repetitions, every program path in
f
by a test executing an accepting path in
p
?
Fig. 2 presents our
late-precondition method
. It consists in “exploring
p
after
f
”, that
is, searching, for each partial path
π
of
f
, a test accepted by
p
after
posting the path
constraints of
π
at
A
i
explore the paths of
f
in the same manner as the
classical DSE method, presented above, in Fig. 1, except that the test generation step
A
3
is replaced by another DSE-like exploration
A
2
.Thesteps
A
1
-
A
5
for the precondition
p
.Atthe
A
5
, the process keeps in the constraint store the constraints for
π
all the time
and adds those for the current partial path
ρ
in
p
when necessary. If
A
1
-
steps
A
3
finds a test
t
satisfying the precondition,
t
also satisfies the path constraints of
π
and the exploration
of
p
stops. Otherwise, the process explores all paths of
p
to check that no admissible
test executes the partial path
π
of
f
.
This method treats a C precondition in a completely automatic way and is available
online [8] (see e.g. example MergePrecond). It never considers again the same path of
f
. The “exploring
p
before
f
” approach cannot guarantee this property, so the same
path in
f
may be covered several times. In addition, our technique allows us to continue
to benefit from incremental constraint solving approach (where the constraints of the
same partial path
π
are never re-posted and re-solved again), one of the main forces of
the P
AT H
C
RAWLER
method.
4
Experimental Evaluation
Fig. 3 presents selected experiments of path test generation with P
AT H
C
RAWLER
for
some typical examples and compares our technique with a native precondition (when
it can be expressed so in P
AT H
C
RAWLER
) and with an early C precondition called
before (or in the beginning of) the function under test. The indicators include total test
generation time, the number of explored (covered and infeasible) paths and, for the late
treatment, number of calls to the precondition function (step
A
4
in Fig. 2). The third
column illustrates the form of the
essential part
of the precondition (shown in italic
below). Ex. 1 is a merge of two given
sorted arrays
t
,
t
into a third one. Ex. 2 checks
for a given
upper triangular matrix
M
if
M
2
=0. Ex. 3 and Ex. 4 contain the same
function computing the order of a given
permutation
p
, but this property is ensured in
different ways: we check that
p
:
{
0
,...,n
−
1
}→{
0
,...,n
−
1
}
is
injective
in Ex. 3
