使用 frama-c 切片答案

【问题标题】：Slicing using frama-c使用 frama-c 切片
【发布时间】：2017-01-20 10:36:47
【问题描述】：

我正在使用 frama-c 来做一些关于程序切片的实验。该工具很棒，并且有很多不同类型的切片（例如，按结果或按语句）。我正在使用如下程序数据结构：

typedef struct ComplexData {
    int x;
    int y;
    char string_[100];
    size_t n;
} ComplexData;

这只是一个示例，以便了解 frama-c 如何根据函数产生的结果对程序进行切片。基本上，main 方法调用一个返回ComplexData 类型值的函数。 如何进行不同执行之间的比较？结构的每个值都有一个检查？ 喜欢this？

【问题讨论】：

【解决方案1】：

Frama-C 的选项-slice-return f 指示切片器保留所有有助于计算f 的返回码的语句。对于您的类型ComplexData，这意味着任何字段的内容。任何计算的语句，例如y 或string_ 中的一个字符将被保留。

关于不同执行之间的比较，静态切片器实际上工作方式不同。它们在所有可能的执行中近似每个函数的行为。（在 Frama-C 的情况下，这是使用称为 abstract interpretation 的技术完成的。）因此，没有必要比较两次执行。

【讨论】：

非常感谢您的明确回复。我阅读的大多数文章都描述了动态切片，特别是它们试图比较不同执行的轨迹。那么，抽象解释可以只用于静态切片吗？最后，关于我读到的内容，轨迹存储在一个输出文件中，我只看到了基于数据原语（如整数）的标准。出于这个原因，我认为数据结构也有类似的比较。即使在这种情况下，需要比较每个字段。
对，我忘了动态切片。我相应地编辑了我的答案。抽象解释本质上是静态的，所以我认为它不能用于动态切片。
好的。你是对的。无论如何，当您必须比较复杂的数据结构时，它可能具有很大的优势。