If possible, you should use the klee-replay tool for tests generated using --posix-runtime. See http://klee.github.io/tutorials/testing-coreutils/ for an example.
Best, Cristian On 02/04/2015 18:25, Attila Török wrote: > Hello! > > I have encountered a problem while replaying klee tests using the > kleeRuntest library, and this is the only other reference I could find > to it: > https://keeda.stanford.edu/pipermail/klee-dev/2011-August/000727.html > Sadly even this went unanswered for years. > > What I found out is, the problem only occurs if I specify the > --posix-runtime option to klee upon testing, then the ktest file will > contain an extra 4 byte long object, named "model_version", which will > be the first in the list. > And it seems like the objects are not identified by their name (is that > solely for us, humans, to make it less confusing?), but only by the > order of their creation - I mean the order of calls to the > klee_make_symbolic function - and their index in the ktest file. Which > seems a bit strange to me. > > If I remove the --posix-runtime option, I get a few more undefined > reference warnings before the testing begins, but can't see any other > disadvantages. Still, the less warnings the better, right? > > Anyways, is there any way to make the error a bit more verbose, so the > cause of it can be a bit more easily found out, or maybe using the names > to identify the objects? Would that be a good idea? Or should I (or the > runtest library maybe) somehow be able to use up that extra 0. object > while replaying, making the rest of them match up in the list? > > Thanks, > Attila > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
