[klee-dev] Generate all solutions

Daniel Liew daniel.liew at imperial.ac.uk
Fri Sep 12 11:49:00 BST 2014


On 12 September 2014 03:54, Daniel Dunbar <daniel at zuster.org> wrote:
> One "hack" to do this is to simply loop over all of bytes of the symbolic
> variable, and test each bit in them (you probably can't let the optimizer
> run on this code though, as it will figure out what is happening and remove
> it).

Just as a small note for recent versions of LLVM/Clang you could
probably use the "optnone" attribute [1] on the function to prevent
the optimizer from modifying the "concretizeByte()" function.

[1] http://clang.llvm.org/docs/AttributeReference.html#optnone-clang-optnone




More information about the klee-dev mailing list