[klee-dev] Fwd:

[Daniel Liew]

> Is it that because incorrected way to generate *.bc using wllvm and extract
> script?

wllvm is a bit of hack. The ``lli`` tool probably seems to expect
various instructions to be removed because it can be JIT'ed. You can
try passing -force-interpreter=true to lli to see if you progress
further by avoiding the JIT.

You could try running

$ opt -verify php.bc
$ opt -lint php.bc

To see try and see if any obvious problems can be found on the bitcode
wllvm produced.

This probably won't help but you could also try running this on php.bc

$ opt -internalise-public-api-list=main -internalize -globaldce php.bc
-o php.opt.bc

to get a new bitcode module (php.opt.bc) which will have dead code
stripped out of it. WLLVM doesn't use a proper linker so php.bc will
probably have A LOT of dead code

Hope that helps.

Thanks,
Dan.