Polyspace Code Prover

Detecting Run-T ime Errors

Polyspace Code Prover uses abstract interpretation with static code analysis to prove, identify, and diagnose run-time errors such as overflows, divide by zeros, and out-of-bound pointers. This technique completely and comprehensively verifies all run-time conditions and automatically provides a diagnostic of proven, failed, unreachable, or unproven for each code operation. In the verification results produced by Polyspace Code Prover, each C or C++ operation is color-coded to indicate its status:

Green: proven free of run-time errors
Red: proven faulty each time the operation is executed
Gray: proven unreachable (may indicate a functional issue)
Orange: unproven operation may be faulty under certain conditions

Color-coded run-time error attributes identified by Polyspace Code Prover.

Run-time error attributes identified by Polyspace Code Prover.

Errors detected include:

  • Overflows, underflows, divide-by-zero, and other arithmetic errors
  • Out-of-bounds array access and illegally dereferenced pointers
  • Always true/false statement
  • Noninitialized class members (C++)
  • Read access to noninitialized data
  • Access to null this pointer (C++)
  • Dead code
  • Dynamic errors related to object programming, inheritance, and exception handling (C++)
Next: Viewing Range Information

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