A forum for Spin users
You are not logged in.
Pages: 1
Hi Gerard,
Thanks for the update of Spin 6.1.0 that fixed the problem I raised last time:
inline test_inline(a)
{
test_inline1(a);
assert(a == 1);
goto Return;
Return:
a = 1;
}
inline test_inline1(a)
{
goto Return;
Return:
a = 2;
}
active proctype test()
{
int a = 0;
test_inline(a);
}
But I still got problem on the labels declared in an inline. Basically I hope to call an inline more than once in a process, like below:
inline test_inline(a)
{
assert(a == 1);
goto Return;
Return:
a = 1;
}
active proctype test()
{
int a = 0;
test_inline(a);
test_inline(a);
}
SPIN rejects to compile it because of duplicate Return label:
spin: test1.pml:7, Error: label Return redeclared saw ''}' = 125'
I really hope the scoped label can be supported just like a normal variable in an inline. This makes it much simpler to extract a C function as inline. Is it possible?
Offline
I can confirm this works great in 6.2 and is extremely useful
Offline
Pages: 1