我正在使用 jspin 并尝试在 c_code 表达式中包含 stdio.h 库:
c_code
{
#include <stdio.h>
}
但是,我收到以下错误:
spin: error: No file 'stdio.h'
我检查了安装 mingw 的目录,里面有 stdio.h。因此,我想,这都是关于错误的道路。如何在 jspin 中设置包含路径?
尝试:
c_decl {
\#include <stdio.h>
}
这\#
是关键部分(对于 c_decl 的 Spinroot.com)。另外,使用c_decl{}
因为.h
文件不包含代码。
[编辑] 关于 fprintf() 不显示输出;我不能说我知道原因。我试过你的特定代码。结果如下:
ebg@ebg$ rm /tmp/foo.bar
ebg@ebg$ spin -a test.pml
ebg@ebg$ gcc -o test pan.c
ebg@ebg$ ./test
hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 6.2.4 -- 21 November 2012)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 12 byte, depth reached 2, errors: 0
3 states, stored
0 states, matched
3 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in init
(0 of 2 states)
pan: elapsed time 0 seconds
ebg@ebg$ cat /tmp/foo.bar
some str
这是我使用的代码:
c_decl {
\#include <stdio.h>
}
init {
c_code {
FILE *file;
file = fopen ("/tmp/foo.bar", "a+");
fprintf (file, "%s", "some str");
fclose (file);
}
}