Thanks for the explanation. I'll have a look at the suggestions below.
On 26-07-13 16:58, Eric Eide wrote:
"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.
-- Kees
