Polyspace Bug Finder ignores #if when checking macro values.

I'm running a Polyspace Bug Finder analysis on some CPP code, with the following macro defined (via Configuration -> Macros):

CPU_FAMILY=I80X86

A header file from a library I'm using has the following:

#if     CPU_FAMILY==MC680X0
#include <arch/mc68k/excMc68kLib.h>
#endif  /* CPU_FAMILY==MC680X0 */

When analysing, I get the warning:

Warning: could not find include file "arch/Mc68kLIb.h"

It's correct that I don't have this header file, but the line should never have been parsed, due to the #if.

Please can someone tell me what I'm doing wrong?

Thanks.

Martin

Answer 1

[Anirban]

There could one of two things going on:

1. MC680X0 and I80X86 are not defined in the code provided to Polyspace. You are probably missing paths to some compiler headers in the Polyspace project.
2. CPU_FAMILY is #define-d to MC680X0 in the code provided to Polyspace.

I explain the cases in detail below.

Case 1: MC680X0 and I80X86 are not defined

Let me give you an example. If you verify this code:

#if CPU_FAMILY==MC680X0
#include <arch/mc68k/excMc68kLib.h>
#endif

void main() {
    int j = 1;
    int k = j;
}

With the macro definition CPU_FAMILY=I80X86, you will see the replacement happening in the results, that is, you will see something like: #if I80X86==MC680X0. But the #include is not preprocessed out. This is because Code Prover has no knowledge of what I80X86 and MC680X0 are. #if does essentially integer comparisons, so unless I80X86 and MC680X0 are defined, Code Prover will not be able to do the comparison. You can check this by changing the code a bit to define those two macros. Like below:

#define MC680X0 1
#define I80X86 2

#if CPU_FAMILY==MC680X0
#include <arch/mc68k/excMc68kLib.h>
#endif

void main() {
    int j = 1;
    int k = j;
}

You will see that the #if comparison now works and the #include is preprocessed out.

Somewhere, in your compiler headers, the macros I80X86 and MC680X0 must be defined (which is how the #if-s will work). Somehow, in the way you set up the Polyspace project, those compiler headers did not get provided. So, for Polyspace, I80X86 and MC680X0 are two opaque things.

Case 2: CPU_FAMILY defined in headers

If CPU_FAMILY is defined in your headers to MC680X0, it will override your macro definition in the configuration. To check this, you can verify this code by setting CPU_FAMILY=I80X86:

#define MC680X0 1
#define I80X86 2

#define CPU_FAMILY MC680X0

#if CPU_FAMILY==MC680X0
#include <arch/mc68k/excMc68kLib.h>
#endif

void main() {
    int j = 1;
    int k = j;
}

You will see that the macro CPU_FAMILY takes the value defined in the code and not in the configuration.

[Martin Walker]

Hi Anirban,

Thank you for the detailed answer. Sorry for the delay getting back to you on it.

Using the modifications for Case 1, the problem goes away, showing that I must be missing those definitions. I will attempt to find them somewhere within the library and make sure they are included. I will mark your answer as the accepted one. Thanks again.

Martin