slice - Which Frama-C version is best suited to develop a slicing plugin?

Question

I want to explore Frama-C to apply Assertion-based Slicing (using ACSL notation). I have found that there are several different versions of Frama-C with some different features. My question is which version is best suited to develop a a slicing plugin to Frama-C and to manipulate the AST created by Frama-C.

Answer 1

Frama-C 中已经有一个切片插件（所有版本）。

此插件使用值分析插件的结果，该插件假定写入在 ACSL 断言中的属性（在尝试验证它们之后）。

因此，根据您所说的“基于断言的切片”（并注意首先出现在 Google 中的文章是在付费墙后面），您打算做的可能已经作为 Frama-C 插件存在（并且一个在最后两个或三个 Frama-C 版本中运行良好的版本）。

无论如何，要回答您的问题，最好使用最新版本，即撰写本文时的 Fluorine 20130601。

---

Frama-C 中现有的切片功能示例：

$ cat t.c
int f(unsigned int x)
{
  int y;
  /*@ assert x == 0 ; */
  if (x)
    y = 9;
  else
    y = 10;
  return y;
}

$ frama-c -sparecode t.c -main f 
...
t.c:4:[value] Assertion got status unknown.
...
/* Generated by Frama-C */
int f(unsigned int x)
{
  int y;
  /*@ assert x ≡ 0; */
  ;
  y = 10;
  return (y);
}

当您谈到“基于断言的切片”时，以上是您所想到的吗？

注意：Frama-C 的选项-sparecode是标准“保留程序的所有结果”的切片选项。它仍然会删除任何没有后果的陈述，例如y=3;in y=3; y=4;，并且基于 Frama-C 的价值分析，它会删除由于价值分析的结果而被认为无法到达或没有后果的任何陈述。

另一个例子来说明：

$ cat t.c
int f(unsigned int x)
{
  int y;
  int a, b;
  int *p[2] = {&a, &b};
  /*@ assert x == 0 ; */  
  a = 100;
  b = 200;
  if (x)
    y = 9;
  else
    y = 10;
  return y + *(p[x]);
}

$ frama-c -sparecode t.c -main f 
...
t.c:6:[value] Assertion got status unknown.
...
/* Generated by Frama-C */
int f(unsigned int x)
{
  int __retres;
  int y;
  int a;
  int *p[2];
  p[0] = & a;
  /*@ assert x ≡ 0; */
  ;
  a = 100;
  y = 10;
  __retres = y + *(p[x]);
  return (__retres);
}