Spinroot

A forum for Spin users

You are not logged in.

#1 2010-12-15 09:11:40

sekky
Member
Registered: 2010-12-15
Posts: 2

Compile Error of pan.c generated by SPIN 6.0 in Windows

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

#2 2010-12-15 17:16:47

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

Re: Compile Error of pan.c generated by SPIN 6.0 in Windows

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

#3 2010-12-16 09:29:26

sekky
Member
Registered: 2010-12-15
Posts: 2

Re: Compile Error of pan.c generated by SPIN 6.0 in Windows

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

#4 2010-12-17 20:02:34

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

Re: Compile Error of pan.c generated by SPIN 6.0 in Windows

Problem is fixed in the current Spin Version 6.0.1.

Offline

#5 2011-02-09 07:35:43

suji
Member
Registered: 2011-02-09
Posts: 4

Re: Compile Error of pan.c generated by SPIN 6.0 in Windows

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

Board footer

Powered by FluxBB