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

【问题标题】：How to trace a variable and slice all the code that it touches with Frama-C如何使用 Frama-C 跟踪变量并切片它接触的所有代码
【发布时间】：2021-10-05 15:02:38
【问题描述】：

是否可以使用 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，我可以获得预期的输出。但是有没有什么方法可以在不明确指定切片命令中的函数名的情况下获得相同的效果？

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

【问题讨论】：

标签： frama-c

【解决方案1】：

我不确定-slice-calls 是否正在做你想做的事。根据frama-c -slicing-help：

-slice-calls 选择对函数 f1,...,fn 及其所有效果的每个调用。

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

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

-slice-rd 选择对左值 v1,...,vn 的读取访问（地址在作为入口点的函数的开头进行评估）

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

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

【讨论】：