Main Content

polyspace-autosar

(DOS/UNIX) Run Polyspace Code Prover on code implementation of AUTOSAR software components

collapse all in page

Syntax

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder [-sources-dir codeFolder] [OPTIONS]
polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder -output-platform-project
polyspace-autosar -create-project projectFolder -select-arxml-files arxmlFiles [-select-arxml-files arxmlFiles] -select-source-files codeFiles [-select-source-files codeFiles] [OPTIONS]
polyspace-autosar -update-project prevProjectFile [OPTIONS]
polyspace-autosar -update-and-clean-project prevProjectFile [OPTIONS]
polyspace-autosar -help

Description

Note

This Polyspace® command is available in polyspaceroot\polyspace\bin. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b (see also Installation Folder for desktop products or Installation Folder for server products). To avoid typing the full path to this command, add this location to the PATH environment variable in your operating system.

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder [-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. You can view the results for each software component individually or upload them to Polyspace Access for an overview.

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

example

polyspace-autosar -create-project projectFolder -arxml-dir arxmlFolder -sources-dir codeFolder -output-platform-project 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 and modularizes the code implementation (.c files) in codeFolder based on the specifications. A project is created for each software component and the all projects are stored in a workspace. The analysis runs Code Prover on each project for the checks. The Code Prover results are stored in projectFolder. After analysis, you can open the workspace psar_workspace.pswks from projectFolder in the Polyspace Platform user interface. You can view the results for each software component individually or get an overview by uploading the results to Polyspace.

polyspace-autosar -create-project projectFolder -select-arxml-files arxmlFiles [-select-arxml-files arxmlFiles] -select-source-files codeFiles [-select-source-files codeFiles] [OPTIONS] creates a Polyspace project from AUTOSAR specifications as in the preceding syntax but allows you to exclude specific files or folders from analysis using shell patterns or regular expressions.

polyspace-autosar -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 html file prevProjectFile from the previous analysis and only reanalyzes the code implementation of software components that changed since that analysis.

You can use additional options for troubleshooting.

example

polyspace-autosar -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 only reanalyzes 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.

example

polyspace-autosar -help shows all options available for polyspace-autosar.

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 in the current folder.

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code

The analysis creates a Polyspace project with several modules. Each module collects the C code implementation of a software component. The analysis runs Code Prover on each module and checks the code for run-time errors or mismatch with ARXML specifications.

After analysis, you can open the results in several ways. See Review Polyspace Results on AUTOSAR Code.

Update an ARXML or code file. For instance, in Linux®, you can touch a file to indicate an update. Check if the updates affected results of the Code Prover analysis. For an updated analysis, provide the project file psar_project.html created in the previous step.

polyspace-autosar -update-project polyspace\psar_project.xhtml

If you update an ARXML file, the entire analysis is repeated. If you update your source code, the analysis is repeated only for software components whose code implementation was updated.

Instead of running Code Prover on all software components, check specific software components only.

For instance, suppose a software component has the fully qualified path pkg.component.bhv. You can run Code Prover only on this software component.

polyspace-autosar -create-project polyspace -arxml-dir arxml -sources-dir code -autosar-behavior pkg.component.bhv

You can run Code Prover on all software components but later choose to update the analysis for specific software components only.

polyspace-autosar -update-project polyspace\psar_project.xhtml -autosar-behavior pkg.component.bhv

If you do not reanalyze a software component that has been updated, the analysis shows that the software component might be out of date.

You can also update the analysis for specific software components and remove all traces of other software components.

polyspace-autosar -update-and-clean-project polyspace\psar_project.xhtml -autosar-behavior pkg.component.bhv

Input Arguments

collapse all

Folder name, specified as a string (in double quotes). If the folder exists, it must be empty.

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

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

  • For subsequent updates on the command line, use the file psar_project.html.

See also Review Polyspace Results on AUTOSAR Code.

Example: "C:\Polyspace_Projects\proj_swc1"

Folder name, specified as a string (in double quotes). You can omit the double quotes if your folder paths do not contain spaces.

UNC paths are not supported for the folder name.

Example: "C:\arxml_swc1"

Folder name, specified as a string (in double quotes). You can omit the double quotes if your folder paths do not contain spaces.

To specify multiple root folders containing sources, repeat the -sources-dir option. If you specify multiple root folders, they must not overlap. For instance, one root folder cannot be a subfolder of the other.

UNC paths are not supported for the folder name.

Example: "C:\code_swc1"

Root folder containing ARXML files followed by file and folder inclusions and exclusions, specified as a string. To create this string:

  1. Use the Linux find command to search for the files and folders to include and exclude.

  2. Copy the find options and enclose them in double quotes.

For examples, see Select AUTOSAR XML (ARXML) and Code Files for Polyspace Analysis.

Root folder containing code (.c and .h) files followed by file and folder inclusions and exclusions, specified as a string. To create this string:

  1. Use the Linux find command to search for the files and folders to include and exclude.

  2. Copy the find options and enclose them in double quotes.

For examples, see Select AUTOSAR XML (ARXML) and Code Files for Polyspace Analysis.

Path to the previously created project file psar_project.html, specified as a string (in double quotes). You can omit the double quotes if your folder paths do not contain spaces.

Example: "C:\Polyspace_Projects\proj1\psar_project.html"

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

General options

OptionDescription
-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. You can use this information to see when an error was introduced.

-options-file OPTION_FILE

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

You can run polyspace-autosar as:

polyspace-autosar -options-file opts.txt

If an option that is directly specified with the polyspace-autosar command conflicts with an option in the options file, the directly specified option is used. For instance, in this example, the folder proj is used to save the Polyspace project.

polyspace-autosar -create-project proj -options-file opts.txt

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 SWCs behaviors with respect to any change in the arxml files or C source code since the last analysis. These options allow you to control the update.

OptionDescription
-autosar-behavior AUTOSAR_QUALIFIED_NAME

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

To specify multiple software components, repeat the option. Alternatively, you can do one of the following:

  • Use shell patterns similar to the patterns used with -select-arxml-files and -select-source-files.

    For examples, see Select AUTOSAR XML (ARXML) and Code Files for Polyspace Analysis.

  • 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:

      -autosar-behavior pkg.component.bhv

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

      -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. Unless you 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. Unless you 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

OptionDescription
-autosar-datatype AUTOSAR_QUALIFIED_NAME

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

To specify multiple data types, repeat the option. Alternatively, you can do one of the following:

  • Use shell patterns similar to the patterns used with -select-arxml-files and -select-source-files.

    For examples, see Select AUTOSAR XML (ARXML) and Code Files for Polyspace Analysis.

  • 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:

      -autosar-datatype pkg.datatypes.type

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

      -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:

      -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 the issue happens. To convert to a warning, use -Eno-autosar-xmlReaderSameUuidForDifferentElements. For conflicting UUID-s, 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-s), use these options to toggle between a warning and an error.

