Polyspace: Defines-Handling not correct?

Hi, i hv sepecified somme defines in the optionsfile: -D CPU=2; -D CPU_SLAVE=2; -D CPU_MASTER=1; -D PLATFORM=2

Also i hv a function with some code:

void base_mt_register(void)
{
#if (CPU == CPU_SLAVE)
  RegisterMeasGroup("M_IN_SL", meas_in_table, MEAS_GRP_IN, base_meas_in_t);
  RegisterMeasGroup("M_CORE_SL", meas_core_table, MEAS_GRP_CORE, meas_core_t);
  RegisterMeasGroup("M_OUT_SL", meas_out_table, MEAS_GRP_OUT, meas_out_t);
#endif

#if (CPU == CPU_MASTER)
  RegisterMeasGroup("M_CORE_MA", meas_core_table, MEAS_GRP_CORE_MA, meas_core_t);
  RegisterMeasGroup("M_OUT_MA", meas_out_table, MEAS_GRP_OUT_MA, meas_out_t);
#endif
  return;
}

RegisterMeasGroup(...) is also a define: RegisterMeasGroupBlabla(...)

PS told me now that M_CORE_MA is undefined!? But this code should never be verified? In the corresponding ci file the function looks like this (which is wrong!?):

 void base_mt_register(void)
{
...many blank lines....

RegisterMeasGroupBlabla( "M_CORE_MA", meas_core_table, MEAS_GRP_CORE_MA, sizeof(meas_core_t), sizeof(meas_core_table) / sizeof(struct symbol_info), "test.c", __func__, 130);
RegisterMeasGroupBlabla( "M_OUT_MA", meas_out_table, MEAS_GRP_OUT_MA, sizeof(meas_out_t), sizeof(meas_out_table) / sizeof(struct symbol_info), "test.c", __func__, 131);

return;
}

Why PS execute this code? I think PS hv a problem with defines/macros!

Maybe you can please help me? Best regards Thomas

Answer 1

[Christian Bard]

Dear Thomas, with current version of Polyspace Code Prover (for instance R2014b) and default options, it works as expected.

[Thomas]

Hello, certainly it works on R2014b - but I'm using R2013a instead. At R2013 it works also - after I've founded the "problem". For this case I've printed the defines on some code segments. The problem was more complicated:

1. there was an (wrong) existing (master)headerfile, which overwrote the cpu-define
2. the (then) necessary additional (master)headerfile was missing - correct

-> the defines were not defined, which was correct.

Regards Thomas