A forum for Spin users
You are not logged in.
Pages: 1
Hello
I have a problem concerning inline macros and spin 6.01. I used to pass a whole array to an inline macro such that recurring work could be done there. But spin 6.0.1 doesn't let me pass a whole array anymore, but requires a specific element. Is there a way how I can still pass a whole array to an inline macro?
Kind regards
Here is a minimal example, which works in spin 5.2.5 but not with spin 6.0.1
mtype {start, end};
chan chs[2]=[1] of {mtype, byte};
inline parallelsplit(chs_out, num_out, msg, id) {
byte i;
i=0;
do
:: i< num_out ->
chs_out[i]!msg,id;
i++;
:: i== num_out ->
i=0;
break;
od;
}
active proctype A() {
mtype msg; byte id;
msg = start;
id=1;
parallelsplit(chs, 2, msg, id);
}
Spin 6.0.1 finds the following error:
spin: test.pml:21, Error: missing array index for 'chs' saw '',' = 44'
Offline
you're right. it's a bit unfortunate, but indeed you cannot use an incomplete reference anymore.
the only way around it that i can think of would be to write the inline as a macro, but that's not very pretty of course.
Offline
Hi,
This restriction will remain in future versions of SPIN?
Offline
Hi,
Since my question is similar to miss_mare's, I post my question here. I use Spin 6.2.6.
As he said, I pass a whole array and meet "spin: test.pml:11, Error: missing array index for ...".
int a[3];
inline foo(b) {
printf("a[1]==%d\n",b[1]);
}
active proctype main() {
a[0]=0;
a[1]=1;
a[2]=2;
foo(a);
}
But, Spin looks to run normally with the error message in simulation mode.
a[1]==1
1 process created
and generate pan.c in verification mode.
Also, I see a specification
http://spinroot.com/spin/Man/inline.html
A whole array looks to be passed for me.
Could you tell me which I shouldn't pass a whole array in current version?
(To pass a whole array is so useful.)
If I can use it with the error message, is there anything I should take care of?
Offline
The warning is issued for the use of the array basename 'a' in the inline call to foo(a).
Generally, that would be an error since it uses a is if it were a scalar, instead of an array.
With spin -I model.pml you can check though that the conversion does happen as you likely intended, and it generates a correct pan.c.
So in this case it is safe to ignore the warning/error message.
Offline
Thank you so much for the quick response.
I will try "spin -I" and check it.
Offline
Pages: 1