slice - Frama-C 中的条件切片

Question

我的最后一个问题( Understanding Frama-C slicer results )是一个精确的例子，但正如我所说，我的目标是知道是否可以使用 Frama-C 进行一些条件切片(向前和向后)。可能吗？

更准确地说，我无法获得该程序的精确部分:

/*@ requires a >= b;

  @ assigns \nothing;

  @ ensures \result == a;
*/
int example4_instr1(int a, int b){
    int max = a;
    if(a < b)
        max = b;
    return max;
}

通过使用好的参数/选项，是否有可能在这种情况/一般情况下得到我想要的东西？

Answer 1

正如帕斯卡在他的 answer to your previous question 中提到的那样，Frama-C 的向后和向前切片基于称为值(value)分析的分析结果。这种分析是非关系性的；这意味着它只保留有关变量数值范围的信息，而不保留有关例如两个变量之间的差异。因此，它无法跟踪您的不平等a >= b 。这解释了为什么测试的两个分支 if (a < b)似乎已被关注。

如果没有来自用户的更多信息(但是，在本示例中，您可以编写的任何内容都无法帮助值(value)分析)或其他分析，则向后切片必须考虑 if可能会或可能不会被采取。不幸的是，这会导致程序中没有任何内容被删除。