自旋验证 - 对随机和随机的未定义引用

Question

我目前正在学习 Promela/Spin。我的问题是我无法验证我的程序。

我使用以下命令创建我的平移文件：spin_64bits.exe -a x.pr --- 一切都很好。

现在，当我尝试通过 gcc pan.c（gcc -o pan pan.c，无论如何）编译 pan.c 时，我收到一个错误，即存在对 srandom 和 random 的未定义引用。

注意：当我分别用 srand() 和 rand() 交换它们时它确实有效，但老实说，我不想在每次想要运行验证时打开 pan.c 并对其进行编辑。

也许我必须使用另一个编译器？我正在使用 MinGW。

Answer 1

编辑：请参阅MaxGhost 的评论以获得更好的实践（“将这些编译标志添加到您的项目中：-Dsrandom=srand-Drandom=rand”）

---

似乎有人或其他人偶然发现了这篇文章，所以我不妨让对我有用的答案更加明显。

转到您的 MinGW 文件夹，搜索 stdlib.h (C:\MinGW\include) 并输入（在其他 #defines 的某处，例如：#include 下方 <_mingw.h> ):

#define random rand
#define srandom srand