Why do I get the red check "Illegally dereferenced pointer" in Polyspace Code Prover when attempting to set a buffer for a pointer to a struct?

Given is a struct with the following definition,

struct
{
    uint8 myfield1[2U];
    uint8 myfield2;
    uint8 myfield3[2U];
    uint8 myfield4;
    uint8 myfield5[2U];
} my_struct;

 

Then, a pointer to an instance of this struct is created and assigned to have a buffer size of, namely,

 

uint8 buffer_size[9];
pMyStruct = (my_struct*)&buffer_size; 

 

Since the struct 'my_struct' should occupy 7 bytes and the buffer size is 9, there should be no such red check asserted from Polyspace Code Prover in this case.

Why do I get the red check "Illegally dereferenced pointer" in Polyspace Code Prover when attempting to set a buffer for a pointer to a struct?

Answer 1

[MathWorks Support Team]

This issue is a result of packing of structures in C, see the following thread,

https://stackoverflow.com/questions/4306186/structure-padding-and-packing

Therefore, the actual size of the struct 'my_struct' is 12 due to the padding that it is assumed by Polyspace Code Prover. The red check that Polyspace asserts then makes sense, given that the buffer of the pointer that points to this struct is set to a size of 9 bytes.

Please check if the actual compiler supports packing of structs. If so, then please enable the option "Allow partial allocation of structures" that can be found under the tab "Code Prover Verification" -> "Check Behavior" -> "Pointer" in Polyspace Configuration, to have Polyspace not assert this red check, see the following documentation for more information,

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

If the compiler does not pack the structs in the way mentioned above, then your code will result in an error due to buffer size mismatch.