Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct)

Allow arithmetic on pointer to a structure field so that it points to another field

Description

This option affects a Code Prover analysis only.

Specify that a pointer assigned to a structure field can point outside its bounds as long as it points within the structure.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node. See Dependency for other options you must also enable.

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. See Dependency for other options you must also enable.

Command line and options file: Use the option -allow-ptr-arith-on-struct. See Command-Line Information.

Why Use This Option

Use this option to relax the check for illegally dereferenced pointers. Once you assign a pointer to a structure field, you can perform pointer arithmetic and use the result to access another structure field.

Settings

On

A pointer assigned to a structure field can point outside the bounds imposed by the field as long as it points within the structure. For instance, in the following code, unless you use this option, the verification will produce a red Illegally dereferenced pointer check:

void main(void) {
struct S {char a; char b; int c;} x;
char *ptr = &x.b;
ptr ++;
*ptr = 1; // Red on the dereference, because ptr points outside x.b
}

Off (default)

A pointer assigned to a structure field can point only within the bounds imposed by the field.

Tips

• The verification does not allow a pointer with negative offset values. This behavior occurs irrespective of whether you choose the option Enable pointer arithmetic across fields.

• Using this option can slightly increase the number of orange checks. The option relaxes the constraint that a pointer to a structure field cannot point to other fields of the structure. In exchange for relaxing this constraint, the verification loses precision on the boundary of fields within a structure and treats the structure as a whole. Pointer dereferences that were previously green can now turn orange.

  Use this option if you follow a policy of reviewing red checks only and you need to work around red checks from pointer arithmetic within a structure.

• Before using this option, consider the costs of using pointer arithmetic across different fields of a structure.

  Unlike an array, members of a structure can have different data types. For efficient storage, structures use padding to accommodate this difference. When you increment a pointer pointing to a structure member, you might not point to the next member. When you dereference this pointer, you cannot rely on what you are reading or writing to.

Dependency

This option is available only if you set Source code language (-lang) to C.

Command-Line Information

Parameter: -allow-ptr-arith-on-struct

Default: Off

Example (Code Prover): polyspace-code-prover -sources file_name -allow-ptr-arith-on-struct

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -allow-ptr-arith-on-struct