Main Content

polyspaceAutosar

Run Polyspace Code Prover on code implementation of AUTOSAR software components using MATLAB scripts

collapse all in page

Syntax

[status, msg] = polyspaceAutosar('-create-project',projectFolder,'-arxml-dir',arxmlFolder,'-sources-dir',codeFolder,options)
[status, msg] = polyspaceAutosar('-update-project',prevProjectFile,options)
[status, msg] = polyspaceAutosar('-update-and-clean-project',prevProjectFile,options)
[status, msg, out] = polyspaceAutosar(___)

Description

[status, msg] = polyspaceAutosar('-create-project',projectFolder,'-arxml-dir',arxmlFolder,'-sources-dir',codeFolder,options) checks the code implementation of AUTOSAR software components for run-time errors and violation of data constraints in the corresponding AUTOSAR XML specifications. The analysis parses the AUTOSAR XML specifications (.arxml files) in arxmlFolder, modularizes the code implementation (.c files) in codeFolder based on the specifications, and runs Code Prover on each module for the checks. The Code Prover results are stored in projectFolder. After analysis, you can open the project psar_project.psprj from projectFolder in the Polyspace® user interface or the file psar_project.xhtml in a web browser. You can view the results for each software component individually.

You can use additional options for troubleshooting, for instance, to perform only certain parts of the update and track down an issue or to provide extra header files or define macros.

example

[status, msg] = polyspaceAutosar('-update-project',prevProjectFile,options) updates the Code Prover analysis results based on changes in ARXML files or C source code since the last analysis. The update uses the XHTML file prevProjectFile from the previous analysis and reanalyzes only the code implementation of software components that changed since that analysis.

You can use additional options for troubleshooting.

[status, msg] = polyspaceAutosar('-update-and-clean-project',prevProjectFile,options) updates the Code Prover analysis results based on changes in ARXML files or C source code since the last analysis. The update reanalyzes only the code implementation of software components that changed since the previous analysis. A clean update also removes information about software components that are out of date. For instance, if you use an additional option to force the update for specific software components and other SWC-s have also changed, a clean update removes those other SWC-s from the Polyspace project.

You can use additional options for troubleshooting.

[status, msg, out] = polyspaceAutosar(___) runs a Code Prover analysis using the same options as before. The output, instead of appearing in the MATLAB® Command Window, is redirected to a character vector out.

Note

Before you run Polyspace from MATLAB, you must link your Polyspace and MATLAB installations. See Integrate Polyspace with MATLAB and Simulink or Integrate Polyspace Server Products with MATLAB.

Examples

collapse all

Suppose your ARXML files are in a folder arxml and your C source files in a folder code in the current folder.

Run Code Prover on all software components defined in your ARXML files. Store the results in a folder polyspace-project in a temporary folder.

The folder must not already exist. If previous results exist in that folder, you can update those results. An update only reanalyzes source files that changed since the previous run.

exampleDir = fullfile(polyspaceroot,'polyspace',...
    'examples','doc_cxx','polyspace_autosar');
arxmlDir = fullfile(exampleDir, 'arxml');
sourceDir = fullfile(exampleDir, 'code');

tempDir = tempdir;
projectDir = fullfile(tempDir, 'polyspace-project');
prevProjectFile = fullfile(projectDir, 'psar_project.xhtml');

% Update project file if it already exists, else create new project
projectDirAlreadyExists = isfolder(projectDir);

if projectDirAlreadyExists
    [status, msg] = polyspaceAutosar('-update-project', ...
        prevProjectFile);
else
    [status, msg] = polyspaceAutosar('-create-project', projectDir, ...
    '-arxml-dir', arxmlDir, ...
    '-sources-dir', sourceDir...
    '-generate-autosar-headers');;
end

Note that the example uses the option -generate-autosar-headers to generate the AUTOSAR headers (Rte_ headers and Os.h, Compiler.h, etc.). When running polyspaceAutosar on your source code, you can use your own AUTOSAR headers by omitting this option and using the -I option to point to appropriate include folders.

Input Arguments

collapse all

Folder name, specified as a character vector. If the folder exists, it must be empty.

After analysis, the folder contains two project files psar_project.psprj and psar_project.xhtml.

  • To see the results, open the project file psar_project.psprj in the Polyspace user interface or the file psar_project.xhtml in a web browser.

  • For subsequent updates using MATLAB scripts, use the project file psar_project.xhtml.

See also Review Polyspace Results on AUTOSAR Code.

Example: 'C:\Polyspace_Projects\proj_swc1'

Folder name, specified as a character vector.

UNC paths are not supported for the folder name.

Example: 'C:\arxml_swc1'

Folder name, specified as a character vector.

UNC paths are not supported for the folder name.

Example: 'C:\code_swc1'

Path to the previously created project file psar_project.xhtml, specified as a character vector.

Example: 'C:\Polyspace_Projects\proj1\psar_project.xhtml'

Options to control creation of a Polyspace project and subsequent analysis. You primarily use the options for troubleshooting, for instance, to perform only certain parts of the update and narrow down an issue or to provide extra header files or define macros.

