Why IR is needed for symbolic execution?

Question

For example, KLEE works on LLVM bitcode.

Can we build symbolic execution directly on C source code?

Answer 1

Each LLVM IR contains only one simple operation, but one C statement could contains multiple operations. For example, a[i] = b[i]; could be split into:

addr = b + i; // getElementPtr instruction
tmp = *addr; // load instruction
addr1 = a + i; // getElementPtr instruction
*addr1 = tmp; // store instruction

So it's much more simple to process LLVM IR than source code for a symbolic executor.