Spinroot

ChristianH

Member

Registered: 2015-12-02

Posts: 7

Run in InitExpression of Variable Declaration causes Compile Errors

Hi folks,

I potentially found a bug in Spin today. Consider the following minimal example:

init{
	byte childPid = run SomeProc();
	assert(childPid == 1);
}

proctype SomeProc(){
	skip;
}

This model is syntactically correct (as confirmed by spin) and it violates none of the restrictions for the run-expression mentioned on the man pages. However, as it turns out, this model is not translated into compilable C-code by Spin leading to the following compile error:

pan.c: In function ‘addproc’:
pan.c:830:39: error: ‘II’ undeclared (first use in this function)
   ((P0 *)pptr(h))->childPid = addproc(II, 1, 1);
                                       ^

I guess this should be fixed.

By the way, the example compiles (and verifies) correctly if we do not use run in the init expression for the variable childPid (i.e., declaring childPid first and then using the run expression as right-hand side of an assignment).

Cheers,
Christian

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Run in InitExpression of Variable Declaration causes Compile Errors

Good find!  Using 'run' in a variable initialization is unexpected.
In the next release (6.4.6) it'll be flagged as an error. (It's too hard to make it work.)