我如何判断 KLEE 指令中涉及的变量是符号的还是具体的

Question

我想知道当KLEE执行涉及变量的指令时，是否有办法判断变量在KLEE中是否是符号的。

Answer 1

有一个用于此目的的 API。

/* Return true if the given value is symbolic (represented by an
* expression) in the current state. This is primarily for debugging
* and writing tests but can also be used to enable prints in replay
* mode.
*/
unsigned klee_is_symbolic(uintptr_t n);