Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2021-08-13 09:29:25
- jllang
- Member
- From: Finland
- Registered: 2021-05-05
- Posts: 29
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: 29
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: 29
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
