Spin verification - undefined reference to random and srandom

5.3k views Asked by At

I am currently learning Promela/Spin. The problem I have is that I can't verify my programs.

I create my pan files with: spin_64bits.exe -a x.pr --- all's fine until here.

Now when I try to compile pan.c via gcc pan.c (gcc -o pan pan.c, whatever) I get an error that there are undefined references to srandom and random.

Note: It does work when I exchange those with srand() and rand() respectively, but to be honest, I don't want to open pan.c and edit it everytime I want to run a verification.

Do I have to use another compiler perhaps? I'm using MinGW.

1

There are 1 answers

1
Beko On BEST ANSWER

Edit: see MaxGhost's comment for better practice ("add these compile flags to your project: -Dsrandom=srand -Drandom=rand")


Seems like one or the other person stumbles upon this post, so I may as well make the answer that worked for me more visible.

Go to you MinGW folder, search for stdlib.h (C:\MinGW\include) and type in (somewhere along the other #defines, e.g.: below #include <_mingw.h>):

#define random rand
#define srandom srand