Spinroot

A forum for Spin users

You are not logged in.

#1 2011-07-12 07:09:31

Gordon
Member
Registered: 2011-07-12
Posts: 6

Error parsing -2147483648

The promela parser seems not to read the smallest integer value (32 bit) correctly. In the following example spin will print out
-2147483647.


int v;

proctype all() {
  v = -2147483648;
  printf("%d\n", v);
}
init
{
run all();
}

Offline

#2 2011-07-12 16:22:24

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

Re: Error parsing -2147483648

fascinating -- the bug is actually in the atoi call which seems to make
atoi(2147483648) equal to 21474883647
you can confirm this by compiling and executing this little C program:
#include <stdio.h>

int
main(void)
{   int v;
     v = -2147483648;
     printf("%d, %d\n", v, atoi("2147483648"));
}

which on my machine prints -2147483648, 2147483647

So it's not Spin that's doing this -- but quite fascinating that atoi would do it!

Offline

#3 2011-07-12 16:38:22

Gordon
Member
Registered: 2011-07-12
Posts: 6

Re: Error parsing -2147483648

Hi,

I think you can not blame atoi for this bug. The atoi function might have been called with the sign which would not lead to this behaviour.
Atoi("2147483648") is not a valid test case for this issue. 2147483648 has NO representation in signed 32bit (-2147483648 does). Atoi("-2147483648") will hopefully lead to the expected result. So the bug is most probably in the call of atoi.

Last edited by Gordon (2011-07-12 16:46:31)

Offline

#4 2011-07-13 01:51:16

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

Re: Error parsing -2147483648

no it really is as i described -- but this seems to happen only on cygwin
(just compile and execute that little program I included to confirm it)
what platform/OS are you using?

Offline

#5 2011-07-13 08:30:36

Gordon
Member
Registered: 2011-07-12
Posts: 6

Re: Error parsing -2147483648

Dear Administrator,

I don't doubt that the behaviour of atoi is like you described it. However x = -2147483648 is a valid promela statement with the semantics, that x becomes -2147483648. I had a look into the grammar and lex part of spin (Version 6.10) and believe that the bug is within the lexer. The token "-2147483648" is NOT recognized as a CONST. Instead the lexer recognizes '-' and than '2147483648' as two separate tokens. The grammar rule for expr than creates an atoi call for 2147483648 (which is not defined but returns MAX_INT). the minus is applied later and leads to the described behaviour. So you have to to fix the lexer!

Offline

#6 2011-07-13 16:13:20

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

Re: Error parsing -2147483648

you describe the problem correctly, but the solution is not quite that simple.
note that "expr - CONST" is in the grammar, but not "expr CONST"

so, i do maintain that the bug is in cygwin's version of atoi -- it should not be returning MAX_INT unless it's argument is MAX_INT -- it would be fair for it to flag an error of course, but i don't think it is reasonable to return a different number than what is provided in the ascii argument
i'll look into it some more though

Offline

#7 2011-07-14 08:33:52

Gordon
Member
Registered: 2011-07-12
Posts: 6

Re: Error parsing -2147483648

Fine. It is important for a verification tool to be correct. So i am looking forward for a fixed version of spin. I have the windows version of spin (compiled with cl). Does the unix/linux version parse the number correctly? If atoi is called with 2147483648 i don't know how this could work on unix/linux. If the unix atoi flags an error it would'nt correct the result. Atoi has no chance to give the correct answer because the answer does not fit into 32bit. However, thank you for the support. The important point is, that this error should be fixed somewhere.

Offline

#8 2011-07-14 16:13:57

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

Re: Error parsing -2147483648

it's a fair point.  i think the best i can do is to flag an error if something unexpected like this happens.  atoi() does not generate an error, but strtol() does -- so i'll switch to that for the next release of spin -- and report an error if the conversion has an 'unexpected' result (i.e., when errno gets set)
clearly for any value that is truly outside the full 32-bit signed integer range, something similar will happen, and that too will then be flagged as an error

Offline

Board footer

Powered by FluxBB