Polyspace compilation fails when it should give only a warning. How to suppress it?

I want to fix discrepancies between Poly Bug Finder and compiler used for actual program.

My options are:

-lang C

-compiler keil

-target powerpc

-c-version c99

Polyspace compilation failed on error: a void function may not return a value.

By C99 standard this is only a constraint, so it should throw only a warning, which the compiler does. Interestingly, compiler also throws hundreds of other warnings, but they don't faze Polyspace compilation and it succeeds with them.

Is there a way to suppress errors like this when compiling in Polyspace?

Answer 1

[Anirban]

What compiler are you using for actual compilation? Just trying to see why you picked -compiler keil for the Polyspace analysis.

[Wojciech]

Thank you, your hunch was correct. I'm using Arm Compiler 6 and mistakenly thought it's a part of Keil compilers. I've changed it to armclang (and target to appropriate one) and can see no discrepancies now.