Here are the software tools that Eric Eide and John Regehr developed during the research described in their EMSOFT 2008 paper.
If you have questions or comments about this software, please feel free to contact Eric or John.
randprog is a random generator of C programs that use volatile variables. The generated programs are “closed,” meaning that their behavior does not depend on external inputs or timing. They are also “nearly strictly conforming,” meaning that their behaviors are well-defined by the C language standard, with a few deliberately chosen exceptions.
Within these limits, the goal of randprog is to generate random programs with a wide range of behaviors and characteristics. This makes randprog useful for finding bugs in the ways that C compilers treat volatile variables. Read the paper for more details.
randprog is free software, distributed under a BSD-style license.
volcheck is a binary instrumentation tool, based on Valgrind, for monitoring the memory behavior of programs. In particular, it is useful for observing the behaviors of the executables that C compilers create from the program sources generated by randprog.
The Valgrind platform manages the instrumentation and execution of the test program that is being examined. As new parts of the (binary) program are reached during execution, Valgrind invokes volcheck to instrument the binary code. The instrumentation that volcheck inserts causes information about each memory access to be printed to stdout as the accesses occur. When the test program terminates, volcheck outputs a summary of all the memory accesses that the test program performed.
We distribute volcheck within a copy of Valgrind. Both are free software, distributed under the GNU General Public License.
We will make other parts of our testing framework, including the automated testing infrastructure, available from this Web page in the future. Please contact Eric Eide and John Regehr if you have any questions.
|Eric Eide <email@example.com>||Last modified: Wed May 6 13:08:30 MDT 2009|