Hey Suresh, I'm not sure that what you are looking for exists. Klee is designed to test programs and create test suites. It will find assertion violations and other common errors. If you're looking to verify that a particular path through the program is semantically correct, however, you're going to have to find some type of specification for each program. From that point, you could use the inputs/ouputs generated by Klee to make sure they all match the specifications. As I said, however, I don't know where you will be able to find any formal specifications for core-utils.
The only option I can think of is to use some competing implementation of the core-utils and verify that they each produce the same outputs given the same inputs. Hope that helps, Eric Rizzi ________________________________ From: [email protected] <[email protected]> on behalf of suresh_khatiwada <[email protected]> Sent: Saturday, May 30, 2015 5:43 AM To: [email protected] Subject: [klee-dev] About KLEE How can we plan to construct oracles while testing Coreutils using KLEE? Sent on the go with Vodafone
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
