c - 使用 frama-c 进行切片

Question

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

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

这只是一个示例，用于理解frama-c如何通过函数产生的结果来分割程序。基本上，main 方法调用一个返回ComplexData 类型值的函数。 不同执行之间的比较是如何进行的？对结构体的每个值都有一个检查？比如this ？

Answer 1

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

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