Any plan to sync with KLEE 2.1 or merge to KLEE 2.1?

[ghost]

Thanks for the excellent work.

Any plan to sync with KLEE 2.1 or merge to KLEE 2.1?

:)

[yxliang01]

+1 the floating point support is important while this codebase is quite outdated now.

[ccadar]

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, I'd be happy to discuss it. The main issue that requires more thought is the change to the expression representation done in KLEE-Float.

[qrort]

I would like to have FP exressions in KLEE. I have synced the klee-float with mainline here and am looking forward to discussing further changes needed to be done.

[ccadar]

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 has a significant impact on the core of KLEE. The question is whether it is possible to integrate the changes in such a way that the core of KLEE is minimally affected. This would require incremental changes and careful measurements.

I am also considering right now experimenting with supporting FP programs via fixed-point arithmetic, see the last project at https://klee.github.io/projects/.

My proposal would be to first submit your changes to this repository. There is still interest in this extension, but it's starting to show its age, as you can see in the open issues. In fact, even the Docker container is difficult to run these days, as Arch Linux changed its packaging format in the meantime.