[klee-dev] "ERROR: object sizes differ" when using --posix-runtime

[Attila Török]

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
-------------- next part --------------
HTML attachment scrubbed and removed