floating-point - 在 Frama-c wp 插件中对变量使用 sqrtf() 函数和负浮点值

Question

我正在尝试计算需要sqrtf()函数调用的特定函数的最弱前提条件。这是我的代码中的一段 -

void func(float err1_10, float err2_10){
float x1_00,......,x20_00;
float x1_10,......,x20_10;  
float x_mkfirm1,x_mkfirm2;  
float dist_00=0, dist_10=5, a00=0, a01=0, a10=-100, a11=0, b00=100,b10=0, u=2;
................................  
................................  
................................
x20_00=a00*x19_00+a01*x19_10+u*b00;  
x20_10=a10*x19_00+a11*x19_10+u*b10;  
x_mkfirm1=sqrtf((x20_00*x20_00)+(x20_10*x20_10));  
x_mkfirm2=sqrtf((x0_00*x0_00)+(x0_10*x0_10));  
//@ assert P: (x_mkfirm1/x_mkfirm2 >= 1) ;  
}     

我已经包括了“math.h”。每当我运行 wp 插件时，它都会 显示 - frama-c-in.c:3:[kernel] 警告：函数 sqrtf 的代码和规范都没有，从原型生成默认分配。它也没有为这个特定的断言生成最弱的前提条件。
此外，我正在尝试对变量使用负浮点值（-0.4007）。它向我显示以下错误：浮点常数 0.4007 未准确表示。