How can I have Polyspace Bug Finder detect overflows on static variables within functions?

Given is a C-code that consists also of static variables, whose values can be modified based on the number of function calls. Consider the following case where 'counter' is a static variable of function 'fun()'

 

void fun(void) {
    static uint16 counter = 0;
    counter++;
}

It is sought for the workflow that allows Polyspace to report a possible overflow on the latter static variable, which may occur if function 'fun()' is called enough times, namely,

 

void fun2(void) {
    for (int i = 0; i <65537; i++)
        fun();
}

How can I have Polyspace Bug Finder detect overflows on static variables within functions?

Answer 1

[MathWorks Support Team]

Please note that Polyspace Bug Finder does not know the context into which function 'fun' is used, therefore it cannot conclude whether an overflow on variable 'counter' may be encountered, as the variable is declared as 'static', meaning that whether an overflow may occur or not solely depends on the calling context. Polyspace Bug Finder does not take into consideration a calling context for the provided functions and analyze them as they are provided.

On the other hand Polyspace Code Prover is using a calling context for the functions provided therein. You may chose to provide an own calling context by means of a 'main()' function or you can have Polyspace Code Prover generate a 'main()' function automatically that randomly calls the functions in your project.

If you verify the code snippet above using Polyspace Code Prover you will notice that an orange check is asserted, meaning that Polyspace Code Prover recognizes that an overflow in that location may occur.

For this use case Polyspace Code Prover instead of Polyspace Bug Finder should be employed.