c - 使用 frama-c 切片

Question

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

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

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

score 2 · Accepted Answer

-slice-return fFrama-C的选项指示切片器保留所有有助于计算f. 对于您的 type ComplexData，这意味着任何字段的内容。任何计算 eg 的语句y或中的一个字符都string_将被保留。

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

1 回答 1