Coverity的掃描 - 註釋或模型來分析某一點的可達性的節目

Question

考慮下面的程序：

int main(){ 
    float x = non_det_float(); 
    float y = NAN; 

    if (isnan(y) && x == 1.0f){ 
    some_error(); 
    } 
} 

讓non_det_float（）是它可以返回任何浮動的功能。 （這樣的非確定性浮動）

設some_error（）是終止該程序中的錯誤。

問題：

1. 是Coverity的掃描能夠分析some_error（）是否可達或不？或者簡單地說「some_error（）是死代碼」？

2. 是Coverity的掃描能夠模擬非確定性花車/雙打或甚至不確定性的循環？

如果這有可能，那將是很好的知道如何。 我們必須定義一個模型嗎？我們是否必須使用一些註釋？

在此先感謝。

Answer 1

這是（我認爲）相當於停機問題，並且因此是不可判定（即，總有定義爲它不能知道是否some_function（）被調用或不）。

這並不是說不能頻繁猜測或可靠地知道，但不會有必要的情況，其中它不能。