-
Notifications
You must be signed in to change notification settings - Fork 14
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Any plan to sync with KLEE 2.1 or merge to KLEE 2.1? #3
Comments
+1 the floating point support is important while this codebase is quite outdated now. |
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. |
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. |
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. |
Thanks for the excellent work.
Any plan to sync with KLEE 2.1 or merge to KLEE 2.1?
:)
The text was updated successfully, but these errors were encountered: