replay erros when using embedded C

yuchoi · 2012-02-06 08:56:12

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

spinroot · 2012-02-07 01:41:22

did you remember to use c_track statements to track all the relevant state information?
(i.e., the values of act_count and act_max clearly have state information that should be tracked by the model checker).
much of this is discussed in some detail in the book and in the feaver user guide....
even with all that -- it can be tough setting this up, but when it works it can be very powerful

yuchoi · 2012-02-07 03:33:54

I did use c_track for those variables as I indicated in my question.

spinroot · 2012-02-07 05:13:06

sorry i missed that -- in general if a counter-example cannot be replayed it is because of missing c_track statements.
check the first statement in the trace that on replay cannot be executed -- that typically contains a variable that wasn't tracked...

Spinroot

#1 2012-02-06 08:56:12

replay erros when using embedded C

#2 2012-02-07 01:41:22

Re: replay erros when using embedded C

#3 2012-02-07 03:33:54

Re: replay erros when using embedded C

#4 2012-02-07 05:13:06

Re: replay erros when using embedded C

Board footer