A forum for Spin users
You are not logged in.
Pages: 1
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
Pages: 1