Как указать путь к библиотекам C в jspin?

Question

Я использую jspin и пытаюсь включить библиотеку stdio.h в выражение c_code:

c_code
{
    #include <stdio.h>
}

Однако я получаю следующую ошибку:

spin: error: No file 'stdio.h'

Я проверил каталог, в котором установлен mingw, и в нем есть stdio.h. Таким образом, я полагаю, все дело в неправильных путях. Как я могу установить включить путь в jspin?

Answer 1

Пытаться:

c_decl {
  \#include <stdio.h>
}

\# является критической частью ( Spinroot.com для c_decl). Также используйте c_decl{} так как .h файлы не содержат код

[edit] Относительно 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);
  }
}