使用 frama-c 切片

Slicing using frama-c

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

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

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

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

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