Information Technology Reference
In-Depth Information
(
A
1
) init., set precond.,
π
:=
ε
Notation
f
C function under test
π
current partial path in
f
p
C function that checks if a test
t
satisfies the precondition of
f
ρ
current partial path in
p
ok
(
A
2
) symb. exec.
π
in
f
(
A
3
) generate test
t
fail
ok
fail
ok
(
A
5
) compute next
π
(
A
4
) execute
f
on
t
no more paths in
f
finish
Fig. 1.
Basic P
AT H
C
RAWLER
test generation method (with a native precondition)
(
A
1
) init.,
π
:=
ε
ok
(
A
2
) symb. exec.
π
in
f
(
A
1
)
ρ
:=
ε
ok
(
A
2
) symb. exec.
ρ
in
p
(
A
3
) generate test
t
fail
ok
fail
ok
fail
ok
p
is
false
on
t
A
5
) compute next
ρ
A
4
) execute
p
on
t
(
(
p
is true on
t
no more paths in
p
A
5
) compute next
π
A
4
) execute
f
on
t
(
(
no more paths in
f
finish
Fig. 2.
Our late-precondition method using a precondition defined in a separate C function
3
Late-Precondition Method
Usual Test Generation in P
AT H
C
RAWLER
In Fig. 1 we briefly present (following
[7, Sec.2.1]) the DSE-based test generation method for a C function
f
implemented
in P
AT H
C
RAWLER
.Step
A
1
creates a logical variable for each input of
f
and posts
the constraints for the precondition of
f
(given in an internal format). The depth-first
exploration of program paths (steps
A
2
symboli-
cally executes the current partial path
π
in
f
and posts corresponding path constraints,
solved at
A
2
-
A
5
) starts with the empty path
ε
.
A
3
in order to generate a test
t
activating a path starting with
π
.If
A
2
or
A
3
fails, i.e.,
π
is infeasible, then
A
5
continues directly to the next partial path in a
depth-first search. If a test
t
is found,
A
4
executes
f
on
t
and observes the complete
executed path and its results. Note that some solvers (e.g., Colibri the constraint solver
used in P
AT H
C
RAWLER
) support incremental constraint solving. That is why, if the
constraints are sent to the solver during the symbolic execution and if the solver detects
the infeasibility of a path at steps
A
2
-
A
3
, the process skips
A
4
and goes to
A
5
.
Late-Precondition Process.
Let us assume given the precondition of
f
defined by
a C function
p
, returning true (a non-zero value) when the inputs are admissible for
f
. One could suggest to filter inputs by
p
before exploring
f
. It can be done when
the precondition is a conjunction of elementary conditions (it is the case in the native
