了解 Frama-C 切片器结果

Question

我想知道是否可以使用 Frama-C 进行某种前向条件切片，并且我正在使用一些示例来了解如何实现这一目标。

\n\n

我有一个简单的例子，它似乎导致切片不精确，我不明白为什么。这是我想要切片的函数：

\n\n

int f(int a){\nint x;\nif(a == 0)\n    x = 0;\nelse if(a != 0)\n    x = 1;\nreturn x;\n}\n

\n\n

如果我使用这个规范：

\n\n

/*@ requires a == 0;\n  @ ensures \\old(a) == a;\n  @ ensures \\result == 0;\n*/\n

\n\n

然后 Frama-C 使用“f -slice-return”标准和 f 作为入口点返回以下切片（这是精确的）：

\n\n

/*@ ensures \\result \xe2\x89\xa1 0; */\nint f(void){\n  int x;\n  x = 0;\n  return x;\n}\n

\n\n

但是当使用这个规范时：

\n\n

/*@ requires a != 0;\n  @ ensures \\old(a) == a;\n  @ ensures \\result == 1;\n*/\n

\n\n

然后所有指令（和注释）保留（当我等待返回该切片时：

\n\n

/*@ ensures \\result \xe2\x89\xa1 1; */\nint f(void){\n  int x;\n  x = 1;\n return x;\n}\n

\n\n

）

\n\n

最后一种情况，切片是否不精确？在这种情况下，可能是什么原因造成的？

\n\n

问候，

\n\n

罗曼

\n\n

编辑：我写了“else if(a != 0) ...”，但问题仍然是“else ...”

\n

Answer 1

在 Frama-C 中，切片插件依赖于称为值分析的初步静态分析插件的结果。

\n\n\n\n

此值分析可以表示变量的值（在本例a中a == 0为值集{ 0 }），但很难表示a已知时的值a != 0。在后一种情况下，如果a尚不知道 是正值还是负值，则值分析插件需要近似 的值集a。如果a已知为正数，例如如果它是unsigned int，则非零值可以表示为区间，但值分析插件无法表示int除 0\xe2\x80\ 之外的 \xe2\x80 \x9call 类型的值x9d。

\n\n\n\n

如果你愿意改变前置条件，可以写成更容易被价值分析插件理解的形式（与价值分析选项一起-slevel）：

\n\n

$ cat t.c\n/*@ requires a < 0 || a > 0 ;\n  @ ensures \\old(a) == a;\n  @ ensures \\result == 0;\n*/\n\nint f(int a){\nint x;\nif(a == 0)\n    x = 0;\nelse if(a != 0)\n    x = 1;\nreturn x;\n}\n$ frama-c -slevel 10 t.c -main f -slice-return f -then-on 'Slicing export' -print \n\xe2\x80\xa6\n/* Generated by Frama-C */\n/*@ ensures \\result \xe2\x89\xa1 0; */\nint f(void)\n{\n  int x;\n  x = 1;\n  return x;\n}\n

\n