Buffer size allocation

When declaring an array of type USINT32 (typedef'd to unsigned long): USINT32 buffer[512] and passing the array as a function argument, the size of that buffer, according to polyspace, is dependent on the size of a char (as defined in the target settings). In the target settings, a long is defined as 32 bits. This would indicate the above buffer would contain 512*4=2048 bytes. This is however only the case when the size of a char is set to 8 bits. If setting the size of a char to 16 bit in the target settings, polyspace will indicate the size of the buffer to be 1024 bytes, even though the size setting of char should not have influence on the size of the buffer. Could you clarify this behaviour for me?

Another issue I run into is that when checking the result settings from within polyspace, the target settings are not displayed correctly. They will show the current settings from the project manager, and not the settings as used in the verification. Neither is the correct name of the generic target displayed (it always displays mcpu). Thank you!

Answer 1

[Walter Roberson]

C has no specific "byte" data type. A "byte" in C is the size of char, and the size of everything else is measured in units of the size of char. 1024 16-bit bytes is the same amount of storage as 2048 8-bit bytes.

In computers, "byte" is not defined as 8 bits: it is instead approximately "the smallest naturally-addressable storage unit". "Naturally addressable" here is distinguished from the possibility that the computer might have special instructions able to access smaller units (such as bits or nibbles).

In the late 1970's to early 1980's, it looked for a time as if 9-bit bytes were going to become predominant, as DEC and Honeywell had some fairly advanced systems that used 9 bit bytes.

Answer 2

[Alexandre De Barros]

Hi!

There is indeed a problem in the tooltip with the size in bytes of pointers when the size of char is 16 bits.

In the example above, the size should be 2 bytes, not 4.

There is an EBR (External Bug Report) on our website:

http://www.mathworks.com/support/bugreports/818994

Answer 3

[Guy Rigot]

Hi Walter, thanks for your comment. This however does not answer my question. Please let me clarify. The platform I work on only uses 32 bit primitives, even a char is 32 bits long, this is however not settable in polyspace, so I have set it to 16 bits.

I have defined a buffer as USINT32 data[1013]. like I said the USINT32 is typedefd to unsigned long. In the target settings a long is set to 32 bits. Now, when char is set to 8 bits in target settings, Polyspace tells me about the pointer to the buffer:

parameter data (pointer to unsigned int 32, size: 32 bits):
  pointer is not null
  points to 4 bytes at offset 0 in buffer of 4052 bytes, so is within bounds (if memory is allocated)

When the char size is to 16 bits, polyspace tells me the following:

parameter data (pointer to unsigned int 32, size: 32 bits):
    pointer is not null
    points to 4 bytes at offset 0 in buffer of 2026 bytes, so is within bounds (if memory is allocated)

I find the top statement according to my expectations (4052=1013*4), regarding the buffer size. The bottom statement is strange however in my opinion. First of all, the size of a char should not influence the size of the buffer. Or, if polyspace also defines size in units of type char (like you stated, and this would make sense here since 2026 is the number of char units in the buffer in the 16bit char case), then the statement in polyspace should be rephrased. Thanks for your effort and hope you can clear the issue for me!

[Walter Roberson]

You are right, in that context if "byte" meant character units, then in the second case it should say "points to 2 bytes".

Sorry, I don't have any further ideas; we have had very few polyspace questions come through so I do not have any product-specific background knowledge to go on.