如何使用 Frama-C 跟踪变量并切片它接触的所有代码

Question

是否可以使用 Frama-C 跟踪一个变量并将它接触到的所有代码切片？例如考虑以下程序：

#include <stdio.h>

#define SIZE 512

int storage[SIZE];

void insert(int index, int val) {
    storage[index] = val;
}

int main(int argc, char *argv[]) {
    int x = 10;
    int y = 20;
    int z = 30;

    z = 0; /* some change to unrelated var */

    insert(x, y);

    return 0;
}

我对变量 x 的预期切片是：

#include <stdio.h>

#define SIZE 512

int storage[SIZE];

void insert(int index, int val) {
    storage[index] = val;
}

int main(int argc, char *argv[]) {
    int x = 10;
    int y = 20;

    insert(x, y);

    return 0;
}

我怎样才能做到这一点？到目前为止，我已经尝试关注 frama-c slice_issue.c -no-frama-c-stdlib -kernel-msg-key -slice-value x -then-on 'Slicing export' -print。它生成以下切片：

/* Generated by Frama-C */
int main(void)
{
  int __retres;
  int x = 10;
  __retres = 0;
  return __retres;
}

如果我在 slice 命令中提供 -slice-calls insert，我可以获得预期的输出。但是有没有办法在不在切片命令中明确指定函数名称的情况下获得相同的效果？

提前致谢。任何提示或对文档的指向将不胜感激。

Answer 1

我不确定 -slice-calls 是否按照您的要求行事。根据 frama-c -slicing-help:

-slice-calls <f1, ..., fn> select every calls to functions f1,...,fn, and all their effect.

换句话说，无论参数之一是否为 x，您都将对 insert 的任何调用添加到切片标准（例如，如果您将调用替换为 insert(z,y)，它也会被保留在切片中。

在我看来，您更喜欢 -slice-rd x。再次引用 frama-c -slicing-help:

-slice-rd <v1, ..., vn> select the read accesses to left-values v1,...,vn (addresses are evaluated at the beginning of the function given as entry point)

因此，insert(x,y); 被添加到切片标准中，因为有对 x 的读取访问权限，而不是因为它是对 insert（和 insert(z,y)按预期被丢弃）。

就是说，如果您真的想跟踪对所有函数的所有调用，就像许多将一组函数作为参数的选项一样，您可以使用 -slice-calls @all（参见第 3.3.3 节） Frama-C's user manual)

如何使用 Frama-C 跟踪变量并切片它接触的所有代码

How to trace a variable and slice all the code that it touches with Frama-C

frama-c