magnus.myreen at gmail.com
Sun Mar 5 07:39:44 UTC 2017
On 5 March 2017 at 05:48, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> The comment next to the number here
> val large_int = ``268435457:int`` (* 2**28-1 *)
> does not match. (2**28-1 = 268435455).
> Which is correct?
I think it could even be (2**29)-1.
> Can this number be defined somewhere?
It is defined. It is defined there in bvl_to_bvi.
> And verified (connected to some
> proof)? Would backend_common be preferable for the definition than
It is meant to be a number that's large enough into fit a smallint
when all the tag bits and sign bits are taken into account. I needed
the number there in bvl_to_bvi, but I don't have access to the machine
size then. It seemed like too much effort to propagate the machine
size into the BVI semantics (and bvl_to_bvi compiler).
It doesn't matter if this number is a bit smaller than necessary, and
the number might disappear if we compile large numbers more
efficiently in the future.
I wouldn't worry about it, since there are much bigger issues to deal
with: I'll send a message in a little bit about max_app.
More information about the Developers