frama-c - 是否有可能在 Frama-C 中获得反向动态切片？

Question

我从 Frama-c 得到一个后向切片，但看起来它是一个静态切片而不是动态切片。

frama-c 中是否有特定选项来获得动态后向切片？

Answer 1

根据维基百科，

动态切片包含实际上影响程序特定执行的程序点处变量值的所有语句，而不是可能影响程序任意执行程序点处变量值的所有语句。

Frama-C 的切片插件以来自价值分析插件的值为条件，它相信代表在感兴趣的执行集中执行发生的所有值。为了配置 Frama-C 的切片插件进行动态切片，您只需要让值分析对应于单个执行即可。使用main没有输入、没有volatile变量、没有调用未知函数并传递选项-slevel 999999999的函数frama-c应该使值分析在您选择的程序的单次执行中表现为 C 解释器，如先前对另一个问题的回答中所述，这篇博文和这篇文章。