Dear Jesse,

finally some time to look into this bug.

On Wed, Jun 08, 2011 at 04:47:23PM -0400, Jesse M Draper wrote:
> Cil handles the constant 0x80000000 incorrectly on my 64-bit machine, making
> it a signed int instead of an unsigned int.

Agreed.

> The following also seems to work for me and may be simpler:
> 
> --- src/cilint.ml       (revision 12173)
> +++ src/cilint.ml       (working copy)
> @@ -200,7 +200,7 @@
>            bits - truncmax
>         in
>         let trunc =
> -       if i > max || i < -max then
> +       if i >= max || i <= -max then
>            if i > truncmax then
>              BitTruncation
>            else

Hmm, I don't understand this piece of code very well, but assuming the
"big_int" part below is correct (is it?), it should rather be:
> @@ -200,7 +200,7 @@
>            bits - truncmax
>         in
>         let trunc =
> -       if i > max || i < -max then
> -           if i > truncmax then
> +       if i >= max || i < -max then
> +           if i >= truncmax then
>              BitTruncation
>            else

(I'd rather have the Small and Big branches as close as possible, to make the
logic more clear.)

What do you think?

Best,
-- 
Gabriel

------------------------------------------------------------------------------
Special Offer -- Download ArcSight Logger for FREE!
Finally, a world-class log management solution at an even better 
price-free! And you'll get a free "Love Thy Logs" t-shirt when you
download Logger. Secure your free ArcSight Logger TODAY!
http://p.sf.net/sfu/arcsisghtdev2dev
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users

Reply via email to