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（）被调用或不）。

这并不是说不能频繁猜测或可靠地知道，但不会有必要的情况，其中它不能。