邮资-C，非确定性的浮点值

问题描述：

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

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

我不知道如何必须使用邮资-C，来模拟非确定性浮动。

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

我想得到some_error（）可达的结果，如果x是NaN。

所以我的问题是：

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

函数：'nondet_float（）'返回一个未初始化的局部变量的内容。结果是未定义的行为。建议重新思考，也许通过使用'srand（）'和'rand（）'来获得浮点值。 – user3629249

答

Frama-C是一个插件集合，具有对无限/ NaN浮点值的不同级别的支持。我相信WP支持NaN和infinites;但这可能取决于您选择的数字模型（选件-wp-model）。

对于抽象解释插件（EVA，以前的Value），NaN和infinites暂时不受支持。分析器假设（并证明）所有浮点值都是有限的。 Frama-C Sulphur将增加对非限制性的支持。

此外，您的nondet_float函数无论如何都是无效的。 C标准禁止返回未初始化的值，并且该函数将被标记为不正确。 EVA。相反，您应该使用一个没有正文的函数，其中第assigns \result \from \nothing作为其规范。

你能举个例子吗？我不太明白你的意思。 – Derping

答案的哪一部分。另外，你打算使用哪个插件？ – byako

一个例子：“相反，您应该使用一个没有body的函数，并且该子句将\ result \ from \ nothing作为它的规范。” 最好我需要一个插件，我可以证明/反驳一个特定的代码片段的可达性。对于我的例子，我想知道是否可以调用some_error（）。哪个WP和抽象解释都可以。还有Aorai，在我理解后执行Trace Abstraction。因为我需要NAN/INF的支持，所以我不能使用我猜的抽象解释，所以我必须使用WP/Aorai插件。 – Derping

邮资-C，非确定性的浮点值

相关推荐