Correct Handling of Floating-Point Computations in Symbolic Execution

Bernard Botella 1 Arnaud Gotlieb 2 Claude Michel 3
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Symbolic execution is a program testing technique which evaluates statements with symbolic input data along a selected path of the control flow graph. The process involves the computation of path conditions that tend to be simplified or solved in order either to get test data that sensitize the selected path or to demonstrate infeasibility of the path. In the presence of floating-point computations, the current strategy consists in using a constraint solver based on rationals or reals. Unfortunately, even when the computations conform ANSI/IEEE-754 floating-point arithmetic, this leads not only to approximative results but also to incorrect ones. For example, a path can be labeled as infeasible by using a constraint solver on the rationals although there exist floating-point input data that sensitize it. This paper shows how to evaluate symbolically the expressions when floating-point variables are involved in the computations. The focus is on the design and the implementation of projection functions required to solve path conditions over the floats. The proposed approach handles not only the numeric values of floating-point variables but also the symbolic values, such as infinities and NaNs. A symbolic execution environment of C floating-point computations is currently under development. Some very first experimental results are reported.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00071433
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 5:32:21 PM
Last modification on : Friday, November 16, 2018 - 1:22:18 AM
Long-term archiving on : Sunday, April 4, 2010 - 10:13:31 PM

Identifiers

  • HAL Id : inria-00071433, version 1

Citation

Bernard Botella, Arnaud Gotlieb, Claude Michel. Correct Handling of Floating-Point Computations in Symbolic Execution. [Research Report] RR-5150, INRIA. 2004. ⟨inria-00071433⟩

Share

Metrics

Record views

207

Files downloads

133