Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2017-07-14 12:03:36
- DavidFarago
- Member
- Registered: 2011-10-17
- Posts: 21
What causes these pan.c errors when checking for non-progress cycles?
Using Spin Version 6.4.6 -- 2 December 2016 on a Mac, I get the following errors in pan.c when checking for non-progress cycles:
* error: expected expression
* error: use of undeclared identifier 'Pclaim'
Unfortunately, I may not post the promela file, and a simplified version does not lead to these errors but to a successful non-progress cycle check.
What causes these errors? With a hint, I might be able to avoid these errors or write a simplified version that still exposes these errors.
------------------------------------
Here is the output from the problematic promela file:
Checking syntax and generating the pan.c verifier ...
/opt/local/bin/spin -a sSDPV1.pml
...
the model contains 12 never claims: ...
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N REQ0)
or use e.g.: spin -search -ltl REQ0 sSDPV1.pml
No Syntax Error.
Starting verification...
gcc -DMEMLIM=1024 -DNP -DNOFAIR -DNOCLAIM -DXUSAFE -O2 -w -o pan pan.c
pan.c:7485:26: error: expected expression
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:18: error: use of undeclared identifier 'Pclaim'
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:51: error: expected expression
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:7485:43: error: use of undeclared identifier 'Pclaim'
if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])
^
pan.c:8796:39: error: expected expression
printf(" (%s)\n", procname[((Pclaim *)pptr(0))->_t]);
^
pan.c:8796:31: error: use of undeclared identifier 'Pclaim'
printf(" (%s)\n", procname[((Pclaim *)pptr(0))->_t]);
^
6 errors generated.
Verification: Compile-Time Error - Process ExitValue: 1
Last edited by DavidFarago (2017-07-14 12:06:00)
Offline
#2 2017-07-15 17:23:18
Re: What causes these pan.c errors when checking for non-progress cycles?
I bet the error also goes away if you remove -DNOCLAIM from the compilation directives?
Looks like a bug, where -DNOCLAIM also removes the definition of the claim state structure
from the pan.h file, which leads to the compilation error because it is still referred to in the pan.c file.
Will check into this for the next release.
Thanks for reporting that!
Offline
#3 2017-07-15 17:43:11
Re: What causes these pan.c errors when checking for non-progress cycles?
Some more on this: I do not see how the first 4 warnings could happen
if the code is compiled -DNOCLAIM.
There's only 1 single line in the spin source code that can print that
output and it is disabled by the compiler directive -DNOCLAIM
(it's conditional on VERI being defined, which is only defined when
NOCLAIM is not defined)
So that's a mystery.
Offline