Polyspace Code Prover
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.
You can further visualize the control flow using the call hierarchy and the call flow graphs.