小编roo*_*roo的帖子

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

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

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

如果我使用这个规范：

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

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

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

但是当使用这个规范时：

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