On Tue, Dec 07, 2010 at 10:22:54AM -0500, Denver Gingerich wrote: > I'd like to use KLEE-FP to generate test cases for various floating > point inputs, similar to what is done for integers in Tutorial One > (http://klee.llvm.org/Tutorial-1.html). However, it seems like this > might be outside of the cross checking scope of the current KLEE-FP. > Is the test generation I described possible with KLEE-FP? If not, is > it something that is easy and/or likely to be implemented?
Hi Denver, KLEE-FP uses a constraint solver (currently STP) to generate test cases, so this isn't possible at the moment. Given a constraint solver with an FP theory this would be easy - hopefully one will be released soon. For more information see here: http://www.cprover.org/SMT-LIB-Float/ Thanks, -- Peter
