[klee-dev] How to preserve program variables?

[Daniel Liew]

> I am using klee-gcc to compile 'findutils', but I don't know why the
variables are all replaced with temp variables(such as %10),

Because LLVM intermediate representation uses single-static assignment form
(
http://en.wikipedia.org/wiki/Static_single_assignment_form  SSA)

> how can I generate the bytecode and reserve the program variables.

You cannot completely (running the reg2mem pass may help a little) because
LLVM uses SSA.

If you need to see what statement in your C code corresponds to an LLVM
instruction you can try this quickly by running KLEE with
-debug-print-instruction . Note this will slow down execution considerably.

Hope that helps.
-------------- next part --------------
HTML attachment scrubbed and removed