Polyspace Code Prover
You can use Polyspace Code Prover to verify generated code or mixed code which contains both generated and handwritten code. Code-level defect results in the automatically generated code are traced back to the model in Simulink. You can identify which parts of the model are reliable; and correct design problems that will cause errors in the code. You can also identify potential problems between the interface of generated and handwritten code. For example, the mixing of hand-written S-Function code with generated code could result in a problem where incorrect ranges of signals in the interface cause a run-time error.
Polyspace Code Prover also supports tracing run-time results to dSPACE® TargetLink® blocks and IBM Rational Rhapsody models.