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
