A forum for Spin users

You are not logged in.

#1 2012-11-14 14:31:29

Registered: 2011-05-13
Posts: 43

Bitstate in Spin6.2.3

I might hit a bug in SPIN6.2.3 with the bitstate option.  The following is the error message prompted in iSpin 1.1.0.  The verification in version 6.2.2 with bitstate on the same model is successful.

My PC is 64 bit Windows 7.  I run Spin with Cygwin.

verification result:
spin -a  battery.pml
gcc-3 -DMEMLIM=5120 -O2 -DBITSTATE -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
/cygdrive/c/Users/lfeng/AppData/Local/Temp/cc7QDuCG.o:pan.c:(.text+0xbfdc): undefined reference to `_o_hash32'
/cygdrive/c/Users/lfeng/AppData/Local/Temp/cc7QDuCG.o:pan.c:(.text+0xc15b): undefined reference to `_o_hash64'
/usr/lib/gcc/i686-pc-cygwin/3.4.4/../../../../i686-pc-cygwin/bin/ld: /cygdrive/c/Users/lfeng/AppData/Local/Temp/cc7QDuCG.o: bad reloc address 0x20 in section `.data'
/usr/lib/gcc/i686-pc-cygwin/3.4.4/../../../../i686-pc-cygwin/bin/ld: final link failed: Invalid operation
collect2: ld returned 1 exit status


#2 2012-11-15 23:46:43

Registered: 2010-11-18
Posts: 678

Re: Bitstate in Spin6.2.3

Will be fixed in the next release (6.2.3).
You can simply remove the offending lines with the assignments to o_hash from pan.c, since they're not needed in this mode. (Sorry, that's a bit clumsy, but at least it gives you a workaround for now.)


Board footer

Powered by FluxBB