Codeprover: all variables are unused

I am running polyspace codeprover on our software project. It seems like all variables are reported to be unused. Looking at the html report (Developer template):

There exists no reachable operation on variable ‘xxx’.

This message is repeated for every variable that we have (or close to, i didn't check all of them). The entrypoints (option -entry-points) are copied from our bugfinder configuration (which nicely detects missing critical sections) and contains our interrupts and boot point. The function main() is not included as that one gets called from the boot point. But it seems like the while-loop that we have in main() does not get taken into account...

Our boot point is implemented in a crt0.S in assembler. From that assembler code we call C-functions which eventually lead to main() being executed. Is codeprover/bugfinder able to handle this target-specific assembler? And can it find the entrypoint for main()? Or does it implicitly assume main() is an entrypoint?

I always assumed our configuration for bugfinder was ok, but looking at the codeprover results, and writing this down, makes me think how bugfinder/codeprover can know the non-interrupt entrypoint main().

Answer 1

[Alexandre De Barros]

Hello,

If Polyspace Code Prover is able to find a function called main, it will automatically use it as the main entry point. By the way, Polyspace works with the C language only, so your assembly code is ignored/stubbed.

You are writing that you have a while loop in the main. That could be the explanation for the unreachable code. Indeed, with Code Prover (not Bug Finder) when the end of the main is unreachable, the entry-points (tasks, interrupts) are not "launched".

It means that you should see your entry-points in the list of unreachable functions in the dashboard (Code covered by verification).

And in this case, see this page to see what you have to do: https://www.mathworks.com/help/codeprover/ug/model-tasks-if-main-contains-infinite-loop.html

Best regards,

Alexandre

[Stein Heselmans]

We're running codeprover from CI, so headless with html 'Develop' templated output. I don't see any functions in the unreachable functions section of that html report (No unreachable functions were found). I would expect a few however, as our gcc-linker reports some functions as not used and throws them out of the executable... So I am not sure how well this "unreachable functions" output is reliable? In the terminal, i see some '<function> is dead code' logs, but why do these functions not appear in that unreachable functions section?

Anyway, i tried the hint on the page you linked in your answer. I #ifdef'ed main and replaced it with a function background_tasks() which does loop forever, and added this function to the entrypoints. The main() is just empty now. I even tried that without ifdef'ing, to eliminate my compiler directive -D__POLYSPACE__ being passed or not. Having the main() not loop forever, does have an impact on the reported html: - some extra green/red/orange checks are reported, - some of the reports for unused variables are gone (hooray!!!) - i even get some extra 'Potentially unprotected variable' now.

I still see some suspicious report for unused variables, but the biggest part of those seem valid now. I'll accept your answer and re-open when needed. Thanks for the support.

Answer 2

[Stein Heselmans]

Additional cause identified: for some variables codeprover is not able to decide on the range it should use. For e.g. read-only hardware registers, configuration parameters, DMA buffers the software does not write values to these 'variables'.

I used the -data-range-specifications option on command line, or similar in GUI in order to fix the ranges of those values.