-- B611006.A -- -- Grant of Unlimited Rights -- -- The Ada Conformity Assessment Authority (ACAA) holds unlimited -- rights in the software and documentation contained herein. Unlimited -- rights are the same as those granted by the U.S. Government for older -- parts of the Ada Conformity Assessment Test Suite, and are defined -- in DFAR 252.227-7013(a)(19). By making this public release, the ACAA -- intends to confer upon all recipients unlimited rights equal to those -- held by the ACAA. These rights include rights to use, duplicate, -- release or disclose the released technical data and computer software -- in whole or in part, in any manner and for any purpose whatsoever, and -- to have or permit others to do so. -- -- DISCLAIMER -- -- ALL MATERIALS OR INFORMATION HEREIN RELEASED, MADE AVAILABLE OR -- DISCLOSED ARE AS IS. THE ACAA MAKES NO EXPRESS OR IMPLIED -- WARRANTY AS TO ANY MATTER WHATSOEVER, INCLUDING THE CONDITIONS OF THE -- SOFTWARE, DOCUMENTATION OR OTHER INFORMATION RELEASED, MADE AVAILABLE -- OR DISCLOSED, OR THE OWNERSHIP, MERCHANTABILITY, OR FITNESS FOR A -- PARTICULAR PURPOSE OF SAID MATERIAL. -- -- Notice -- -- The ACAA has created and maintains the Ada Conformity Assessment Test -- Suite for the purpose of conformity assessments conducted in accordance -- with the International Standard ISO/IEC 18009 - Ada: Conformity -- assessment of a language processor. This test suite should not be used -- to make claims of conformance unless used in accordance with -- ISO/IEC 18009 and any applicable ACAA procedures. -- --* -- -- OBJECTIVE: -- -- Check that, for a primitive operation of a type T, that a class-wide -- precondition or postcondition expression cannot make calls to -- nonprimitive operations of type T or functions of T'Class. -- -- Check that, for a primitive operation of a type T, that a class-wide -- precondition or postcondition expression cannot use a global object -- of type T or T'Class as a parameter to a primitive operation of type T. -- -- Check that a primitive subprogram is illegal if the corresponding -- expression for an inherited class-wide precondition or postcondition -- expression would be illegal. -- -- TEST DESCRIPTION: -- These objectives descend from changes made by AI12-0113-1, part -- of Technical Corrigendum 1 (ISO/IEC 8652:2012/Corr1:2016). -- The purpose of these rules is to ensure that the interpretation of -- class-wide precondition and postcondition expressions can be -- meaningfully inherited. We don't want to allow calls to routines that -- don't have equivalents for a descendant type, nor parameters that -- wouldn't have a matching type for a descendant type. (The first two -- objectives cover these cases.) -- -- We don't try to prevent all problems up-front, as they would be -- unnecessarily limiting. Thus we have a instantiation-like legality -- rule recheck on inherited class-wide precondition and postcondition -- expressions. This prevents abstract routines from being called -- in one of these expressions. -- -- CHANGE HISTORY: -- 04 Feb 2016 RLB Created test. -- 22 Feb 2016 RLB Corrected operations of Intf to be abstract. -- --! package B611006 is -- Correct root types: type Root is tagged null record; function Is_OK (Obj : Root) return Boolean; procedure Proc1 (Obj : in out Root) with Pre'Class => Is_OK (Obj); -- OK. procedure Proc2 (Obj : in out Root) with Post'Class => Is_OK (Obj); -- OK. type Intf is limited interface; function Is_Old (Obj : Intf) return Boolean is abstract; procedure Proc3 (Obj : in out Intf) is abstract with Pre'Class => Is_Old (Obj); -- OK. procedure Proc4 (Obj : in out Intf) is abstract with Post'Class => Is_Old (Obj); -- OK. type NRT is new Root with null record; package Pack1 is function Fooey return NRT'Class; function Blooey return NRT; function Is_Bad (Obj : in NRT) return Boolean; function Is_Cool (Obj : in NRT'Class) return Boolean; end Pack1; -- First objective: procedure Proc1 (Obj : in out NRT) with Pre'Class => Is_OK (Obj); -- OK. procedure Proc2 (Obj : in out NRT) with Post'Class => Is_OK (Obj); -- OK. procedure Proc3 (Obj : in out NRT) with Pre'Class => Pack1.Is_Bad (Obj); -- ERROR: procedure Proc4 (Obj : in out NRT) with Post'Class => Pack1.Is_Bad (Obj); -- ERROR: -- As always, the situation with class-wide types is asymetrical: -- an object of a descendant of type NRT can be passed to a -- parameter of NRT'Class, but an object of type NRT'Class cannot be -- passed to a parameter of a descendant of type NRT. Thus Fooey -- below is illegal, but Is_Cool is legal. procedure Proc5 (Obj : in out NRT) with Pre'Class => Is_OK (Pack1.Fooey); -- ERROR: procedure Proc6 (Obj : in out NRT) with Post'Class => Is_OK (Pack1.Fooey); -- ERROR: procedure Proc7 (Obj : in out NRT) with Pre'Class => Is_OK (Pack1.Blooey); -- ERROR: procedure Proc8 (Obj : in out NRT) with Post'Class => Is_OK (Pack1.Blooey); -- ERROR: procedure Proc9 (Obj : in out NRT) with Pre'Class => Pack1.Is_Cool (Obj); -- OK. procedure ProcA (Obj : in out NRT) with Post'Class => Pack1.Is_Cool (Obj); -- OK. -- Second objective: -- Note: Because an object of type T freezes type T, and we cannot -- freeze T, the global objects have to be access objects of some sort. -- We assume that these objects are initialized in the body (which we -- don't show in this test). type Acc_NRT is access all NRT; Specific_Glob : Acc_NRT; type Acc_NRT_Class is access all NRT'Class; Classwide_Glob : Acc_NRT_Class; Unrelated_Glob : Boolean := True; procedure ProcB (Obj : in out NRT) with Pre'Class => Obj /= Specific_Glob.all; -- ERROR: procedure ProcC (Obj : in out NRT) with Post'Class => Obj /= Specific_Glob.all; -- ERROR: procedure ProcD (Obj : in out NRT) with Pre'Class => Obj /= Classwide_Glob.all; -- ERROR: procedure ProcE (Obj : in out NRT) with Post'Class => Obj /= Classwide_Glob.all; -- ERROR: procedure ProcF (Obj : in out NRT) with Pre'Class => Is_OK (Obj) and Unrelated_Glob; -- OK. procedure ProcG (Obj : in out NRT) with Post'Class => Is_OK (Obj) and Unrelated_Glob; -- OK. -- Third objective: package Pack2 is type NAT is abstract new Root with null record; function Is_OK (Obj : NAT) return Boolean is abstract; procedure Proc1 (Obj : in out NAT); -- ERROR: -- The inherited Pre'Class expression Is_OK (Obj) makes -- a non-dispatching call on an abstract routine. -- A statically bound call of the form Proc1 (NAT(Some_Obj)); -- would have to evaluate this expression. procedure Proc2 (Obj : in out NAT) is abstract; -- OK. -- We don't recheck class-wide precondition and postcondition -- expressions for abstract routines, as they can't be called, -- either with a statically bound call or through a dispatching -- call. end Pack2; package Pack3 is type NAT2 is abstract new Root with null record; function Is_OK (Obj : NAT2) return Boolean is abstract; procedure Proc1 (Obj : in out NAT2) is abstract; -- OK. -- Inherits procedure Proc2 (Obj : in out NAT2), which is illegal -- for the same reason as above. -- ERROR: end Pack3; package Pack4 is type NAT3 is abstract new Root and Intf with null record; function Is_OK (Obj : NAT3) return Boolean; function Is_Old (Obj : NAT3) return Boolean is abstract; -- Inherits procedure Proc1 (Obj : in out NAT3) and -- procedure Proc2 (Obj : in out NAT3), which are OK as Is_OK is not -- abstract. procedure Proc3 (Obj : in out NAT3); -- ERROR: procedure Proc4 (Obj : in out NAT3) is abstract; -- OK. end Pack4; package Pack5 is type NAT4 is abstract new Root and Intf with null record; function Is_OK (Obj : NAT4) return Boolean; function Is_Old (Obj : NAT4) return Boolean is abstract; -- Inherits procedure Proc1 (Obj : in out NAT4) and -- procedure Proc2 (Obj : in out NAT4), which are OK as Is_OK is not -- abstract. procedure Proc3 (Obj : in out NAT4) is abstract; -- OK. -- Inherits procedure Proc4 (Obj : in out NAT4), which is illegal. -- ERROR: end Pack5; end B611006;