Main Content

Event and Memory Zone Specifications for Impact Analysis in Polyspace Code Prover

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 an 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).

You can define variables and function arguments (or return value) as sources and sinks for impact analysis. See Source and Sink Specifications for Impact Analysis in Polyspace Code Prover. When specifying sources and sinks, you can detail the following information:

  • Specific events associated with a source or sink (required).

    For instance, you can specify that a variable acts as a sink only when its value is read.

  • Memory zones associated with a source or sink (optional).

    For instance, for a variable of structured type, you can specify that only one particular field acts as a sink.

  • What constitutes an impact on a sink (optional) – the value of the sink or the reachability of an event associated with the sink.

This topic shows how to specify events, memory zones, and dependencies for impact analysis in Polyspace Code Prover. For more information on the impact analysis workflow, see Prove Absence of Impact Between Objects in C/C++ Program.

Event Specification

The event that you can associate with an impact-source or impact-sink depends on whether the source or the sink is a variable or function argument.

Variables

A typical variable specification looks like the following:

<variable>
  <match>
    <match-declaration>
      <match-qualified-name value="airVolumicMassDensity"/>
    </match-declaration>
  </match>
  <impact-source id="Air Mass Density Reading" event="onRead"/>
</variable>
This source specification with an id of Air Mass Density Reading defines an impact-source that matches the variable airVolumicMassDensity. The event onRead is associated with this specification, which means that each time the variable airVolumicMassDensity is read, Code Prover considers the read as the beginning of a data or control flow. For instance, if you used the following impact specification, Code Prover detects an impact if there is a data or control flow beginning from the read of the variable airVolumicMassDensity.
<impact source=""Air Mass Density Reading" sink="x Position Display" />

EventDescription
onReadData or control flow begins or ends at variable read depending on whether the variable is a source or sink.
onWriteData or control flow begins or ends at variable write depending on whether the variable is a source or sink.
onReadOrWriteData or control flow begins at variable use (read or write) depending on whether the variable is a source or sink.

Functions

A typical function specification looks like the following:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="x Position Display" event="onCallEntry" memory="(Argument (Function) 0)"/>
</function>
This sink specification with an id of x Position Display defines an impact-sink that matches the function with name writeToDisplay. The event onCallEntry is associated with this specification, which means that each time the function writeToDisplay is called, Code Prover considers the call as the end of a data or control flow. For instance, if you used the following impact specification, Code Prover detects an impact if there is a data or control flow ending at the call to the function writeToDisplay.
<impact source=""Air Mass Density Reading" sink="x Position Display" />

EventDescription
onCallEntry

  • If the function is an impact source, data or control flow begins at the function call.

  • If the function is an impact sink, data or control flow ends at the function call.

onCallReturn

  • If the function is an impact source, data or control flow begins when the function returns to its caller.

  • If the function is an impact sink, data or control flow ends when the function returns to its caller.

onStart

  • If the function is an impact source, data or control flow begins at the start of the function definition.

  • If the function is an impact sink, data or control flow ends at the start of the function definition.

onReturn

  • If the function is an impact source, data or control flow begins at the end of the function definition.

  • If the function is an impact sink, data or control flow ends at the end of the function definition.

Memory Specification

Instead of specifying an entire variable or function as a source or sink, you can specify that only part of the memory zone that matches the variable or function must act as source or sink.

For instance, the following specification states that the first argument of the function writeToDisplay must act as an impact sink:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="x Position Display" event="onCallEntry" memory="(Argument (Function) 0)"/>
</function>
If the first argument of the function is a pointer, you can specify the value it points to as the sink by changing the specification to:
<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="x Position Display" event="onCallEntry" memory="(Indirect (Argument (Function) 0))"/>
</function>

The following table lists the ways to specify parts of a memory zone in an impact specification file. If you skip the memory attribute, the effect is the same as specifying memory="(Variable)".

SpecificationDescription
(Variable)

The entire variable.

(Return(Function))

The function return value

For example, to specify that the return value of the function writeToDisplay must act as a sink, use the following specification:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="x Position Display" event="onCallReturn" memory="(Return(Function))"/>
</function>
(Argument (Function) n)

The (n + 1)-th function argument

For example, to specify that the first argument of the function writeToDisplay must act as a sink, use the following specification:

