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

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>