> 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. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