<function>
  <match>
    <match-declaration>
       <match-qualified-name value="writeToDisplay"/>
    </match-declaration>
  </match>
  <impact-sink id="x Position Display" event="onCallEntry" memory="(Argument (Function) 0)"/>
</function>

Use the event attribute to specify where the impact flow begins or ends. For instance, instead of the function call, you can specify the return from the function as the beginning of the impact flow.

(Indirect (ptr))

The contents of the memory zone that ptr points to

For example, to specify that the first argument of the function writeToDisplay is a pointer and the pointed memory zone must act as a sink, use the following specification:

<function>
	<match>
		<match-declaration>
			<match-qualified-name value="writeToDisplay"/>
		</match-declaration>
	</match>
	<impact-sink id="x Position Display"
	             event="onCallEntry"
	             memory="(Indirect (Argument (Function) 0))"/>
</function>
(Field (structVar) fieldName)

The field fieldName of the structured variable structVar

For example, to specify that the first argument of the function writeToDisplay is a structure and the field aField of this structure must act as a sink, use the following specification:

<function>
	<match>
		<match-declaration>
			<match-qualified-name value="writeToDisplay"/>
		</match-declaration>
	</match>
	<impact-sink id="x Position Display"
	             event="onCallEntry"
	             memory="(Field (Argument (Function) 0) aField)"/>
</function>
(Array (arrayVar) (Constant idx))

The elements at index idx of the array variable arrayVar

For example, to specify that the first argument of the function writeToDisplay is an array and the first element of this array must act as a sink, use the following specification:

<function>
	<match>
		<match-declaration>
			<match-qualified-name value="writeToDisplay"/>
		</match-declaration>
	</match>
	<impact-sink id="x Position Display"
	             event="onCallEntry"
	             memory="(Array (Argument (Function) 0) (Constant 0))"/>
</function>
(Array (arrayVar) (Interval (Constant beg) (Constant end)))

The elements between indices beg and end of the array variable arrayVar

For example, to specify that the first argument of the function writeToDisplay is an array and the first 10 elements of this array must act as a sink, use the following specification:

<function>
	<match>
		<match-declaration>
			<match-qualified-name value="writeToDisplay"/>
		</match-declaration>
	</match>
	<impact-sink id="x Position Display"
	             event="onCallEntry"
	             memory="(Array (Argument (Function) 0) (Interval (Constant 0) (Constant 9)))"/>
</function>
(Array (arrayVar) (Any))

All elements of the array variable arrayVar

For example, to specify that the first argument of the function writeToDisplay is an array and all elements of this array must act as a sink, use the following specification:

<function>
	<match>
		<match-declaration>
			<match-qualified-name value="writeToDisplay"/>
		</match-declaration>
	</match>
	<impact-sink id="x Position Display"
	             event="onCallEntry"
	             memory="(Array (Argument (Function) 0) (Any))"/>
</function>
(This(Function))

Pointer to base object containing the current method, in other words, the this pointer (C++ only).

For example, consider the following class:

class Number {
    public:
        void read(int x, int* y);
        int getN() {
            return N;
        }
    private:
        int N;
};
Suppose the method Number::read() is not yet defined but you want to specify that when this method is invoked, the data member Number::N of the corresponding object is modified. Suppose also that Number::N acts as an impact source following this modification. To define this source, you can enter the following specification:
<function>                
    <match>
        <match-declaration>
            <match-qualified-name value="Test::read"/>
        </match-declaration>
    </match>
    <impact-source id="readThis" 
                   event="onCallReturn" 
                   memory="(Field (Indirect (This (Function))) N)"/>
</function>

Dependency Specification

When specifying an impact sink, you can optionally add a dependency attribute to indicate what constitutes an impact on the sink – the value of the sink or the reachability of an event associated with the sink.

For instance, the following specification indicates that Code Prover must consider the variable xCoordPosition as impacted only if its value depends on the source of impact.

<variable>
  <match>
    <match-declaration>
      <match-qualified-name value="xCoordPosition"/>
    </match-declaration>
  </match>
  <impact-sink id="x Position Display" event="onWrite" dependency="data"/>
</variable>

The following table lists all possible dependencies. If you skip the dependency attribute, the effect is the same as specifying dependency="dataOrControl".

DependencyDescription
dataValue of the sink
controlWhether the sink is reached
dataOrControlValue or reachability of sink

See Also

| | | |

Related Topics