Run Polyspace on AUTOSAR Code Using Build Command

This topic describes a component-based approach to verifying AUTOSAR code with Polyspace. For an integration analysis approach, see Choose Between Component-Based and Integration Analysis of AUTOSAR Code with Polyspace.

If you use the AUTOSAR methodology for software development with a build command for compilation, you can reuse existing artifacts to specify source files and compilation options for Code Prover.

• You can reuse the source file specification in AUTOSAR XML files.

  Polyspace^® can read AUTOSAR XML specifications and extract source files involved in each software component into modules for subsequent Code Prover run-time checks. If you use the AUTOSAR methodology for software development, you can reuse the modularization built into this methodology for a modular Code Prover analysis. See polyspace-autosar.

• You can reuse compilation options specified in your build command.

  Polyspace can trace your build command and detect the compiler invoked along with compilation options such as paths to standard includes and macro definitions. See polyspace-configure.

This topic shows how to combine the two approaches and automate your Code Prover analysis.

Example Files

To follow the steps in this tutorial, use the demo files in polyspaceroot/polyspace/examples/doc_cxx/polyspace_autosar_configure.

The example uses a Linux-based makefile and Linux path separators. To run the example in Windows^®, make appropriate modifications.

Run Code Prover Without Compilation Options

Copy the contents of the demo folder into a temporary folder, for instance, /tmp/demo/. Navigate to that folder.

cd /tmp/demo

Run Code Prover on the ARXML and source files in the subfolder mRtwDemoAutosar_autosar_rtw. Save results in the folder /tmp/res.

polyspace-autosar -create-project /tmp/res \
-arxml-dir mRtwDemoAutosar_autosar_rtw \
-sources-dir mRtwDemoAutosar_autosar_rtw \
-generate-autosar-headers

Note the compilation errors. For instance, in the /tmp/res/.extract folder, open the file GPIO_read.log. You see a #error directive because the macro MY_DEFINE_FROM_SIMULINK is not defined.

If you open the file GPIO_read.c in /tmp/demo/mRtwDemoAutosar_autosar_rtw, you see the line causing the issue.

#ifndef MY_DEFINE_FROM_SIMULINK
#error Missing MY_DEFINE_FROM_SIMULINK
#endif

This line is supposed to cause an error during preprocessing unless the macro MY_DEFINE_FROM_SIMULINK is defined.

Run Code Prover with Compilation Options from Build Command

The makefile mRtwDemoAutosar.mk in /tmp/demo/mRtwDemoAutosar_autosar_rtw defines macros and paths to include folders. For instance, the previously missing macro MY_DEFINE_FROM_SIMULINK is defined in the line:

DEFINES_CUSTOM = -DMY_DEFINE_FROM_SIMULINK

Navigate to the folder containing the makefile.

cd /tmp/demo/mRtwDemoAutosar_autosar_rtw

Extract compilation options from a build command that uses this makefile mRtwDemoAutosar.mk. For instance, if you installed MATLAB^® in /usr/local/MATLAB/R2018b, you can trace the makefile like this.

polyspace-configure -no-sources \
-output-options-file psoptions -allow-overwrite\
make -B -f mRtwDemoAutosar.mk START_DIR=.. \
MATLAB_ROOT=/usr/local/MATLAB/R2018b buildobj

The compilation options in the makefile are converted to Polyspace analysis options and saved in the options file psoptions. The -no-sources option ensures that the polyspace-configure command extracts compilation options only and not sources. START_DIR and MATLAB_ROOT are variables specific to the demo makefile and might not be required in other makefiles that you use.

Remove results from any previous run of the polyspace-autosar command.

rm -r /tmp/res

Provide the options file psoptions created in the previous step to the polyspace-autosar command.

polyspace-autosar -create-project /tmp/res \
-arxml-dir . \
-sources-dir .\
-generate-autosar-headers \
-extra-options-file psoptions

You no longer see the compilation errors because Code Prover is now aware of the compilation options that you used in your build command.