PR# 18027 Wrong tag for postcondition of {BYTE_NODE}.size

Problem Report Summary

Submitter: prestoat2000

Category: Compiler

Priority: Medium

Date: 2011/11/30

Class: Bug

Severity: Non-critical

Number: 18027

Release: 7.0.88046

Confidential: No

Status: Open

Responsible:

Environment: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.9.0.10) Gecko/2009042715 Firefox/3.0.10 Solaris 10

Synopsis: Wrong tag for postcondition of {BYTE_NODE}.size

Description

Routine {BYTE_NODE}.size is

        size: INTEGER
                do
                        Result := 0
                ensure
                        Result_greater_or_equal_to_one: Result >= 0
                end

The tag for the postcondition should be "result_nonnegative", since
the current tag doesn't match the postcondition.

To Reproduce

Problem Report Interactions