Polyspace "Maximum Stack Usage" calculation on ARM systems wrong

Hi,

I'm wonder about the Maximum Stack Usage results in Polyspace, because they are not divisible by 4, e.g.73 bytes. I've configured -align=32 and -target=arm but this does not help. I'm pretty sure that the target compiler is using for stack allocation always 4 bytes, even if I use a byte, because of architecture needs.

I'm missing some configuration in Polyspace?

Thank you in advance.

Best Mario

Answer 1

[Anirban]

Hi,

-target=arm uses these settings (for the armcc compiler for instance):

https://www.mathworks.com/help/bugfinder/ref/armv5compilercompilerarmcc.html

As you can see, char is 1 byte for this target. The alignment applies only to char-s embedded in a structure and not to isolated char-s. Let's take this example:

typedef struct {
    char charVal;
    int intVal;
}Record;

Record globalRecord;

void init (void) {
    Record localRecord = globalRecord;
}

Here, if you calculate stack usage of the function init with these options:

 -main-generator -main-generator-calls unused -align 8 -stack-usage
 

You see that the stack usage is 5 (char = 1 + int = 4).

If you change to:

 -main-generator -main-generator-calls unused -align 32 -stack-usage
 

You see that the stack usage is 8 (multiple of 4, as you expect). 3 additional bytes were added as padding for storage.

But in either case, if there is an individual char not embedded in an aggregate type, it contributes 1 byte. The requirement for alignment does not apply.