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().
Best Answer