Main Content

Specify sources and sinks (-impact-specifications)

Specify XML file that identifies program elements as sources and sinks for impact analysis

Since R2023b

Description

This option affects a Code Prover analysis only.

Specify source-sink pairs in XML format for impact analysis in Code Prover. If you designate a pair of objects as source and sink and enable impact analysis, Code Prover can prove if the source has no impact on the sink.

The XML file for specifying sources and sinks assigns ID-s to variables or function arguments or function parameters, and then lists impact expectations using a pair of ID-s. For instance:

<no-impact source="air_density_calibration" sink="display_x_pos" />
specifies that a variable with an ID of air_density_calibration is not expected to impact another variable with an ID of display_x_pos.

For more information on how to assign id-s, see the sample specification file polyspaceroot\polyspace\verifier\cxx\impact-specifications-template.xml.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Run Time Errors > Check Behavior node.

Command line and options file: Use the option -impact-analysis. See Command-Line Information.

Why Use This Option

If you want certain variables in your program to be unrelated to certain other variables, you can enable impact analysis in Code Prover. For instance, you might want outputs from certain AUTOSAR software components to be completely unrelated to certain inputs. You can list all input/output pairs where you expect no impact between the inputs and outputs and check if your program meets this design specification.

Settings

Enter the path to the XML file that specifies the sources and sinks for impact analysis.

Dependencies

This option is available only if you enable impact analysis using the option Enable impact analysis (-impact-analysis).

Command-Line Information

Parameter: -impact-specifications
Value: Path to sourcesAndSinks.xml
Default: Off
Example (Code Prover): polyspace-code-prover -sources file_name -impact-analysis -impact-specifications sourcesAndSinks.xml
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -impact-analysis -impact-specifications sourcesAndSinks.xml

Version History

Introduced in R2023b

See Also

| | |

Topics