Green is the most valuable color provided by Code Prover. With the Polyspace coloring paradigm, Green checks are those that have been PROVEN not to occur. In other words, if you see a green divide by zero check in your report, that means that the particular divide being checked CANNOT have a divide by zero under the provided circumstances.
Polyspace does this proof with a formal methods analysis. The coloring paradigm used provides 4 possible colors at every check in the code. So for example, at every point in the code that could have an out of bounds array index, divide by zero, overflow, or other semantic run-time error, a mathematical proof is performed that determines the possibility that this error could occur. The 4 colors are as follows:
- Green - As already stated, the issue being checked has been proven not to occur.
- Red - In this case, you have a systematic error. In other words, if your program's control flow reaches this point, regardless of which path it takes, the error will occur. You should not see many of these in your code, unless they are there by design with some specific error handling routines for instance. If the red is not intentional, you should correct these issues and re-run analysis before looking at results of any other color. They often have knock-on affects for the proof provided for other findings.
- Gray - In this case, Polyspace is showing you that the code is logically unreachable. Sometimes dead code is intentional; however, other cases it is not and can hide important initialization or other data flow paths which can impact your findings also. Like red findings, these should be addressed before addressing the 4th and final category...
- Orange - This, in my opinion, is the second most important color in Polyspace only after the Green. Orange represents vulnerability in your code. When you see Orange, Polyspace has shown that there are possible data flows or control flows in your provided code which allow the particular error to be possible. Remember, at any point in your code, Polyspace is considering all possible paths (control flow and data flow) through that point. If you have an orange finding, Polyspace was not able to mark all of those paths through that point as green. When you are first implementing a system, this is extremely valuable to help you understand where your particular unit under development is vulnerable. This lets you be aware of places in your code where you need to make design choices in order to prevent those vulnerabilities. Those design choices will either be additional code, re-architecture to avoid those issues, or sometimes using your development processes to make sure that an interface only gets called with specific data ranges for example. No matter which design choice you make, you should be able to make the change and provide Polyspace with the necessary assumptions in order to see your orange finding turn green on subsequent analysis.