2

我的最后一个问题（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;
}

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

4

1 回答 1

2

正如 Pascal 在他对您之前的问题的回答中提到的，Frama-C 的后向和前向切片基于称为值分析的分析结果。这种分析是非关系的；这意味着它只保留有关变量的数值范围的信息，而不是有关例如两个变量之间的差异的信息。因此，它无法跟踪您的不平等a >= b。if (a < b)这解释了为什么似乎遵循了测试的两个分支。

如果没有来自用户的更多信息（但是，在这个例子中，你可以写的任何东西都不会帮助价值分析），或者没有其他分析，反向切片必须考虑if可能会或可能不会被采用。不幸的是，这会导致程序中没有任何内容被切掉。

于 2013-07-15T21:42:16.427 回答