我有一点 c 的 sn-p，看起来像这样：
double sum(double a, double b) {
return a+b; }
当我用 eva-wp 运行它时，我得到了错误：
non-finite double value. assert \is_finite(\add_double(a, b));
但是当我添加：
requires \is_finite(\add_double(a, b));
然后它的状态未知。
我觉得我犯了一个非常简单的错误，但我不知道它是什么！
【问题讨论】：
标签： frama-c
如果我们考虑file.c：
/*@ requires \is_finite(\add_double(a,b)); */
double sum(double a, double b) {
return a+b;
}
并使用frama-c -eva -main sum file.c 启动 Eva，我们确实有一个未知状态，并且警报仍然存在。事实上，这是两个不同的问题。
首先，当主入口点中有requires 子句时，Eva 会尝试根据它计算的通用初始状态对其进行评估，其中double 值可以是任何有限的double（甚至无限或 NaN，取决于内核选项 -warn-special-float 的值）。在这种通用状态下，requires 不成立，因此 Unknown 状态。
其次，Eva 无法利用 requires 子句将初始状态减少到属性持有的抽象状态：这需要在 a 和 b 之间保持某种关系，这不在 Eva 当前实现的抽象域的范围内。因此，分析是使用与没有requires 完全相同的抽象状态完成的，并导致相同的警报。
为了验证requires（并使警报消失），您可以使用包装函数，该函数将构建更合适的初始状态并调用分析中的函数，例如
#include <float.h>
#include "__fc_builtin.h"
/*@ requires \is_finite(\add_double(a,b)); */
double sum(double a, double b) {
return a+b;
}
void wrapper() {
double a = Frama_C_double_interval(-DBL_MAX/2, DBL_MAX/2);
double b = Frama_C_double_interval(-DBL_MAX/2, DBL_MAX/2);
double res = sum(a,b);
}
Frama_C_double_interval，在__fc_builtin.h 和$(frama-c -print-share-path)/libc 中声明，以及其他标量类型的类似函数，返回作为参数给出的边界之间的随机双精度数。因此，从 Eva 的角度来看，结果是在相应的区间内。通过启动frama-c -eva -main wrapper file.c，我们没有任何警报（requires 有效）。更一般地说，此类包装器通常是构建初始状态以使用 Eva 进行分析的最简单方法。
【讨论】：