False negatives for MISRA 9.3 missed for float array partial initialization

Hello,

Initializing an array of float in the following way:

float array_a[10] = { 0.0 };

should raise the MISRA violation 9.3, that forbids partial array initialization. However the polyspace code prover is not detecting this

violation. Please confirm if this is a false negative or some other issue. Thanks in advance.

https://forum.misra.org.uk/thread-1357.html

Related to the question here:

https://de.mathworks.com/matlabcentral/answers/1773835-false-positive-candidate-rule-10-3-for-float-array-zero-initialization

Answer 1

[Christian Bard]

That is a specific Polyspace implementation of the rule 9.3. We have extended the exception 1 of the rule 9.3 with 0.0 and 0.0f.

[David Sosa]

Thanks for you reply. Could you provide a small justification on why this is fine?

[Christian Bard]

Amplification of the rule is about to initialize all elements of the array as soon as explicitely one is initialized. Exception applies on 0 and it looks like that float array_f[10] = { 0 }; is compliant but not float array_f[10] = { 0.0f }; Same for double array_d[10] = { 0 }; but not for double array_d[10] = {0.0};

From my stand point, not including 0.0 and 0.0f is really a very strict application of the rule because almost all compilers will mostly generate same assembly code for 0, 0.0 and 0.0f. Including 0.0 and 0.0f do not go against its rationale.

[David Sosa]

Ok. I understand the your rationale. Thanks for the detailed reply.