Cristian Cadar

@zpzigi754 we would be happy to have support for uclibc-ng in KLEE. So if you would like to work on this, we would be happy to discuss and review your...

Hi @lipeng28, thanks again for your contribution. Can I ask you two things: (1) Could you split this into two different PRs, since the two changes are unrelated. (2) Can...

Looking at your logs, I can see that your code invokes `sin` and `cos` with a symbolic argument: ``` KLEE: WARNING ONCE: calling external: sin((FAbs w64 (ReadLSB w64 0 x)))...

@guaguagou yes. You would need to reconfigure it first to make sure the implementations for these functions are included. You should also make sure uclibc provides these functions, but I...

Unfortunately, we don't have any concrete plans, but I agree it would be nice to have this in mainline KLEE. Of course, if anyone would like to tackle this incrementally,...

Copying the core of my response on the mailing list, in case you'd like to continue the chat here: My main concern is that KLEE-Float changes the expression representation, which...

Don't you guys maintain a regression test suite?

Could it though? Maybe some simplified versions if the whole thing takes too long?