Polyspace Code Prover

Viewing Range Information

Polyspace Code Prover tracks control and data flow through the software and displays range information associated with variables and operators. By placing your cursor over an operator or variable, a tooltip message displays the range information. The formal method known as abstract interpretation enables determination of accurate range information for the purpose of proving that the software is free of certain run-time errors. You can use range information to debug your software or to ensure that certain variables or operations do not violate specified range limits.

In the example below, Polyspace Code Prover has determined that the division operation consists of a range between -1701 to 3276 for the left operand; right operand is 9. The resulting range after division is -189 to 364.

Tooltip displaying the possible ranges for all run time conditions.
Tooltip displaying the possible ranges for all run time conditions.

You can further visualize the control flow using the call hierarchy and the call flow graphs.

Call flow graph displaying the order of function calls in an interprocedural analysis.
The order of function calls in an interprocedural analysis.
Next: Tracking Software Quality Metrics

Try Polyspace Code Prover

Get trial software

Mejores Prácticas para la Verificación y Validación de modelos Simulink y Código C

View webinar