Spinroot

Hi,

I have been experimenting with embedded C on a relatively large-sized C code.
The idea of directly embedding C code into Promela model is great, but it hasn't been easy to understand its analysis result.

Here is the code fragment that made me confused.
---------------------------------------------------------------------------
  c_code{ act_count = tpl_dyn_proc_table[Ptask_manager->task_id]->activate_count;
               act_max =  tpl_stat_proc_table[Ptask_manager->task_id]->max_activate_count;

               printf(" act_count = %d, act_max = %d \n", act_count, act_max);
   };
       
  if
  :: c_expr{act_count < act_max}
                  -> c_code{ printf(" ------------------ OK --------------- \n");};
  :: else ->    c_code{ printf(" ------------------ NOT OK: %d >= %d --------------- \n",tpl_dyn_proc_table[Ptask_manager->task_id]->activate_count,         
                                                                                                                          tpl_stat_proc_table[Ptask_manager->task_id]->max_activate_count  );};
  fi;
------------------------------------------------------------------------------------

A counter-example trace reports the following case:
       ...
       act_count = 5, act_max = 5
       ------------------ OK -------------------
       ...
which is inconsistent with the code, since act_count is not less than act_max, it should print out "NOT OK", instead of "OK".
The related error message was like this:
"pan: error, next transition UNEXECUTABLE on replay
     most likely causes: missing c_track statements
       or illegal side-effects in c_expr statements"

but, I could not figure out what is wrong in the model since  act_count, act_max, tpl_dyn_proc_table, tpl_stat_proc_table are all traced using c_track statement and
I do not see illegal side-effects in c_expr statements. 

Any hint would be greatly appreciated,

Yunja