Attribute Result (GNAT Reference Manual) (original) (raw)

Next: Attribute Round, Previous: Attribute Restriction_Set, Up: Implementation Defined Attributes [Contents][Index]

4.50 Attribute Result ¶

function'Result can only be used with in a Postcondition pragma for a function. The prefix must be the name of the corresponding function. This is used to refer to the result of the function in the postcondition expression. For a further discussion of the use of this attribute and examples of its use, see the description of pragma Postcondition.