Main Content

Prove Absence of Impact Between Objects in C/C++ Program

You can use Polyspace® Code Prover™ to prove that two objects in your C/C++ program do not impact each other. If you designate the two objects as a source and a sink, a Code Prover analysis can detect if the source values impact the sink values or can prove the absence of impact. An impact occurs if there is uninterrupted data flow from the source to the sink (or if the value of the source variable determines if the sink variable acquires a specific value).

This example shows how to set up and run impact analysis in Polyspace Code Prover.

Example Files

To follow the steps in this tutorial, use the source files in the folder polyspaceroot\polyspace\examples\doc_cxx\impact_analysis. This folder contains some C source files and an XML file for impact specifications. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b.

Step 1: Define Sources, Sinks, and Expected Impact

The impact specification file, in this case, impact.xml, defines the sources and sinks in an XML format. The XML format follows this structure:

<?xml version="1.0" encoding="UTF-8"?>
<impact-specifications xmlns="http://www.mathworks.com/PolyspaceImpactSpecifications">
  <!-- Define variables that can act as source or sink>
  <variables>
      <!--Define each variable inside a 'variable' element, assign id -->
        <variable>
        </variable>
  </variables>
  <!-- Define function arguments or return values that can act as source or sink -->
  <functions>
      <!--Define each function argument or return value inside a 'function' element, assign id -->
        <function>
        </function>
  </functions>
  <!-- Define expected impact or no-impact using pairs of source-sink id-s-->
  <expect>
       <impact source="someSourceId" sink="someSinkId"/>
       <no-impact source="otherSourceId" sink="otherSinkId"/>
  </expect>
</impact-specifications>

In the XML file, inside a variable or function element, you can define a single variable or function, or a class of variables or functions. You define each variable (or class of variables) and each function (or class of functions) inside a match element and assign one or more id-s to this element.. For instance:

  • To specify that a variable airVolumicMassDensity acts as a source, you define the variable element as follows: 

    <variable>
  <match>
    <match-declaration>
      <match-qualified-name value="airVolumicMassDensity"/>
    </match-declaration>
  </match>
  <impact-source id="air density calibration" event="onRead"/>
</variable>

  • To specify that arguments of the function writeToDisplay act as sinks, you define the function element as follows: 

    <function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="display x pos" event="onCallEntry" memory="(Argument (Function) 0)"/>
  <impact-sink id="display y pos" event="onCallEntry" memory="(Argument (Function) 1)"/>
  <impact-sink id="display value" event="onCallEntry" memory="(Argument (Function) 2)"/>
</function>

You later use these id-s to define source-sink pairs in one of these elements in the XML file:

For example, if you expect that the variable airVolumicMassDensity has no impact on the first argument of the writeToDisplay function when the function is called, specify a no-impact element as follows:

<no-impact source="air density calibration" sink="display x pos" />

For a comprehensive list of syntaxes, see Source and Sink Specifications for Impact Analysis in Polyspace Code Prover.

Step 2: Specify Impact Analysis Options

You can run impact analysis in the Polyspace user interface or at the command line.

To run impact analysis, you have to specify these options:

If you are using an options file to run the analysis at the command-line, you can enter these options in the file along with other options:

-impact-analysis
-impact-specifications impact.xml
-impact-analysis-only

Step 3: Run Analysis and Review Results

To start impact analysis, after configuring the required options, run Polyspace Code Prover.

The analysis results contain outcomes of these checks:

  • Expected impact: For each impact element in your specification file with a source-sink pair, the check determines if the source had the expected impact on the sink.

    The check color is:

    • Red if there is a proven absence of impact.

    • Orange if there is a possible impact.

  • Expected absence of impact: For each no-impact element in your specification file with a source-sink pair, the check determines if the source actually had no impact on the sink.

    The check color is:

    • Green if there is a proven absence of impact.

    • Orange if there is a possible impact.

For more information on how to review the results, see Review Results of Impact Analysis in Polyspace Code Prover.

See Also

| | | |

Related Topics