Coverity 扫描 - 用于分析程序中某个点的可达性的注释或模型

Question

给定以下程序:

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

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

设 non_det_float() 是一个可以返回任何 float 的函数。 (所以是一个不确定的 float )

设 some_error() 为终止程序的错误。

问题:

1. coverity scan 是否能够分析 some_error() 是否可达？或者只是说“some_error() 是死代码”？

2. 覆盖扫描是否能够模拟非确定性浮点/ double ，甚至非确定性循环？

如果这一切都是可能的，那么很高兴知道如何实现。 我们必须定义一个模型吗？我们必须使用一些注释吗？

提前致谢。

Answer 1

这(我认为)相当于停止问题，因此是不可判定的(即，总是存在无法知道 some_function() 是否被调用的定义)。

这并不是说它不能经常猜测或可靠地知道，但必然存在它不能猜测或知道的情况。