Coverity scan - 注释或模型来分析程序中某个点的可达性

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. 覆盖扫描是否能够分析 some_error() 是否可达？或者简单地说“some_error() 是死代码”？

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

如果有任何可能的话，很高兴知道如何做。 我们必须定义一个模型吗？我们必须使用一些注释吗？

提前致谢。

Answer 1

这（我认为）等同于停止问题，因此无法确定（即，始终存在无法知道 some_function() 是否被调用的定义）。

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