Why is my variable assigned a range of values in Polyspace Code Prover?

I have the following code written in C language:

const volatile float V[3] = {1.F, 2.F, 3.F};
const volatile W[3] = {4.F, 5.F, 6.F};

void fun1(void){
   float x;
   x = fun2((float *) &(V[0]), (float *) &(W[0]));
}

float fun2(float p1[], float p2[]){
   return p1[0]*p2[0];
}

When using Polyspace Code Prover, variable "x" is assigned a range of possible values. However, I would expect the value of "x" to be uniquely determined by the code execution.

 

Why is variable "x" assigned a range of values instead of a single numerical value?

Answer 1

[MathWorks Support Team]

In order for Polyspace Code Prover to be able to assign a single numerical value to variable "x", you need to perform the following steps:

 

1) Polyspace Code Prover assigns full range to "volatile" global variables. A non-intrusive way to override this behavior is to go into Configuration > Target & Compiler > Macros and add the Macro

volatile=  

Another option is to modify the code by removing the "volatile" keyword. For more information on Polyspace Code Prover assumptions about volatile variables, please refer to the following link:

https://www.mathworks.com/help/releases/R2020a/codeprover/ref/volatile-variables.html

 

2) Add the keyword "float" in the declaration of the variable "W". Otherwise, this variable will be considered as "int" and information will be lost while casting and performing operations when calling the function "fun2". If the keyword "float" is not used,  Polyspace Code Prover will therefore assign a range to the variable "x".

3) Variables "V" and "W" are declared as "constant", and therefore there is no need to set constraints for them. In Configuration > Inputs & Stubbing you can remove any potential file setting constraints, and untick the "Ignore default initialization of global variables" field. Since these arrays are small, Polyspace Code Prover will be precise in the computation of the range. For large arrays, only the minimum and maximum values may be considered instead.