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

Question

我想探索Frama-C应用基于断言的切片（使用ACSL符号）。 我发现有几个不同版本的Frama-C具有一些不同的功能。 我的问题是哪个版本最适合为Frama-C开发切片插件，以及如何操作由Frama-C创建的AST。

Answer 1

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

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

所以，这取决于你所说的“基于断言的切片”是什么（要意识到，在谷歌首次出现的文章是付费墙），你打算做的可能是已经存在一个邮资-C塞什么-in（以及最后两个或三个Frama-C版本运行良好的一个）。

无论如何要回答你的问题，使用最好的版本是最新的版本，这是氟本文20130601。

---

现有的切片功能实例邮资-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;,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); 
}