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