Bug 488 - A missing 32-bit signed integer
Summary: A missing 32-bit signed integer
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: libutap (show other bugs)
Version: unspecified
Hardware: Macintosh Mac OS
: P2 minor
Assignee: Alexandre David
URL:
: 471 (view as bug list)
Depends on:
Blocks: 471
  Show dependency treegraph
 
Reported: 2010-04-30 19:05 CEST by Christopher A. Stone
Modified: 2010-05-25 17:06 CEST (History)
1 user (show)

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Christopher A. Stone 2010-04-30 19:05:58 CEST
By declaring a large-enough integer range, all 32-bit signed integers appear to be representable except for the most negative integer, -2147483648  (i.e., -2^31).

If I declare
  int[-2147483648,2147483647] x;

then

(a) the assignment
         x = -2147483648
      actually causes
         x == -2147483647
      in the simulator.

(b) the assignment 
         x = -2147483647
      followed by an edge
         x = x-1
      causes the simulator to complain about the successors
      not being well-defined.

(c) the assignment
         x = -2147483647
      followed by an edge
         x = x-2
      does wrap around properly according to 32-bit arithmetic, 
      leading to  
         x == 2147483647
      in the simulator.

For faithful modeling it would be nice to have the entire 32-bit integer range available, even if any particular simulation only uses a small subset of this range.  

If this is not a bug but a implementation decision, it would be nice if the allowable integers were documented.  (I looked, but only found the default 16-bit range mentioned in the help file.)
Comment 1 Alexandre David 2010-05-25 16:33:11 CEST
This is caused by the lexer that only recognizes (non-negative) natural numbers.
Comment 2 Alexandre David 2010-05-25 16:50:07 CEST
Fixed in rev. 4537 for 4.0 and 4536 in the trunk.
Now constant overflows are also detected.
Comment 3 Marius Mikučionis 2010-05-25 17:06:03 CEST
*** Bug 471 has been marked as a duplicate of this bug. ***