Hi Aleksei,
From what I understand, you managed to rebase the KLEE-Float extension
on top of KLEE's mainline. That's great!
As I mentioned on GitHub, 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 the KLEE-Float
project at https://github.com/srg-imperial/klee-float. There is still
interest in that 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.
Best,
Cristian
On 22/11/2020 21:08, Aleksei Pleshakov wrote:
I currently have the https://github.com/srg-imperial/klee-float
<https://t.co/iq6VMQHLS7?amp=1>patch along with some FP intrinsics
supported here: https://github.com/qrort/klee
<https://t.co/EbHLzazVQf?amp=1>. You have mentioned that you'd be happy
to discuss the possibilities of this to be merged in mainline KLEE in
this issue <https://github.com/srg-imperial/klee-float/issues/3>. I am
willing to take the work that needs to be done. Can we discuss it? :)
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
