Spinroot

A forum for Spin users

You are not logged in.

#1 2021-08-13 09:29:25

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

The -I flag is not documented in Spin online reference

The help command of spin lists the following flag: "-I show result of inlining and preprocessing". This flag seems to be missing from the online documentation at https://spinroot.com/spin/Man/Spin.html

Offline

#2 2021-08-13 09:31:47

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: The -I flag is not documented in Spin online reference

By the way, does the -I flag produce the final PROMELA model that goes to the verifier executable? I sometimes get really strange line numbers in error messages produced by pan. They don't seem to correspond with the line numbers in my PROMELA source code.

Offline

#3 2021-08-13 12:00:30

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: The -I flag is not documented in Spin online reference

Interesting, the syntax produced by the -I flag contains undocumented features, such as anonymous blocks and labels starting with a colon. Additionally, Spin refuses to digest its own output, because the -I flag generates syntax errors...

Offline

#4 2022-03-01 19:06:45

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: The -I flag is not documented in Spin online reference

the output of the -I flag is not a valid Promela model -- it's mostly a debugging aid to see how inlines and macros are expanded internally

Offline

Board footer

Powered by FluxBB