Hi,
We had the same issue in our tool Symbiotic (
https://github.com/staticafi/symbiotic/) that can use KLEE internally.
This is what we had to do to make it somehow work (apart from compiling the
program with -m32):
1) compile 32-bit libraries (
Hi,
I don't know any KLEE-specific or symbolic-execution-specific list, but you
may be interested in these benchmarks:
https://github.com/sosy-lab/sv-benchmarks/
>From my own experience a lot of them can be analyzed by KLEE.
Best Regards,
Marek
On Sun, Dec 4, 2016 at 11:56 PM, Sean Heelan
Hi list,
I have this small trivial program:
#include
int main(void)
{
int n;
klee_make_symbolic(, sizeof n, "n");
klee_assume(n < 0);
if (n/2 > 0)
assert(0);
return 0;
}
KLEE (on master from git) says that the assertion is violated, although
since n is negative, then n/2
Hi,
it looks like new ABI problem. LLVM is probably linked against the old C++
STL ABI and now you compile with new ABI (haven't you upgraded gcc to
5.1?). Check
https://gcc.gnu.org/onlinedocs/libstdc++/manual/using_dual_abi.html
Cheers,
Marek
On Tue, Nov 3, 2015 at 7:15 PM, Ren Kimura
And -c option to clang, so that it won't try to call linker.
On 21 January 2015 at 18:50, Dan Liew d...@su-root.co.uk wrote:
You're missing several things
* The -emit-llvm command line argument to clang (the most important
thing here, you're not trying to build a native binary here)
*
