Spinroot

A forum for Spin users

You are not logged in.

#1 2011-10-06 11:01:42

KeesPronk
Member
Registered: 2011-01-04
Posts: 12

Exceptions not propagated (back) to iSpin?

I am having the following (very stupid) program divzero.pml:

init{
    int k;
    k = k + 1;
    k = k / 0;   
    skip;   
}

When I work from the command prompt:
spin -a divzero.pml         // is ok
gcc -w -o pan pan.c        // is ok; BTW leaving out the -w will draw my attention to the error made
./pan                             // will report a floating point exception, which is OK.

However, when running from iSpin:

- the simulator is silent
- the verifier is silent; the only action I notice is that the processor load is increased.

So it seems exceptions are not propagated back into iSpin?

Offline

#2 2011-10-06 17:08:31

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

Re: Exceptions not propagated (back) to iSpin?

Do you not see the warning from the compilation step?

Offline

Board footer

Powered by FluxBB