A forum for Spin users
You are not logged in.
Pages: 1
I have one more question.
I tried to use 'embedded c code' in SPIN version 6.
active proctype ex1()
{ int x;
do
:: c_expr { Pex1->x < 10 } ->
c_code { Pex1->x++; }
:: x < 10 -> x++
:: else -> break
od
}
% spin -a -v ccode.pml
% gcc -o pan pan.c
In file included from pan.c:5259:
pan.m: In function ‘do_transit’:
pan.m:22: error: ‘P0’ has no member named ‘x’
pan.m:31: error: ‘P0’ has no member named ‘x’
In pan.h file, variable x is prefixed by '_1_'.
typedef struct P0 { /* ex1 */
unsigned _pid : 8; /* 0..255 */
unsigned _t : 2; /* proctype */
unsigned _p : 5; /* state */
int _1_x;
} P0;
That is effected by the new scoping rule, I'm just guessing.
When SPIN runs with the option -O, it compiles successfully.
Is such a reference 'Pex1->x' in c_code unavailable in SPIN6's new scoping rule?
Offline
yes -- good observation
you can either use the name of x as it is disambiguated in the pan.h file,
or, perhaps better in this case, revert to the original scope rules, using
spin -O -a model.pml
(where the O is a capital O, not a zero)
Offline
Pages: 1