I have a question about how Klee goes about creating test cases at the end of its run. It seems that it goes through the cexPreferences that are associated with each MemoryObject, adding on as many as it possibly can. (as seen in lib/Core/Executor.cpp::getSymbolicSolution())
In many cases, however, it seems that not all of these additional constraints can be added to the state. I assume this because when I just stick on all of the cexPreferences to the state and call getInitialValues(), I get a lot of errors in the test suite. My Questions are: 1) Where do the constraints in cexPrefences come from when Klee simulates running a command line program? Are there different types of constraints on command line arguments and input files? 2) What does not fully applying all of the constraints in cexPreferences mean about the testcase that is created? Is it not fully representative of the path that was actually taken through the program or is their a possibility of two tests traversing equivalent paths? 3) What does it mean about a state when a constraint in cexPreferences can't be applied? (i.e. solver->mustBeTrue(tmp, Expr::createIsZero(*pi), mustBeTrue == false); 3) Are paths leading to states where all the constraints in cexPreferences aren't possible traversing impossible paths? 4) Why are the constraints stored in the cexPreferences not simply added in the beginning of the run so that unused information isn't calculated? Sorry for the multitude of questions and thanks, Eric Rizzi
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
