Brian Heilig wrote:
> I think there is a bug in the postcondition of Boolean_bits in
> ki_platform.ge revision 1.9. Boolean_bytes is a once routine in
> KL_PLATFORM that depends on Boolean_bits (using VE or SE). But the
> postcondition of Boolean_bits uses the result of Boolean_bytes. Here
> is the definition of Boolean_bits in KI_PLATFORM
>
> Boolean_bits: INTEGER is
> -- Number of bits in a value of type BOOLEAN
> deferred
> ensure
> large_enough: Result >= 1
> small_enough: Result <= Boolean_bytes * Byte_bits
> end
>
> Notice how this is different from the postcondition in Character_bits
> for example:
>
> Character_bits: INTEGER is
> -- Number of bits in a value of type CHARACTER
> deferred
> ensure
> -- Note: Postcondition commented out to avoid recursive
> -- call in once-function in KL_PLATFORM:
> -- definition: Result = Character_bytes * Byte_bits
> more_than_byte: Result >= Byte_bits
> end
>
> I think Boolean_bits was just missed.

This is fixed now.
Thank you for reporting this problem.

--
Eric Bezault
mailto:ericb@...
http://www.gobosoft.com