Polyspace® products verify C, C++, and Ada code by detecting run-time errors before code is compiled and executed. Polyspace verification uses formal methods not only to detect errors, but to prove mathematically that certain classes of run-time errors do not exist.
To verify the source code, you set up verification parameters in a project, run the verification, and review the results. A graphical user interface helps you to efficiently review verification results. The software assigns a color to operations in the source code as follows:
Green – Indicates that an operation is proven to not have certain kinds of error.
Red – Indicates that an operation is proven to have at least one error.
Gray – Indicates unreachable code.
Orange – Indicates that the operation can have an error along some execution paths.
The color-coding helps you to quickly identify errors and find the exact location of an error in the source code. After you fix errors, you can easily run the verification again.