Why does Polyspace Code Prover show a function returning a value with full range which seems to ignore DRS variable constraints in R2018b?

I am using Polyspace Code Prover with some C code and am seeing a function analyzed to return the full range of my variable type (float) even though I believe it should be constrained with ranges I setup in my DRS (Data Range Specification) file for the function parameters. Why is this happening?

This is my example C code function signature: 

FUNC(float32) foo(const boolean boolVarOne, const volatile float32 *floatVarOne, const volatile float32 *floatVarTwo)

When these parameters are constrained in the DRS file, I expect my function to only be able to output between [-10.0, 10.0]. However, I see the full range of a float instead being called when I look at my function implemented with these constrained arguments.

Answer 1

[MathWorks Support Team]

There are two reasons you are seeing this unexpected behavior.

First, the Polyspace Code Prover is a static analyzer that is not analyzing each call of the function but instead uses abstract modeling. The function "foo" is called many times in the source code with different contexts (i.e. different values for parameters). This means that Polyspace will merge all contexts when it will analyze the function "foo". The side effect leads to return full range as soon as one call among the many times is called with full-range parameters. Option "-inline" helps Polyspace considering each call separately ("-inline foo"). For more information, please refer to the following documentation page:

Please run the below command in the MATLAB R2018b command window to get the release specific documentation

web(fullfile(docroot, 'codeprover/ref/inlineinline.html'))

Second, the two parameters associated with the function "foo" prototype are "volatile". As soon as Polyspace Code Prover considers a variable or a parameter volatile, it always considers full-range values for it even if constraints are added to a DRS file. Please see the following documentation page for more information on how Code Prover interacts with a volatile variable that can change without a write operation.

Please run the below command in the MATLAB R2018b command window to get the release specific documentation

web(fullfile(docroot, 'codeprover/ref/volatile-variables.html'))

If you remove the volatile keyword from the two parameter of the function and relaunch Polyspace Code Prover with the "-inline" option, it will help Polyspace Code Prover be more precise. Afterwards, the range returned by function "foo" at the line of interest should match your expectations.

Please follow the below link to search for the required information regarding the current release:

https://www.mathworks.com/help/