Timotej Kapus
Timotej Kapus
Wouldn't this be better as a ktest tool option, similar to the binary output one?
What about some sort of usage like this `klee -test-gen-callback="ktest-tool --to-xml"`, where klee calls the `system("ktest-tool --to-xml" + test_caste)`. I guess the only annoying thing is that this would need...
Note that this can still hapen when `llvm.memcpy` intrinsic (which doesn't get dbg info), gets lowered to `memcpy`
Here is a small example: ```C typedef struct _DDSVector3 { float x, y, z; } DDSVector3; static inline void VectorSubtract3(const DDSVector3 left, const DDSVector3 right, DDSVector3 *destination) { destination->x =...
Well the problem here is debug information, so if you strip it, it will work ofcourse. The problem is that you lose the debug information. That means that if you...
It still prints stuff like "potential NULL pointer derefernce", but doesn't tell you: "at myprogram.c:12". The actuall symbolic execution is not impacted as you say.
My workaround patch for this is just to add some random debug info to these calls. I guess the challenge is to find the "right" debug info to attach.
I guess this is an LLVM issue, that LLVM project doesn't have, so I doubt they will fix it. I guess in clang something deals with these memcpy intrinsics before...
I've checked this with sqlite and a seed and it works, so this implementation looks ok. I don't think this can be a CI test, but I want to document...
I've also now put ZESTI searcher on top of it. This is functionally everything I wanted to upstream.