klee - 可以将函数调用的返回值设为符号以绕过执行该函数吗？

Question

我想避免进行程序间符号执行。也许有一个没有任何约束的返回值，并且可能解析为任何可能的具体值。

这样的事情甚至可能吗？

我想这样做的原因是我想避免执行某些具有非常大循环并且不真正修改全局数据的函数。

标签： klee

Answer 1

如果可以操作源代码，则可以将这些函数调用替换为make_symbolic函数，在该函数中，您基本上创建了一个新的符号变量并将其作为原始函数调用的返回值返回。或者你可以重写这些函数来返回一个新的符号值。