-- B611002.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 Pre and Post cannot be specified on a subprogram body that is
-- acting as a completion.
--
-- CHANGE HISTORY:
-- 03 Feb 2016 RLB Created test.
package B611002P is
procedure Spec1 (P : in out Natural);
procedure Spec2 (P : in out Natural);
function Spec4 (P : Natural) return Natural;
procedure Spec5 (P : in out Natural);
procedure Spec6 (P : in out Natural);
function Spec8 (P : Natural) return Natural;
end B611002P;
package body B611002P is
procedure No_Spec1 (P : in out Natural)
with Pre => P mod 2 = 0 is -- OK.
begin
P := P * 2;
end No_Spec1;
procedure Spec1 (P : in out Natural)
with Pre => P mod 2 = 0 is -- ERROR:
begin
P := P * 2;
end Spec1;
procedure Spec2 (P : in out Natural) is separate
with Pre => P mod 2 = 0; -- ERROR:
procedure Spec3 (P : in out Natural);
procedure Spec3 (P : in out Natural)
with Pre => P mod 2 = 0 is -- ERROR:
begin
P := P * 2;
end Spec3;
function No_Spec4 (P : Natural) return Natural is (P * 2)
with Pre => P mod 2 = 0; -- OK.
function Spec4 (P : Natural) return Natural is (P * 2)
with Pre => P mod 2 = 0; -- ERROR:
procedure No_Spec5 (P : in out Natural)
with Post => P mod 2 = 0 is -- OK.
begin
P := P * 2;
end No_Spec5;
procedure Spec5 (P : in out Natural)
with Post => P mod 2 = 0 is -- ERROR:
begin
P := P * 2;
end Spec5;
procedure Spec6 (P : in out Natural) is separate
with Post => P mod 2 = 0; -- ERROR:
procedure Spec7 (P : in out Natural);
procedure Spec7 (P : in out Natural)
with Post => P mod 2 = 0 is -- ERROR:
begin
P := P * 2;
end Spec7;
function No_Spec8 (P : Natural) return Natural is (P * 2)
with Post => P mod 2 = 0; -- OK.
function Spec8 (P : Natural) return Natural is (P * 2)
with Post => P mod 2 = 0; -- ERROR:
end B611002P;
-- Note: The following are provided for completeness. Processing these units
-- is not required.
separate (B611002P)
procedure Spec2 (P : in out Natural) is -- OPTIONAL ERROR:
begin
P := P * 2;
end Spec2;
separate (B611002P)
procedure Spec6 (P : in out Natural) is -- OPTIONAL ERROR:
begin
P := P * 2;
end Spec6;
with B611002P;
procedure B611002 is
Var : Integer := 0;
begin
B611002P.Spec1 (Var);
end B611002;