A forum for Spin users
You are not logged in.
I'm using SPIN in Windows.
Today I found spin6.0 is released and tried it.
But I met compile error of pan.c.
I read pan.h and found that strange codes are generated as shown below.
S_F_MAP src_file3 [] = {
{ ""-"", 0, 0 },
・・・・
I think that description of pangen3.c line 171 is wrong.
pangen3.c
171: lastdef.name = "\"-\"";
it should be as shown below.
171: lastdef.name = "-";
With gcc, compile of the pan.c is ended successfully and
I am not familiar with the code of SPIN.
So, I might have some misunderstanding.
Offline
Thanks for this report. I think you are right and it will be corrected in 6.0.1.
You'll be interested to hear that this particular line has been in the code since version 3.2.4 from 10 January 1999 (almost 12 years).
This makes me interested to know what Spin model managed to trigger this bug, because normally this default value isn't used. Could you show the model? (Or if you don't want to show it here, please send it to [email protected])
Thanks!
Offline
I'm using SPIN to verify a firmware of an embedded xxx and
I can't show my model.
So, I made a small model which has the same error with SPIN6.0.0.
-----------------------------
chan c1 = [10] of { int };
chan c2 = [10] of { int };
active proctype proc1()
{
int msg;
do
::c1?msg->
if
::msg == 1->
c2!3;
::msg == 2->
c2!4;
fi;
od;
}
active proctype proc2()
{
int msg;
c1!1;
do
::c2?msg->
if
::msg == 3->
c1!1;
::msg == 4->
c1!2;
fi;
od;
}
-----------------------------
>You'll be interested to hear that this particular line has been in the code since version 3.2.4 from 10 January 1999 (almost 12 years).
With SPIN5.2.2, verification of the model was successfull and pan.h doesn't look wrong.
So, I think changes at 6.0.0 affects the generation rules of pan.h.
Offline
This problem is related to a bug. I had to deal with a similar situation three months back. I had sought the help of a friend of mine who is a spin expert. He told me that it was a bug and he was able to fix it for me. Anyway it is reassuring to note that the new version is free of such problems.
Offline