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