The default analysis stops with an error if the issue happens. To convert to a warning, use -Eno-autosar-xmlReaderTooManyUuids. For conflicting UUID-s, 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

OptionDescription
-include PREINCLUDE_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.

If you specify only a file name, the file must be present in the folder from which the command is run. To specify files in other folders, provide their full paths or relative paths from the current folder.

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. If you change the file contents, you must rerun the code extraction and subsequent parts of the analysis.

To specify several files, enter the option once for each file, for instance, -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 INCLUDE_FOLDER

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:

-extra-project-options "-I INCLUDE_FOLDER"

-D DEFINE

Specify macros that the analysis must consider as defined.

For instance, if you specify:

-D _WIN32
the preprocessor conditional #ifdef _WIN32 succeeds and the corresponding branch is executed.

-U UNDEFINE

Specify macros that the analysis must consider as undefined.

For instance, if you specify:

-U _WIN32
the preprocessor conditional #ifndef _WIN32 succeeds and the corresponding branch is executed.

Options to control Code Prover checks

OptionDescription
-extra-project-options POLYSPACE_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 you use with the polyspace-code-prover or polyspace-code-prover-server command. 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:

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

Note that these options of polyspace-code-prover do not need to be specified:

  • -sources: polyspace-autosar extracts the required source files.

  • -I: You specify include folders with the -I option of polyspace-autosar.

  • Inputs and Stubbing options such as -data-range-specifications: External data constraints in your ARXML files are extracted automatically with polyspace-autosar. You cannot specify constraints explicitly.

  • Multitasking options such as -entry-points: You cannot perform a multitasking analysis with polyspace-autosar. To detect data races, create a separate project for the entire application and explicitly add your source folders. Specify the ARXML files relevant for multitasking and run Bug Finder. For more information, see ARXML files selection (-autosar-multitasking).

  • Code Prover Verification options associated with main generation: A main function is generated (in the file psar_prove_main.c) when you create a Polyspace project from an AUTOSAR description. The main function calls functions that implement runnable entities in the software components. The generated main is needed for the Code Prover analysis. You cannot change the properties of this main function.

-extra-options-file OPTIONS_FILE

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 polyspace-configure and generate an options file for subsequent Code Prover analysis. Suppress inclusion of sources in the options file with the -no-sources option.

    polyspace-configure -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.

    polyspace-autosar ... -extra-options-file options.txt

See also Run Polyspace on AUTOSAR Code Using Build Command.

-show-prove AUTOSAR_QUALIFIED_NAME

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

Version History

Introduced in R2018a

See Also

| | |

Topics