There could one of two things going on:
- 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.
- 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.
