c - Frama-c，非确定性浮点值

Question

例如，我使用以下函数:

float nondet_float(){
  float x;
  return x;
}

int main(){
  float x = nondet_float();
  if(isnan(x)){
    some_error();
  }
}

我想知道如何使用 frama-c 来模拟非确定性 float 。

我想要的是，变量 x 被认为是任何可能的浮点值，包括 -inf、+inf 和 NaN。

如果 x 为 NaN，我希望得到 some_error() 可访问的结果。

所以我的问题是:

如何模拟非确定性 float ？如何测试某些函数调用的可达性？

Answer 1

Frama-C 是插件的集合，对无限/NaN 浮点值有不同程度的支持。我相信 WP 支持 NaN 和无穷大；但这可能取决于您选择的数字模型(选项 -wp-model)。

抽象解释插件(EVA，原Value)暂时不支持NaN和infinites。分析器假设(并证明)所有浮点值都是有限的。 Frama-C Sulfur 中将添加对非有限的支持。

此外，您的nondet_float 函数在任何情况下都是无效的。 C 标准禁止返回未初始化的值，并且此函数将被标记为不正确，例如伊娃。相反，您应该使用没有主体的函数，并使用子句 assigns\result\from\nothing 作为其规范。