Spinroot

A forum for Spin users

You are not logged in.

#1 2016-07-27 14:44:56

ChristianH
Member
Registered: 2015-12-02
Posts: 7

Certain Allowed Variable Names cause Compile Errors upon Verification

Hi folks,

I stumbled across some unexpected behavior when using Spin today. By accident, I defined a proctype with parameters named "start1" and "start2", which seemed to be totally OK from my perspective. The Spin syntax checker is also fine with it, however, when I tried to run the verifier on my model, I received an bunch of strange looking errors:

pan.h:416:16: error: expected identifier before numeric constant
 #define start2 0 /* np_ */
                ^
pan.c:24:45: note: in definition of macro ‘Offsetof’
 #define Offsetof(X, Y) ((ulong)(&(((X *)0)->Y)))
                                             ^
pan.h:175:41: note: in expansion of macro ‘start2’
 #define Air1 (sizeof(P1) - Offsetof(P1, start2) - 1*sizeof(int))
                                         ^
pan.c:524:40: note: in expansion of macro ‘Air1’
 short Air[] = {  (short) Air0, (short) Air1, (short) Air2 };
                                        ^
In file included from pan.c:31:0:
pan.c: In function ‘addproc’:
pan.h:417:16: error: expected identifier before numeric constant
 #define start1 1
                ^
pan.c:816:20: note: in expansion of macro ‘start1’
   ((P1 *)pptr(h))->start1 = par0;
                    ^
pan.h:416:16: error: expected identifier before numeric constant
 #define start2 0 /* np_ */
                ^
pan.c:817:20: note: in expansion of macro ‘start2’
   ((P1 *)pptr(h))->start2 = par1;
                    ^
pan.c: In function ‘c_locals’:
pan.h:417:16: error: expected identifier before numeric constant
 #define start1 1
                ^
pan.c:13964:52: note: in expansion of macro ‘start1’
  printf(" int    start1: %d\n", ((P1 *)pptr(pid))->start1);
                                                    ^
pan.h:416:16: error: expected identifier before numeric constant
 #define start2 0 /* np_ */
                ^
pan.c:13965:52: note: in expansion of macro ‘start2’
  printf(" int    start2: %d\n", ((P1 *)pptr(pid))->start2);

You can use the following minimal example to reproduce the error:

init{
	run someProc(1,2);
}

proctype someProc(int start1; int start2){
	skip;
}

So, what's the problem here? As it turns out, Spin generates the following Macros in pan.h:

#define start2	0 /* np_ */
#define start1	1

and these Macros interfere with the variables that are generated for the parameters that I used in my model. I guess that there are more macros that your variable names might interfere with. Thus, whenever you encounter such errors, consider renaming the variables and parameters that the C preprocessor complains about when trying to expand macros. I hope this post helps some people saving some time :-).

In addition, it might be worth renaming those macros in future versions using some less common names, for example, by prefixing them with "Spin__Macro__" or something like this.

Cheers,

Christian

Offline

#2 2016-08-27 21:14:44

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

Re: Certain Allowed Variable Names cause Compile Errors upon Verification

Thanks for the bug report. A name-clash with internal variable names.
I've changed more of the internally used names to use a leading underscore.
Will be included in 6.4.6.

Offline

Board footer

Powered by FluxBB