A forum for Spin users
You are not logged in.
Pages: 1
hi!
I have some doubts about the c_code. I have a piece of promela code with C code embedded in, but it didn't work without the -a option:
int i, j;
proctype test(int a) {
int ilocal;
progress:
i = 0;
do
:: i < a ->
i++;
printf("i = %d\n", i);
c_code {
now.i++;
Ptest->ilocal = 1478;
now.j = 8741;
};
assert(ilocal == 1478 && j == 8741);
printf("after c_code i = %d\n", i);
:: else -> break;
od
}
init {
run test(15);
}
When i simulate the code by iSpin, it reports an access violation as bellow:
7: proc 1 (test) a.pml:15 (state 5) [{c_code1}]
spin: a.pml:16, Error: assertion violated
spin: text of failed assertion: assert(((ilocal==1478)&&(j==8741)))
It seems that the embedded C code not run at all, please help me.
Thanks.
Pages: 1