David Alexander Molnar and David Wagner

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2007-23

February 4, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.pdf

We propose an approach that combines symbolic execution and run-time type inference from a sample program run to generate test cases, and we apply our approach to signed/unsigned conversion errors in programs. A signed/unsigned conversion error occurs when a program makes control flow decisions about a value based on treating it as a signed integer, but then later converts the value to an unsigned integer in a way that breaks the program's implicit assumptions. Our tool follows the approach of Larson and Austin in using an example input to pick a program path for analysis, and we use symbolic execution to attempt synthesis of a program input exhibiting an error. We describe a proof of concept implementation that uses the Valgrind binary analysis framework and the STP decision procedure, and we report on preliminary experiences. Our implementation is available at http://www.sf.net/projects/catchconv .

---

BibTeX citation:

@techreport{Molnar:EECS-2007-23,
    Author= {Molnar, David Alexander and Wagner, David},
    Title= {Catchconv: Symbolic execution and run-time type inference for integer conversion errors},
    Year= {2007},
    Month= {Feb},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.html},
    Number= {UCB/EECS-2007-23},
    Abstract= {We propose an approach that combines symbolic execution and run-time type inference from a sample program run to generate test cases, and we apply our approach to signed/unsigned conversion errors in programs. A signed/unsigned conversion error occurs when a program makes control flow decisions about a value based on treating it as a signed integer, but then later converts the value to an unsigned integer in a way that breaks the program's implicit assumptions. Our tool follows the approach of Larson and Austin in using an example input to pick a program path for analysis, and we use symbolic
execution to attempt synthesis of a program input exhibiting an error. We describe a proof of concept implementation that uses the Valgrind binary analysis framework and the STP decision procedure, and we report on preliminary experiences. Our implementation is available at http://www.sf.net/projects/catchconv .},
}

EndNote citation:

%0 Report
%A Molnar, David Alexander 
%A Wagner, David 
%T Catchconv: Symbolic execution and run-time type inference for integer conversion errors
%I EECS Department, University of California, Berkeley
%D 2007
%8 February 4
%@ UCB/EECS-2007-23
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-23.html
%F Molnar:EECS-2007-23