2

问题描述

我正在开发一个 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[]);
4

1 回答 1

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 手册的第 8.2 节中有更详细的描述） ，以及它们的内容。

using 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*数组中。但我认为它只是源于减少你原来的例子，对于切片本身并不重要。

于 2020-05-05T11:37:44.933 回答