Spinroot

A forum for Spin users

You are not logged in.

#1 2016-07-27 15:00:37

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

Offline

#2 2016-08-27 21:01:34

spinroot
forum
Registered: 2010-11-18
Posts: 695
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.)

Offline

Board footer

Powered by FluxBB