Information Technology Reference
In-Depth Information
A Late Treatment of C Precondition
in Dynamic Symbolic Execution Testing Tools
Mickael Delahaye
1
and Nikolai Kosmatov
2
1
Universite Grenoble Alpes, LIG, 38041 Grenoble, France
firstname.lastname@imag.fr
2
CEA, LIST, Software Reliability Laboratory, PC 174, 91191 Gif-sur-Yvette, France
firstname.lastname@cea.fr
Abstract.
This paper presents a novel technique for handling a precondition
in dynamic symbolic execution (DSE) testing tools. It delays precondition con-
straints until the end of the program path evaluation. This method allows Path-
Crawler, a DSE tool for C programs, to accept a precondition defined as a C func-
tion. It provides a convenient way to express a precondition even for developers
who are not familiar with specification formalisms. Our initial experiments show
that it is more efficient than early precondition treatment, and has a limited over-
head compared to a native treatment of a precondition directly expressed in con-
straints. It has also proven useful for combinations of static and dynamic analysis.
Keywords:
test input generation, dynamic symbolic execution, concolic testing,
executable preconditions.
1
Introduction
In software testing, the
precondition
of the program under test (often called
test context
)
specifies the admissible values of program inputs on which the program is supposed to
be executed and should be tested. This ability to select test input domains is essential to
test generation. Indeed, it allows concentrating the testing effort on admissible inputs of
the program. The most common use of the test precondition is to select inputs for which
the behavior of the program is specified. In that particular case, the test precondition
corresponds to the specification precondition. Other uses include testing outside the
specification to check for unwanted behaviors and partitioning the test domain.
In the case of automated test input generation tools, the precondition offers two inter-
esting challenges. First, one must encode the precondition in a formalism understood by
the tool. Second, the tool must take into account the precondition in its test generation
process to minimize rejects for test inputs outside the precondition.
P
AT H
C
RAWLER
[1] is a test input generation tool for C programs. It is based on
dynamic symbolic execution
(DSE), a technique that combines concrete execution and
symbolic execution of the program under test. Originally P
AT H
C
RAWLER
accepted a
precondition written in a declarative constraint-based formalism specific to the tool,
referred below as
native precondition
. But user feedback encouraged us to find an al-
ternative solution.
