Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » accessing embedded c code variables from the promela code » 2011-05-25 13:36:45

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.

Board footer

Powered by FluxBB