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
