Spinroot

A forum for Spin users

You are not logged in.

#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

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

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

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

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

Board footer

Powered by FluxBB