#97 Warning about truncation is incorrect

Bug
closed-fixed
nobody
None
5
2009-04-24
2008-09-28
Anonymous
No

In Cil.truncateInteger64, the variable 'chopped', which is used to see if truncation has occurred, is incorrectly set. It is currently set to

Int64.shift_right_logical i (64 - nrBits),

but it should be

Int64.shift_right_logical i nrBits.

In addition, the test for 'choppedness' seems a bit odd. For example, why should converting 0xffffffff80000000 and 0x80000000 to a C 'int' *both* return 'false' for whether truncation occurred? Here's a similar example: converting 0x80 to a signed char would return 'false' for whether truncation occurred, even though the input represented 128 and the output is -128.

I am using CIL 1.3.6.

-Elnatan Reisner
elnatan@cs.umd.edu

Discussion

  • David Gay
    David Gay
    2009-04-15

    Fixing in 1.3.7 (first part). There's a comment about the reason for the oddness "(* matth: also suppress the warning if we only chop off 1s. This is probably due to a negative number being cast to an unsigned value. While potentially a bug, this is almost always what the programmer intended. *)"

     
  • David Gay
    David Gay
    2009-04-16

    • status: open --> pending-fixed
     
  • David Gay
    David Gay
    2009-04-24

    • status: pending-fixed --> closed-fixed