哪个Frama-C版本最适合开发切片插件？

Question

我想探索Frama-C以应用基于断言的切片(使用ACSL表示法).我发现有几种不同版本的Frama-C具有一些不同的功能.我的问题是哪个版本最适合为Frama-C开发一个切片插件并操纵Frama-C创建的AST.

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);
}