Polyspace Code Prover (R2014b) - Float32 Overflow due to static local variables

Hello,

I have the following code function. When I check the code with Polyspace Code Prover (R2014b), I get an "orange" Overflow in the formula (*1) due to the static local variable "X_Sa2_LPF_UnitDelay" that is assumed with the full float32 range (-3.4029E+38 .. 3.4029E+38). But by the algorithem (low-pass-filter) the variable value can not larger as the Value of input "Sa1_InRaw". The Input "Sa1_InRaw" is limited by DRS to +/-50. "Sa1_Constant" is a constant with a also fixed range.

Can I limit static local variables in the configuration? Can I avoid this overflow by any other option?

float Sa1_InRaw;
float Sa1_OutFilt;

const float Sa1_Constant = 0.3F;

void Sa3_LPF1(void) {

float Sa2_LPF_Add;
static float X_Sa2_LPF_UnitDelay = 0.F;

Sa2_LPF_Add = ((Sa1_InRaw - X_Sa2_LPF_UnitDelay) * Sa1_Constant) + X_Sa2_LPF_UnitDelay; //(*1)
X_Sa2_LPF_UnitDelay = Sa2_LPF_Add;

Sa1_OutFilt = Sa2_LPF_Add;
}

Thanks in advance! Best Regards, Thomas

Answer 1

[Alexandre De Barros]

Hello Thomas,

I've tried your code snippet with the version R2016b and everything is green (and X_Sa2_LPF_UnitDelay is not full-range).

Could you try with this version R2016b or R2017a, the last version?

If it's still orange, please contact the technical support, and attach the verification log to your request.

Best regards,

Alex

Answer 2

[t.katemann]

Hello Alexandre,

thanks for the quick answer. Now I have tried to check the code snippet with Version R2016b, but I get the same orange overflow in the formula at the plus-sign.

Sa2_LPF_Add = ((Sa1_InRaw - X_Sa2_LPF_UnitDelay) * Sa1_Constant) + X_Sa2_LPF_UnitDelay;

I tried it only with the Default configuration of Polyspace, except of I set in DRS Sa1_InRaw = -50..50 (permanent).

Do you use some special Polyspace configuration that you generally recommend?

Do you use excacly the same code sinppet, were "static float X_Sa2_LPF_UnitDelay = 0.F;" is defined as local within the main() function?

I can also send the demo project with the issue to the technical support.

thanks again!

Best Regards, Thomas

Answer 3

[Manuel Duss]

Hi together,

we´ve got the same problem like thomas. But we have to use Polyspace 2015b. Did anybody have a solution for this?

Thanks!

Best Regards Manuel