Marek Chalupa
Marek Chalupa
For KLEE, we can redirect the stdout/stderr during executing the external calls to new file descriptors (opened over /dev/stdnull for instance), so that they do not get mixed with the...
There's a problem with 32-bit vs 64-bit build of uclibc. AFAIK there's no way how to tell KLEE that it should use the bitcode with the right architecture.
Could you introduce me into the problem a bit? > This should be fixed in upstream KLEE as well. Is there already a related bug in upstream KLEE?
> However, writing to the padding is UB as opposed to reading. btw. I couldn't find where it is said that writing the padding bytes is UB. I only found...
Hmm, this is output from KLEE, so it is probably there. I'll take a look.
Yep, solving this should probably solve also #103 . We need to: - [ ] enable symbolic argv in `KLEE` (and other verification backends). KLEE allows only a bounded argv,...
Yes, I am able to reproduce this one. KLEE does not find any error not even on the original file without any optimizations and slicing, so the problem should be...
Interesting -- in this case the POSIX and man pages diverge. From man pages: ``` if size is equal to zero, and ptr is not NULL, then the call is...
It works without slicing, so the problem may be in the data dependence analysis.
Yep, the problem is that the slicer removes the call to `free` as it does not consider such a case witch comparing pointers could happen.