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

正如Pascal在他的answer to your previous question中提到的，Frama-C的向後和向前切片基於名爲「值分析」的分析結果。這種分析是非關係的;這意味着它只保留關於變量數值範圍的信息，但不包含例如兩個變量之間的差異。因此，它不能跟蹤你的不平等a >= b。這解釋了爲什麼測試if (a < b)的兩個分支似乎都遵循了。

如果沒有來自用戶的更多信息（但在本例中，您可以編寫的內容都不會幫助進行價值分析）或其他分析，則反向分片必須考慮可能或不可以採用if。這不幸的結果是一個程序中沒有任何東西被切掉。