Why do I get an Illegally Deferenced Pointer red check in Polyspace Code Prover when performing pointer arithmetics using a field of a struct?

It is sought to use the field of a struct to perform pointer arithmetics within the struct and access other elements of the struct. This workflow is demonstrated using function 'foo()' in the code snippet below,

 

// Define structure
typedef struct
{
    unsigned char myfield1;
    unsigned char myfield2;
    unsigned char myfield3;
} mystruct;

// Instantiate structure
mystruct mystructinst;

// Function where fields of the struct are accessed using pointer arithmetics
void foo(const unsigned char* inp)
{
    unsigned char dest[3];
    *(&dest[0]) = *(&inp[0]);
    *(&dest[1]) = *(&inp[1]);
    *(&dest[2]) = *(&inp[2]);
}

// Provide calling context for the function foo
void goo() {
   foo(&mystructinst.myfield1);
}

When performing Polyspace Code Prover analysis on the latter file, then an Illegally Dereferenced Pointer (IDP) red check is asserted, see the following screenshot,

Why do I get an Illegally Deferenced Pointer red check in Polyspace Code Prover when performing pointer arithmetics using a field of a struct?

Answer 1

[MathWorks Support Team]

In this case the adress of the first field of struct 'mystructinst.myfield1' is passed as input to the stub-function 'goo()'. Polyspace Code Prover at this point cannot ensure that the fields are continuously stored in memory regarding the struct 'mystructinst' and thus asserts this IDP red check, as 'inp[1]' is thought as being out of bound. The fields of a struct can be stored in the memory using padding among other, thus it can be that they are not stored continuously in memory.

If one is sure that the fields of the struct are continuously stored in memory when the code is compiled, then there are two workflows that would allow this red IDP check to diappear:

Workaround 1:

Please consider enabling option "Enable pointer arithmetic accross fields" under the section "Pointer" in the tab "Code Prover Verification" -> "Check Behavior" which would allow Polyspace to consider that the fields of the struct are continuously stored in memory and thus not assert the latter red IDP, see the following screenshot,

Please note that this option is beneficial only when all the datatypes of the fields in the struct are the same, i.e. when no padding maybe added by the compiler. For this option, please refer to our documentation page,

https://de.mathworks.com/help/codeprover/ref/enablepointerarithmeticacrossfieldsallowptrarithonstruct.html

where it is mentioned the following:

 

"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."

Please take into consideration the latter note before using this option.

Workaround 2:

This workaround is invasive to the code, meaning that the code has to be motified. Accordigly, please consider using the address of the struct instead of the address of an element of the struct in the stub function 'goo()' in this case, namely,

void goo() {
   foo(&mystructinst);
}

This way Polyspace will be able to tell that the fields of the struct are continuously stored in memory, thus not asserting the latter IDP red check without the need of activating the latter option as in Workaround 1.