在Frama-C中有可能获得向后动态切片吗？

Question

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

在frama-c中有一个特定的选项来获得一个动态的向后切片吗？

Answer 1

根据Wikipedia的说法，

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

Frama-C的切片插件以值分析插件的值为条件，它采用值分析插件来表示一组感兴趣的执行中发生的所有值。为了将Frama-C的切片插件配置为动态切片，只需将值分析对应于一次执行即可。使用没有输入的main函数，没有volatile变量，没有对未知函数的调用，并将选项-slevel 999999999传递给frama-c，应该会使值分析在您选择的程序的单次执行过程中表现为C解释器，如this previous answer to another question、this blog post和this article中所述。