Re: Bug in KI_PLATFORM?

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-D6Qt/9opevxWk0Htik3J/[email protected]
http://www.gobosoft.com



------------------------ Yahoo! Groups Sponsor --------------------~--> 
Most low income households are not online. Help bridge the digital divide today!
http://us.click.yahoo.com/cd_AJB/QnQLAA/TtwFAA/saFolB/TM
--------------------------------------------------------------------~-> 

To Post a message, send it to:   [email protected]
To Unsubscribe, send a blank message to: [email protected] 
Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/gobo-eiffel/

<*> To unsubscribe from this group, send an email to:
    [email protected]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/