Why do I see a range regarding the size of local variables in terms of the metric "Higher Estimate Of Sitze Of Local Variables" in Polyspace Code Prover?

Given is the following function,

 

uint8 foo(uint8) {
  uint8 arr[2] = {1, 2};
  uint8 val = arr[1];

  return val;
}

which is verified using Polyspace Code Prover. Polyspace Code Prover reports a variable value for metric "Higher Estimate Of Sitze Of Local Variables" as 3 .. 5.

Why do I see a range regarding the size of local variables in terms of the metric "Higher Estimate Of Sitze Of Local Variables" in Polyspace Code Prover?

Answer 1

[MathWorks Support Team]

The reason for this variable value of metric "Higher Estimate Of Sitze Of Local Variables" is because function 'foo' can be called in the following valid ways,

uint8 a = 1;
foo(a);

or even

foo();

In the former way the value of metric "Higher Estimate Of Sitze Of Local Variables" will be 4 since the output argument is not used, whereas in the latter case it will be 3 since neither the input nor the output variable of the function is used.

If both the input and the output variables are defined, then the size of the local variables of function 'foo' will be 5 bytes, which is the maximum size of its local variables.