Hi, On 12 June 2017 at 13:12, Henrik Tjäder <[email protected]> wrote: > Hi, > > Reading (1) and quoting Dan Liew, > > "I'm aware of klee-fp. However I should warn you (so that you don't > waste time doing this) that I (and another research institution) have > already extended KLEE with floating point support using Z3. We intend > to open source our implementations in the very near future." > > I am curious about the state of this ongoing work, and if there are any > need for testers or such.
Just to note my fork of KLEE that supports floating point arithmetic is now open source [1]. You can build it is as normal but you * Have to build using CMake * You have to build with Z3 support and use that as the constraint solver. The intention is to eventually upstream this implementation along with the implementation of one of my collaborators [2]. It will be several months before this happens though. Have fun, Dan [1] https://github.com/srg-imperial/klee-float [2] https://github.com/danielschemmel/klee-z3float-aachen _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
