Benefits of Using Polyspace Static Analysis Tools with Generated Code

You can use Polyspace® static analysis tools such as Polyspace Bug Finder™ and Polyspace Code Prover™ integrates with code generating tools such as Embedded Coder® and MATLAB® Coder. This integration allows for a streamlined workflow, as well and increased precision of the Polyspace analysis and automated justification of certain coding rule violations.

Streamlined Workflow

Polyspace integrates with Simulink® and MATLAB from the same release, which provides a streamlined workflow when analyzing generated code:

  • Run Polyspace analysis directly from the Simulink toolstrip or the MATLAB command window. Change Polyspace configurations using the Polyspace tab in the Configuration parameter dialog-box. See:

  • Automate Polyspace analyses by using MATLAB scripts. Polyspace supports MATLAB functions and classes that allow you to configure a Polyspace analysis, run the analysis, and export results in a variety of formats. Setup a script to automate routine Polyspace tasks in a server environment using MATLAB. If you have a configured Polyspace project, generate a MATLAB script to automate running the same analysis repeatedly. See Bug Finder Analysis with MATLAB Scripts.

  • Choose the scope of Polyspace analysis when analyzing model containing a hierarchy of referenced Simulink models. Exclude all referenced models, or include models up to a specific depth. See Model reference verification depth.

  • If your Simulink model references other models that you previously analyzed using Polyspace, you can choose to exclude those referenced model. See Ignore model references.

  • Share Polyspace configurations across multiple Simulink models. See Use custom project file.

  • Polyspace supports a distributed workflow for modeling and code generation. You can extract all relevant Polyspace options from a Simulink model and archive the options along with the generated code. When analyzing the generated code, using the extracted options produces a more precise analysis. See Run Polyspace Analysis by Using the Packaged Options Files.

Enhanced Precision

When analyzing code generated from Simulink models, Polyspace extracts information about the generated code from the model and sets analysis options accordingly to produce more precise analysis. For example:

  • Polyspace can impose the bounds of an inport or outport block on an input or output variable of the generated code. Constraining the input and output variables reduces the number of orange checks and false positive violations that would otherwise be reported. See External Constraints on Polyspace Analysis of Generated Code.

  • Polyspace uses a set of analysis options by default when analyzing code generated by Embedded Coder. By using these options, Polyspace runs an analysis that is aware of the code structure and assumptions that were made when generating the code. This results in fewer orange checks and false positive violations that would be reported otherwise. See External Constraints on Polyspace Analysis of Generated Code.

  • If your model specifies bounds of the input or output of a referenced model, Polyspace can verify the bounds in generated code. See Verify If Input and Output of Referenced Model Are Within Bounds (Polyspace Code Prover).

  • You can generate AUTOSAR and adaptive AUTOSAR compliant code using Embedded Coder. When analyzing the generated AUTOSAR or adaptive AUTOSAR code, Polyspace automatically obtains the data range specifications for the input and output variables from the Simulink model, resulting in a more precise analysis.

Automated Justification of Coding Rule Violations

The generated code can contain constructs that are reported by static analysis tools as violation of MISRA™ coding rules. The constructs in generated code that violate some MISRA coding rules are often justifiable. Embedded Coder and MATLAB Coder can insert annotations in the generated code to certain violations of MISRA coding rule violations. Polyspace supports these annotations and does not report violations on the annotated code. Supported annotations include:

  • MW:begin ... MW:end — If you set the properties JustifyMISRAViolations and GenerateComments to true, MATLAB Coder™ inserts code annotations that justify known MISRA C++:2008 and AUTOSAR C++14 violations.

    For example, in this generated code, the function test_init() violates MISRA C++:2008 Rule 0-1-8. If you set the properties JustifyMISRAViolations and GenerateComments of the code configuration object to true, MATLAB Coder inserts MW:begin and MW:end comments around the function:

    // MW:begin MISRA-CPP:0-1-8 "Justify"
void test_init()  
{
  int i;  
}
// MW:end MISRA-CPP:0-1-8 "Justify"
    Polyspace recognizes the MW:begin and MW:end annotations and shows the annotated results as Justified in the results list.

    These annotations are not inserted for Polyspace Code Prover runtime checks. For more information, see Generate C/C++ Code with Improved MISRA and AUTOSAR Compliance (Embedded Coder).

  • MW:operator — When generating code from a model, Embedded Coder inserts the code annotation MW:operator to justify violations of certain coding rules arising from misuse of an operation.

    For example, this code justifies a violation of MISRA C:2012 Dir 4.1 arising from the - operation:

    uint32_T qY;

/* Sum: '<Root>/SubUnsigned' incorporates:
 *  Inport: '<Root>/In1'
 *  Inport: '<Root>/In2'
 */
qY = U1 -
     /*MW:operator MISRA2012:D4.1 CERT-C:INT30-C 'Justifying MISRA C rule violation'*/
     /*MW:OvSatOk*/ U2;
if(qY > U1) {
	qY = 0U;
}
    Polyspace looks for violations arising from the operator preceding the MW:operator annotation in the code, and annotates the violations as Justified in the results list.

    To disable annotating operators, clear the configuration parameter Operator annotations (Embedded Coder). For more details, see Annotate Code for Justifying Polyspace Checks (Embedded Coder).

  • MW:OvSatOk, MW:OvBitwiseOk, MW:OvCarryOk — When generating code, Embedded Coder can sometimes utilize overflows to perform certain legitimate operations. Embedded Coder inserts these annotations in the generated code so that the overflow-related Polyspace Code Prover run-time checks appear justified in your results list.

    To disable annotating operators, clear the configuration parameter Operator annotations (Embedded Coder). For more details, see Annotate Code for Justifying Polyspace Checks (Embedded Coder).

See Also

| |

Topics