Specify each option as a character vector, followed by the option value as a separate character vector. For instance, you can specify an options file opts.txt by using the syntax polyspaceAutosar(...,'-options-file','opts.txt').

General options

OptionValueDescription
'-verbose' 

Save additional information about the various phases of command execution (verbose mode). The file psar_project.log and other auxiliary files store this additional information.

If an error occurs in command execution, the error message is stored in a separate file, irrespective of whether you enable verbose mode. Running in verbose mode only stores the various phases of execution. Use this information to see when an error was introduced.

'-options-file'Options file name, for instance, 'opts.txt'.

Use an options file to supplement or replace the command-line options. In the options file, specify each option on a separate line. Begin a line with # to indicate comments.

An options file opts.txt can look like this:

# Store Polyspace results
-create-project polyspace
# ARXML Folder
-arxml-dir arxml
# SOURCE Folder
-sources-dir code

If an option that is directly specified with the polyspaceAutosar function conflicts with an option in the options file, the directly specified option is used.

You typically use an options file to store and reuse options that are common to multiple projects.

'-generate-autosar-headers' 

Generate AUTOSAR headers (Rte_ headers and Os.h, Compiler.h, etc.) instead of using the ones found in the source folders.

Options to control update of project

If you update a project, by default, the analysis results are updated for all AUTOSAR SWC behaviors with respect to any change in the ARXML files or C source code since the last analysis. Control the update by using these options.

OptionValueDescription
'-autosar-behavior'Full qualified name of SWC behavior, for instance, 'pkg.component.bhv'.

Check the implementation of software components whose internal behavior-s are specified. The default analysis considers all software components present in the ARXML specifications.

To specify multiple software components, repeat the option. Alternatively, use regular expressions to specify a group of software components under the same package.

For instance:

  • To specify the software component whose internal behavior has the fully qualified name pkg.component.bhv, use:

    polyspaceAutosar(...,
'-autosar-behavior',...
'pkg.component.bhv')

  • To specify the software components whose internal behavior-s have fully qualified names beginning with pkg.component, use:

    polyspaceAutosar(...,
'-autosar-behavior',...
'pkg.component\..*')
    The \. represents the package name separator . (dot) and the .* represents any number of characters.

'-do-not-update-autosar-prove-environment' 

Do not read the ARXML specifications. Use ARXML specifications stored from the previous analysis.

Use this option during project updates to compare the code against previous specifications. If you do not use this option, project updates read the entire ARXML specifications again.

'-do-not-update-extract-code' 

Do not read the C source code. Use source code stored from the previous analysis.

Use this option during project updates to compare the previous source code against ARXML specifications. If you do not use this option, project updates consider all changes to the source code since the previous analysis.

'-do-not-update-verification' 

Read the ARXML specifications and C code implementation only but do not run the Code Prover analysis.

Use this option during project updates to investigate errors introduced in the ARXML specifications or compilation errors introduced in the source code. You can first fix these issues, and then run the Code Prover analysis.

Options to control parsing of ARXML specifications

OptionValueDescription
'-autosar-datatype'Full qualified name of data type, for instance, 'pkg.datatypes.type'

Import definition of AUTOSAR data types specified. The default analysis imports only data types specified in the internal behavior of software components that you verify.

To specify multiple data types, repeat the option. Alternatively, use regular expressions to specify all data types under the same package.

For instance:

  • To specify a data type that has the fully qualified name pkg.datatypes.type, use:

    polyspaceAutosar(...,
'-autosar-datatype',...
'pkg.datatypes.type')

  • To specify data types that have fully qualified names beginning with pkg.datatypes, use:

    polyspaceAutosar(...,
'-autosar-datatype',...
'pkg.datatypes\..*')
    The \. represents the package name separator . (dot) and the .* represents any number of characters.

  • To force import of all data types, use:

    polyspaceAutosar(...,
'-autosar-datatype',...
'.*\..*')

'-Eautosar-xmlReaderSameUuidForDifferentElements'

'-Eno-autosar-xmlReaderSameUuidForDifferentElements'

 

If multiple elements in the ARXML specifications have the same universal-unique-identifier (UUID), use these options to toggle between a warning and an error.

The default analysis stops with an error if this issue happens. To convert to a warning, use '-Eno-autosar-xmlReaderSameUuidForDifferentElements'. For conflicting UUIDs, the analysis stores the last element read and continues with a warning.

The subsequent executions continue to use the warning mode. To revert back to an error, use '-Eautosar-xmlReaderSameUuidForDifferentElements'.

'-Eautosar-xmlReaderTooManyUuids'

'-Eno-autosar-xmlReaderTooManyUuids'

 

If the same element in the ARXML specifications has different universal-unique-identifiers (UUID), use these options to toggle between a warning and an error.

The default analysis stops with an error if this issue happens. To convert to a warning, use '-Eno-autosar-xmlReaderTooManyUuids'. For conflicting UUIDs, the analysis stores the last element read and continues with a warning.

The subsequent executions continue to use the warning mode. To revert back to an error, use '-Eautosar-xmlReaderTooManyUuids'.

