Spinroot

A forum for Spin users

You are not logged in.

#1 2011-05-12 11:45:26

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Scope for labels again

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

#2 2011-05-13 03:31:37

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

Re: Scope for labels again

I'll look into it!

Offline

#3 2011-08-06 19:11:42

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

Re: Scope for labels again

this will be fixed in the next release of Spin (likely version 6.1.1)

Offline

#4 2012-10-26 19:57:19

dschumann
Member
Registered: 2012-10-26
Posts: 3

Re: Scope for labels again

I can confirm this works great in 6.2 and is extremely useful

Offline

Board footer

Powered by FluxBB