"Kees" == Kees Bakker <[email protected]> writes:
Kees> Does anyone have suggestions how to avoid reduction that
Kees> reads/writes outside an array.
To reject these types of reduced programs, your predicate script needs to
reject programs that have undefined behavior. Our paper about C-Reduce
discusses the problem:
http://www.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf
(Section 5, "Test-Case Validity.")
In the paper, we used two tools, KCC and Frama-C, to find and reject reduced
programs that have undefined behavior. The C-Reduce distribution contains some
simple examples of their use, in the `tests' directory.
Since we wrote the paper, Clang has incorporated "sanitizer" tools that can
also help to weed out such programs. These include:
clang -fsanitize=address
clang -fsanitize=undefined
For more about these, check out:
http://clang.llvm.org/docs/UsersManual.html
http://clang.llvm.org/docs/AddressSanitizer.html
I recommend that you apply clang-based sanitizers first, because they are
faster than KCC and Frama-C. If clang truns out not to be sufficient for your
needs, try Frama-C.
Kees> (( BTW I'm not sure if this is a creduce bug. ))
We don't consider the generation of programs with undefined behaviors to be a
bug in C-Reduce. For example, if you are tracking down a compiler-crash bug,
you may not care if the test program has undefined behavior or not. "What you
care about" is specified by the predicate script.
C-Reduce is general; it is the job of the predicate script to guide the search
that C-Reduce drives.
Good luck! ---
Eric.
--
-------------------------------------------------------------------------------
Eric Eide <[email protected]> . University of Utah School of Computing
http://www.cs.utah.edu/~eeide/ . +1 (801) 585-5512 voice, +1 (801) 581-5843 FAX