'-Wno-autosar-xmlDuplicateType'

 

Use this option to suppress warnings about duplicate types in ARXML.

The duplicate type warning messages can look like this:

Type arrayType is already defined 
in another file.

Options to control reading of C source code

OptionValueDescription
'-include'Header file

Specify header files to be #include-ed by each file involved in the analysis. For instance, -include file1.h makes the analysis behave as if there is a line #include 'file1.h' in every source file. The #include-ed file can contain Polyspace-specific workarounds for compilation errors, such as data type and macro definitions.

You can provide the header files with data type and macro definitions only during project creation. For subsequent updates, you can change the contents of this file but not provide a new file. Also, this file must not be in the same folder as the Polyspace project and results.

To specify several files, enter the option once for each file, for instance:

polyspaceAutosar(...,
 '-include', 'file1.h', '-include', 'file2.h')

If you additionally define macros or undefine them using the options '-D' or '-U', for definitions that conflict with the ones in PREINCLUDE_FILE, the -D or -U specifications prevail.

'-I'Folder containing header files.

Specify folders containing header files. The analysis looks for #include-d files in this folder. The folder must be a subfolder of your source code folder.

Repeat the option for multiple folders. The analysis looks for header files in these folders in the order in which you specify them.

If you want to specify folders that are not in the source code folder, use the option:

polyspaceAutosar(...,
 '-extra-project-options','-I INCLUDE_FOLDER')

'-D'Name of macro, for instance, '_WIN32.

Specify macros that the analysis must consider as defined.

For instance, if you specify:

polyspaceAutosar(...,
 '-D','_WIN32')
the preprocessor conditional #ifdef _WIN32 succeeds and the corresponding branch is executed.

'-U'Name of macro, for instance, '_WIN32.

Specify macros that the analysis must consider as undefined.

For instance, if you specify:

polyspaceAutosar(...,
 '-U','_WIN32')
the preprocessor conditional #ifndef _WIN32 succeeds and the corresponding branch is executed.

Options to control Code Prover checks

OptionValueDescription
'-extra-project-options'Space-separated list of options.

Specify additional options for the Code Prover analysis. The options that you specify do not apply to the ARXML parsing or code extraction, but only to the subsequent Code Prover analysis.

Use this method to specify analysis options that are used in a non-AUTOSAR Code Prover analysis. See Complete List of Polyspace Code Prover Analysis Options.

For instance, you might want to specify a compiler and target architecture. By default, compilation of projects created from AUTOSAR specifications use the gnu4.7 compiler and i386 architecture.

To specify a visual11.0 compiler with x86_64 architecture, enter this option:

polyspaceAutosar(...,
 '-extra-project-options','-compiler visual11.0 -target x86_64')
See also Compiler (-compiler) and Target processor type (-target).

'-extra-options-file'File with Polyspace options.

Specify additional options for the Code Prover analysis in an options file. The options that you specify do not apply to the ARXML parsing or code extraction, but only to the subsequent Code Prover analysis.

For instance, you can trace your build command to gather compiler options, macro definitions and paths to include folders, and provide this information in an options file for analysis of code implementation of AUTOSAR software components.

  1. Trace your build command (for instance, make) with the polyspaceConfigure function and generate an options file for subsequent Code Prover analysis. Suppress inclusion of sources in the options file with the -no-sources option.

    polyspaceConfigure -output-options-file options.txt -no-sources make

  2. Run Code Prover on AUTOSAR code with polyspace-autosar. Provide your ARXML folder, source folders and other options. In addition, provide the earlier generated options file with the -extra-options-file option.

    polyspaceAutosar(...,
 '-extra-options-file','options.txt')

'-show-prove'Full qualified name of SWC behavior, for instance, 'pkg.component.bhv'.

After analysis, open results for a specific software component whose internal behavior is specified.

Output Arguments

collapse all

Boolean flag indicating whether the analysis ran to completion. If the analysis is completed, the return value is 0, otherwise it is a nonzero value.

If you see a nonzero value, check the second output argument of polyspaceAutosar for error messages.

You can also look for error messages in the file psar_project.xhtml in your project folder. You can use this XHTML file to determine which software components were analyzed.

See Troubleshoot Polyspace Analysis of AUTOSAR Code.

Analysis log, specified as a structure with these fields:

Type of message, returned as one of three character vectors:

  • 'info': Information such as current stage of analysis.

  • 'warning': Warnings that do not stop analysis but can cause errors later.

  • 'error': Errors that can stop the entire analysis or analysis of specific software components.

To check for errors, use this type information. For instance, to check for errors in the structure msg, use this code:

% Convert to table for logical indexing
msgTable = struct2table(msg);

% Check which messages have the type 'error'
errorMatches = (strcmp(msgTable.Criticity, 'error'));

% Read the error messages to another table
errorMessage = msgTable(errorMatches, :);

Content of message, returned as a character vector.

Example: 'Start Extract user-implementation for Behavior ''pkg.tst002.swc001.bhv001''...'

Analysis log, returned as a character vector.

Version History

Introduced in R2018b

See Also

Topics