Spinroot

feng_lei_76

Member

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

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

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.)