Frama-C：使用指针时获取函数输出

Question

我需要获取函数所有输出的列表。当我在以下代码中使用 From-插件时

void add(int *sum, int a, int b)
{
    *sum = a + b;
}

int main()
{
    int result;
    add(&result, 1, 2);
}

它告诉我 result 是 add 函数的输出。这当然是正确的，但我希望插件在某处提到 sum 。我知道 sum 是一个指针，在函数中没有被修改，所以它不是输出，但是 *sum 被修改了，我想知道.有没有一种简单的（或任何）方法可以实现这一目标？

Answer 1

如果您将 add 设置为您的主要入口点，您可能能够检索到您想要的信息：

$ frama-c -main add -deps file.c
[...]
[from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
[from] Function add:
  S_sum[0] FROM sum; a; b

基本上，S_sum[0] 是 *sum：Value（From 依赖）生成一个初始状态，其中指针是 NULL 或指向到一个名称类似于指针之一的块，并且默认情况下具有两个元素。有一些命令行选项可以调整默认行为（有关更多信息，请参阅 Value Analysis manual），但您可能会发现，对于更复杂的示例，您需要编写（或生成）一个包装函数来设置调用函数之前更复杂的初始状态。在这种情况下，您必须跟踪哪个指针指向何处才能重建信息。

大部分问题是在 Value 的抽象状态下，sum 映射到一组 L 可能的位置（此处简化为单例），但是*sum 本身不是对象。写访问将简单地更新映射到 L 元素的所有值。因此，从 From 的角度来看，一切看起来都像是对 result 的修改（如果更改入口点，则为 S_sum[0]）。

Frama-C：使用指针时获取函数输出

Frama-C: Getting function outputs when using pointers

c

frama-c