frama-c 切片插件似乎丢弃了使用的堆栈值

Question

问题描述

我正在开发一个 frama-c 插件，它使用切片插件作为库来删除自动生成的代码中未使用的位。不幸的是，切片插件丢弃了一堆实际使用的堆栈值。只要它们的地址包含在传递给抽象外部函数的结构中，就可以使用它们。

简单示例

这是一个更简单的示例，它模拟了与我相同的一般结构。

/* Abstract external function */
void some_function(int* ints[]);

int main() {
  int i;
  int *p = &i;
  int *a[] = { &p };
  some_function(a);
  return 0;
}

当使用frama-c-gui -slice-calls some_function experiment_slicing.c 对这个示例进行切片时（我还没有弄清楚如何在没有 gui 的情况下调用命令行时查看切片输出）它会删除除声明 int *a[]; 和对 some_function 的调用之外的所有内容。

尝试修复

我尝试通过添加 ACSL 注释来修复它。 但是，我认为合理的规范（见下文）不起作用

/*@ requires \valid(ints) && \valid(ints[0]);
 */
void some_function(int* ints[]);

然后我尝试使用具有所需行为的分配（见下文）。然而，这不是一个正确的规范，因为该函数实际上从未写入指针，而是需要读取它以获得正确的功能。我担心如果我继续使用这种不正确的规范，它会导致奇怪的问题。

/*@ requires \valid(ints) && \valid(ints[0]);
   assigns  *ints;
*/
void some_function(int* ints[]);

Answer 1

您在正确的轨道上：您应该在这里使用assigns 子句：它将指示内存状态的哪些部分与调用未定义函数有关。但是，您需要提供完整的 assigns 子句及其 \from 部分（指示读取哪个内存位置以计算写入的内存位置的新值）。

我在您的示例中添加了一个int 变量，因为您的函数没有返回结果（void 返回类型）。对于返回某些内容的函数，您还应该有一个子句assigns \result \from ...;：

int x;

/*@ assigns x \from indirect:ints[..], *(ints[..]); */
void some_function(int* ints[]);

int main() {
  int i;
  int*p = &i;
  int *a[] = { &p };
  some_function(a);
  return 0;
}

assigns 子句表示some_function 可能会更改x 的值，并且新值将根据存储在ints[..] 中的地址计算得出 （indirect 标签表明我们没有直接使用它们的值，这在Eva's manual 的第 8.2 节中有更详细的描述）及其内容。

使用frama-c -slice-calls some_function file.c -then-last -print（最后一个参数在这里用于在标准输出上打印结果文件：-then-last 表示以下选项应该对创建的最后一个 Frama-C 项目进行操作，在这种情况下，由切片，-print 打印该项目的 C 代码。您也可以使用-ocode output.c 将代码的漂亮打印重定向到output.c。）给出以下结果：

* Generated by Frama-C */
void some_function(int **ints);

void main(void)
{
  int i;
  int *p = & i;
  int *a[1] = {(int *)(& p)};
  some_function(a);
  return;
}

另外请注意，您的示例类型不正确：&p 是指向 int 指针的指针，因此应存储在 int** 数组中，而不是 int* 数组中。但我认为它仅源于减少您的原始示例，并且对于切片本身并不重要。