Spinroot

A forum for Spin users

You are not logged in.

#1 2011-03-11 15:00:45

miss_mare
Member
Registered: 2011-03-11
Posts: 1

Passing array to an inline macro

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

#2 2011-03-11 23:30:39

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Passing array to an inline macro

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

#3 2011-07-21 11:46:39

João Martins
Member
Registered: 2011-05-18
Posts: 4

Re: Passing array to an inline macro

Hi,

This restriction will remain in future versions of SPIN?

Offline

#4 2011-07-21 16:04:44

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Passing array to an inline macro

you're right that currently there's no plan to change this. sorry!

Offline

#5 2014-03-26 08:35:27

abet
Member
Registered: 2014-02-28
Posts: 14

Re: Passing array to an inline macro

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

#6 2014-03-27 05:17:22

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Passing array to an inline macro

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

#7 2014-03-27 09:27:56

abet
Member
Registered: 2014-02-28
Posts: 14

Re: Passing array to an inline macro

Thank you so much for the quick response.
I will try "spin -I" and check it.

Offline

Board footer

Powered by FluxBB