Hi,
Used non-shared variables are somewhat like green checks in Code Prover. They are not warnings. Since Code Prover reports all global variables, it does the following classification:
- Shared variables : potentially unprotected (warning shown in orange), protected (benign and shown in green)
- Unshared variables : unused (shown in grey), used (benign and not shown in any color since the proof aspect of Code Prover was not invoked)
As you can see, shared protected globals and unshared used globals are benign, and you do not need to fix anything. Just like green checks on divisions tell that Code Prover did evaluate the status of all divisions for division by zero, these are a way to tell the user that Code Prover did evaluate the status of all global variables.
